Magnitude conjecture

MagnitudeConjecture.CategoryTheory.FiniteDimensionalModuleIndecomposable

Local endomorphism rings of finite-dimensional linear modules #

The category of finite-support pointwise finite-dimensional linear functors is closed under retracts inside the ambient functor category. It is therefore idempotent-complete. Evaluation on the finite support embeds each endomorphism space into a finite product of finite-dimensional pointwise endomorphism spaces. Hence an indecomposable object has local endomorphism ring by the generic finite-dimensional Fitting criterion.

source
instance MagnitudeConjecture.CoveringHom.isLinearModule_stableUnderRetracts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type uK) [Field k] [CategoryTheory.Linear k C] :
(IsLinearModule k).IsStableUnderRetracts

Additivity and linearity of a module-valued functor are preserved by retracts.

source
instance MagnitudeConjecture.CoveringHom.linearModuleCategory_isIdempotentComplete {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type uK) [Field k] [CategoryTheory.Linear k C] :
CategoryTheory.IsIdempotentComplete (LinearModuleCategory k)

The category of linear module-valued functors is idempotent-complete.

source
instance MagnitudeConjecture.CoveringHom.isFiniteDimensionalModule_stableUnderRetracts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type uK) [Field k] [CategoryTheory.Linear k C] :
(IsFiniteDimensionalModule k).IsStableUnderRetracts

Pointwise finite-dimensionality and finite object support are preserved by retracts of linear modules.

source
instance MagnitudeConjecture.CoveringHom.finiteDimensionalModuleCategory_isIdempotentComplete {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type uK) [Field k] [CategoryTheory.Linear k C] :
CategoryTheory.IsIdempotentComplete (FiniteDimensionalModuleCategory k)

The category of finite-support pointwise finite-dimensional linear modules is idempotent-complete.

source
noncomputable def MagnitudeConjecture.CoveringHom.finiteDimensionalModuleEndEvaluation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type uK) [Field k] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) :
CategoryTheory.End M →ₗ[k] (X : ↑(moduleSupport k M.obj.obj)) → CategoryTheory.End (M.obj.obj.obj ↑X)

Evaluation on the finite support of a module gives a linear map from its endomorphism space into the product of its pointwise endomorphism spaces.

Instances For
    source
    theorem MagnitudeConjecture.CoveringHom.finiteDimensionalModuleEndEvaluation_injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type uK) [Field k] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) :
    Function.Injective ⇑(finiteDimensionalModuleEndEvaluation k M)

    Evaluation on the support detects a natural endomorphism.

    source
    instance MagnitudeConjecture.CoveringHom.finiteDimensionalModuleEnd_finiteDimensional {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type uK) [Field k] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) :
    FiniteDimensional k (CategoryTheory.End M)

    Endomorphism spaces of finite-support pointwise finite-dimensional modules are finite-dimensional.

    source
    theorem MagnitudeConjecture.CoveringHom.finiteDimensionalModule_end_isLocalRing {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type uK) [Field k] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) (hM : CategoryTheory.Indecomposable M) :
    IsLocalRing (CategoryTheory.End M)

    An indecomposable finite-support pointwise finite-dimensional linear module has local endomorphism ring.

    source
    noncomputable def MagnitudeConjecture.CoveringHom.finiteDimensionalModuleEndLinearModuleAlgEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type uK) [Field k] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) :
    CategoryTheory.End M ≃ₐ[k] CategoryTheory.End M.obj

    The finite-dimensional full-subcategory inclusion identifies the two k-algebra structures on endomorphism rings.

    Instances For
      source
      instance MagnitudeConjecture.CoveringHom.finiteDimensionalModuleLinearModuleEnd_finiteDimensional {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type uK) [Field k] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) :
      FiniteDimensional k (CategoryTheory.End M.obj)

      Endomorphisms of the underlying linear module of a finite-dimensional module form a finite-dimensional vector space.

      source
      theorem MagnitudeConjecture.CoveringHom.finiteDimensionalModule_linearModule_end_isLocalRing {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type uK) [Field k] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) (hM : CategoryTheory.Indecomposable M) :
      IsLocalRing (CategoryTheory.End M.obj)

      Localness of a finite-dimensional module's endomorphism ring passes to its underlying linear module.