Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleInjectiveSocle

Simple socles of indecomposable injective right modules #

A nonzero simple submodule of an indecomposable injective module is an essential submodule: injectivity and the local endomorphism ring turn its inclusion into an injective envelope. Consequently every simple submodule lies in it, so it is the whole socle.

source
def MagnitudeConjecture.moduleSocleFGObj {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] (I : FGModuleCat Bᵐᵒᵖ) :
FGModuleCat Bᵐᵒᵖ

The socle of a finitely generated right module, bundled again as a finitely generated right module.

Instances For
    source
    def MagnitudeConjecture.moduleSocleInclusion {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] (I : FGModuleCat Bᵐᵒᵖ) :
    moduleSocleFGObj I ⟶ I

    The canonical inclusion of the bundled socle.

    Instances For
      source
      @[simp]
      theorem MagnitudeConjecture.moduleSocleInclusion_apply_val {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] (I : FGModuleCat Bᵐᵒᵖ) (x : ↑(moduleSocleFGObj I)) :
      (ModuleCat.Hom.hom (moduleSocleInclusion I).hom) x = ↑x
      source
      instance MagnitudeConjecture.moduleSocleInclusion_mono {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] (I : FGModuleCat Bᵐᵒᵖ) :
      CategoryTheory.Mono (moduleSocleInclusion I)
      source
      theorem MagnitudeConjecture.moduleSocle_isSimple_of_injective_indecomposable {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (I : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Injective I] (hI : CategoryTheory.Indecomposable I) :
      IsSimpleModule Bᵐᵒᵖ ↥(moduleSocle Bᵐᵒᵖ ↑I)

      An indecomposable injective finitely generated right module has simple socle.

      source
      theorem MagnitudeConjecture.moduleSocleInclusion_isEssential_of_injective_indecomposable {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (I : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Injective I] (hI : CategoryTheory.Indecomposable I) :
      IsEssentialMono (moduleSocleInclusion I)

      For an indecomposable injective right module, its canonical socle inclusion is essential.

      source
      theorem MagnitudeConjecture.moduleSocleInclusion_comp_eq_zero_of_not_iso {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (I M : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Injective I] (hI : CategoryTheory.Indecomposable I) (hM : CategoryTheory.Indecomposable M) (hnoniso : ¬Nonempty (I ≅ M)) (f : I ⟶ M) :
      CategoryTheory.CategoryStruct.comp (moduleSocleInclusion I) f = 0

      Every map from an indecomposable injective module to a nonisomorphic indecomposable module kills the injective module's socle.

      source
      theorem MagnitudeConjecture.RightModule.projectiveNakayamaFGObj_indecomposable {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (P : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] (hP : CategoryTheory.Indecomposable P) :
      CategoryTheory.Indecomposable (projectiveNakayamaFGObj P)

      The Nakayama image of an indecomposable finite projective right module is indecomposable.

      source
      theorem MagnitudeConjecture.RightModule.projectiveNakayamaFGObj_moduleSocle_isSimple {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (P : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] (hP : CategoryTheory.Indecomposable P) :
      IsSimpleModule Bᵐᵒᵖ ↥(moduleSocle Bᵐᵒᵖ ↑(projectiveNakayamaFGObj P))

      The Nakayama image of an indecomposable finite projective right module has simple socle.