Two-arm successors for stable representables

This file formalizes the local step in Auslander--Reiten's proof of Corollary 3.8. A stable generator carries one incoming irreducible arm that is already zero. In a right almost-split middle term of arity at most two, that arm splits off and leaves at most one nonzero indecomposable complement. The opposite component of the almost-split kernel supplies the killed arm at the next stage.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteIndecomposableDecomposition_indecomposable_of_n_le_one {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {X : FinitelyGeneratedCategory A} (d : CategoryTheory.FiniteIndecomposableDecomposition X) (hd : d.n ≤ 1) (hX : ¬CategoryTheory.Limits.IsZero X) : CategoryTheory.Indecomposable X

A nonzero finitely generated module admitting a displayed indecomposable decomposition with at most one occurrence is indecomposable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.splitMonoComplement_rightComponent_isIrreducible {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x i : S.IndecCategory} {E : FinitelyGeneratedCategory A} (f : E ⟶ S.fgObj i) (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f) (hfmin : QuotientSubmoduleEquidistribution.IsRightMinimal f) (t : S.fgObj x ⟶ E) [CategoryTheory.IsSplitMono t] (d : QuotientSubmoduleEquidistribution.SplitMonoComplement t) (j : S.IndecCategory) (e : S.fgObj j ≅ d.complement) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (CategoryTheory.CategoryStruct.comp e.hom (CategoryTheory.CategoryStruct.comp d.inclusion f))

The complementary component of a minimal right almost-split map is irreducible once the complement is identified with a chosen indecomposable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.splitMonoComplement_leftComponent_isIrreducible {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {source x : S.IndecCategory} {E : FinitelyGeneratedCategory A} (a : S.fgObj source ⟶ E) (ha : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit a) (hamin : QuotientSubmoduleEquidistribution.IsLeftMinimal a) (t : S.fgObj x ⟶ E) [CategoryTheory.IsSplitMono t] (d : QuotientSubmoduleEquidistribution.SplitMonoComplement t) (j : S.IndecCategory) (e : S.fgObj j ≅ d.complement) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (CategoryTheory.CategoryStruct.comp a (CategoryTheory.CategoryStruct.comp d.projection e.inv))

Dually, projecting a minimal left almost-split map to the same indecomposable complement gives the killed irreducible arm for the next stable generator.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.IsStableChainGenerator {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) (h : S.fgObj i ⟶ C) : Prop

A cyclic stable image is on the Auslander--Reiten chain when one irreducible incoming arrow is already killed in the stable quotient.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.IsRepresentableChainGenerator {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) {G : CoveringHom.FiniteDimensionalModuleCategory k} (i : S.IndecCategory) (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G) : Prop

A cyclic image of an arbitrary finite functor is on the Auslander--Reiten chain when one irreducible incoming arm is killed by its generating map.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.killedIrreducible_source_eq_of_nonzero_stableImageRadical {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) {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) (hRzero : ¬CategoryTheory.Limits.IsZero (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion i) (S.finiteProjectiveStableImagePresentation i h))))) (x : S.IndecCategory) (d : S.fgObj x ⟶ S.fgObj i) (hd : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism d) (hdzero : CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap d) (S.finiteRestrictedToProjectiveStableMap i h) = 0) (x' : S.IndecCategory) (d' : S.fgObj x' ⟶ S.fgObj i) (hd' : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism d') (hdzero' : CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableMap d') (S.finiteRestrictedToProjectiveStableMap i h) = 0) : x' = x

If the radical of a cyclic stable image is nonzero, the two-arm bound makes the source label of an irreducible incoming arm killed by the generator unique. One killed arm splits from the right almost-split middle; its complement is the nonzero radical-generating arm, so a second killed arm cannot split through that complement.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_representableChainGenerator_radicalSuccessor {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) {G : CoveringHom.FiniteDimensionalModuleCategory k} (i : S.IndecCategory) (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G) (hgood : S.IsRepresentableChainGenerator i p) (hp : p ≠ 0) (hiNonprojective : ¬CategoryTheory.Projective (S.fgObj i)) (hRzero : ¬CategoryTheory.Limits.IsZero (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion i) (S.finiteRepresentableImagePresentation i p))))) : ∃ (j : S.IndecCategory) (q : S.finiteRestrictedContravariantRepresentable (S.fgObj j) ⟶ G), S.IsRepresentableChainGenerator j q ∧ q ≠ 0 ∧ Nonempty (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion i) (S.finiteRepresentableImagePresentation i p))) ≅ S.finiteRepresentableImage j q)

The two-arm successor step depends only on a cyclic representable image, not on the stable-representable origin of its ambient finite functor.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRepresentableImage_isUniserial_of_twoArm {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) {G : CoveringHom.FiniteDimensionalModuleCategory k} (hsupport : ∀ (i : S.IndecCategory) (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G), p ≠ 0 → ¬CategoryTheory.Projective (S.fgObj i)) (i : S.IndecCategory) (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G) (hgood : S.IsRepresentableChainGenerator i p) (hp : p ≠ 0) : IsUniserialObject (S.finiteRepresentableImage i p)

If nonzero maps into a fixed finite functor can only be generated at nonprojective module labels, the two-arm bound makes every chain-generated cyclic image uniserial.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_stableChainGenerator_radicalSuccessor {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) {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C) (hgood : S.IsStableChainGenerator i h) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) (hRzero : ¬CategoryTheory.Limits.IsZero (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion i) (S.finiteProjectiveStableImagePresentation i h))))) : ∃ (j : S.IndecCategory) (g : S.fgObj j ⟶ C), S.IsStableChainGenerator j g ∧ S.finiteRestrictedToProjectiveStableMap j g ≠ 0 ∧ Nonempty (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion i) (S.finiteProjectiveStableImagePresentation i h))) ≅ S.finiteProjectiveStableImage j g)

The local Auslander--Reiten successor step. Under a two-summand bound on right almost-split middles, every nonzero radical stage of a chain generator is another cyclic stable image carrying its next killed arm.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableImage_isUniserial_of_twoArm {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) {C : FinitelyGeneratedCategory A} (i : S.IndecCategory) (h : S.fgObj i ⟶ C) (hgood : S.IsStableChainGenerator i h) (hstable : S.finiteRestrictedToProjectiveStableMap i h ≠ 0) : IsUniserialObject (S.finiteProjectiveStableImage i h)

Under the two-arm bound, every nonzero cyclic stable image already on the Auslander--Reiten chain is uniserial.