Initial stable-socle map from an irreducible projective submodule

An irreducible inclusion U ⟶ P into an indecomposable projective extends through the minimal left almost-split map starting at U. The resulting split epimorphism from the almost-split middle onto P induces a map from the opposite endpoint to P/U. This is the distinguished nonzero stable map which initializes Auslander--Reiten Corollary 3.8.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_cokernel_factorization_of_stable_nonzero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {U : FinitelyGeneratedCategory A} (p : Fin S.n) (g : U ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) (i : S.IndecCategory) (h : S.fgObj i ⟶ CategoryTheory.Limits.cokernel g) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) : ∃ (r : S.fgObj p ⟶ S.fgObj i), CategoryTheory.CategoryStruct.comp r h = CategoryTheory.Limits.cokernel.π g

A nonzero stable map into the quotient by an irreducible projective submodule contains the projective quotient map as a factor. This is the stable-functor form of Auslander--Reiten IV, Proposition 2.7.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_cokernel_epi_of_stable_nonzero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {U : FinitelyGeneratedCategory A} (p : Fin S.n) (g : U ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) (i : S.IndecCategory) (h : S.fgObj i ⟶ CategoryTheory.Limits.cokernel g) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) : CategoryTheory.Epi h

Consequently, a nonzero stable map into this quotient is epic.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_selectedQuotient_factorization_of_stable_nonzero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {U : FinitelyGeneratedCategory A} (p : Fin S.n) (g : U ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) (i : S.IndecCategory) (h : S.fgObj i ⟶ S.fgObj (S.irreducibleIntoProjective_cokernelLabel p g hg hp)) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) : ∃ (r : S.fgObj p ⟶ S.fgObj i), CategoryTheory.CategoryStruct.comp r h = S.irreducibleIntoProjective_quotientMap p g hg hp

The Proposition 2.7 factorization is invariant under the chosen indecomposable coordinates for the cokernel.

A useful functor-category consequence of the Proposition 2.7 factor: the factor from the projective target annihilates every simple generator of a stable subfunctor.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_factor_comp_simpleGenerator_eq_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {U : FinitelyGeneratedCategory A} (p : Fin S.n) (g : U ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) (i : S.IndecCategory) (h : S.fgObj i ⟶ CategoryTheory.Limits.cokernel g) {T : CoveringHom.FiniteDimensionalModuleCategory k} (t : T ⟶ S.finiteProjectiveStableContravariantRepresentable (CategoryTheory.Limits.cokernel g)) [CategoryTheory.Mono t] (pmap : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ T) (hpt : CategoryTheory.CategoryStruct.comp pmap t = S.finiteRestrictedToProjectiveStableMap i h) (r : S.fgObj p ⟶ S.fgObj i) (hr : CategoryTheory.CategoryStruct.comp r h = CategoryTheory.Limits.cokernel.π g) : CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap r) pmap = 0

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableRadicalInclusion_comp_nonzero_to_simple_eq_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) {T : CoveringHom.FiniteDimensionalModuleCategory k} [CategoryTheory.Simple T] (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ T) (hp : p ≠ 0) : CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion i) p = 0

Every simple quotient of a restricted indecomposable representable kills its categorical radical.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableMap_comp_nonzero_to_simple_eq_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (d : C ⟶ S.fgObj i) (hd : ¬CategoryTheory.IsSplitEpi d) {T : CoveringHom.FiniteDimensionalModuleCategory k} [CategoryTheory.Simple T] (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ T) (hp : p ≠ 0) : CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap d) p = 0

Consequently every nonretraction into the representing indecomposable is killed by a nonzero simple quotient of its restricted representable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.nonretraction_comp_simpleStableGenerator_eq_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C : FinitelyGeneratedCategory A} (i j : S.IndecCategory) (d : S.fgObj j ⟶ S.fgObj i) (hd : ¬CategoryTheory.IsSplitEpi d) (h : S.fgObj i ⟶ C) {T : CoveringHom.FiniteDimensionalModuleCategory k} [CategoryTheory.Simple T] (t : T ⟶ S.finiteProjectiveStableContravariantRepresentable C) [CategoryTheory.Mono t] (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ T) (hp : p ≠ 0) (hpt : CategoryTheory.CategoryStruct.comp p t = S.finiteRestrictedToProjectiveStableMap i h) : S.finiteRestrictedToProjectiveStableMap j (CategoryTheory.CategoryStruct.comp d h) = 0

