Ascending socle induction for stable representables

This file connects the distinguished essential stable socle associated to an irreducible projective submodule with the abstract uniserial-extension step. The remaining source-specific task is to identify and control the successive socles of the displayed cokernels.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableFunctor {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor (FinitelyGeneratedCategory A) (CoveringHom.FiniteDimensionalModuleCategory k)

Restricted contravariant Yoneda, with both source and target kept in the finite module categories used by the stable-representable argument.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableFunctor_additive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.finiteRestrictedContravariantRepresentableFunctor.Additive

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentable_projective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (C : FinitelyGeneratedCategory A) : CategoryTheory.Projective (S.finiteRestrictedContravariantRepresentable C)

Restricted representables of arbitrary finitely generated modules are projective: decompose the module into chosen indecomposables and use additivity of restricted Yoneda.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_eq_finiteRestrictedContravariantRepresentableMap {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) (C : FinitelyGeneratedCategory A) (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ S.finiteRestrictedContravariantRepresentable C) : ∃ (h : S.fgObj i ⟶ C), S.finiteRestrictedContravariantRepresentableMap h = p

Restricted Yoneda is full for maps whose source is one chosen indecomposable, even when the represented target is decomposable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableMap_injective_from_fgObj {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) (C : FinitelyGeneratedCategory A) : Function.Injective fun (h : S.fgObj i ⟶ C) => S.finiteRestrictedContravariantRepresentableMap h

Restricted Yoneda detects equality of maps out of a chosen indecomposable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedContravariantRepresentableMap_injective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (B C : FinitelyGeneratedCategory A) : Function.Injective fun (h : B ⟶ C) => S.finiteRestrictedContravariantRepresentableMap h

Restricted Yoneda detects equality of maps between arbitrary finitely generated modules. Decomposing the source reduces this to detection from the chosen indecomposable representatives.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_eq_finiteRestrictedContravariantRepresentableMap_to_fgObj {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (B : FinitelyGeneratedCategory A) (i : S.IndecCategory) (p : S.finiteRestrictedContravariantRepresentable B ⟶ S.finiteRestrictedContravariantRepresentable (S.fgObj i)) : ∃ (h : B ⟶ S.fgObj i), S.finiteRestrictedContravariantRepresentableMap h = p

Restricted Yoneda is full for maps into a chosen indecomposable as well; the source is first decomposed into chosen indecomposables.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_splitEpi_with_map_eq_of_finiteRestrictedContravariantRepresentable_splitEpi {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (B : FinitelyGeneratedCategory A) (i : S.IndecCategory) (a : S.finiteRestrictedContravariantRepresentable B ⟶ S.finiteRestrictedContravariantRepresentable (S.fgObj i)) (ha : CategoryTheory.IsSplitEpi a) : ∃ (r : B ⟶ S.fgObj i), CategoryTheory.IsSplitEpi r ∧ S.finiteRestrictedContravariantRepresentableMap r = a

A split epimorphism from an arbitrary restricted representable onto a chosen indecomposable representable is induced by a split epimorphism of modules, with the inducing equation retained.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_splitEpi_of_finiteRestrictedContravariantRepresentable_splitEpi {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (B : FinitelyGeneratedCategory A) (i : S.IndecCategory) (a : S.finiteRestrictedContravariantRepresentable B ⟶ S.finiteRestrictedContravariantRepresentable (S.fgObj i)) (ha : CategoryTheory.IsSplitEpi a) : ∃ (r : B ⟶ S.fgObj i), CategoryTheory.IsSplitEpi r

A split epimorphism between restricted representables reflects to a split epimorphism of the representing modules.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_projectiveFactor_of_finiteRestrictedStableComposites_eq {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {B C : FinitelyGeneratedCategory A} (p : Fin S.n) (q : S.fgObj p ⟶ C) [CategoryTheory.Epi q] (hp : CategoryTheory.Projective (S.fgObj p)) (f g : B ⟶ C) (hfg : CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap f) (S.finiteProjectiveStableQuotient C) = CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap g) (S.finiteProjectiveStableQuotient C)) : ∃ (s : B ⟶ S.fgObj p), S.finiteRestrictedContravariantRepresentableMap (CategoryTheory.CategoryStruct.comp s q) = S.finiteRestrictedContravariantRepresentableMap f - S.finiteRestrictedContravariantRepresentableMap g

Equality after passing to the restricted projective-stable representable lifts, at the representable level, to a difference through a chosen projective epimorphism. This is the exactness step needed to retain the actual projective coordinate in the multiplicity-sensitive first-socle comparison.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.arrowMultiplicity_pos_of_splitEpi_minimalRightAlmostSplitMiddle {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i c : S.IndecCategory) (hi : ¬CategoryTheory.Projective (S.fgObj i)) (r : (S.minimalRightAlmostSplitAt i).middle ⟶ S.fgObj c) (hr : CategoryTheory.IsSplitEpi r) : 0 < FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData c i

A chosen indecomposable split quotient of a minimal right almost-split middle contributes a positive incoming-arrow multiplicity.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightKernelMap_comp_splitEpi_isIrreducible {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i c : S.IndecCategory) (hi : ¬CategoryTheory.Projective (S.fgObj i)) (r : (S.minimalRightAlmostSplitAt i).middle ⟶ S.fgObj c) (hr : CategoryTheory.IsSplitEpi r) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (CategoryTheory.CategoryStruct.comp (S.rightKernelMap ⟨i, hi⟩) r)

Projecting the Auslander--Reiten kernel inclusion to an indecomposable split quotient of the middle term gives the corresponding translated irreducible arm.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.minimalRightAlmostSplit_splitEpi_simpleCover_proportional {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i c : S.IndecCategory) (hi : ¬CategoryTheory.Projective (S.fgObj i)) {L : CoveringHom.FiniteDimensionalModuleCategory k} [CategoryTheory.Simple L] (pL : S.finiteRestrictedContravariantRepresentable (S.fgObj c) ⟶ L) (hpL : pL ≠ 0) (r r' : (S.minimalRightAlmostSplitAt i).middle ⟶ S.fgObj c) (hr : CategoryTheory.IsSplitEpi r) (hr' : CategoryTheory.IsSplitEpi r') : ∃ (a : k), CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap r') pL = a • CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap r) pL

For a fixed simple cover, two split quotient coordinates from the same minimal right almost-split middle induce scalar-proportional maps. Indeed, after subtracting the scalar detected on one chosen section, an independent split quotient would exhibit two copies of the same indecomposable in the middle. Representation-finite square-freeness rules this out.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.minimalRightAlmostSplit_quotientMaps_proportional_of_boundary {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) {L G : CoveringHom.FiniteDimensionalModuleCategory k} [CategoryTheory.Simple L] (l : L ⟶ G) [CategoryTheory.Mono l] (hl : IsEssentialMono l) (H H' : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G) (a a' : S.finiteRestrictedContravariantRepresentable (S.minimalRightAlmostSplitAt i).middle ⟶ L) (ha : CategoryTheory.CategoryStruct.comp a l = CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap (S.minimalRightAlmostSplitAt i).map) H) (ha' : CategoryTheory.CategoryStruct.comp a' l = CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap (S.minimalRightAlmostSplitAt i).map) H') (α : k) (hprop : a' = α • a) : CategoryTheory.CategoryStruct.comp H' (CategoryTheory.Limits.cokernel.π l) = CategoryTheory.CategoryStruct.comp (α • H) (CategoryTheory.Limits.cokernel.π l)

