Infinite special right ladders

This file iterates the split-complement successor construction from Iyama, Tau-categories I, Section 3.2. Starting from an arbitrary special arrow, it produces the full dependent family of normalized special arrows and chosen right-mesh ladder rungs. The zero-padded summand of the initial normalization is retained explicitly for the radical-power argument in Lemma 6.4.1(1)(i).

The construction is entirely categorical: it uses no presentation or classification of a concrete algebra or its modules.

structure QuotientSubmoduleEquidistribution.Iyama.RightLadder.SpecialSplitState {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 : FiniteRightTauCategoryData C Ind) (Y : C) : Type (max u v)

One normalized special split factor through a chosen right mesh. The object U remembers the zero-padded source summand of the arrow which was normalized to obtain this state.

• Z : C
• U : C
• j : self.Z ⟶ (T.rightMesh Y).X₂
• j_split : CategoryTheory.IsSplitMono self.j
• special : IsSpecial T.radical (CategoryTheory.CategoryStruct.comp self.j (CategoryTheory.CategoryStruct.comp (T.rightMesh Y).g (T.rightTermIso Y).hom))

instance QuotientSubmoduleEquidistribution.Iyama.RightLadder.instIsSplitMonoJ {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 : FiniteRightTauCategoryData C Ind} {Y : C} (s : SpecialSplitState T Y) : CategoryTheory.IsSplitMono s.j

def QuotientSubmoduleEquidistribution.Iyama.RightLadder.SpecialSplitState.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 : FiniteRightTauCategoryData C Ind} {Y : C} (s : SpecialSplitState T Y) : s.Z ⟶ Y

The essential special arrow represented by a normalized state.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.SpecialSplitState.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 : FiniteRightTauCategoryData C Ind} {Y : C} (s : SpecialSplitState T Y) : IsSpecial T.radical s.b

noncomputable def QuotientSubmoduleEquidistribution.Iyama.RightLadder.SpecialSplitState.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 : FiniteRightTauCategoryData C Ind} {Y : C} (s : SpecialSplitState T Y) : (T.rightMesh Y).X₁ ⟶ (splitMonoComplement s.j).complement

The raw successor obtained from the complement of the split mesh factor.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.SpecialSplitState.rawSuccessor_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 : FiniteRightTauCategoryData C Ind} {Y : C} (s : SpecialSplitState T Y) : IsSpecial T.radical s.rawSuccessor

structure QuotientSubmoduleEquidistribution.Iyama.RightLadder.SpecialNormalization {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 : FiniteRightTauCategoryData C Ind) {X Y : C} (a : X ⟶ Y) : Type (max u v)

A special arrow together with one chosen split-factor normalization.

• state : SpecialSplitState T Y
• arrowIso : Nonempty (CategoryTheory.Arrow.mk a ≅ CategoryTheory.Arrow.mk (CategoryTheory.Limits.biprod.desc self.state.b 0))

noncomputable def QuotientSubmoduleEquidistribution.Iyama.RightLadder.chooseSpecialNormalization {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 : FiniteRightTauCategoryData C Ind) {X Y : C} (a : X ⟶ Y) (ha : IsSpecial T.radical a) : SpecialNormalization T a

Choose the special split-factor normal form of an arbitrary special arrow.

@[reducible, inline]

abbrev QuotientSubmoduleEquidistribution.Iyama.RightLadder.PackedSpecialSplitState {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 : FiniteRightTauCategoryData C Ind) : Type (max u u v)

Pack a dependent state together with its current right endpoint.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.RightLadder.nextNormalization {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 : FiniteRightTauCategoryData C Ind) {Y : C} (s : SpecialSplitState T Y) : SpecialNormalization T s.rawSuccessor

Normalize the raw successor of a state.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.RightLadder.nextPackedState {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 : FiniteRightTauCategoryData C Ind) (p : PackedSpecialSplitState T) : PackedSpecialSplitState T