A stable class generating a simple subfunctor vanishes after precomposition by every nonretraction into its representing indecomposable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightAlmostSplit_comp_simpleStableGenerator_factors_projectiveEpi {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {P C : FinitelyGeneratedCategory A} (q : P ⟶ C) [CategoryTheory.Epi q] (hP : CategoryTheory.Projective P) (i : S.IndecCategory) (h : S.fgObj i ⟶ C) {T : CoveringHom.FiniteDimensionalModuleCategory k} [CategoryTheory.Simple T] (t : T ⟶ S.finiteProjectiveStableContravariantRepresentable C) [CategoryTheory.Mono t] (pmap : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ T) (hpmap : pmap ≠ 0) (hpt : CategoryTheory.CategoryStruct.comp pmap t = S.finiteRestrictedToProjectiveStableMap i h) : have B := S.minimalRightAlmostSplitAt i; ∃ (a : B.middle ⟶ P), CategoryTheory.CategoryStruct.comp a q = CategoryTheory.CategoryStruct.comp B.map h

The chosen minimal right almost-split map at a simple stable generator becomes liftable through any projective epimorphism presenting the ambient stable representable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.simpleStableGenerator_not_factors_projectiveEpi {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {P C : FinitelyGeneratedCategory A} (q : P ⟶ C) [CategoryTheory.Epi q] (hP : CategoryTheory.Projective P) (i : S.IndecCategory) (h : S.fgObj i ⟶ C) {T : CoveringHom.FiniteDimensionalModuleCategory k} [CategoryTheory.Simple T] (t : T ⟶ S.finiteProjectiveStableContravariantRepresentable C) [CategoryTheory.Mono t] (pmap : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ T) (hpmap : pmap ≠ 0) (hpt : CategoryTheory.CategoryStruct.comp pmap t = S.finiteRestrictedToProjectiveStableMap i h) : ¬∃ (a : S.fgObj i ⟶ P), CategoryTheory.CategoryStruct.comp a q = h

A morphism representing a nonzero generator of a simple stable subfunctor cannot lift through a projective epimorphism.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_simpleStableGenerator_pullback_isRightAlmostSplit {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) (i : S.IndecCategory) (h : S.fgObj i ⟶ CategoryTheory.Limits.cokernel g) {T : CoveringHom.FiniteDimensionalModuleCategory k} [CategoryTheory.Simple T] (t : T ⟶ S.finiteProjectiveStableContravariantRepresentable (CategoryTheory.Limits.cokernel g)) [CategoryTheory.Mono t] (pmap : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ T) (hpmap : pmap ≠ 0) (hpt : CategoryTheory.CategoryStruct.comp pmap t = S.finiteRestrictedToProjectiveStableMap i h) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.cokernel.π g) h)

Pulling the irreducible projective quotient back along a generator of a simple stable subfunctor produces a right almost-split epimorphism.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_pullback_isRightMinimal_of_isRightAlmostSplit {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) (i : S.IndecCategory) (h : S.fgObj i ⟶ CategoryTheory.Limits.cokernel g) (hAS : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.cokernel.π g) h)) : QuotientSubmoduleEquidistribution.IsRightMinimal (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.cokernel.π g) h)

Any right almost-split pullback projection along the irreducible projective quotient is already right minimal: its kernel is the indecomposable source of the irreducible inclusion.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_simpleStableGenerator_pullback_isRightMinimal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) (i : S.IndecCategory) (h : S.fgObj i ⟶ CategoryTheory.Limits.cokernel g) {T : CoveringHom.FiniteDimensionalModuleCategory k} [CategoryTheory.Simple T] (t : T ⟶ S.finiteProjectiveStableContravariantRepresentable (CategoryTheory.Limits.cokernel g)) [CategoryTheory.Mono t] (pmap : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ T) (hpmap : pmap ≠ 0) (hpt : CategoryTheory.CategoryStruct.comp pmap t = S.finiteRestrictedToProjectiveStableMap i h) : QuotientSubmoduleEquidistribution.IsRightMinimal (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.cokernel.π g) h)

