The split-complement step in Iyama right ladders

This file isolates the categorical diagram behind Iyama, Tau-categories I, Section 3.2. A split-monic factor of the current arrow through a right mesh, together with a padded decomposition of the next raw arrow, determines all maps and relations in one explicit right-ladder step.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.RightLadder.transportedSwappedComplementIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {Z M Y : C} {j : Z ⟶ M} [CategoryTheory.IsSplitMono j] (d : SplitMonoComplement j) (e : d.complement ≅ Y) : M ≅ Y ⊞ Z

A split complement, after changing the complementary object by an isomorphism and swapping the two factors, identifies the ambient object with Y ⊞ source.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.exists_stepComplex_iso_of_split_factor_and_padded_next {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (S : CategoryTheory.ShortComplex C) {YPrev ZPrev ZNext YNext U : C} (ePrev : S.X₃ ≅ YPrev) (j : ZPrev ⟶ S.X₂) [CategoryTheory.IsSplitMono j] (d : SplitMonoComplement j) (bNext : ZNext ⟶ YNext) (eX : S.X₁ ≅ ZNext ⊞ U) (eY : d.complement ≅ YNext) (heNext : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp S.f d.projection) eY.hom = CategoryTheory.CategoryStruct.comp eX.hom (CategoryTheory.Limits.biprod.desc bNext 0)) : have bPrev := CategoryTheory.CategoryStruct.comp j (CategoryTheory.CategoryStruct.comp S.g ePrev.hom); ∃ (f : YNext ⟶ YPrev) (g : ZNext ⟶ ZPrev) (h : U ⟶ ZPrev) (comm : CategoryTheory.CategoryStruct.comp bNext f = CategoryTheory.CategoryStruct.comp g bPrev) (hzero : CategoryTheory.CategoryStruct.comp h bPrev = 0), Nonempty (S ≅ stepComplex bPrev bNext f g h comm hzero)

Invariant one-step extraction from a split mesh factor.

j is the split-monic factor of the current essential arrow through S.g. The next raw arrow is S.f ≫ d.projection. The isomorphisms eX and eY and the equation heNext record its arrow-category isomorphism to the padded arrow (bNext, 0). From these data all four horizontal maps and both relations in Iyama's displayed step are forced, and S is isomorphic to the resulting explicit step complex.

The right endpoint is allowed to be merely isomorphic to YPrev, matching the chosen-mesh interface of FiniteTauCategoryData.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.isRightMinimal_splitFactor_chosen_rightMesh {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteRightTauCategoryData C Ind) {Z Y : C} (j : Z ⟶ (T.rightMesh Y).X₂) [CategoryTheory.IsSplitMono j] : IsRightMinimal (CategoryTheory.CategoryStruct.comp j (CategoryTheory.CategoryStruct.comp (T.rightMesh Y).g (T.rightTermIso Y).hom))

A split-monic factor of a chosen right mesh map is right minimal, also after the recorded endpoint isomorphism.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.isRightMinimal_add_mem_square_splitFactor_chosen_rightMesh {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteRightTauCategoryData C Ind) {Z Y : C} (j : Z ⟶ (T.rightMesh Y).X₂) [CategoryTheory.IsSplitMono j] (r : Z ⟶ Y) (hr : r ∈ (T.radical.ideal.pow 2).hom Z Y) : IsRightMinimal (CategoryTheory.CategoryStruct.comp j (CategoryTheory.CategoryStruct.comp (T.rightMesh Y).g (T.rightTermIso Y).hom) + r)

Every radical-square perturbation of a split-monic chosen-right-mesh factor is again right minimal.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.isSpecial_splitFactor_of_isSpecial_padded {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteRightTauCategoryData C Ind) {Z U Y : C} (j : Z ⟶ (T.rightMesh Y).X₂) [CategoryTheory.IsSplitMono j] (hpadded : IsSpecial T.radical (CategoryTheory.Limits.biprod.desc (CategoryTheory.CategoryStruct.comp j (CategoryTheory.CategoryStruct.comp (T.rightMesh Y).g (T.rightTermIso Y).hom)) 0)) : IsSpecial T.radical (CategoryTheory.CategoryStruct.comp j (CategoryTheory.CategoryStruct.comp (T.rightMesh Y).g (T.rightTermIso Y).hom))