If two maps out of one indecomposable restricted representable have scalar-proportional restrictions along the minimal right almost-split map, then they become scalar-proportional after quotienting by an essential simple subobject.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.not_projective_of_finiteRestrictedToProjectiveStableMap_ne_zero {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) : ¬CategoryTheory.Projective (S.fgObj i)

A nonzero stable map cannot be generated by a projective module.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_eq_finiteRestrictedToProjectiveStableMap {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) (C : FinitelyGeneratedCategory A) (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ S.finiteProjectiveStableContravariantRepresentable C) : ∃ (h : S.fgObj i ⟶ C), S.finiteRestrictedToProjectiveStableMap i h = p

Every map from a chosen indecomposable restricted representable to a stable representable is induced by an actual module morphism.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_restrictedRepresentable_lift_of_nonzero_cokernel {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {H G : CoveringHom.FiniteDimensionalModuleCategory k} (m : H ⟶ G) [CategoryTheory.Mono m] (hquotient : ¬CategoryTheory.Limits.IsZero (CategoryTheory.Limits.cokernel m)) : ∃ (T : CoveringHom.FiniteDimensionalModuleCategory k) (t : T ⟶ CategoryTheory.Limits.cokernel m) (i : S.IndecCategory) (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ T) (h : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G), CategoryTheory.Simple T ∧ CategoryTheory.Mono t ∧ p ≠ 0 ∧ h ≠ 0 ∧ CategoryTheory.CategoryStruct.comp h (CategoryTheory.Limits.cokernel.π m) = CategoryTheory.CategoryStruct.comp p t

Every chosen simple subobject of a nonzero cokernel lifts from one indecomposable restricted representable. This projective lifting statement does not require the subobject being quotiented out to be simple or essential.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.restrictedRepresentableLift_contains_of_waist {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {H G T : CoveringHom.FiniteDimensionalModuleCategory k} (m : H ⟶ G) [CategoryTheory.Mono m] (hm : IsUniserialObject.IsWaistSubobject (CategoryTheory.Subobject.mk m)) (t : T ⟶ CategoryTheory.Limits.cokernel m) [CategoryTheory.Mono t] (i : S.IndecCategory) (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ T) (hp : p ≠ 0) (h : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G) (hcomp : CategoryTheory.CategoryStruct.comp h (CategoryTheory.Limits.cokernel.π m) = CategoryTheory.CategoryStruct.comp p t) : CategoryTheory.Subobject.mk m ≤ CategoryTheory.Limits.imageSubobject h

A representable lift which is nonzero modulo a waist subobject contains that subobject.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_restrictedRepresentable_lift_of_nonzero_essentialSimpleCokernel {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {L G : CoveringHom.FiniteDimensionalModuleCategory k} [CategoryTheory.Simple L] (l : L ⟶ G) [CategoryTheory.Mono l] (hl : IsEssentialMono l) (hquotient : ¬CategoryTheory.Limits.IsZero (CategoryTheory.Limits.cokernel l)) : ∃ (T : CoveringHom.FiniteDimensionalModuleCategory k) (t : T ⟶ CategoryTheory.Limits.cokernel l) (i : S.IndecCategory) (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ T) (h : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G), CategoryTheory.Simple T ∧ CategoryTheory.Mono t ∧ p ≠ 0 ∧ h ≠ 0 ∧ CategoryTheory.CategoryStruct.comp h (CategoryTheory.Limits.cokernel.π l) = CategoryTheory.CategoryStruct.comp p t ∧ CategoryTheory.Subobject.mk l ≤ CategoryTheory.Limits.imageSubobject h

Above a simple essential layer, every chosen simple subobject of the cokernel lifts from a single indecomposable representable. Essentiality forces the lifted cyclic image to contain the preceding layer.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.restrictedRepresentableLift_cokernel_simple {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {L G T : CoveringHom.FiniteDimensionalModuleCategory k} (l : L ⟶ G) [CategoryTheory.Mono l] [CategoryTheory.Simple T] (t : T ⟶ CategoryTheory.Limits.cokernel l) [CategoryTheory.Mono t] (i : S.IndecCategory) (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ T) (hp : p ≠ 0) (h : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G) (hcomp : CategoryTheory.CategoryStruct.comp h (CategoryTheory.Limits.cokernel.π l) = CategoryTheory.CategoryStruct.comp p t) (hle : CategoryTheory.Subobject.mk l ≤ CategoryTheory.Limits.imageSubobject h) : ∃ (lH : L ⟶ S.finiteRepresentableImage i h), CategoryTheory.Mono lH ∧ CategoryTheory.CategoryStruct.comp lH (S.finiteRepresentableImageInclusion i h) = l ∧ CategoryTheory.Simple (CategoryTheory.Limits.cokernel lH)

The lifted cyclic image is the next one-step extension of the preceding essential layer: its quotient by that layer is the chosen simple subobject of the ambient cokernel.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableImageRadical_eq_of_essentialSimpleCokernel {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {L : CoveringHom.FiniteDimensionalModuleCategory k} [CategoryTheory.Simple L] {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) (l : L ⟶ S.finiteProjectiveStableImage i h) [CategoryTheory.Mono l] (hl : IsEssentialMono l) [CategoryTheory.Simple (CategoryTheory.Limits.cokernel l)] : CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion i) (S.finiteProjectiveStableImagePresentation i h)) = CategoryTheory.Subobject.mk l

In a nonzero cyclic stable image, any simple essential layer with simple quotient is exactly the pushed-forward representable radical.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableImageRadical_eq_of_uniserialSimpleCokernel {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {L : CoveringHom.FiniteDimensionalModuleCategory k} {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) (hH : IsUniserialObject (S.finiteProjectiveStableImage i h)) (l : L ⟶ S.finiteProjectiveStableImage i h) [hlmono : CategoryTheory.Mono l] [hlsimple : CategoryTheory.Simple (CategoryTheory.Limits.cokernel l)] : CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion i) (S.finiteProjectiveStableImagePresentation i h)) = CategoryTheory.Subobject.mk l

In a uniserial cyclic stable image, any subobject with simple cokernel is the pushed-forward representable radical.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableImage_projectiveCover_split_from_rightAlmostSplitMiddle {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {L : CoveringHom.FiniteDimensionalModuleCategory k} [CategoryTheory.Simple L] {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) (l : L ⟶ S.finiteProjectiveStableImage i h) [CategoryTheory.Mono l] (hl : IsEssentialMono l) [CategoryTheory.Simple (CategoryTheory.Limits.cokernel l)] (P : MinimalProjectivePresentation L) {B : FinitelyGeneratedCategory A} (b : B ⟶ S.fgObj i) (hb : QuotientSubmoduleEquidistribution.IsRightAlmostSplit b) : ∃ (a : S.finiteRestrictedContravariantRepresentable B ⟶ P.p), CategoryTheory.IsSplitEpi a ∧ CategoryTheory.CategoryStruct.comp a (CategoryTheory.CategoryStruct.comp P.f l) = CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap b) (S.finiteProjectiveStableImagePresentation i h)

The projective cover of the preceding simple layer splits from the restricted representable of the right almost-split middle at the next cyclic generator. This is the projective-cover comparison underlying the special case of Auslander--Reiten Proposition 2.6 used in the socle induction.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableImage_projectiveCover_split_from_rightAlmostSplitMiddle_of_uniserial {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {L : CoveringHom.FiniteDimensionalModuleCategory k} {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) (hH : IsUniserialObject (S.finiteProjectiveStableImage i h)) (l : L ⟶ S.finiteProjectiveStableImage i h) [CategoryTheory.Mono l] [CategoryTheory.Simple (CategoryTheory.Limits.cokernel l)] (P : MinimalProjectivePresentation L) {B : FinitelyGeneratedCategory A} (b : B ⟶ S.fgObj i) (hb : QuotientSubmoduleEquidistribution.IsRightAlmostSplit b) : ∃ (a : S.finiteRestrictedContravariantRepresentable B ⟶ P.p), CategoryTheory.IsSplitEpi a ∧ CategoryTheory.CategoryStruct.comp a (CategoryTheory.CategoryStruct.comp P.f l) = CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap b) (S.finiteProjectiveStableImagePresentation i h)

The projective-cover comparison does not require the preceding layer to be simple: it is enough that the candidate cyclic image is uniserial and the preceding layer has simple quotient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableImage_moduleCover_split_from_rightAlmostSplitMiddle_of_uniserial {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C : FinitelyGeneratedCategory A} (j : S.IndecCategory) (g : S.fgObj j ⟶ C) (gstable : S.finiteRestrictedToProjectiveStableMap j g ≠ 0) (i : S.IndecCategory) (h : S.fgObj i ⟶ C) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) (lH : S.finiteProjectiveStableImage j g ⟶ S.finiteProjectiveStableImage i h) [CategoryTheory.Mono lH] (hH : IsUniserialObject (S.finiteProjectiveStableImage i h)) [CategoryTheory.Simple (CategoryTheory.Limits.cokernel lH)] : ∃ (r : (S.minimalRightAlmostSplitAt i).middle ⟶ S.fgObj j), CategoryTheory.IsSplitEpi r ∧ QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (CategoryTheory.CategoryStruct.comp (S.rightKernelMap ⟨i, ⋯⟩) r) ∧ CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap r) (CategoryTheory.CategoryStruct.comp (S.finiteProjectiveStableImagePresentation j g) lH) = CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap (S.minimalRightAlmostSplitAt i).map) (S.finiteProjectiveStableImagePresentation i h)

