Reversed domination and finite comparison propagation

This is the explicit triangular-matrix step used when a finite left ladder is read backwards against a right ladder. It is entirely categorical: no concrete algebra or module classification is involved.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.isSplitMono_comp_of_isSplitMono {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : CategoryTheory.IsSplitMono f) (hg : CategoryTheory.IsSplitMono g) : CategoryTheory.IsSplitMono (CategoryTheory.CategoryStruct.comp f g)

The composite of two explicitly split-monic morphisms is split monic.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.splitMono_components_of_displayed_steps {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) {X Y : C} {S R : CategoryTheory.ShortComplex C} (eS : T.leftMesh X ≅ S) (eR : T.rightMesh Y ≅ R) (phi : S ⟶ R) (hphi₁ : CategoryTheory.IsSplitMono phi.τ₁) : CategoryTheory.IsSplitMono phi.τ₂ ∧ CategoryTheory.IsSplitMono phi.τ₃

Transport dual mixed split lifting across displayed mesh isomorphisms.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.splitEpi_components_of_displayed_steps {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) {X Y : C} {S R : CategoryTheory.ShortComplex C} (eS : T.leftMesh X ≅ S) (eR : T.rightMesh Y ≅ R) (phi : S ⟶ R) (hphi₃ : CategoryTheory.IsSplitEpi phi.τ₃) : CategoryTheory.IsSplitEpi phi.τ₁ ∧ CategoryTheory.IsSplitEpi phi.τ₂

Transport mixed split-epi lifting across displayed mesh isomorphisms.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.exists_reversedStrongDomination_rung_data {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) {YLPrev ZLPrev YLNext ZLNext UL ZRPrev YRPrev ZRNext YRNext UR : C} (dPrev : YLPrev ⟶ ZLPrev) (dNext : YLNext ⟶ ZLNext) (lf : YLPrev ⟶ YLNext) (lg : ZLPrev ⟶ ZLNext) (lh : ZLPrev ⟶ UL) (lcomm : CategoryTheory.CategoryStruct.comp lf dNext = CategoryTheory.CategoryStruct.comp dPrev lg) (lhzero : CategoryTheory.CategoryStruct.comp dPrev lh = 0) (bPrev : ZRPrev ⟶ YRPrev) (bNext : ZRNext ⟶ YRNext) (rf : YRNext ⟶ YRPrev) (rg : ZRNext ⟶ ZRPrev) (rh : UR ⟶ ZRPrev) (rcomm : CategoryTheory.CategoryStruct.comp bNext rf = CategoryTheory.CategoryStruct.comp rg bPrev) (rhzero : CategoryTheory.CategoryStruct.comp rh bPrev = 0) (eLeft : Nonempty (T.leftMesh YLPrev ≅ LeftLadder.stepComplex dPrev dNext lf lg lh lcomm lhzero)) (eRight : Nonempty (T.rightMesh YRPrev ≅ RightLadder.stepComplex bPrev bNext rf rg rh rcomm rhzero)) (square : CategoryTheory.Arrow.mk dPrev ⟶ CategoryTheory.Arrow.mk (CategoryTheory.Limits.biprod.desc bNext 0)) (hsquare : CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.left square)) : ∃ (phiStep : LeftLadder.stepComplex dPrev dNext lf lg lh lcomm lhzero ⟶ RightLadder.stepComplex bPrev bNext rf rg rh rcomm rhzero) (nextSquare : CategoryTheory.Arrow.mk (CategoryTheory.Limits.biprod.lift dNext 0) ⟶ CategoryTheory.Arrow.mk bPrev), CategoryTheory.IsSplitMono phiStep.τ₁ ∧ CategoryTheory.IsSplitMono phiStep.τ₂ ∧ CategoryTheory.IsSplitMono phiStep.τ₃ ∧ CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.left nextSquare) ∧ CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.right nextSquare) ∧ CategoryTheory.Arrow.Hom.right nextSquare = phiStep.τ₃ ∧ CategoryTheory.Arrow.Hom.left square = phiStep.τ₁ ∧ CategoryTheory.Arrow.Hom.right square = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp phiStep.τ₂ CategoryTheory.Limits.biprod.fst) ∧ CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp phiStep.τ₂ CategoryTheory.Limits.biprod.fst) = 0