The pullback projection attached to a simple stable generator is right minimal.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_factor_not_isSplitEpi {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {U : FinitelyGeneratedCategory A} (p : Fin S.n) (g : U ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) (i : S.IndecCategory) (h : S.fgObj i ⟶ CategoryTheory.Limits.cokernel g) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) (r : S.fgObj p ⟶ S.fgObj i) (hr : CategoryTheory.CategoryStruct.comp r h = CategoryTheory.Limits.cokernel.π g) : ¬CategoryTheory.IsSplitEpi r

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_factor_thru_radical {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {U : FinitelyGeneratedCategory A} (p : Fin S.n) (g : U ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) (i : S.IndecCategory) (h : S.fgObj i ⟶ CategoryTheory.Limits.cokernel g) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) (r : S.fgObj p ⟶ S.fgObj i) (hr : CategoryTheory.CategoryStruct.comp r h = CategoryTheory.Limits.cokernel.π g) : ∃ (l : S.finiteRestrictedContravariantRepresentable (S.fgObj p) ⟶ S.finiteRestrictedContravariantRepresentableRadical i), CategoryTheory.CategoryStruct.comp l (S.finiteRestrictedContravariantRepresentableRadicalInclusion i) = S.finiteRestrictedContravariantRepresentableMap r

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_source_not_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : ¬CategoryTheory.Injective (S.fgObj u)

The source of an irreducible monomorphism cannot be injective.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_leftExtensionFactor {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) : (S.minimalLeftAlmostSplitAt u).middle ⟶ S.fgObj p

The factor from the chosen left almost-split middle to the projective target.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_leftExtensionFactor_comp {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) : CategoryTheory.CategoryStruct.comp (S.minimalLeftAlmostSplitAt u).map (S.irreducibleIntoProjective_leftExtensionFactor u p g hg) = g

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_leftExtensionFactor_comp_assoc {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) {Z : FGModuleCat Aᵐᵒᵖ} (h : S.fgObj p ⟶ Z) : CategoryTheory.CategoryStruct.comp (S.minimalLeftAlmostSplitAt u).map (CategoryTheory.CategoryStruct.comp (S.irreducibleIntoProjective_leftExtensionFactor u p g hg) h) = CategoryTheory.CategoryStruct.comp g h

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_leftExtensionFactor_isSplitEpi {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) : CategoryTheory.IsSplitEpi (S.irreducibleIntoProjective_leftExtensionFactor u p g hg)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_leftExtensionComplement {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) : QuotientSubmoduleEquidistribution.SplitEpiComplement (S.irreducibleIntoProjective_leftExtensionFactor u p g hg)

The complement to the projective summand in the left almost-split middle.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_initialStableMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : CategoryTheory.Limits.cokernel (S.minimalLeftAlmostSplitAt u).map ⟶ S.fgObj (S.irreducibleIntoProjective_cokernelLabel p g hg hp)

The map from the cokernel of the left almost-split inclusion to the selected quotient P/U.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_cokernelπ_comp_initialStableMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (S.minimalLeftAlmostSplitAt u).map) (S.irreducibleIntoProjective_initialStableMap u p g hg hp) = CategoryTheory.CategoryStruct.comp (S.irreducibleIntoProjective_leftExtensionFactor u p g hg) (S.irreducibleIntoProjective_quotientMap p g hg hp)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_cokernelπ_comp_initialStableMap_assoc {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) {Z : FGModuleCat Aᵐᵒᵖ} (h : S.fgObj (S.irreducibleIntoProjective_cokernelLabel p g hg hp) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (S.minimalLeftAlmostSplitAt u).map) (CategoryTheory.CategoryStruct.comp (S.irreducibleIntoProjective_initialStableMap u p g hg hp) h) = CategoryTheory.CategoryStruct.comp (S.irreducibleIntoProjective_leftExtensionFactor u p g hg) (CategoryTheory.CategoryStruct.comp (S.irreducibleIntoProjective_quotientMap p g hg hp) h)

The following raw version is useful for the socle argument, before transporting the quotient to the chosen skeleton coordinates.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_initialStableMapRaw {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) : CategoryTheory.Limits.cokernel (S.minimalLeftAlmostSplitAt u).map ⟶ CategoryTheory.Limits.cokernel g