At an arbitrary uniserial cyclic stage, the module generating the preceding layer splits from the minimal right almost-split middle of a one-step cyclic extension.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableImage_nextExtension_label_eq_of_nonzeroRadical {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (harity : ∀ (z : S.IndecCategory), ¬CategoryTheory.Projective (S.fgObj z) → FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData z ≤ 2) {C : FinitelyGeneratedCategory A} (j : S.IndecCategory) (g : S.fgObj j ⟶ C) (gstable : S.finiteRestrictedToProjectiveStableMap j g ≠ 0) (hRzero : ¬CategoryTheory.Limits.IsZero (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion j) (S.finiteProjectiveStableImagePresentation j g))))) (i i' : S.IndecCategory) (h : S.fgObj i ⟶ C) (h' : S.fgObj i' ⟶ C) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) (hstable' : S.finiteRestrictedToProjectiveStableMap i' h' ≠ 0) (lH : S.finiteProjectiveStableImage j g ⟶ S.finiteProjectiveStableImage i h) (lH' : S.finiteProjectiveStableImage j g ⟶ S.finiteProjectiveStableImage i' h') [CategoryTheory.Mono lH] [CategoryTheory.Simple (CategoryTheory.Limits.cokernel lH)] [CategoryTheory.Mono lH'] [CategoryTheory.Simple (CategoryTheory.Limits.cokernel lH')] (hH : IsUniserialObject (S.finiteProjectiveStableImage i h)) (hH' : IsUniserialObject (S.finiteProjectiveStableImage i' h')) (hlHcomp : CategoryTheory.CategoryStruct.comp lH (S.finiteProjectiveStableImageInclusion i h) = S.finiteProjectiveStableImageInclusion j g) (hlHcomp' : CategoryTheory.CategoryStruct.comp lH' (S.finiteProjectiveStableImageInclusion i' h') = S.finiteProjectiveStableImageInclusion j g) : i' = i

Above a cyclic predecessor with nonzero radical, two one-step uniserial extensions have the same generator label. Their translated kernel arms are both irreducible incoming arms killed by the predecessor generator, whose source is unique under the two-arm bound.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableImage_nextExtension_quotientMaps_proportional {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {C : FinitelyGeneratedCategory A} (j : S.IndecCategory) (g : S.fgObj j ⟶ C) (gstable : S.finiteRestrictedToProjectiveStableMap j g ≠ 0) {R : CoveringHom.FiniteDimensionalModuleCategory k} (s : R ⟶ S.finiteProjectiveStableImage j g) [CategoryTheory.Mono s] [CategoryTheory.Simple (CategoryTheory.Limits.cokernel s)] (i : S.IndecCategory) (h h' : S.fgObj i ⟶ C) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) (hstable' : S.finiteRestrictedToProjectiveStableMap i h' ≠ 0) (lH : S.finiteProjectiveStableImage j g ⟶ S.finiteProjectiveStableImage i h) (lH' : S.finiteProjectiveStableImage j g ⟶ S.finiteProjectiveStableImage i h') [CategoryTheory.Mono lH] [CategoryTheory.Simple (CategoryTheory.Limits.cokernel lH)] [CategoryTheory.Mono lH'] [CategoryTheory.Simple (CategoryTheory.Limits.cokernel lH')] (hH : IsUniserialObject (S.finiteProjectiveStableImage i h)) (hH' : IsUniserialObject (S.finiteProjectiveStableImage i h')) (hlHcomp : CategoryTheory.CategoryStruct.comp lH (S.finiteProjectiveStableImageInclusion i h) = S.finiteProjectiveStableImageInclusion j g) (hlHcomp' : CategoryTheory.CategoryStruct.comp lH' (S.finiteProjectiveStableImageInclusion i h') = S.finiteProjectiveStableImageInclusion j g) (htopEssential : IsEssentialMono (cokernelInclusionOfComp s (S.finiteProjectiveStableImageInclusion j g))) : ∃ (α : k), CategoryTheory.CategoryStruct.comp (S.finiteRestrictedToProjectiveStableMap i h') (CategoryTheory.Limits.cokernel.π (S.finiteProjectiveStableImageInclusion j g)) = CategoryTheory.CategoryStruct.comp (α • S.finiteRestrictedToProjectiveStableMap i h) (CategoryTheory.Limits.cokernel.π (S.finiteProjectiveStableImageInclusion j g))

At an arbitrary noninitial cyclic stage, scalar proportionality on the simple top of the predecessor descends through the two-step quotient. The essentiality of that simple top in the ambient quotient is the induction invariant supplied by the preceding successor step.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_nextCyclicWaistExtension_of_nonzero_cokernel {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {H G : CoveringHom.FiniteDimensionalModuleCategory k} (m : H ⟶ G) [CategoryTheory.Mono m] (hmEssential : IsEssentialMono m) (hmWaist : IsUniserialObject.IsWaistSubobject (CategoryTheory.Subobject.mk m)) (hH : IsUniserialObject H) (hquotient : ¬CategoryTheory.Limits.IsZero (CategoryTheory.Limits.cokernel m)) : ∃ (i : S.IndecCategory) (h : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G) (mK : H ⟶ S.finiteRepresentableImage i h), h ≠ 0 ∧ CategoryTheory.Mono mK ∧ CategoryTheory.CategoryStruct.comp mK (S.finiteRepresentableImageInclusion i h) = m ∧ CategoryTheory.Simple (CategoryTheory.Limits.cokernel mK) ∧ IsUniserialObject (S.finiteRepresentableImage i h) ∧ IsEssentialMono (S.finiteRepresentableImageInclusion i h)

A nonterminal cyclic waist layer admits a larger cyclic layer with simple quotient. The waist property supplies the containment which, at later stages, cannot be obtained from essentiality alone.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableImage_nextExtension_cokernelMap_essential {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (harity : ∀ (z : S.IndecCategory), ¬CategoryTheory.Projective (S.fgObj z) → FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData z ≤ 2) {C : FinitelyGeneratedCategory A} (j : S.IndecCategory) (g : S.fgObj j ⟶ C) (gstable : S.finiteRestrictedToProjectiveStableMap j g ≠ 0) (hRzero : ¬CategoryTheory.Limits.IsZero (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion j) (S.finiteProjectiveStableImagePresentation j g))))) {R : CoveringHom.FiniteDimensionalModuleCategory k} (s : R ⟶ S.finiteProjectiveStableImage j g) [CategoryTheory.Mono s] [CategoryTheory.Simple (CategoryTheory.Limits.cokernel s)] (hJ : IsUniserialObject (S.finiteProjectiveStableImage j g)) (hjWaist : IsUniserialObject.IsWaistSubobject (CategoryTheory.Subobject.mk (S.finiteProjectiveStableImageInclusion j g))) (htopEssential : IsEssentialMono (cokernelInclusionOfComp s (S.finiteProjectiveStableImageInclusion j g))) (i : S.IndecCategory) (h : S.fgObj i ⟶ C) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) (lH : S.finiteProjectiveStableImage j g ⟶ S.finiteProjectiveStableImage i h) [hlHmono : CategoryTheory.Mono lH] [hlHsimple : CategoryTheory.Simple (CategoryTheory.Limits.cokernel lH)] (hH : IsUniserialObject (S.finiteProjectiveStableImage i h)) (hlHcomp : CategoryTheory.CategoryStruct.comp lH (S.finiteProjectiveStableImageInclusion i h) = S.finiteProjectiveStableImageInclusion j g) : ∃ (t₀ : CategoryTheory.Limits.cokernel lH ⟶ CategoryTheory.Limits.cokernel (S.finiteProjectiveStableImageInclusion j g)), CategoryTheory.Mono t₀ ∧ IsEssentialMono t₀ ∧ CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π lH) t₀ = CategoryTheory.CategoryStruct.comp (S.finiteProjectiveStableImageInclusion i h) (CategoryTheory.Limits.cokernel.π (S.finiteProjectiveStableImageInclusion j g)) ∧ IsEssentialMono (cokernelInclusionOfComp lH (S.finiteProjectiveStableImageInclusion i h))

At an arbitrary noninitial cyclic stage, a chosen one-step extension gives an essential simple top in the quotient by its predecessor.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableRepresentable_isUniserial_of_cyclicWaistStage {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (harity : ∀ (z : S.IndecCategory), ¬CategoryTheory.Projective (S.fgObj z) → FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData z ≤ 2) {C : FinitelyGeneratedCategory A} (j : S.IndecCategory) (g : S.fgObj j ⟶ C) (gstable : S.finiteRestrictedToProjectiveStableMap j g ≠ 0) (hRzero : ¬CategoryTheory.Limits.IsZero (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion j) (S.finiteProjectiveStableImagePresentation j g))))) {R : CoveringHom.FiniteDimensionalModuleCategory k} (s : R ⟶ S.finiteProjectiveStableImage j g) [CategoryTheory.Mono s] [CategoryTheory.Simple (CategoryTheory.Limits.cokernel s)] (hJ : IsUniserialObject (S.finiteProjectiveStableImage j g)) (hmEssential : IsEssentialMono (S.finiteProjectiveStableImageInclusion j g)) (hmWaist : IsUniserialObject.IsWaistSubobject (CategoryTheory.Subobject.mk (S.finiteProjectiveStableImageInclusion j g))) (htopEssential : IsEssentialMono (cokernelInclusionOfComp s (S.finiteProjectiveStableImageInclusion j g))) : IsUniserialObject (S.finiteProjectiveStableContravariantRepresentable C)