If the zero-padded arrow defined by a split mesh factor is special, then its essential component is special. This is Iyama's padded-source cancellation step.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.isSpecial_leftMesh_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) (A : C) : IsSpecial T.radical (T.leftMesh A).f

The first map of every chosen left mesh is special. This supplies the μ⁻ seed in Iyama's right-ladder existence theorem.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.exists_factor_through_chosen_rightMesh {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteRightTauCategoryData C Ind) {X Y : C} (a : X ⟶ Y) (ha : CategoricalRadical.IsRadicalMorphism a) : ∃ (k : X ⟶ (T.rightMesh Y).X₂), CategoryTheory.CategoryStruct.comp k (CategoryTheory.CategoryStruct.comp (T.rightMesh Y).g (T.rightTermIso Y).hom) = a

Every radical arrow into Y factors through the second map of the chosen right mesh at Y, after applying the recorded right-endpoint isomorphism.

This is the first operation in the special-arrow construction. It follows directly from the radical approximation field of the chosen right tau-sequence; no Krull--Schmidt decomposition is involved yet.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.exists_special_splitFactor_normalForm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteRightTauCategoryData C Ind) {X Y : C} (a : X ⟶ Y) (ha : IsSpecial T.radical a) : ∃ (Z : C) (U : C) (j : Z ⟶ (T.rightMesh Y).X₂), CategoryTheory.IsSplitMono j ∧ IsSpecial T.radical (CategoryTheory.CategoryStruct.comp j (CategoryTheory.CategoryStruct.comp (T.rightMesh Y).g (T.rightTermIso Y).hom)) ∧ Nonempty (CategoryTheory.Arrow.mk a ≅ CategoryTheory.Arrow.mk (CategoryTheory.Limits.biprod.desc (CategoryTheory.CategoryStruct.comp j (CategoryTheory.CategoryStruct.comp (T.rightMesh Y).g (T.rightTermIso Y).hom)) 0))

Iyama's special-arrow split normalization.

Every special arrow is isomorphic to a zero-padded arrow b, where b is obtained by composing a split monomorphism with the chosen right mesh map. The essential arrow b is again special. This is the categorical content of Tau I, 3.6.1(1), with no module-category realization.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.exists_chosen_rightMesh_step_of_split_factor_and_padded_next {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteRightTauCategoryData C Ind) {YPrev ZPrev ZNext YNext U : C} (j : ZPrev ⟶ (T.rightMesh YPrev).X₂) [CategoryTheory.IsSplitMono j] (bNext : ZNext ⟶ YNext) (eX : (T.rightMesh YPrev).X₁ ≅ ZNext ⊞ U) (eY : (splitMonoComplement j).complement ≅ YNext) (heNext : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (T.rightMesh YPrev).f (splitMonoComplement j).projection) eY.hom = CategoryTheory.CategoryStruct.comp eX.hom (CategoryTheory.Limits.biprod.desc bNext 0)) : have bPrev := CategoryTheory.CategoryStruct.comp j (CategoryTheory.CategoryStruct.comp (T.rightMesh YPrev).g (T.rightTermIso YPrev).hom); ∃ (f : YNext ⟶ YPrev) (g : ZNext ⟶ ZPrev) (h : U ⟶ ZPrev) (comm : CategoryTheory.CategoryStruct.comp bNext f = CategoryTheory.CategoryStruct.comp g bPrev) (hzero : CategoryTheory.CategoryStruct.comp h bPrev = 0), Nonempty (T.rightMesh YPrev ≅ stepComplex bPrev bNext f g h comm hzero)

Chosen-right-mesh specialization of the invariant one-step theorem.

Once j is the split-monic essential factor of the current arrow and the raw successor is displayed as (bNext, 0), idempotent completeness supplies the complement and hence the entire explicit right-ladder step.