An abstract almost-split interface for the forward cofinite-two criterion

This file isolates the Auslander--Reiten input needed for the forward half of the manuscript's mixed cofinite-two criterion. It proves the usual correspondence between the indecomposable summands of a minimal almost-split middle term and irreducible morphisms. It also proves that a supplied finite-length almost-split map can be replaced by a minimal one. Existence of ordinary almost-split maps is still left as a separate input.

structure QuotientSubmoduleEquidistribution.IsRightAlmostSplit {C : Type u} [CategoryTheory.Category.{v, u} C] {E Z : C} (f : E ⟶ Z) : Prop

A morphism f : E ⟶ Z is right almost split when it is not a split epimorphism and every morphism into Z which is not a split epimorphism factors through it.

Here "non-split epimorphism" is used in the standard AR sense of a morphism which is not a retraction; the morphism being factored need not itself be categorically epic.

• not_isSplitEpi : ¬CategoryTheory.IsSplitEpi f
• factors {X : C} (g : X ⟶ Z) : ¬CategoryTheory.IsSplitEpi g → ∃ (h : X ⟶ E), CategoryTheory.CategoryStruct.comp h f = g

structure QuotientSubmoduleEquidistribution.IsLeftAlmostSplit {C : Type u} [CategoryTheory.Category.{v, u} C] {Z E : C} (f : Z ⟶ E) : Prop

The dual notion of a left almost-split morphism.

• not_isSplitMono : ¬CategoryTheory.IsSplitMono f
• factors {X : C} (g : Z ⟶ X) : ¬CategoryTheory.IsSplitMono g → ∃ (h : E ⟶ X), CategoryTheory.CategoryStruct.comp f h = g

def QuotientSubmoduleEquidistribution.HasIrreducibleMorphism {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : C) : Prop

Existence of an irreducible morphism between two objects.