Finite ascending-socle induction from a noninitial cyclic waist stage. The two-arm bound makes every successive simple top essential, so the waist strictly grows until it is the whole stable representable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_nextCyclicEssentialExtension_of_nonzero_cokernel {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {L G : CoveringHom.FiniteDimensionalModuleCategory k} [CategoryTheory.Simple L] (l : L ⟶ G) [CategoryTheory.Mono l] (hl : IsEssentialMono l) (hquotient : ¬CategoryTheory.Limits.IsZero (CategoryTheory.Limits.cokernel l)) : ∃ (i : S.IndecCategory) (h : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G) (lH : L ⟶ S.finiteRepresentableImage i h), h ≠ 0 ∧ CategoryTheory.Mono lH ∧ CategoryTheory.CategoryStruct.comp lH (S.finiteRepresentableImageInclusion i h) = l ∧ CategoryTheory.Simple (CategoryTheory.Limits.cokernel lH) ∧ IsEssentialMono lH ∧ IsUniserialObject (S.finiteRepresentableImage i h) ∧ IsEssentialMono (S.finiteRepresentableImageInclusion i h)

Every nonterminal simple essential layer lies in a larger essential cyclic layer whose quotient by it is simple. This is the existence half of the ascending socle successor; the two-arm argument must still prove uniqueness of the simple layer in the ambient quotient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_leftExtensionComplement_zero_or_indecomposable {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (harity : ∀ (i : S.IndecCategory), ¬CategoryTheory.Projective (S.fgObj i) → FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData i ≤ 2) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : CategoryTheory.Limits.IsZero (S.irreducibleIntoProjective_leftExtensionComplement u p g hg).complement ∨ CategoryTheory.Indecomposable (S.irreducibleIntoProjective_leftExtensionComplement u p g hg).complement

Under the two-arm bound, removing the distinguished projective summand from the right almost-split middle at the first stable-socle generator leaves either zero or one indecomposable complement.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_initialStableMapRaw_kernel_zero_or_indecomposable {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (harity : ∀ (i : S.IndecCategory), ¬CategoryTheory.Projective (S.fgObj i) → FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData i ≤ 2) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : CategoryTheory.Limits.IsZero (CategoryTheory.Limits.kernel (S.irreducibleIntoProjective_initialStableMapRaw u p g hg)) ∨ CategoryTheory.Indecomposable (CategoryTheory.Limits.kernel (S.irreducibleIntoProjective_initialStableMapRaw u p g hg))

Under the two-arm bound, the kernel of the raw first-socle generator is zero or indecomposable. This is the kernel-language form of the preceding split-complement count and is the exact object that must be identified with the translated next socle generator in the first presentation of Auslander--Reiten Theorem 3.7.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_exists_nextStableCyclicEssentialExtension {k A : Type u} [Field k] [IsAlgClosed 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)) (hquotient : ¬CategoryTheory.Limits.IsZero (CategoryTheory.Limits.cokernel (S.finiteProjectiveStableImageInclusion (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp)))) : ∃ (i : S.IndecCategory) (h : S.fgObj i ⟶ S.fgObj (S.irreducibleIntoProjective_cokernelLabel p g hg hp)) (lH : S.finiteProjectiveStableImage (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp) ⟶ S.finiteProjectiveStableImage i h), S.finiteRestrictedToProjectiveStableMap i h ≠ 0 ∧ CategoryTheory.Mono lH ∧ CategoryTheory.CategoryStruct.comp lH (S.finiteProjectiveStableImageInclusion i h) = S.finiteProjectiveStableImageInclusion (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp) ∧ CategoryTheory.Simple (CategoryTheory.Limits.cokernel lH) ∧ IsEssentialMono lH ∧ IsUniserialObject (S.finiteProjectiveStableImage i h) ∧ IsEssentialMono (S.finiteProjectiveStableImageInclusion i h)

If the quotient above the distinguished first stable socle is nonzero, the next essential cyclic layer may be generated by an actual stable module morphism into P/U.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_firstSocleCover_split_from_nextRightAlmostSplitMiddle {k A : Type u} [Field k] [IsAlgClosed 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)) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) (lH : S.finiteProjectiveStableImage (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp) ⟶ S.finiteProjectiveStableImage i h) [CategoryTheory.Mono lH] (hlH : IsEssentialMono lH) [CategoryTheory.Simple (CategoryTheory.Limits.cokernel lH)] : ∃ (a : S.finiteRestrictedContravariantRepresentable (S.minimalRightAlmostSplitAt i).middle ⟶ S.finiteRestrictedContravariantRepresentable (S.fgObj (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp))), CategoryTheory.IsSplitEpi a ∧ CategoryTheory.CategoryStruct.comp a (CategoryTheory.CategoryStruct.comp (S.finiteProjectiveStableImagePresentation (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp)) lH) = CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap (S.minimalRightAlmostSplitAt i).map) (S.finiteProjectiveStableImagePresentation i h)

