The distinguished stable socle extension in a finite functor category

At a nonprojective indecomposable endpoint over an algebraically closed field, the residue map of the local endomorphism algebra descends to projective-stable endomorphisms and takes the stable identity to one. The finite-representable stable Hom--Ext formula transports this functional to a nonzero extension class. Pullback along every nonretraction kills that class, so every short exact realization has a right almost-split terminal map.

@[reducible, inline]

abbrev MagnitudeConjecture.CoveringHom.FiniteModule {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : Type (max (max u v) (v + 1))

theorem MagnitudeConjecture.CoveringHom.isSplitEpi_right_of_comp {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {W X Y : FiniteModule} (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.CoveringHom.isSplitEpi_smul_id_of_ne_zero {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : FiniteModule) {c : k} (hc : c ≠ 0) : CategoryTheory.IsSplitEpi (c • CategoryTheory.CategoryStruct.id X)

A nonzero scalar multiple of the identity is a retraction.

theorem MagnitudeConjecture.CoveringHom.endomorphism_eq_zero_of_not_isSplitEpi_of_eq_smul_id {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : FiniteModule) (hscalar : ∀ (r : X ⟶ X), ∃ (c : k), c • CategoryTheory.CategoryStruct.id X = r) (r : X ⟶ X) (hr : ¬CategoryTheory.IsSplitEpi r) : r = 0

At a scalar-endomorphism object, every nonretraction endomorphism is zero.

noncomputable def MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.stableIdentityFunctional {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} {M : FiniteModule} [IsAlgClosed k] (_P : TwoStepMinimalFiniteRepresentablePresentation hP M) (hM : ¬CategoryTheory.Projective M) (hMind : CategoryTheory.Indecomposable M) : ProjectiveStable.Hom M M →ₗ[k] k

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

@[simp]

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.stableIdentityFunctional_id {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} {M : FiniteModule} [IsAlgClosed k] (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (hM : ¬CategoryTheory.Projective M) (hMind : CategoryTheory.Indecomposable M) : (P.stableIdentityFunctional hM hMind) (ProjectiveStable.mk (CategoryTheory.CategoryStruct.id M)) = 1

noncomputable def MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.stableSocleClass {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteModule} [IsAlgClosed k] [CategoryTheory.HasExt FiniteModule] (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (hM : ¬CategoryTheory.Projective M) (hMind : CategoryTheory.Indecomposable M) : CategoryTheory.Abelian.Ext M (nakayamaKernel hI P) 1

The distinguished extension class selected by the stable identity.

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.stableSocleClass_ne_zero {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteModule} [IsAlgClosed k] [CategoryTheory.HasExt FiniteModule] (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (hM : ¬CategoryTheory.Projective M) (hMind : CategoryTheory.Indecomposable M) : stableSocleClass hI P hM hMind ≠ 0

The distinguished class is nonzero.

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.pullback_stableSocleClass_eq_zero_of_not_isSplitEpi {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteModule} [IsAlgClosed k] [CategoryTheory.HasExt FiniteModule] (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (hM : ¬CategoryTheory.Projective M) (hMind : CategoryTheory.Indecomposable M) {Y : FiniteModule} (g : Y ⟶ M) (hg : ¬CategoryTheory.IsSplitEpi g) : (CategoryTheory.Abelian.Ext.mk₀ g).comp (stableSocleClass hI P hM hMind) ⋯ = 0

Every nonretraction pullback of the distinguished class vanishes.

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.ShortComplex.ShortExact.isRightAlmostSplit_of_extClass_annihilator {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt FiniteModule] {S : CategoryTheory.ShortComplex FiniteModule} (hS : S.ShortExact) (hne : hS.extClass ≠ 0) (hannihilates : ∀ {Y : FiniteModule} (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.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.stableSocleClass_realization_isRightAlmostSplit {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteModule} [IsAlgClosed k] [CategoryTheory.HasExt FiniteModule] (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (hM : ¬CategoryTheory.Projective M) (hMind : CategoryTheory.Indecomposable M) {E : FiniteModule} (i : nakayamaKernel hI P ⟶ E) (q : E ⟶ M) (zero : CategoryTheory.CategoryStruct.comp i q = 0) (hS : { X₁ := nakayamaKernel hI P, X₂ := E, X₃ := M, f := i, g := q, zero := zero }.ShortExact) (hclass : hS.extClass = stableSocleClass hI P hM hMind) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit q

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

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.exists_stableSocleClass_realization_rightAlmostSplit {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteModule} [IsAlgClosed k] [CategoryTheory.HasExt FiniteModule] (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (hM : ¬CategoryTheory.Projective M) (hMind : CategoryTheory.Indecomposable M) : ∃ (E : FiniteModule) (i : nakayamaKernel hI P ⟶ E) (q : E ⟶ M) (zero : CategoryTheory.CategoryStruct.comp i q = 0) (hS : { X₁ := nakayamaKernel hI P, X₂ := E, X₃ := M, f := i, g := q, zero := zero }.ShortExact), hS.extClass = stableSocleClass hI P hM hMind ∧ QuotientSubmoduleEquidistribution.IsRightAlmostSplit q

The distinguished class has a realization whose quotient map is right almost split.