One reversed cross-ladder domination rung.

The input is a square from the current essential left arrow to the next zero-padded right arrow, split monic on sources. The output is a square from the next zero-padded left arrow to the previous essential right arrow, split monic on both components.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.exists_reversedStrongDomination_rung {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) {YLPrev ZLPrev YLNext ZLNext UL ZRPrev YRPrev ZRNext YRNext UR : C} (dPrev : YLPrev ⟶ ZLPrev) (dNext : YLNext ⟶ ZLNext) (lf : YLPrev ⟶ YLNext) (lg : ZLPrev ⟶ ZLNext) (lh : ZLPrev ⟶ UL) (lcomm : CategoryTheory.CategoryStruct.comp lf dNext = CategoryTheory.CategoryStruct.comp dPrev lg) (lhzero : CategoryTheory.CategoryStruct.comp dPrev lh = 0) (bPrev : ZRPrev ⟶ YRPrev) (bNext : ZRNext ⟶ YRNext) (rf : YRNext ⟶ YRPrev) (rg : ZRNext ⟶ ZRPrev) (rh : UR ⟶ ZRPrev) (rcomm : CategoryTheory.CategoryStruct.comp bNext rf = CategoryTheory.CategoryStruct.comp rg bPrev) (rhzero : CategoryTheory.CategoryStruct.comp rh bPrev = 0) (eLeft : Nonempty (T.leftMesh YLPrev ≅ LeftLadder.stepComplex dPrev dNext lf lg lh lcomm lhzero)) (eRight : Nonempty (T.rightMesh YRPrev ≅ RightLadder.stepComplex bPrev bNext rf rg rh rcomm rhzero)) (square : CategoryTheory.Arrow.mk dPrev ⟶ CategoryTheory.Arrow.mk (CategoryTheory.Limits.biprod.desc bNext 0)) (hsquare : CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.left square)) : ∃ (nextSquare : CategoryTheory.Arrow.mk (CategoryTheory.Limits.biprod.lift dNext 0) ⟶ CategoryTheory.Arrow.mk bPrev), CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.left nextSquare) ∧ CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.right nextSquare)

The split-monic output-square projection of the full reversed-rung comparison data.

Global reversed propagation

structure QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.ReversedRightPrefix {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) (n : ℕ) : Type (max u v)

A right-ladder prefix whose indexing has already been reversed, so its rung i runs from the arrow at i.castSucc to the arrow at i.succ. This removes all subtraction arithmetic from the propagation theorem.

• Z : Fin (n + 1) → C
• Y : Fin (n + 1) → C
• U : Fin (n + 1) → C
• b (i : Fin (n + 1)) : self.Z i ⟶ self.Y i
• f (i : Fin n) : self.Y i.castSucc ⟶ self.Y i.succ
• g (i : Fin n) : self.Z i.castSucc ⟶ self.Z i.succ
• h (i : Fin n) : self.U i.castSucc ⟶ self.Z i.succ
• comm (i : Fin n) : CategoryTheory.CategoryStruct.comp (self.b i.castSucc) (self.f i) = CategoryTheory.CategoryStruct.comp (self.g i) (self.b i.succ)
• hzero (i : Fin n) : CategoryTheory.CategoryStruct.comp (self.h i) (self.b i.succ) = 0
• meshIso (i : Fin n) : Nonempty (T.rightMesh (self.Y i.succ) ≅ RightLadder.stepComplex (self.b i.succ) (self.b i.castSucc) (self.f i) (self.g i) (self.h i) ⋯ ⋯)