For a next cyclic layer above the distinguished first stable socle, the representable covering that first socle splits from the right almost-split middle at the next generator.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_firstSocleModule_split_from_nextRightAlmostSplitMiddle {k A : Type u} [Field k] [IsAlgClosed 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)) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) (lH : S.finiteProjectiveStableImage (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp) ⟶ S.finiteProjectiveStableImage i h) [CategoryTheory.Mono lH] (hlH : IsEssentialMono lH) [CategoryTheory.Simple (CategoryTheory.Limits.cokernel lH)] : ∃ (r : (S.minimalRightAlmostSplitAt i).middle ⟶ S.fgObj (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp)), CategoryTheory.IsSplitEpi r ∧ QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (CategoryTheory.CategoryStruct.comp (S.rightKernelMap ⟨i, ⋯⟩) r) ∧ CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap r) (CategoryTheory.CategoryStruct.comp (S.finiteProjectiveStableImagePresentation (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp)) lH) = CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap (S.minimalRightAlmostSplitAt i).map) (S.finiteProjectiveStableImagePresentation i h)

The representable splitting above reflects to modules: the chosen module covering the distinguished first stable socle is a direct summand of the right almost-split middle at the next generator, and its restricted Yoneda map retains the projective-presentation compatibility.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_firstSocleStableComposites_eq {k A : Type u} [Field k] [IsAlgClosed 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)) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) (lH : S.finiteProjectiveStableImage (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp) ⟶ S.finiteProjectiveStableImage i h) [CategoryTheory.Mono lH] (hlH : IsEssentialMono lH) [CategoryTheory.Simple (CategoryTheory.Limits.cokernel lH)] (hlHcomp : CategoryTheory.CategoryStruct.comp lH (S.finiteProjectiveStableImageInclusion i h) = S.finiteProjectiveStableImageInclusion (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp)) : ∃ (r : (S.minimalRightAlmostSplitAt i).middle ⟶ S.fgObj (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp)), CategoryTheory.IsSplitEpi r ∧ QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (CategoryTheory.CategoryStruct.comp (S.rightKernelMap ⟨i, ⋯⟩) r) ∧ CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap (CategoryTheory.CategoryStruct.comp r (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp))) (S.finiteProjectiveStableQuotient (S.fgObj (S.irreducibleIntoProjective_cokernelLabel p g hg hp))) = CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap (CategoryTheory.CategoryStruct.comp (S.minimalRightAlmostSplitAt i).map h)) (S.finiteProjectiveStableQuotient (S.fgObj (S.irreducibleIntoProjective_cokernelLabel p g hg hp)))

