Special successors in Iyama left ladders

This file proves the categorical dual of Iyama, Tau-categories I, 3.6.1(2)(ii). A special split-epimorphic cofactor through the first map of a left tau-sequence has a special complementary successor through the second map. No concrete algebra or module classification is used.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.exists_automorphisms_lifting_left_endpoint_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : LeftTauSequence 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 left-tau-sequence endpoint uniqueness.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.nonempty_successor_iso_of_splitCofactors_arrow_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : LeftTauSequence S) {Z Z' Q Q' : C} (p : S.X₂ ⟶ Z) [CategoryTheory.IsSplitEpi p] (p' : S.X₂ ⟶ Z') (i : Q ⟶ S.X₂) (i' : Q' ⟶ S.X₂) (hip : CategoryTheory.CategoryStruct.comp i p = 0) (hip' : CategoryTheory.CategoryStruct.comp i' p' = 0) (hi : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι i hip)) (hi' : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι i' hip')) (e : CategoryTheory.Arrow.mk (CategoryTheory.CategoryStruct.comp S.f p) ≅ CategoryTheory.Arrow.mk (CategoryTheory.CategoryStruct.comp S.f p')) : Nonempty (CategoryTheory.Arrow.mk (CategoryTheory.CategoryStruct.comp i S.g) ≅ CategoryTheory.Arrow.mk (CategoryTheory.CategoryStruct.comp i' S.g))

Invariant well-definedness of the complementary left successor.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.exists_factor_through_tau_g_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 : W ⟶ S.X₃} (hr : r ∈ (R.ideal.pow (n + 1)).hom W S.X₃) : ∃ b ∈ (R.ideal.pow n).hom W S.X₂, CategoryTheory.CategoryStruct.comp b S.g = r

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

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

A middle-term automorphism realizes a perturbation of the raw left successor while changing the split cofactor in the same radical power.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.exists_splitCofactor_kernel_lifting_left_successor_perturbation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : CategoricalRadical.NilpotentRadicalData C) {S : CategoryTheory.ShortComplex C} (hS : LeftTauSequence S) {Z : C} (p : S.X₂ ⟶ Z) [CategoryTheory.IsSplitEpi p] (d : SplitEpiComplement p) (n : ℕ) (hn : 1 ≤ n) (r : d.complement ⟶ S.X₃) (hr : r ∈ (R.ideal.pow (n + 1)).hom d.complement S.X₃) : ∃ (p' : S.X₂ ⟶ Z) (i' : d.complement ⟶ S.X₂) (hip' : CategoryTheory.CategoryStruct.comp i' p' = 0) (_hi' : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι i' hip')), CategoryTheory.IsSplitEpi p' ∧ CategoryTheory.CategoryStruct.comp S.f p' - CategoryTheory.CategoryStruct.comp S.f p ∈ (R.ideal.pow (n + 1)).hom S.X₁ Z ∧ CategoryTheory.CategoryStruct.comp i' S.g = CategoryTheory.CategoryStruct.comp d.inclusion S.g + r

Representative form of the perturbation lift using a genuine kernel of the perturbed split cofactor.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.isSpecial_rawComplementLeftSuccessor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : CategoricalRadical.NilpotentRadicalData C) {S : CategoryTheory.ShortComplex C} (hS : LeftTauSequence S) {Z : C} (p : S.X₂ ⟶ Z) [CategoryTheory.IsSplitEpi p] (d : SplitEpiComplement p) (ha : IsSpecial R (CategoryTheory.CategoryStruct.comp S.f p)) : IsSpecial R (CategoryTheory.CategoryStruct.comp d.inclusion S.g)

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

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.isSpecial_chosenLeftMesh_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 : FiniteTauCategoryData C Ind) {Y Z : C} (p : (T.leftMesh Y).X₂ ⟶ Z) [CategoryTheory.IsSplitEpi p] (ha : IsSpecial T.radical (CategoryTheory.CategoryStruct.comp (T.leftTermIso Y).inv (CategoryTheory.CategoryStruct.comp (T.leftMesh Y).f p))) : IsSpecial T.radical (CategoryTheory.CategoryStruct.comp (splitEpiComplement p).inclusion (T.leftMesh Y).g)

Chosen-left-mesh form of complementary successor specialness.