The next packed state in the infinite special right ladder.

structure QuotientSubmoduleEquidistribution.Iyama.RightLadder.SpecialRightLadderRung {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 : FiniteRightTauCategoryData C Ind) (p : PackedSpecialSplitState T) : Type v

All maps, relations, and the chosen-mesh identification in one successive special right-ladder rung.

• f : (nextPackedState T p).fst ⟶ p.fst
• g : (nextPackedState T p).snd.Z ⟶ p.snd.Z
• h : (nextPackedState T p).snd.U ⟶ p.snd.Z
• comm : CategoryTheory.CategoryStruct.comp (nextPackedState T p).snd.b self.f = CategoryTheory.CategoryStruct.comp self.g p.snd.b
• hzero : CategoryTheory.CategoryStruct.comp self.h p.snd.b = 0
• meshIso : Nonempty (T.rightMesh p.fst ≅ stepComplex p.snd.b (nextPackedState T p).snd.b self.f self.g self.h ⋯ ⋯)

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.nonempty_specialRightLadderRung {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 : FiniteRightTauCategoryData C Ind) (p : PackedSpecialSplitState T) : Nonempty (SpecialRightLadderRung T p)

Every normalized special state has a next explicit right-ladder rung.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.RightLadder.chooseSpecialRightLadderRung {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 : FiniteRightTauCategoryData C Ind) (p : PackedSpecialSplitState T) : SpecialRightLadderRung T p

A chosen rung; the choice is immaterial to the existence theorem.

def QuotientSubmoduleEquidistribution.Iyama.RightLadder.iteratePackedState {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 : FiniteRightTauCategoryData C Ind) (p₀ : PackedSpecialSplitState T) : ℕ → PackedSpecialSplitState T

Primitive recursion of the normalized special states.

structure QuotientSubmoduleEquidistribution.Iyama.RightLadder.InfiniteSpecialRightLadder {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 : FiniteRightTauCategoryData C Ind) {X Y₀ : C} (a₀ : X ⟶ Y₀) : Type (max u v)

An infinite special right ladder beginning at an arbitrary arrow.

U 0 is the zero-padded branch in the normalization of the initial arrow; the rung at n uses U (n+1), exactly as in Iyama's displayed ladder.

• Y : ℕ → C
• Z : ℕ → C
• U : ℕ → C
• b (n : ℕ) : self.Z n ⟶ self.Y n
• b_special (n : ℕ) : IsSpecial T.radical (self.b n)
• initialIso : Nonempty (CategoryTheory.Arrow.mk a₀ ≅ CategoryTheory.Arrow.mk (CategoryTheory.Limits.biprod.desc (self.b 0) 0))
• f (n : ℕ) : self.Y n.succ ⟶ self.Y n
• g (n : ℕ) : self.Z n.succ ⟶ self.Z n
• h (n : ℕ) : self.U n.succ ⟶ self.Z n
• comm (n : ℕ) : CategoryTheory.CategoryStruct.comp (self.b n.succ) (self.f n) = CategoryTheory.CategoryStruct.comp (self.g n) (self.b n)
• hzero (n : ℕ) : CategoryTheory.CategoryStruct.comp (self.h n) (self.b n) = 0
• meshIso (n : ℕ) : Nonempty (T.rightMesh (self.Y n) ≅ stepComplex (self.b n) (self.b n.succ) (self.f n) (self.g n) (self.h n) ⋯ ⋯)

noncomputable def QuotientSubmoduleEquidistribution.Iyama.RightLadder.infiniteSpecialRightLadder {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 : FiniteRightTauCategoryData C Ind) {X Y₀ : C} (a₀ : X ⟶ Y₀) (ha₀ : IsSpecial T.radical a₀) : InfiniteSpecialRightLadder T a₀

Construct the dependent infinite right ladder of an arbitrary special arrow. All choices are categorical and classification-free.