The retained first-socle presentation compatibility remains an equality after inclusion into the ambient stable representable. In module terms, the two resulting composites into P/U therefore differ by a map through the distinguished projective P.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_exists_firstSocleProjectiveCorrection {k A : Type u} [Field k] [IsAlgClosed 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)) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) (lH : S.finiteProjectiveStableImage (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp) ⟶ S.finiteProjectiveStableImage i h) [CategoryTheory.Mono lH] (hlH : IsEssentialMono lH) [CategoryTheory.Simple (CategoryTheory.Limits.cokernel lH)] (hlHcomp : CategoryTheory.CategoryStruct.comp lH (S.finiteProjectiveStableImageInclusion i h) = S.finiteProjectiveStableImageInclusion (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp)) : ∃ (r : (S.minimalRightAlmostSplitAt i).middle ⟶ S.fgObj (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp)) (s : (S.minimalRightAlmostSplitAt i).middle ⟶ S.fgObj p), CategoryTheory.IsSplitEpi r ∧ QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (CategoryTheory.CategoryStruct.comp (S.rightKernelMap ⟨i, ⋯⟩) r) ∧ S.finiteRestrictedContravariantRepresentableMap (CategoryTheory.CategoryStruct.comp s (S.irreducibleIntoProjective_quotientMap p g hg hp)) = S.finiteRestrictedContravariantRepresentableMap (CategoryTheory.CategoryStruct.comp r (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp)) - S.finiteRestrictedContravariantRepresentableMap (CategoryTheory.CategoryStruct.comp (S.minimalRightAlmostSplitAt i).map h)

