Magnitude conjecture

MagnitudeConjecture.CategoryTheory.FiniteDimensionalModuleDecomposition

Finite decompositions of finite-dimensional modules #

The total dimension of a finite-support module is the finite sum of its pointwise dimensions. It vanishes only on a zero module and is additive under binary biproduct decompositions. Strong induction on this rank therefore decomposes every finite-dimensional module into finitely many indecomposables.

source
noncomputable def MagnitudeConjecture.CoveringHom.moduleTotalDimension {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) :
ℕ

The sum of the pointwise dimensions of a finite-support module.

Instances For
    source
    theorem MagnitudeConjecture.CoveringHom.moduleFinrank_hasFiniteSupport {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) :
    Function.HasFiniteSupport fun (X : C) => Module.finrank k ↑(M.obj.obj.obj X)

    The pointwise dimension function of a finite-dimensional module has finite support.

    source
    theorem MagnitudeConjecture.CoveringHom.isIso_of_epi_finiteDimensionalModule_endo {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) (e : M ⟶ M) [CategoryTheory.Epi e] :
    CategoryTheory.IsIso e

    Every epic endomorphism of a finite-support pointwise finite-dimensional module is invertible.

    source
    theorem MagnitudeConjecture.CoveringHom.isIso_of_mono_finiteDimensionalModule_endo {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) (e : M ⟶ M) [CategoryTheory.Mono e] :
    CategoryTheory.IsIso e

    Every monic endomorphism of a finite-support pointwise finite-dimensional module is invertible.

    source
    theorem MagnitudeConjecture.CoveringHom.moduleTotalDimension_lt_of_mono_not_isIso {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (N M : FiniteDimensionalModuleCategory k) (i : N ⟶ M) [CategoryTheory.Mono i] (hi : ¬CategoryTheory.IsIso i) :
    moduleTotalDimension N < moduleTotalDimension M

    A proper subobject of a finite module has strictly smaller total pointwise dimension.

    source
    theorem MagnitudeConjecture.CoveringHom.moduleTotalDimension_image_lt_of_not_isIso {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) (e : M ⟶ M) (he : ¬CategoryTheory.IsIso e) :
    moduleTotalDimension (CategoryTheory.Abelian.image e) < moduleTotalDimension M

    The image of a noninvertible endomorphism of a finite module has strictly smaller total pointwise dimension.

    source
    theorem MagnitudeConjecture.CoveringHom.isZero_of_moduleTotalDimension_eq_zero {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) (hM : moduleTotalDimension M = 0) :
    CategoryTheory.Limits.IsZero M

    A finite-dimensional module of total dimension zero is a zero object.

    source
    theorem MagnitudeConjecture.CoveringHom.finiteDimensionalModule_exists_simple_subobject {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) (hM : ¬CategoryTheory.Limits.IsZero M) :
    ∃ (N : FiniteDimensionalModuleCategory k) (i : N ⟶ M), CategoryTheory.Simple N ∧ CategoryTheory.Mono i

    Every nonzero finite-dimensional module contains a simple submodule.

    source
    theorem MagnitudeConjecture.CoveringHom.moduleTotalDimension_biprod {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {X Y Z : FiniteDimensionalModuleCategory k} (e : X ≅ Y ⊞ Z) :
    moduleTotalDimension X = moduleTotalDimension Y + moduleTotalDimension Z

    Total dimension is additive across any displayed binary biproduct decomposition.

    source
    theorem MagnitudeConjecture.CoveringHom.finiteDimensionalModule_finiteIndecomposableDecomposition {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) :
    Nonempty (CategoryTheory.FiniteIndecomposableDecomposition M)

    Every finite-dimensional finite-support linear module admits a finite biproduct decomposition into indecomposable modules.