def QuotientSubmoduleEquidistribution.HasNoIrreducibleEndomorphism {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : Prop

The no-loop input used for an almost-split middle term: there is no irreducible endomorphism of X.

theorem QuotientSubmoduleEquidistribution.noIrreducibleEndomorphism_of_finiteLength {R : Type u} [Ring R] [IsNoetherianRing R] {X : FGModuleCat R} (hX : IsFiniteLength R ↑X) : HasNoIrreducibleEndomorphism X

A finite-length finitely generated module has no irreducible endomorphism.

The canonical epi--mono image factorization of a hypothetical irreducible endomorphism would make one factor split. The split factor is then an isomorphism, making the original endomorphism monic or epic; finite length makes it an isomorphism, contradicting irreducibility.

theorem QuotientSubmoduleEquidistribution.IsRightAlmostSplit.epi_of_nonsplit_epi {C : Type u} [CategoryTheory.Category.{v, u} C] {E Z X : C} {f : E ⟶ Z} (hf : IsRightAlmostSplit f) (g : X ⟶ Z) [CategoryTheory.Epi g] (hg : ¬CategoryTheory.IsSplitEpi g) : CategoryTheory.Epi f

A right almost-split map is epic as soon as its target admits one categorically epic map which is not split.

theorem QuotientSubmoduleEquidistribution.IsLeftAlmostSplit.mono_of_nonsplit_mono {C : Type u} [CategoryTheory.Category.{v, u} C] {Z E X : C} {f : Z ⟶ E} (hf : IsLeftAlmostSplit f) (g : Z ⟶ X) [CategoryTheory.Mono g] (hg : ¬CategoryTheory.IsSplitMono g) : CategoryTheory.Mono f

Dually, a left almost-split map is monic as soon as its source admits one categorical monomorphism which is not split.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.hasNoIrreducibleEndomorphism_obj {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) (z : ι) : HasNoIrreducibleEndomorphism (σ.obj z)

Each chosen skeleton representative has no irreducible endomorphism. Only its recorded finite length is needed.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.isRightAlmostSplit_of_factors_obj {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {z : ι} {E : FGModuleCat R} (f : E ⟶ σ.obj z) (hnosplit : ¬CategoryTheory.IsSplitEpi f) (hfac : ∀ (x : ι) (g : σ.obj x ⟶ σ.obj z), ¬CategoryTheory.IsSplitEpi g → ∃ (h : σ.obj x ⟶ E), CategoryTheory.CategoryStruct.comp h f = g) : IsRightAlmostSplit f

To prove that a map into a chosen indecomposable is right almost split, it suffices to establish the factorization property on the chosen indecomposable representatives. The skeleton decomposition then handles an arbitrary source one component at a time.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.isLeftAlmostSplit_of_factors_obj {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {z : ι} {E : FGModuleCat R} (f : σ.obj z ⟶ E) (hnosplit : ¬CategoryTheory.IsSplitMono f) (hfac : ∀ (x : ι) (g : σ.obj z ⟶ σ.obj x), ¬CategoryTheory.IsSplitMono g → ∃ (h : E ⟶ σ.obj x), CategoryTheory.CategoryStruct.comp f h = g) : IsLeftAlmostSplit f

The left-dual reduction: factorization on the chosen indecomposable representatives implies the full left almost-split property.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.isSplitEpi_of_isSplitMono_between_obj {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {x y : ι} (g : σ.obj x ⟶ σ.obj y) [CategoryTheory.IsSplitMono g] : CategoryTheory.IsSplitEpi g

A split monomorphism between chosen indecomposables is also split epic. The splitting exhibits the source as a retract of the target, so the duplicate-free skeleton identifies their labels; finite length then upgrades the resulting monic endomorphism to an isomorphism.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.isSplitMono_of_isSplitEpi_between_obj {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {x y : ι} (g : σ.obj x ⟶ σ.obj y) [CategoryTheory.IsSplitEpi g] : CategoryTheory.IsSplitMono g

Dually, a split epimorphism between chosen indecomposables is also split monic.

structure QuotientSubmoduleEquidistribution.IndecomposableSkeleton.MinimalRightAlmostSplitDecomposition {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) (z : ι) : Type (max (max uR uι) (w + 1))

A chosen finite indecomposable decomposition of the middle object of a minimal right almost-split map ending at σ.obj z.

• middle : FGModuleCat R
• finiteLength : IsFiniteLength R ↑self.middle
• map : self.middle ⟶ σ.obj z
• rightAlmostSplit : IsRightAlmostSplit self.map
• rightMinimal : IsRightMinimal self.map
• index : FintypeCat
• label : self.index.obj → ι
• decomposition : self.middle ≅ σ.sumOver self.index self.label

structure QuotientSubmoduleEquidistribution.IndecomposableSkeleton.MinimalLeftAlmostSplitDecomposition {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) (z : ι) : Type (max (max uR uι) (w + 1))

A chosen finite indecomposable decomposition of the middle object of a minimal left almost-split map starting at σ.obj z.

• middle : FGModuleCat R
• finiteLength : IsFiniteLength R ↑self.middle
• map : σ.obj z ⟶ self.middle
• leftAlmostSplit : IsLeftAlmostSplit self.map
• leftMinimal : IsLeftMinimal self.map
• index : FintypeCat
• label : self.index.obj → ι
• decomposition : self.middle ≅ σ.sumOver self.index self.label

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.MinimalRightAlmostSplitDecomposition.ofMap {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {z : ι} {E : FGModuleCat R} (f : E ⟶ σ.obj z) (hE : IsFiniteLength R ↑E) (har : IsRightAlmostSplit f) (hmin : IsRightMinimal f) : σ.MinimalRightAlmostSplitDecomposition z

Bundle any supplied minimal right almost-split map with a decomposition provided by the existing skeleton.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.MinimalRightAlmostSplitDecomposition.exists_of_rightAlmostSplit_of_finiteLength {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {z : ι} {E : FGModuleCat R} (f : E ⟶ σ.obj z) (hf : IsRightAlmostSplit f) (hE : IsFiniteLength R ↑E) : Nonempty (σ.MinimalRightAlmostSplitDecomposition z)

Any right almost-split morphism with finite-length middle term can be replaced by a minimal one. Choose an almost-split middle term of least finite length; if an endomorphism fixing its map were noninvertible, its categorical image would give a strictly shorter right almost-split middle term.

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.MinimalLeftAlmostSplitDecomposition.ofMap {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {z : ι} {E : FGModuleCat R} (f : σ.obj z ⟶ E) (hE : IsFiniteLength R ↑E) (hal : IsLeftAlmostSplit f) (hmin : IsLeftMinimal f) : σ.MinimalLeftAlmostSplitDecomposition z

Bundle any supplied minimal left almost-split map with a decomposition provided by the existing skeleton.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.MinimalLeftAlmostSplitDecomposition.exists_of_leftAlmostSplit_of_finiteLength {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {z : ι} {E : FGModuleCat R} (f : σ.obj z ⟶ E) (hf : IsLeftAlmostSplit f) (hE : IsFiniteLength R ↑E) : Nonempty (σ.MinimalLeftAlmostSplitDecomposition z)

Any left almost-split morphism with finite-length middle term can be replaced by a minimal one. This is the dual least-length image argument to exists_of_rightAlmostSplit_of_finiteLength.

structure QuotientSubmoduleEquidistribution.IndecomposableSkeleton.IsLegalQMixedDeletion {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) (p z : ι) : Prop

A legal mixed quotient-side two-point deletion: p is top split-projective, z is not, the labels are distinct, and their complement is quotient-closed.

• ne : p ≠ z
• projective : σ.IsRelativeSplitProjective Set.univ p
• not_projective : ¬σ.IsRelativeSplitProjective Set.univ z
• closed : σ.qClosure.IsClosed {p, z}ᶜ

structure QuotientSubmoduleEquidistribution.IndecomposableSkeleton.IsLegalSMixedDeletion {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) (z i : ι) : Prop

The dual notion of a legal mixed submodule-side deletion.

• ne : z ≠ i
• not_injective : ¬σ.IsRelativeSplitInjective Set.univ z
• injective : σ.IsRelativeSplitInjective Set.univ i
• closed : σ.sClosure.IsClosed {z, i}ᶜ

def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.HasRightSummandIrreducibleCorrespondence {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {z : ι} (A : σ.MinimalRightAlmostSplitDecomposition z) : Prop

The existence-level AR correspondence for a chosen right almost-split middle decomposition: a label occurs in the middle exactly when there is an irreducible map from that indecomposable to the end term.

def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.HasLeftSummandIrreducibleCorrespondence {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {z : ι} (A : σ.MinimalLeftAlmostSplitDecomposition z) : Prop

The dual existence-level AR correspondence for a chosen left almost-split middle decomposition.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.MinimalRightAlmostSplitDecomposition.summandIrreducibleCorrespondence {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} {σ : IndecomposableSkeleton R ι} {z : ι} (A : σ.MinimalRightAlmostSplitDecomposition z) : σ.HasRightSummandIrreducibleCorrespondence A

The indecomposable summands of a minimal right almost-split middle term are exactly the sources of irreducible morphisms to its endpoint.

For an occurring summand, right minimality is applied to the rank-one perturbation which replaces that coordinate by a supplied factorization. Conversely, right almost-splitness factors an irreducible morphism through the middle; irreducibility makes the first factor split monic, and retract support detects the corresponding label.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.MinimalRightAlmostSplitDecomposition.indecomposableRetract_middle_iff_irreducible {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} {σ : IndecomposableSkeleton R ι} {z : ι} (A : σ.MinimalRightAlmostSplitDecomposition z) (x : ι) : Nonempty (CategoryTheory.Retract (σ.obj x) A.middle) ↔ HasIrreducibleMorphism (σ.obj x) (σ.obj z)

Coordinate-free form of the right almost-split summand correspondence: an indecomposable is a retract of the middle term exactly when it is the source of an irreducible morphism to the endpoint.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.MinimalRightAlmostSplitDecomposition.epi_of_not_topSplitProjective {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} {σ : IndecomposableSkeleton R ι} {z : ι} (A : σ.MinimalRightAlmostSplitDecomposition z) (hz : ¬σ.IsRelativeSplitProjective Set.univ z) : CategoryTheory.Epi A.map

Non-top-projectivity of the end term supplies the nonsplit epimorphism needed to show that a right almost-split map is categorically epic.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.MinimalLeftAlmostSplitDecomposition.summandIrreducibleCorrespondence {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} {σ : IndecomposableSkeleton R ι} {z : ι} (A : σ.MinimalLeftAlmostSplitDecomposition z) : σ.HasLeftSummandIrreducibleCorrespondence A

The indecomposable summands of a minimal left almost-split middle term are exactly the targets of irreducible morphisms from its endpoint.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.MinimalLeftAlmostSplitDecomposition.mono_of_not_topSplitInjective {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} {σ : IndecomposableSkeleton R ι} {z : ι} (A : σ.MinimalLeftAlmostSplitDecomposition z) (hz : ¬σ.IsRelativeSplitInjective Set.univ z) : CategoryTheory.Mono A.map

Non-top-injectivity of the start term supplies the nonsplit monomorphism needed to show that a left almost-split map is categorically monic.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.deletedProjective_mem_rightAlmostSplitMiddle {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {p z : ι} (hlegal : σ.IsLegalQMixedDeletion p z) (A : σ.MinimalRightAlmostSplitDecomposition z) (hz_middle : ¬∃ (t : A.index.obj), A.label t = z) : ∃ (t : A.index.obj), A.label t = p

Core quotient-side forcing lemma. For a legal mixed deletion, if the end label z does not occur in the chosen right almost-split middle, then the deleted projective label p must occur there.

Minimality is recorded in A; this elementary forcing step uses only its right almost-split field.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.deletedInjective_mem_leftAlmostSplitMiddle {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {z i : ι} (hlegal : σ.IsLegalSMixedDeletion z i) (A : σ.MinimalLeftAlmostSplitDecomposition z) (hz_middle : ¬∃ (t : A.index.obj), A.label t = z) : ∃ (t : A.index.obj), A.label t = i

Core dual forcing lemma.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.deletedProjective_mem_rightAlmostSplitMiddle_of_correspondence {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {p z : ι} (hlegal : σ.IsLegalQMixedDeletion p z) (A : σ.MinimalRightAlmostSplitDecomposition z) (hcorr : σ.HasRightSummandIrreducibleCorrespondence A) : ∃ (t : A.index.obj), A.label t = p

With the standard existence-level AR correspondence and the finite-length no-loop theorem above, a legal mixed quotient deletion forces the projective label to occur in the minimal right almost-split middle.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.deletedInjective_mem_leftAlmostSplitMiddle_of_correspondence {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {z i : ι} (hlegal : σ.IsLegalSMixedDeletion z i) (A : σ.MinimalLeftAlmostSplitDecomposition z) (hcorr : σ.HasLeftSummandIrreducibleCorrespondence A) : ∃ (t : A.index.obj), A.label t = i

Dual middle-term forcing theorem under the left AR correspondence and the finite-length no-loop theorem.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.hasIrreducible_of_legalQMixedDeletion_of_target_not_middle {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {p z : ι} (hlegal : σ.IsLegalQMixedDeletion p z) (A : σ.MinimalRightAlmostSplitDecomposition z) (hz_middle : ¬∃ (t : A.index.obj), A.label t = z) : HasIrreducibleMorphism (σ.obj p) (σ.obj z)

Forward quotient criterion with target-absence stated directly. This separates the elementary closure argument from the later no-loop input.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.hasIrreducible_of_legalSMixedDeletion_of_source_not_middle {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {z i : ι} (hlegal : σ.IsLegalSMixedDeletion z i) (A : σ.MinimalLeftAlmostSplitDecomposition z) (hz_middle : ¬∃ (t : A.index.obj), A.label t = z) : HasIrreducibleMorphism (σ.obj z) (σ.obj i)

Dual forward criterion with start-label absence stated directly.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.hasIrreducible_of_legalQMixedDeletion {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {p z : ι} (hlegal : σ.IsLegalQMixedDeletion p z) (A : σ.MinimalRightAlmostSplitDecomposition z) : HasIrreducibleMorphism (σ.obj p) (σ.obj z)

Forward mixed quotient criterion for a minimal right almost-split map. Finite length excludes z from the middle; closedness then forces p into the middle, and the proved correspondence produces an irreducible map p ⟶ z.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.hasIrreducible_of_legalSMixedDeletion {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {z i : ι} (hlegal : σ.IsLegalSMixedDeletion z i) (A : σ.MinimalLeftAlmostSplitDecomposition z) : HasIrreducibleMorphism (σ.obj z) (σ.obj i)

Dual forward mixed criterion for a minimal left almost-split map.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.qClosed_compl_pair_iff_hasIrreducible_of_rightAR {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {p z : ι} (hpz : p ≠ z) (hp : σ.IsRelativeSplitProjective Set.univ p) (hz : ¬σ.IsRelativeSplitProjective Set.univ z) (A : σ.MinimalRightAlmostSplitDecomposition z) : σ.qClosure.IsClosed {p, z}ᶜ ↔ HasIrreducibleMorphism (σ.obj p) (σ.obj z)

A minimal right almost-split decomposition and the elementary converse give the full mixed criterion.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.sClosed_compl_pair_iff_hasIrreducible_of_leftAR {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {z i : ι} (hzi : z ≠ i) (hz : ¬σ.IsRelativeSplitInjective Set.univ z) (hi : σ.IsRelativeSplitInjective Set.univ i) (A : σ.MinimalLeftAlmostSplitDecomposition z) : σ.sClosure.IsClosed {z, i}ᶜ ↔ HasIrreducibleMorphism (σ.obj z) (σ.obj i)

Dual full mixed criterion under a minimal left almost-split decomposition.