The left almost-split boundary of an injective module

For an indecomposable injective finite right module I, the canonical map I → I / soc(I) is left almost split and left minimal. The factorization argument uses essentiality of the simple socle: any map out of I which does not split as a monomorphism must kill the socle and hence descend through the quotient.

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

The quotient of a finite right module by its module socle.

def MagnitudeConjecture.moduleSocleQuotientProjection {B : Type u} [Ring B] (I : FGModuleCat Bᵐᵒᵖ) : I ⟶ moduleSocleQuotientFGObj I

The canonical projection I → I / soc(I).

theorem MagnitudeConjecture.moduleSocleQuotientProjection_epi {B : Type u} [Ring B] (I : FGModuleCat Bᵐᵒᵖ) : CategoryTheory.Epi (moduleSocleQuotientProjection I)

The canonical socle-quotient projection is epic.

theorem MagnitudeConjecture.moduleSocleQuotientProjection_isLeftAlmostSplit {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) : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit (moduleSocleQuotientProjection I)

For an indecomposable injective module, the canonical quotient by its socle is left almost split.

theorem MagnitudeConjecture.moduleSocleQuotientProjection_isLeftMinimal {B : Type u} [Ring B] (I : FGModuleCat Bᵐᵒᵖ) : QuotientSubmoduleEquidistribution.IsLeftMinimal (moduleSocleQuotientProjection I)

The canonical socle-quotient projection is left minimal.

theorem MagnitudeConjecture.jacobson_isIndecomposableModule_of_injective {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) (hTop : IsSimpleModule Bᵐᵒᵖ (↑I ⧸ Module.jacobson Bᵐᵒᵖ ↑I)) (hnotSimple : ¬IsSimpleModule Bᵐᵒᵖ ↑I) : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule Bᵐᵒᵖ ↥(Module.jacobson Bᵐᵒᵖ ↑I)

The Jacobson radical of a non-simple indecomposable injective module with simple top is indecomposable.