noncomputable def QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.ReversedRightPrefix.paddedArrow {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {n : ℕ} (R : ReversedRightPrefix T n) (i : Fin (n + 1)) : R.Z i ⊞ R.U i ⟶ R.Y i

structure QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.BoundaryEmbedding {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {n : ℕ} (R : ReversedRightPrefix T n) (U₀ : C) : Type v

A chosen split-monic piece of the complementary object at the reversed boundary. Taking a chosen indecomposable summand here is sufficient for the comparison and avoids any indecomposability hypothesis on the whole complement.

• hom : U₀ ⟶ R.U 0
• isSplitMono : CategoryTheory.IsSplitMono self.hom

def QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.BoundaryEmbedding.identity {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {n : ℕ} (R : ReversedRightPrefix T n) : BoundaryEmbedding R (R.U 0)

The original whole-boundary comparison is the identity special case.

def QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.DiagonalComparisonAt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {U₀ : C} {n : ℕ} (R : ReversedRightPrefix T n) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T U₀ n) (i : Fin (n + 1)) : Prop

The split-monic comparison state along an aligned reversed prefix.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.diagonalComparisonAt_zero_of_boundaryEmbedding {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {U₀ : C} {n : ℕ} (R : ReversedRightPrefix T n) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T U₀ n) (E : BoundaryEmbedding R U₀) : DiagonalComparisonAt R L 0

A split-monic boundary piece gives the first diagonal comparison square.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.diagonalComparisonAt_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {n : ℕ} (R : ReversedRightPrefix T n) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T (R.U 0) n) : DiagonalComparisonAt R L 0

The zero boundary gives the first diagonal comparison square when the whole complementary object is used.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.diagonalComparisonAt_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {U₀ : C} {n : ℕ} (R : ReversedRightPrefix T n) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T U₀ n) (i : Fin n) (h : DiagonalComparisonAt R L i.castSucc) : DiagonalComparisonAt R L i.succ

One aligned diagonal propagation step.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.diagonalComparisonAt_all_of_boundaryEmbedding {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {U₀ : C} {n : ℕ} (R : ReversedRightPrefix T n) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T U₀ n) (E : BoundaryEmbedding R U₀) (i : Fin (n + 1)) : DiagonalComparisonAt R L i

The comparison propagates across every rung of an aligned finite window.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.diagonalComparisonAt_all {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {n : ℕ} (R : ReversedRightPrefix T n) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T (R.U 0) n) (i : Fin (n + 1)) : DiagonalComparisonAt R L i

Whole-boundary specialization of global propagation.

The terminal four-cycle

noncomputable def QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.ReversedRightPrefix.essentialToPaddedSquare {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {n : ℕ} (R : ReversedRightPrefix T n) (i : Fin (n + 1)) : CategoryTheory.Arrow.mk (R.b i) ⟶ CategoryTheory.Arrow.mk (R.paddedArrow i)

The literal inclusion of a right-ladder essential arrow into its zero-padded arrow.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.ReversedRightPrefix.essentialToPaddedSquare_components {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {n : ℕ} (R : ReversedRightPrefix T n) (i : Fin (n + 1)) : CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.left (R.essentialToPaddedSquare i)) ∧ CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.right (R.essentialToPaddedSquare i))

Both components of the right zero-padding square are split monic.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.leftEssentialToPaddedSquare {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {U₀ : C} {n : ℕ} (L : LeftLadder.FiniteSpecialLeftLadderFromZero T U₀ n) (i : Fin (n + 1)) : CategoryTheory.Arrow.mk (L.b i) ⟶ CategoryTheory.Arrow.mk (L.paddedArrow i)

The literal inclusion of a left-ladder essential arrow into its zero-padded arrow.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.leftEssentialToPaddedSquare_components {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {U₀ : C} {n : ℕ} (L : LeftLadder.FiniteSpecialLeftLadderFromZero T U₀ n) (i : Fin (n + 1)) : CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.left (leftEssentialToPaddedSquare L i)) ∧ CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.right (leftEssentialToPaddedSquare L i))

Both components of the left zero-padding square are split monic.

def QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.CrossComparisonAt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {n : ℕ} (R : ReversedRightPrefix T n) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T (R.U 0) n) (i : Fin n) : Prop

The middle edge of the domination chain produced by one reversed rung: the previous essential right arrow contains the next padded left arrow.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.crossComparisonAt_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {n : ℕ} (R : ReversedRightPrefix T n) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T (R.U 0) n) (i : Fin n) (h : DiagonalComparisonAt R L i.castSucc) : CrossComparisonAt R L i

Extract the middle edge before composing it with the two padding inclusions.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.crossComparisonAt_all {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {n : ℕ} (R : ReversedRightPrefix T n) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T (R.U 0) n) (i : Fin n) : CrossComparisonAt R L i

