Basic normalized states and rungs for special left ladders

This file contains the invariant split-epimorphic rung construction and the normalized state records used in the left-ladder half of Iyama, Tau-categories I, Lemma 6.4.1(1)(ii). The two-field builder interface separates target normalization from complementary-successor specialness; subsequent modules construct both fields categorically.

No concrete algebra or module classification occurs in this file.

The invariant split-epimorphic left rung

noncomputable def QuotientSubmoduleEquidistribution.Iyama.LeftLadder.transportedComplementTargetIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {M Z Y : C} {p : M ⟶ Z} [CategoryTheory.IsSplitEpi p] (d : SplitEpiComplement p) (e : d.complement ≅ Y) : M ≅ Y ⊞ Z

A split epimorphism, after replacing its complementary object by an isomorphic object, identifies its source with biprod Y Z.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.exists_stepComplex_iso_of_split_cofactor_and_padded_next {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (S : CategoryTheory.ShortComplex C) {YPrev ZPrev YNext ZNext U : C} (ePrev : S.X₁ ≅ YPrev) (p : S.X₂ ⟶ ZPrev) [CategoryTheory.IsSplitEpi p] (d : SplitEpiComplement p) (bNext : YNext ⟶ ZNext) (eY : d.complement ≅ YNext) (eX : S.X₃ ≅ ZNext ⊞ U) (heNext : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp d.inclusion S.g) eX.hom = CategoryTheory.CategoryStruct.comp eY.hom (CategoryTheory.Limits.biprod.lift bNext 0)) : have bPrev := CategoryTheory.CategoryStruct.comp ePrev.inv (CategoryTheory.CategoryStruct.comp S.f p); ∃ (f : YPrev ⟶ YNext) (g : ZPrev ⟶ ZNext) (h : ZPrev ⟶ U) (comm : CategoryTheory.CategoryStruct.comp f bNext = CategoryTheory.CategoryStruct.comp bPrev g) (hzero : CategoryTheory.CategoryStruct.comp bPrev h = 0), Nonempty (S ≅ stepComplex bPrev bNext f g h comm hzero)

Dual of the invariant split-complement right-rung theorem.

p is the split-epimorphic factor of the current essential arrow through S.f. Its complementary successor is d.inclusion ≫ S.g. An arrow isomorphism from that successor to (bNext,0) determines the entire explicit left-ladder rung and identifies it with S.

Normalized left states and the dual-special interface

structure QuotientSubmoduleEquidistribution.Iyama.LeftLadder.SpecialCosplitState {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) (Y : C) : Type (max u v)

A normalized special arrow obtained by postcomposing the first map of a chosen left mesh with a split epimorphism. The field U records the zero-padded target summand discarded from the essential arrow.

• Z : C
• U : C
• p : (T.leftMesh Y).X₂ ⟶ self.Z
• p_split : CategoryTheory.IsSplitEpi self.p
• special : IsSpecial T.radical (CategoryTheory.CategoryStruct.comp (T.leftTermIso Y).inv (CategoryTheory.CategoryStruct.comp (T.leftMesh Y).f self.p))

instance QuotientSubmoduleEquidistribution.Iyama.LeftLadder.instIsSplitEpiP {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} {Y : C} (s : SpecialCosplitState T Y) : CategoryTheory.IsSplitEpi s.p

def QuotientSubmoduleEquidistribution.Iyama.LeftLadder.SpecialCosplitState.b {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} {Y : C} (s : SpecialCosplitState T Y) : Y ⟶ s.Z

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.SpecialCosplitState.b_special {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} {Y : C} (s : SpecialCosplitState T Y) : IsSpecial T.radical s.b

noncomputable def QuotientSubmoduleEquidistribution.Iyama.LeftLadder.SpecialCosplitState.rawSuccessor {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} {Y : C} (s : SpecialCosplitState T Y) : (splitEpiComplement s.p).complement ⟶ (T.leftMesh Y).X₃

structure QuotientSubmoduleEquidistribution.Iyama.LeftLadder.SpecialConormalization {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} (a : X ⟶ Y) : Type (max u v)

• state : SpecialCosplitState T X
• arrowIso : Nonempty (CategoryTheory.Arrow.mk a ≅ CategoryTheory.Arrow.mk (CategoryTheory.Limits.biprod.lift self.state.b 0))

structure QuotientSubmoduleEquidistribution.Iyama.LeftLadder.SpecialLeftLadderBuilder {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) : Type (max u v)

The two dual-special operations used by the dependent recursion: target split--radical normalization and specialness of the complementary left successor.

• normalize {X Y : C} (a : X ⟶ Y) : IsSpecial T.radical a → SpecialConormalization T a
• rawSuccessor_special {Y : C} (s : SpecialCosplitState T Y) : IsSpecial T.radical s.rawSuccessor