Radical-layer factorization in Iyama left ladders

This file proves the dual radical-layer calculation used in Iyama, Tau-categories I, Lemma 6.4.1(1)(ii). A morphism in the nth radical power out of the source of a zero-initial left ladder factors, after precomposition by an annihilator of the initial arrow, through the first n domain maps. Consequently a nonzero such morphism forces the nth left-ladder domain to be nonzero.

The argument is entirely categorical and uses no concrete algebra or module classification.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.exists_step_factor_of_mem_pow_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (R : CategoricalRadical.NilpotentRadicalData C) {YPrev ZPrev YNext ZNext U W : C} {bPrev : YPrev ⟶ ZPrev} {bNext : YNext ⟶ ZNext} {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} {S : CategoryTheory.ShortComplex C} (hS : LeftTauSequence S) (e : S ≅ stepComplex bPrev bNext f g h comm hzero) (n : ℕ) {r : YPrev ⟶ W} (hr : r ∈ (R.ideal.pow (n + 1)).hom YPrev W) : ∃ rNext ∈ (R.ideal.pow n).hom YNext W, ∃ t ∈ (R.ideal.pow n).hom ZPrev W, r = CategoryTheory.CategoryStruct.comp f rNext + CategoryTheory.CategoryStruct.comp bPrev t

One left mesh lowers a radical-power factor by one, with one component along the next domain and one along the current essential arrow.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.comp_forwardComposite_tail {C : Type u} [CategoryTheory.Category.{v, u} C] (Y : ℕ → C) (f : (n : ℕ) → Y n ⟶ Y (n + 1)) (n : ℕ) : CategoryTheory.CategoryStruct.comp (f 0) (forwardComposite (fun (k : ℕ) => Y (k + 1)) (fun (k : ℕ) => f (k + 1)) n) = forwardComposite Y f (n + 1)

Removing the first index from a family removes the first factor from its forward composite.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.exists_factor_through_forwardComposite {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (R : CategoricalRadical.NilpotentRadicalData C) (n : ℕ) (S : ℕ → CategoryTheory.ShortComplex C) (Y Z U : ℕ → C) (b : (k : ℕ) → Y k ⟶ Z k) (f : (k : ℕ) → Y k ⟶ Y (k + 1)) (g : (k : ℕ) → Z k ⟶ Z (k + 1)) (h : (k : ℕ) → Z k ⟶ U (k + 1)) (comm : ∀ (k : ℕ), CategoryTheory.CategoryStruct.comp (f k) (b (k + 1)) = CategoryTheory.CategoryStruct.comp (b k) (g k)) (hzero : ∀ (k : ℕ), CategoryTheory.CategoryStruct.comp (b k) (h k) = 0) (hS : ∀ (k : ℕ), LeftTauSequence (S k)) (e : ∀ (k : ℕ), Nonempty (S k ≅ stepComplex (b k) (b (k + 1)) (f k) (g k) (h k) ⋯ ⋯)) {P W : C} (p : P ⟶ Y 0) (hp : CategoryTheory.CategoryStruct.comp p (b 0) = 0) {r : Y 0 ⟶ W} (hr : r ∈ (R.ideal.pow n).hom (Y 0) W) : ∃ (t : Y n ⟶ W), CategoryTheory.CategoryStruct.comp p r = CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp (forwardComposite Y f n) t)

The dual radical-layer factorization used in Iyama 6.4.1(1)(ii).

If a prefix p annihilates the current left-ladder arrow, precomposing a J^n morphism by p makes it factor through the first n left-ladder domain maps.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.not_isZero_domain_of_nonzero_mem_pow {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (R : CategoricalRadical.NilpotentRadicalData C) (n : ℕ) (S : ℕ → CategoryTheory.ShortComplex C) (Y Z U : ℕ → C) (b : (k : ℕ) → Y k ⟶ Z k) (f : (k : ℕ) → Y k ⟶ Y (k + 1)) (g : (k : ℕ) → Z k ⟶ Z (k + 1)) (h : (k : ℕ) → Z k ⟶ U (k + 1)) (comm : ∀ (k : ℕ), CategoryTheory.CategoryStruct.comp (f k) (b (k + 1)) = CategoryTheory.CategoryStruct.comp (b k) (g k)) (hzero : ∀ (k : ℕ), CategoryTheory.CategoryStruct.comp (b k) (h k) = 0) (hS : ∀ (k : ℕ), LeftTauSequence (S k)) (e : ∀ (k : ℕ), Nonempty (S k ≅ stepComplex (b k) (b (k + 1)) (f k) (g k) (h k) ⋯ ⋯)) (hbzero : b 0 = 0) {W : C} (r : Y 0 ⟶ W) (hr : r ∈ (R.ideal.pow n).hom (Y 0) W) (hrne : r ≠ 0) : ¬CategoryTheory.Limits.IsZero (Y n)

A nonzero J^n morphism out of the source of a zero-initial left ladder forces the domain of its nth arrow to be nonzero.