Every rung of an aligned finite window supplies its uncomposed middle domination edge.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.nonempty_arrow_iso_of_mutual_splitMono_squares {C : Type u} [CategoryTheory.Category.{v, u} C] (hfinite : ∀ (X : C) (e : X ⟶ X), CategoryTheory.IsSplitMono e → CategoryTheory.IsIso e) {Xa Ya Xb Yb : C} {a : Xa ⟶ Ya} {b : Xb ⟶ Yb} (d : CategoryTheory.Arrow.mk b ⟶ CategoryTheory.Arrow.mk a) (hdleft : CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.left d)) (hdright : CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.right d)) (e : CategoryTheory.Arrow.mk a ⟶ CategoryTheory.Arrow.mk b) (heleft : CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.left e)) (heright : CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.right e)) : Nonempty (CategoryTheory.Arrow.mk a ≅ CategoryTheory.Arrow.mk b)

Two split-monic arrow squares in opposite directions are inverse up to arrow isomorphism when endomorphisms of the receiving endpoints are directly finite.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.isIso_components_of_mutual_splitMono_squares {C : Type u} [CategoryTheory.Category.{v, u} C] (hfinite : ∀ (X : C) (f : X ⟶ X), CategoryTheory.IsSplitMono f → CategoryTheory.IsIso f) {Xa Ya Xb Yb : C} {a : Xa ⟶ Ya} {b : Xb ⟶ Yb} (d : CategoryTheory.Arrow.mk b ⟶ CategoryTheory.Arrow.mk a) (hdleft : CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.left d)) (hdright : CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.right d)) (e : CategoryTheory.Arrow.mk a ⟶ CategoryTheory.Arrow.mk b) (heleft : CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.left e)) (heright : CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.right e)) : CategoryTheory.IsIso (CategoryTheory.Arrow.Hom.left d) ∧ CategoryTheory.IsIso (CategoryTheory.Arrow.Hom.right d)

The forward square itself is componentwise invertible under the same mutual-domination and direct-finiteness hypotheses.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.isSplitEpi_biprod_inr_comp_fst_of_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {A B D E : C} (m : A ⊞ B ⟶ D ⊞ E) (hm : CategoryTheory.IsIso m) (hzero : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp m CategoryTheory.Limits.biprod.fst) = 0) : CategoryTheory.IsSplitEpi (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp m CategoryTheory.Limits.biprod.fst))

In an invertible biproduct matrix with zero upper-left block, the upper-right block is split epic. Its section is the lower-left block of the inverse matrix.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.nonempty_adjacent_arrow_isos_of_splitMono_four_cycle {C : Type u} [CategoryTheory.Category.{v, u} C] (hfinite : ∀ (X : C) (e : X ⟶ X), CategoryTheory.IsSplitMono e → CategoryTheory.IsIso e) {X₀ Y₀ X₁ Y₁ X₂ Y₂ X₃ Y₃ : C} {a₀ : X₀ ⟶ Y₀} {a₁ : X₁ ⟶ Y₁} {a₂ : X₂ ⟶ Y₂} {a₃ : X₃ ⟶ Y₃} (q₀₁ : CategoryTheory.Arrow.mk a₁ ⟶ CategoryTheory.Arrow.mk a₀) (h₀₁l : CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.left q₀₁)) (h₀₁r : CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.right q₀₁)) (q₁₂ : CategoryTheory.Arrow.mk a₂ ⟶ CategoryTheory.Arrow.mk a₁) (h₁₂l : CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.left q₁₂)) (h₁₂r : CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.right q₁₂)) (q₂₃ : CategoryTheory.Arrow.mk a₃ ⟶ CategoryTheory.Arrow.mk a₂) (h₂₃l : CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.left q₂₃)) (h₂₃r : CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.right q₂₃)) (q₃₀ : CategoryTheory.Arrow.mk a₀ ⟶ CategoryTheory.Arrow.mk a₃) (h₃₀l : CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.left q₃₀)) (h₃₀r : CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.right q₃₀)) : Nonempty (CategoryTheory.Arrow.mk a₀ ≅ CategoryTheory.Arrow.mk a₁) ∧ Nonempty (CategoryTheory.Arrow.mk a₁ ≅ CategoryTheory.Arrow.mk a₂) ∧ Nonempty (CategoryTheory.Arrow.mk a₂ ≅ CategoryTheory.Arrow.mk a₃) ∧ Nonempty (CategoryTheory.Arrow.mk a₃ ≅ CategoryTheory.Arrow.mk a₀)