The distinguished stable map before transporting the quotient to the chosen skeleton coordinates.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_cokernelπ_comp_initialStableMapRaw {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (S.minimalLeftAlmostSplitAt u).map) (S.irreducibleIntoProjective_initialStableMapRaw u p g hg) = CategoryTheory.CategoryStruct.comp (S.irreducibleIntoProjective_leftExtensionFactor u p g hg) (CategoryTheory.Limits.cokernel.π g)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_cokernelπ_comp_initialStableMapRaw_assoc {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) {Z : FGModuleCat Aᵐᵒᵖ} (h : CategoryTheory.Limits.cokernel g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (S.minimalLeftAlmostSplitAt u).map) (CategoryTheory.CategoryStruct.comp (S.irreducibleIntoProjective_initialStableMapRaw u p g hg) h) = CategoryTheory.CategoryStruct.comp (S.irreducibleIntoProjective_leftExtensionFactor u p g hg) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π g) h)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_initialStableMapRaw_comp_cokernelIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : CategoryTheory.CategoryStruct.comp (S.irreducibleIntoProjective_initialStableMapRaw u p g hg) (S.irreducibleIntoProjective_cokernelIso p g hg hp).hom = S.irreducibleIntoProjective_initialStableMap u p g hg hp

Transporting the raw distinguished map across the selected cokernel isomorphism gives the distinguished map in skeleton coordinates.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_initialStableMapRaw_comp_cokernelIso_assoc {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) {Z : FGModuleCat Aᵐᵒᵖ} (h : S.fgObj (S.irreducibleIntoProjective_cokernelLabel p g hg hp) ⟶ Z) : CategoryTheory.CategoryStruct.comp (S.irreducibleIntoProjective_initialStableMapRaw u p g hg) (CategoryTheory.CategoryStruct.comp (S.irreducibleIntoProjective_cokernelIso p g hg hp).hom h) = CategoryTheory.CategoryStruct.comp (S.irreducibleIntoProjective_initialStableMap u p g hg hp) h

Transporting the raw distinguished map across the selected cokernel isomorphism gives the distinguished map in skeleton coordinates.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_initialStableMapRaw_kernel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : let a := (S.minimalLeftAlmostSplitAt u).map; let t := S.irreducibleIntoProjective_leftExtensionFactor u p g hg; let b := CategoryTheory.Limits.cokernel.π a; have h := S.irreducibleIntoProjective_initialStableMapRaw u p g hg; CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι t) b) ⋯)