The equality of stable composites can be lifted through the distinguished projective quotient. The resulting correction s is retained as an actual module morphism, rather than merely as a morphism in the functor category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_nextLayer_translatedArrowMultiplicity_pos {k A : Type u} [Field k] [IsAlgClosed 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)) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) (lH : S.finiteProjectiveStableImage (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp) ⟶ S.finiteProjectiveStableImage i h) [CategoryTheory.Mono lH] (hlH : IsEssentialMono lH) [CategoryTheory.Simple (CategoryTheory.Limits.cokernel lH)] : have hi := ⋯; 0 < FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData (S.rightTranslationLabel ⟨i, hi⟩) (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp)

A candidate next essential layer supplies, after Auslander--Reiten translation, an incoming occurrence at the distinguished first-socle generator.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_nextLayer_translationIsoInitialStableMapRawKernel {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (harity : ∀ (j : S.IndecCategory), ¬CategoryTheory.Projective (S.fgObj j) → FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData j ≤ 2) (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)) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) (lH : S.finiteProjectiveStableImage (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp) ⟶ S.finiteProjectiveStableImage i h) [CategoryTheory.Mono lH] (hlH : IsEssentialMono lH) [CategoryTheory.Simple (CategoryTheory.Limits.cokernel lH)] (hlHcomp : CategoryTheory.CategoryStruct.comp lH (S.finiteProjectiveStableImageInclusion i h) = S.finiteProjectiveStableImageInclusion (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp)) : Nonempty (S.fgObj (S.rightTranslationLabel ⟨i, ⋯⟩) ≅ CategoryTheory.Limits.kernel (S.irreducibleIntoProjective_initialStableMapRaw u p g hg))