Four split-monic arrow squares which close to a cycle make every edge an arrow isomorphism under direct finiteness.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.terminal_four_cycle_adjacent_isos {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {n : ℕ} (R : ReversedRightPrefix T n) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T (R.U 0) n) (i : Fin n) (hfinite : ∀ (X : C) (e : X ⟶ X), CategoryTheory.IsSplitMono e → CategoryTheory.IsIso e) (hterminal : Nonempty (CategoryTheory.Arrow.mk (L.b i.succ) ≅ CategoryTheory.Arrow.mk (R.paddedArrow i.succ))) : Nonempty (CategoryTheory.Arrow.mk (R.paddedArrow i.succ) ≅ CategoryTheory.Arrow.mk (R.b i.succ)) ∧ Nonempty (CategoryTheory.Arrow.mk (R.b i.succ) ≅ CategoryTheory.Arrow.mk (L.paddedArrow i.succ)) ∧ Nonempty (CategoryTheory.Arrow.mk (L.paddedArrow i.succ) ≅ CategoryTheory.Arrow.mk (L.b i.succ)) ∧ Nonempty (CategoryTheory.Arrow.mk (L.b i.succ) ≅ CategoryTheory.Arrow.mk (R.paddedArrow i.succ))

Closing one propagated reversed rung by an endpoint isomorphism yields all three cancellation isomorphisms in the terminal diagonal. The first is exactly the previous-right-arrow cancellation needed by the finite ladder certificate.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.terminal_reversed_rung_step_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {U₀ : C} {n : ℕ} (R : ReversedRightPrefix T n) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T U₀ n) (i : Fin n) (hfinite : ∀ (X : C) (e : X ⟶ X), CategoryTheory.IsSplitMono e → CategoryTheory.IsIso e) (hdiag : DiagonalComparisonAt R L i.castSucc) (hterminal : Nonempty (CategoryTheory.Arrow.mk (L.b i.succ) ≅ CategoryTheory.Arrow.mk (R.paddedArrow i.succ))) : Nonempty (LeftLadder.stepComplex (L.b i.castSucc) (L.b i.succ) (L.f i) (L.g i) (L.h i) ⋯ ⋯ ≅ RightLadder.stepComplex (R.b i.succ) (R.b i.castSucc) (R.f i) (R.g i) (R.h i) ⋯ ⋯) ∧ Nonempty (CategoryTheory.Arrow.mk (L.b i.castSucc) ≅ CategoryTheory.Arrow.mk (R.paddedArrow i.castSucc)) ∧ Nonempty (CategoryTheory.Arrow.mk (R.paddedArrow i.succ) ≅ CategoryTheory.Arrow.mk (R.b i.succ)) ∧ Nonempty (CategoryTheory.Arrow.mk (R.b i.succ) ≅ CategoryTheory.Arrow.mk (L.paddedArrow i.succ)) ∧ Nonempty (CategoryTheory.Arrow.mk (L.paddedArrow i.succ) ≅ CategoryTheory.Arrow.mk (L.b i.succ)) ∧ Nonempty (CategoryTheory.Arrow.mk (L.b i.succ) ≅ CategoryTheory.Arrow.mk (R.paddedArrow i.succ))

The load-bearing terminal comparison theorem. The endpoint isomorphism closes the four-cycle, making the exact output square of the chosen rung componentwise invertible. Its third component is therefore split epic; mixed split-epi lifting propagates this backwards, so the full displayed left-to-right mesh comparison is an isomorphism.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.terminalArrowIsoAt_all_of_boundaryEmbedding {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {U₀ : C} {n : ℕ} (R : ReversedRightPrefix T n) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T U₀ n) (E : BoundaryEmbedding R U₀) (hfinite : ∀ (X : C) (e : X ⟶ X), CategoryTheory.IsSplitMono e → CategoryTheory.IsIso e) (hlast : Nonempty (CategoryTheory.Arrow.mk (L.b (Fin.last n)) ≅ CategoryTheory.Arrow.mk (R.paddedArrow (Fin.last n)))) (j : Fin (n + 1)) : Nonempty (CategoryTheory.Arrow.mk (L.b j) ≅ CategoryTheory.Arrow.mk (R.paddedArrow j))

