Special successors in Iyama right ladders

This file formalizes Iyama, Tau-categories I, 3.6.1(2)(i)--(ii), in the split-complement language used by the right-ladder construction. A radical-power perturbation of the raw complement successor lifts to a perturbation of the current split mesh factor in the same power. Cokernel transport proves that the successor depends only on the arrow-isomorphism class of that factor, and hence a special current arrow has a special raw successor.

Everything here is categorical; no module classification or concrete algebra is used.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.exists_automorphisms_lifting_endpoint_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : RightTauSequence S) (e₃ : S.X₃ ≅ S.X₃) : ∃ (e₁ : S.X₁ ≅ S.X₁) (e₂ : S.X₂ ≅ S.X₂), CategoryTheory.CategoryStruct.comp e₁.hom S.f = CategoryTheory.CategoryStruct.comp S.f e₂.hom ∧ CategoryTheory.CategoryStruct.comp e₂.hom S.g = CategoryTheory.CategoryStruct.comp S.g e₃.hom

Component-exposing form of right-tau-sequence endpoint uniqueness.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.nonempty_successor_iso_of_splitFactors_arrow_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : RightTauSequence S) {Z Z' Q Q' : C} (j : Z ⟶ S.X₂) [CategoryTheory.IsSplitMono j] (j' : Z' ⟶ S.X₂) (p : S.X₂ ⟶ Q) (p' : S.X₂ ⟶ Q') (hjp : CategoryTheory.CategoryStruct.comp j p = 0) (hjp' : CategoryTheory.CategoryStruct.comp j' p' = 0) (hp : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ p hjp)) (hp' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ p' hjp')) (e : CategoryTheory.Arrow.mk (CategoryTheory.CategoryStruct.comp j S.g) ≅ CategoryTheory.Arrow.mk (CategoryTheory.CategoryStruct.comp j' S.g)) : Nonempty (CategoryTheory.Arrow.mk (CategoryTheory.CategoryStruct.comp S.f p) ≅ CategoryTheory.Arrow.mk (CategoryTheory.CategoryStruct.comp S.f p'))

Invariant form of the well-definedness of Iyama's l⁺ operation.

If two split factors through the second map of a right tau-sequence are isomorphic as arrows, then the arrows induced on any chosen cokernels of the split factors by the first map are isomorphic.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.exists_factor_through_tau_f_of_mem_pow_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : CategoricalRadical.NilpotentRadicalData C) {S : CategoryTheory.ShortComplex C} (hS : TauApproximation S) (n : ℕ) {W : C} {r : S.X₁ ⟶ W} (hr : r ∈ (R.ideal.pow (n + 1)).hom S.X₁ W) : ∃ b ∈ (R.ideal.pow n).hom S.X₂ W, CategoryTheory.CategoryStruct.comp S.f b = r

Radical-power lifting through the first map of a tau-approximation.

An element of J^(n+1) lifts with coefficient in J^n. This is the filtration-sensitive factorization in Iyama 3.6.1(2)(i).

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.exists_middle_iso_lifting_successor_perturbation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : CategoricalRadical.NilpotentRadicalData C) {S : CategoryTheory.ShortComplex C} (hS : RightTauSequence S) {Z : C} (j : Z ⟶ S.X₂) [CategoryTheory.IsSplitMono j] (d : SplitMonoComplement j) (n : ℕ) (hn : 1 ≤ n) (r : S.X₁ ⟶ d.complement) (hr : r ∈ (R.ideal.pow (n + 1)).hom S.X₁ d.complement) : ∃ (E : S.X₂ ≅ S.X₂), CategoryTheory.CategoryStruct.comp j (CategoryTheory.CategoryStruct.comp E.inv S.g) - CategoryTheory.CategoryStruct.comp j S.g ∈ (R.ideal.pow (n + 1)).hom Z S.X₃ ∧ CategoryTheory.CategoryStruct.comp S.f (CategoryTheory.CategoryStruct.comp E.hom d.projection) = CategoryTheory.CategoryStruct.comp S.f d.projection + r

The matrix lift of a J^(n+1) perturbation of the raw successor.

For n ≥ 1, an isomorphism of the mesh middle term changes the complement successor by the prescribed J^(n+1) arrow while changing the split mesh factor by another arrow in the same radical power.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.exists_splitFactor_cokernel_lifting_successor_perturbation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : CategoricalRadical.NilpotentRadicalData C) {S : CategoryTheory.ShortComplex C} (hS : RightTauSequence S) {Z : C} (j : Z ⟶ S.X₂) [CategoryTheory.IsSplitMono j] (d : SplitMonoComplement j) (n : ℕ) (hn : 1 ≤ n) (r : S.X₁ ⟶ d.complement) (hr : r ∈ (R.ideal.pow (n + 1)).hom S.X₁ d.complement) : ∃ (j' : Z ⟶ S.X₂) (p' : S.X₂ ⟶ d.complement) (hjp' : CategoryTheory.CategoryStruct.comp j' p' = 0) (_hp' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ p' hjp')), CategoryTheory.IsSplitMono j' ∧ CategoryTheory.CategoryStruct.comp j' S.g - CategoryTheory.CategoryStruct.comp j S.g ∈ (R.ideal.pow (n + 1)).hom Z S.X₃ ∧ CategoryTheory.CategoryStruct.comp S.f p' = CategoryTheory.CategoryStruct.comp S.f d.projection + r

Representative form of Iyama 3.6.1(2)(i).

For source exponent N = n + 1 with n ≥ 1, a prescribed J^N perturbation of the complement successor is realized by another split mesh factor whose current arrow differs in J^N. The displayed map p' is a genuine cokernel of the new split factor, not merely an annihilating map.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.isSpecial_rawComplementSuccessor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : CategoricalRadical.NilpotentRadicalData C) {S : CategoryTheory.ShortComplex C} (hS : RightTauSequence S) {Z : C} (j : Z ⟶ S.X₂) [CategoryTheory.IsSplitMono j] (d : SplitMonoComplement j) (ha : IsSpecial R (CategoryTheory.CategoryStruct.comp j S.g)) : IsSpecial R (CategoryTheory.CategoryStruct.comp S.f d.projection)

Iyama 3.6.1(2)(ii), in split-complement form.

If a split factor through the second map of a right tau-sequence is special, then the raw successor obtained by composing the first map with the complement projection is special.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.isSpecial_chosenRightMesh_rawComplementSuccessor {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 Z : C} (j : Z ⟶ (T.rightMesh Y).X₂) [CategoryTheory.IsSplitMono j] (ha : IsSpecial T.radical (CategoryTheory.CategoryStruct.comp j (CategoryTheory.CategoryStruct.comp (T.rightMesh Y).g (T.rightTermIso Y).hom))) : IsSpecial T.radical (CategoryTheory.CategoryStruct.comp (T.rightMesh Y).f (splitMonoComplement j).projection)

Chosen-mesh form of successor specialness, matching the output of the special split-factor normalization theorem.