The kernel identity underlying the one-summand pullback diagram in Auslander--Reiten Proposition 2.4. The kernel of the induced endpoint map to P/U is the restriction of the upper cokernel map to the kernel of the split epimorphism onto P.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_initialStableMapRaw_isPullback {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : let a := (S.minimalLeftAlmostSplitAt u).map; have t := S.irreducibleIntoProjective_leftExtensionFactor u p g hg; have b := CategoryTheory.Limits.cokernel.π a; have q := CategoryTheory.Limits.cokernel.π g; have h := S.irreducibleIntoProjective_initialStableMapRaw u p g hg; CategoryTheory.IsPullback t b q h

The one-summand square used in Auslander--Reiten Proposition 2.4 is a pullback: the middle split epimorphism and the induced maps on the two cokernels recover the upper middle object.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_initialMiddleIsoProjectiveBiprodKernelRaw {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : (S.minimalLeftAlmostSplitAt u).middle ≅ S.fgObj p ⊞ CategoryTheory.Limits.kernel (S.irreducibleIntoProjective_initialStableMapRaw u p g hg)

The first-socle right almost-split middle is the direct sum of the distinguished projective arm and the kernel of the raw stable generator. This is the object-level B ⊕ DTr C₂ decomposition in the first minimal presentation of Auslander--Reiten Theorem 3.7.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_leftExtensionComplementIsoInitialStableMapRawKernel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : (S.irreducibleIntoProjective_leftExtensionComplement u p g hg).complement ≅ CategoryTheory.Limits.kernel (S.irreducibleIntoProjective_initialStableMapRaw u p g hg)

The split complement of the distinguished projective arm is the kernel of the raw first-socle generator. This identifies the two descriptions of the nonprojective part of the first almost-split middle used in Auslander--Reiten Proposition 2.6 and Theorem 3.7.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_simpleStableGenerator_compare_raw_of_lift {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) (i : S.IndecCategory) (h : S.almostSplitSkeleton.obj i ⟶ CategoryTheory.Limits.cokernel g) (hnot : ¬∃ (a : S.almostSplitSkeleton.obj i ⟶ S.fgObj p), CategoryTheory.CategoryStruct.comp a (CategoryTheory.Limits.cokernel.π g) = h) (a : (S.minimalRightAlmostSplitAt i).middle ⟶ S.fgObj p) (ha : CategoryTheory.CategoryStruct.comp a (CategoryTheory.Limits.cokernel.π g) = CategoryTheory.CategoryStruct.comp (S.minimalRightAlmostSplitAt i).map h) : ∃ (e : S.almostSplitSkeleton.obj i ≅ CategoryTheory.Limits.cokernel (S.minimalLeftAlmostSplitAt u).map) (r : S.almostSplitSkeleton.obj i ⟶ S.fgObj p), h = CategoryTheory.CategoryStruct.comp e.hom (S.irreducibleIntoProjective_initialStableMapRaw u p g hg) + CategoryTheory.CategoryStruct.comp r (CategoryTheory.Limits.cokernel.π g)

Every generator of a simple stable subfunctor is, up to an isomorphism of its indecomposable source and a morphism through the projective middle, the distinguished generator constructed from the left almost-split sequence at U. This is the one-summand form of the comparison in Auslander--Reiten Proposition 2.4 and Lemma 2.3.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_simpleStableGenerator_compare_raw {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) (i : S.IndecCategory) (h : S.almostSplitSkeleton.obj i ⟶ CategoryTheory.Limits.cokernel g) {T : CoveringHom.FiniteDimensionalModuleCategory k} [CategoryTheory.Simple T] (t : T ⟶ S.finiteProjectiveStableContravariantRepresentable (CategoryTheory.Limits.cokernel g)) [CategoryTheory.Mono t] (pmap : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ T) (hpmap : pmap ≠ 0) (hpt : CategoryTheory.CategoryStruct.comp pmap t = S.finiteRestrictedToProjectiveStableMap i h) : ∃ (e : S.almostSplitSkeleton.obj i ≅ CategoryTheory.Limits.cokernel (S.minimalLeftAlmostSplitAt u).map) (r : S.almostSplitSkeleton.obj i ⟶ S.fgObj p), h = CategoryTheory.CategoryStruct.comp e.hom (S.irreducibleIntoProjective_initialStableMapRaw u p g hg) + CategoryTheory.CategoryStruct.comp r (CategoryTheory.Limits.cokernel.π g)

Functor-category form of the raw comparison, with the lift and non-lift hypotheses supplied by a nonzero generator of a simple stable subfunctor.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_initialStableMap_stableClass_ne_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : ProjectiveStable.mk (S.irreducibleIntoProjective_initialStableMap u p g hg hp) ≠ 0

The distinguished map from the opposite endpoint of the left almost-split sequence survives in projective-stable Hom.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_leftCokernel_indecomposable {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : CategoryTheory.Indecomposable (CategoryTheory.Limits.cokernel (S.minimalLeftAlmostSplitAt u).map)

The opposite endpoint of the chosen left almost-split sequence is indecomposable.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_leftCokernelLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : Fin S.n

The selected label of the opposite endpoint of the left almost-split sequence starting at the irreducible projective submodule.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_leftCokernelIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : CategoryTheory.Limits.cokernel (S.minimalLeftAlmostSplitAt u).map ≅ S.fgObj (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp)

The opposite endpoint in the coordinates of the chosen skeleton.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_selectedInitialStableMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : S.fgObj (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) ⟶ S.fgObj (S.irreducibleIntoProjective_cokernelLabel p g hg hp)

The distinguished stable-socle map with its source expressed in the chosen indecomposable skeleton.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_simpleStableGenerator_compare_selected {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) (i : S.IndecCategory) (h : S.fgObj i ⟶ S.fgObj (S.irreducibleIntoProjective_cokernelLabel p g hg hp)) {T : CoveringHom.FiniteDimensionalModuleCategory k} [CategoryTheory.Simple T] (t : T ⟶ S.finiteProjectiveStableContravariantRepresentable (S.fgObj (S.irreducibleIntoProjective_cokernelLabel p g hg hp))) [CategoryTheory.Mono t] (pmap : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ T) (hpmap : pmap ≠ 0) (hpt : CategoryTheory.CategoryStruct.comp pmap t = S.finiteRestrictedToProjectiveStableMap i h) : ∃ (e : S.fgObj i ≅ S.fgObj (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp)) (r : S.fgObj i ⟶ S.fgObj p), h = CategoryTheory.CategoryStruct.comp e.hom (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp) + CategoryTheory.CategoryStruct.comp r (S.irreducibleIntoProjective_quotientMap p g hg hp)

In selected skeleton coordinates, every generator of a simple stable subfunctor differs from the distinguished generator only by a source isomorphism and a morphism through the projective quotient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_selectedInitialStableMap_stableClass_ne_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : ProjectiveStable.mk (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp) ≠ 0

Changing the source to the chosen skeleton coordinates does not kill the distinguished stable class.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_selectedInitialStableMap_obj_stableClass_ne_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : ProjectiveStable.mk (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp).hom ≠ 0

The same distinguished morphism is nonzero in stable Hom after forgetting to the ambient module category.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_selectedLeftCokernelMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : (S.minimalLeftAlmostSplitAt u).middle ⟶ S.fgObj (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp)

The right almost-split quotient map of the left almost-split sequence, transported to the chosen endpoint.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_selectedLeftCokernelMap_isRightAlmostSplit {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (S.irreducibleIntoProjective_selectedLeftCokernelMap u p g hg hp)

The transported cokernel map is right almost split.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_selectedLeftCokernelMap_isRightMinimal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : QuotientSubmoduleEquidistribution.IsRightMinimal (S.irreducibleIntoProjective_selectedLeftCokernelMap u p g hg hp)

The transported cokernel map remains right minimal.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_initialProjectiveArm {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : S.fgObj p ⟶ S.fgObj (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp)

The projective summand of the left almost-split middle supplies an irreducible incoming arm at the selected opposite endpoint.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_initialProjectiveArm_isIrreducible {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (S.irreducibleIntoProjective_initialProjectiveArm u p g hg hp)

The projective arm is irreducible.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_selectedLeftCokernelMap_comp_selectedInitialStableMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : CategoryTheory.CategoryStruct.comp (S.irreducibleIntoProjective_selectedLeftCokernelMap u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp) = CategoryTheory.CategoryStruct.comp (S.irreducibleIntoProjective_leftExtensionFactor u p g hg) (S.irreducibleIntoProjective_quotientMap p g hg hp)

The transported right almost-split map followed by the distinguished map factors through the projective quotient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_selectedLeftCokernelMap_comp_selectedInitialStableMap_assoc {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) {Z : FGModuleCat Aᵐᵒᵖ} (h : S.fgObj (S.irreducibleIntoProjective_cokernelLabel p g hg hp) ⟶ Z) : CategoryTheory.CategoryStruct.comp (S.irreducibleIntoProjective_selectedLeftCokernelMap u p g hg hp) (CategoryTheory.CategoryStruct.comp (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp) h) = CategoryTheory.CategoryStruct.comp (S.irreducibleIntoProjective_leftExtensionFactor u p g hg) (CategoryTheory.CategoryStruct.comp (S.irreducibleIntoProjective_quotientMap p g hg hp) h)

The transported right almost-split map followed by the distinguished map factors through the projective quotient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_selectedInitialStableNaturalMap_ne_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : S.finiteRestrictedToProjectiveStableMap (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp) ≠ 0

The selected distinguished morphism induces a nonzero map from its restricted representable into the stable representable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_selectedLeftCokernelMap_comp_selectedInitialStableNaturalMap_eq_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap (S.irreducibleIntoProjective_selectedLeftCokernelMap u p g hg hp)) (S.finiteRestrictedToProjectiveStableMap (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp)) = 0

The whole right almost-split map at the opposite endpoint is killed by the distinguished map in the projective-stable quotient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_selectedInitialStableMap_killsRadical {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp)) (S.finiteRestrictedToProjectiveStableMap (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp)) = 0

The distinguished map kills the radical of its representing indecomposable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_selectedInitialStableImage_simple {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : CategoryTheory.Simple (S.finiteProjectiveStableImage (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp))

The image generated by the distinguished stable class is simple. This is the first socle layer in Auslander--Reiten Theorem 3.7.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_selectedInitialStableImageInclusion_isEssential {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : IsEssentialMono (S.finiteProjectiveStableImageInclusion (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp))

The distinguished simple cyclic image is the essential socle of the stable representable of P/U. Equivalently, every simple subfunctor factors through this one image.