A terminal arrow isomorphism propagates backwards across the entire aligned finite window.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.terminalArrowIsoAt_all {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {n : ℕ} (R : ReversedRightPrefix T n) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T (R.U 0) n) (hfinite : ∀ (X : C) (e : X ⟶ X), CategoryTheory.IsSplitMono e → CategoryTheory.IsIso e) (hlast : Nonempty (CategoryTheory.Arrow.mk (L.b (Fin.last n)) ≅ CategoryTheory.Arrow.mk (R.paddedArrow (Fin.last n)))) (j : Fin (n + 1)) : Nonempty (CategoryTheory.Arrow.mk (L.b j) ≅ CategoryTheory.Arrow.mk (R.paddedArrow j))

Whole-boundary specialization of backward terminal propagation.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.reversedStepIso_all_of_boundaryEmbedding {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {U₀ : C} {n : ℕ} (R : ReversedRightPrefix T n) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T U₀ n) (E : BoundaryEmbedding R U₀) (hfinite : ∀ (X : C) (e : X ⟶ X), CategoryTheory.IsSplitMono e → CategoryTheory.IsIso e) (hlast : Nonempty (CategoryTheory.Arrow.mk (L.b (Fin.last n)) ≅ CategoryTheory.Arrow.mk (R.paddedArrow (Fin.last n)))) (i : Fin n) : Nonempty (LeftLadder.stepComplex (L.b i.castSucc) (L.b i.succ) (L.f i) (L.g i) (L.h i) ⋯ ⋯ ≅ RightLadder.stepComplex (R.b i.succ) (R.b i.castSucc) (R.f i) (R.g i) (R.h i) ⋯ ⋯)

Every aligned pair of reversed left/right rungs is isomorphic once the terminal diagonal closes.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.reversedStepIso_all {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {n : ℕ} (R : ReversedRightPrefix T n) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T (R.U 0) n) (hfinite : ∀ (X : C) (e : X ⟶ X), CategoryTheory.IsSplitMono e → CategoryTheory.IsIso e) (hlast : Nonempty (CategoryTheory.Arrow.mk (L.b (Fin.last n)) ≅ CategoryTheory.Arrow.mk (R.paddedArrow (Fin.last n)))) (i : Fin n) : Nonempty (LeftLadder.stepComplex (L.b i.castSucc) (L.b i.succ) (L.f i) (L.g i) (L.h i) ⋯ ⋯ ≅ RightLadder.stepComplex (R.b i.succ) (R.b i.castSucc) (R.f i) (R.g i) (R.h i) ⋯ ⋯)

Whole-boundary specialization of the rung isomorphisms.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.reversedPreviousCancellationIso_all_of_boundaryEmbedding {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {U₀ : C} {n : ℕ} (R : ReversedRightPrefix T n) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T U₀ n) (E : BoundaryEmbedding R U₀) (hfinite : ∀ (X : C) (e : X ⟶ X), CategoryTheory.IsSplitMono e → CategoryTheory.IsIso e) (hlast : Nonempty (CategoryTheory.Arrow.mk (L.b (Fin.last n)) ≅ CategoryTheory.Arrow.mk (R.paddedArrow (Fin.last n)))) (i : Fin n) : Nonempty (CategoryTheory.Arrow.mk (R.paddedArrow i.succ) ≅ CategoryTheory.Arrow.mk (R.b i.succ))

Every previous essential right arrow cancels its zero padding along the closed reversed window.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.reversedPreviousCancellationIso_all {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {n : ℕ} (R : ReversedRightPrefix T n) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T (R.U 0) n) (hfinite : ∀ (X : C) (e : X ⟶ X), CategoryTheory.IsSplitMono e → CategoryTheory.IsIso e) (hlast : Nonempty (CategoryTheory.Arrow.mk (L.b (Fin.last n)) ≅ CategoryTheory.Arrow.mk (R.paddedArrow (Fin.last n)))) (i : Fin n) : Nonempty (CategoryTheory.Arrow.mk (R.paddedArrow i.succ) ≅ CategoryTheory.Arrow.mk (R.b i.succ))

Whole-boundary specialization of previous-arrow cancellation.