The distinguished stable socle extension

At a nonprojective indecomposable endpoint over an algebraically closed field, the residue map of the local endomorphism algebra descends to stable endomorphisms and takes the stable identity to one. Stable Hom--Ext duality transports this functional to a nonzero extension class whose pullback along every nonretraction vanishes. Consequently every short exact sequence realizing the class has right almost-split terminal map.

theorem MagnitudeConjecture.isSplitEpi_right_of_comp {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] {W X Y : FGModuleCat Bᵐᵒᵖ} (f : W ⟶ X) (g : X ⟶ Y) (hfg : CategoryTheory.IsSplitEpi (CategoryTheory.CategoryStruct.comp f g)) : CategoryTheory.IsSplitEpi g

If a composite is a retraction, its right factor is a retraction.

theorem MagnitudeConjecture.isSplitEpi_smul_id_of_ne_zero {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (X : FGModuleCat Bᵐᵒᵖ) {c : k} (hc : c ≠ 0) : CategoryTheory.IsSplitEpi (c • CategoryTheory.CategoryStruct.id X)

Over a field, a nonzero scalar multiple of the identity is a split epimorphism.

theorem MagnitudeConjecture.fgEndFiniteDimensional {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (X : FGModuleCat Bᵐᵒᵖ) : FiniteDimensional k (CategoryTheory.End X)

theorem MagnitudeConjecture.fgEnd_isLocalRing_of_indecomposable {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (X : FGModuleCat Bᵐᵒᵖ) (hX : CategoryTheory.Indecomposable X) : IsLocalRing (CategoryTheory.End X)

A finitely generated module with indecomposable underlying object has local categorical endomorphism ring.

noncomputable def MagnitudeConjecture.TwoStepMinimalProjectivePresentation.stableIdentityFunctional {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} [IsAlgClosed k] (P : TwoStepMinimalProjectivePresentation X) (hX : ¬CategoryTheory.Projective X) (hXind : CategoryTheory.Indecomposable X) : RightModule.projectiveStableHom X X →ₗ[k] k

The local endomorphism-algebra residue descends to projective-stable endomorphisms of a nonprojective indecomposable module.

@[simp]

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.stableIdentityFunctional_id {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] [IsAlgClosed k] (P : TwoStepMinimalProjectivePresentation X) (hX : ¬CategoryTheory.Projective X) (hXind : CategoryTheory.Indecomposable X) : (P.stableIdentityFunctional hX hXind) (RightModule.projectiveStableClass (CategoryTheory.CategoryStruct.id X)) = 1

noncomputable def MagnitudeConjecture.TwoStepMinimalProjectivePresentation.stableSocleClass {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] [IsAlgClosed k] (P : TwoStepMinimalProjectivePresentation X) (hX : ¬CategoryTheory.Projective X) (hXind : CategoryTheory.Indecomposable X) : CategoryTheory.Abelian.Ext X P.nakayamaKernel 1

The distinguished extension class selected by the stable identity.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.stableSocleClass_ne_zero {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] [IsAlgClosed k] (P : TwoStepMinimalProjectivePresentation X) (hX : ¬CategoryTheory.Projective X) (hXind : CategoryTheory.Indecomposable X) : P.stableSocleClass hX hXind ≠ 0

The distinguished class is nonzero.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.pullback_stableSocleClass_eq_zero_of_not_isSplitEpi {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] [IsAlgClosed k] (P : TwoStepMinimalProjectivePresentation X) (hX : ¬CategoryTheory.Projective X) (hXind : CategoryTheory.Indecomposable X) {Y : FGModuleCat Bᵐᵒᵖ} (g : Y ⟶ X) (hg : ¬CategoryTheory.IsSplitEpi g) : (CategoryTheory.Abelian.Ext.mk₀ g).comp (P.stableSocleClass hX hXind) ⋯ = 0

Every nonretraction pullback of the distinguished class vanishes.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.ShortComplex.ShortExact.isRightAlmostSplit_of_extClass_annihilator {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] {S : CategoryTheory.ShortComplex (FGModuleCat Bᵐᵒᵖ)} (hS : S.ShortExact) (hne : hS.extClass ≠ 0) (hannihilates : ∀ {Y : FGModuleCat Bᵐᵒᵖ} (g : Y ⟶ S.X₃), ¬CategoryTheory.IsSplitEpi g → (CategoryTheory.Abelian.Ext.mk₀ g).comp hS.extClass ⋯ = 0) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit S.g

A nonzero extension class annihilated by all nonretraction pullbacks makes every representing short exact sequence right almost split.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.stableSocleClass_realization_isRightAlmostSplit {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] [IsAlgClosed k] (P : TwoStepMinimalProjectivePresentation X) (hX : ¬CategoryTheory.Projective X) (hXind : CategoryTheory.Indecomposable X) {E : FGModuleCat Bᵐᵒᵖ} (i : P.nakayamaKernel ⟶ E) (q : E ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i q = 0) (hS : { X₁ := P.nakayamaKernel, X₂ := E, X₃ := X, f := i, g := q, zero := zero }.ShortExact) (hclass : hS.extClass = P.stableSocleClass hX hXind) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit q

A realization of the distinguished stable socle class has right almost-split quotient map.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.exists_stableSocleClass_realization_rightAlmostSplit {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] [IsAlgClosed k] [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] (P : TwoStepMinimalProjectivePresentation X) (hX : ¬CategoryTheory.Projective X) (hXind : CategoryTheory.Indecomposable X) : ∃ (E : FGModuleCat Bᵐᵒᵖ) (i : P.nakayamaKernel ⟶ E) (q : E ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i q = 0) (hS : { X₁ := P.nakayamaKernel, X₂ := E, X₃ := X, f := i, g := q, zero := zero }.ShortExact), hS.extClass = P.stableSocleClass hX hXind ∧ QuotientSubmoduleEquidistribution.IsRightAlmostSplit q

The distinguished class has a finite realization, and its quotient map is right almost split.