The translated generator of a next essential layer is exactly the kernel of the raw first-socle map. The projective correction retained from the functor-category comparison rules out the otherwise ambiguous collision with the distinguished projective arm. This is the multiplicity-sensitive core of Auslander--Reiten Proposition 2.6.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_nextLayer_label_eq {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (harity : ∀ (j : S.IndecCategory), ¬CategoryTheory.Projective (S.fgObj j) → FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData j ≤ 2) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) (i i' : S.IndecCategory) (h : S.fgObj i ⟶ S.fgObj (S.irreducibleIntoProjective_cokernelLabel p g hg hp)) (h' : S.fgObj i' ⟶ S.fgObj (S.irreducibleIntoProjective_cokernelLabel p g hg hp)) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) (hstable' : S.finiteRestrictedToProjectiveStableMap i' h' ≠ 0) (lH : S.finiteProjectiveStableImage (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp) ⟶ S.finiteProjectiveStableImage i h) (lH' : S.finiteProjectiveStableImage (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp) ⟶ S.finiteProjectiveStableImage i' h') [CategoryTheory.Mono lH] (hlH : IsEssentialMono lH) [CategoryTheory.Simple (CategoryTheory.Limits.cokernel lH)] [CategoryTheory.Mono lH'] (hlH' : IsEssentialMono lH') [CategoryTheory.Simple (CategoryTheory.Limits.cokernel lH')] (hlHcomp : CategoryTheory.CategoryStruct.comp lH (S.finiteProjectiveStableImageInclusion i h) = S.finiteProjectiveStableImageInclusion (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp)) (hlHcomp' : CategoryTheory.CategoryStruct.comp lH' (S.finiteProjectiveStableImageInclusion i' h') = S.finiteProjectiveStableImageInclusion (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp)) : i' = i

Two candidate next layers above the distinguished first stable socle have the same indecomposable generator. Both translated generators identify with the same raw kernel, and injectivity of Auslander--Reiten translation then recovers equality of the original labels.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_nextLayer_quotientMaps_proportional {k A : Type u} [Field k] [IsAlgClosed 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 h' : S.fgObj i ⟶ S.fgObj (S.irreducibleIntoProjective_cokernelLabel p g hg hp)) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) (hstable' : S.finiteRestrictedToProjectiveStableMap i h' ≠ 0) (lH : S.finiteProjectiveStableImage (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp) ⟶ S.finiteProjectiveStableImage i h) (lH' : S.finiteProjectiveStableImage (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp) ⟶ S.finiteProjectiveStableImage i h') [CategoryTheory.Mono lH] (hlH : IsEssentialMono lH) [CategoryTheory.Simple (CategoryTheory.Limits.cokernel lH)] [CategoryTheory.Mono lH'] (hlH' : IsEssentialMono lH') [CategoryTheory.Simple (CategoryTheory.Limits.cokernel lH')] (hlHcomp : CategoryTheory.CategoryStruct.comp lH (S.finiteProjectiveStableImageInclusion i h) = S.finiteProjectiveStableImageInclusion (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp)) (hlHcomp' : CategoryTheory.CategoryStruct.comp lH' (S.finiteProjectiveStableImageInclusion i h') = S.finiteProjectiveStableImageInclusion (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp)) : ∃ (α : k), CategoryTheory.CategoryStruct.comp (S.finiteRestrictedToProjectiveStableMap i h') (CategoryTheory.Limits.cokernel.π (S.finiteProjectiveStableImageInclusion (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp))) = CategoryTheory.CategoryStruct.comp (α • S.finiteRestrictedToProjectiveStableMap i h) (CategoryTheory.Limits.cokernel.π (S.finiteProjectiveStableImageInclusion (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp)))

Once two next-layer candidates have the same generator label, their maps to the quotient by the distinguished first socle are scalar-proportional.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_nextLayer_cokernelMap_essential {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (harity : ∀ (j : S.IndecCategory), ¬CategoryTheory.Projective (S.fgObj j) → FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData j ≤ 2) (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)) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) (lH : S.finiteProjectiveStableImage (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp) ⟶ S.finiteProjectiveStableImage i h) [CategoryTheory.Mono lH] (hlH : IsEssentialMono lH) [CategoryTheory.Simple (CategoryTheory.Limits.cokernel lH)] (hlHcomp : CategoryTheory.CategoryStruct.comp lH (S.finiteProjectiveStableImageInclusion i h) = S.finiteProjectiveStableImageInclusion (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp)) : ∃ (t₀ : CategoryTheory.Limits.cokernel lH ⟶ CategoryTheory.Limits.cokernel (S.finiteProjectiveStableImageInclusion (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp))), CategoryTheory.Mono t₀ ∧ IsEssentialMono t₀ ∧ CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π lH) t₀ = CategoryTheory.CategoryStruct.comp (S.finiteProjectiveStableImageInclusion i h) (CategoryTheory.Limits.cokernel.π (S.finiteProjectiveStableImageInclusion (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp)))

A chosen next cyclic layer determines an essential simple subobject of the quotient by the distinguished first stable socle. Every simple subobject of that quotient lifts to another next-layer candidate; translation injectivity and square-free boundary proportionality force it to factor through the chosen one.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_nextLayer_top_essential {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (harity : ∀ (j : S.IndecCategory), ¬CategoryTheory.Projective (S.fgObj j) → FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData j ≤ 2) (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)) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) (lH : S.finiteProjectiveStableImage (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp) ⟶ S.finiteProjectiveStableImage i h) [CategoryTheory.Mono lH] (hlH : IsEssentialMono lH) [CategoryTheory.Simple (CategoryTheory.Limits.cokernel lH)] (hlHcomp : CategoryTheory.CategoryStruct.comp lH (S.finiteProjectiveStableImageInclusion i h) = S.finiteProjectiveStableImageInclusion (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp)) : IsEssentialMono (cokernelInclusionOfComp lH (S.finiteProjectiveStableImageInclusion i h))

Canonical-map form of first-successor essentiality.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_selectedInitialStableMap_isStableChainGenerator {k A : Type u} [Field k] [IsAlgClosed 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.IsStableChainGenerator (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp)

The distinguished first stable-socle generator carries the projective irreducible arm killed in the stable quotient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_stableRepresentable_isUniserial_of_socleCokernel {k A : Type u} [Field k] [IsAlgClosed 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)) (hquotient : IsUniserialObject (CategoryTheory.Limits.cokernel (S.finiteProjectiveStableImageInclusion (S.irreducibleIntoProjective_leftCokernelLabel u p g hg hp) (S.irreducibleIntoProjective_selectedInitialStableMap u p g hg hp)))) : IsUniserialObject (S.finiteProjectiveStableContravariantRepresentable (S.fgObj (S.irreducibleIntoProjective_cokernelLabel p g hg hp)))

Once the quotient above the distinguished essential stable socle is uniserial, the entire selected stable representable is uniserial. This is the categorical ascending-socle induction step specialized to the Auslander--Reiten initialization.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.irreducibleIntoProjective_stableRepresentable_isUniserial {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (harity : ∀ (j : S.IndecCategory), ¬CategoryTheory.Projective (S.fgObj j) → FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData j ≤ 2) (u p : Fin S.n) (g : S.fgObj u ⟶ S.fgObj p) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (hp : CategoryTheory.Projective (S.fgObj p)) : IsUniserialObject (S.finiteProjectiveStableContravariantRepresentable (S.fgObj (S.irreducibleIntoProjective_cokernelLabel p g hg hp)))

Under the two-arm bound, the stable representable attached to an irreducible submodule of an indecomposable projective is uniserial.