Radical-power propagation in Iyama right ladders

This file formalizes the annihilator-propagation calculation in Iyama, Tau-categories I, Lemma 6.4.1(1)(i). A weak-kernel right-ladder step moves an annihilator to the next rung up to its complementary term. Iteration and nilpotence then force one complementary composite to be nonzero in the corresponding radical power.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.RightLadder.stepComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {ZPrev YPrev ZNext YNext U : C} (bPrev : ZPrev ⟶ YPrev) (bNext : ZNext ⟶ YNext) (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) : CategoryTheory.ShortComplex C

The explicit right-ladder step from Iyama, Section 3.2:

ZNext ⊞ U → YNext ⊞ ZPrev → YPrev,

with first-map matrix [[bNext, 0], [-g, h]] and second map (f, bPrev).

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.exists_next_annihilator {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {ZPrev YPrev ZNext YNext U W : C} {bPrev : ZPrev ⟶ YPrev} {bNext : ZNext ⟶ YNext} {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} (hweak : ShortComplex.IsWeakKernel (stepComplex bPrev bNext f g h comm hzero)) (sPrev : W ⟶ ZPrev) (hsPrev : CategoryTheory.CategoryStruct.comp sPrev bPrev = 0) : ∃ (sNext : W ⟶ ZNext) (t : W ⟶ U), CategoryTheory.CategoryStruct.comp sNext bNext = 0 ∧ sPrev = CategoryTheory.CategoryStruct.comp sNext g + CategoryTheory.CategoryStruct.comp t h

One weak-kernel right-ladder step propagates an annihilator across the step, up to the complementary U-term.

This is the literal calculation sPrev = sNext ≫ g + t ≫ h and sNext ≫ bNext = 0 in the proof of Iyama 6.4.1(1)(i).

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.stepMaps_mem_radical_of_rightTauSequence_iso_stepComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (R : CategoricalRadical.NilpotentRadicalData C) {ZPrev YPrev ZNext YNext U : C} {bPrev : ZPrev ⟶ YPrev} {bNext : ZNext ⟶ YNext} {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} {S : CategoryTheory.ShortComplex C} (hS : RightTauSequence S) (e : S ≅ stepComplex bPrev bNext f g h comm hzero) : bNext ∈ R.ideal.hom ZNext YNext ∧ g ∈ R.ideal.hom ZNext ZPrev ∧ h ∈ R.ideal.hom U ZPrev

If an explicit right-ladder step is isomorphic to a right tau-sequence, then all three visible components of its first map belong to the chosen categorical radical ideal.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.nextMap_mem_radical_of_rightTauSequence_iso_stepComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (R : CategoricalRadical.NilpotentRadicalData C) {ZPrev YPrev ZNext YNext U : C} {bPrev : ZPrev ⟶ YPrev} {bNext : ZNext ⟶ YNext} {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} {S : CategoryTheory.ShortComplex C} (hS : RightTauSequence S) (e : S ≅ stepComplex bPrev bNext f g h comm hzero) : bNext ∈ R.ideal.hom ZNext YNext

The next horizontal arrow in an explicit right-ladder step is radical.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.nextMap_mem_radical_of_rightTauSequence_nonempty_iso_stepComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (R : CategoricalRadical.NilpotentRadicalData C) {ZPrev YPrev ZNext YNext U : C} {bPrev : ZPrev ⟶ YPrev} {bNext : ZNext ⟶ YNext} {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} {S : CategoryTheory.ShortComplex C} (hS : RightTauSequence S) (e : Nonempty (S ≅ stepComplex bPrev bNext f g h comm hzero)) : bNext ∈ R.ideal.hom ZNext YNext

Nonempty form of radicality of the next horizontal arrow.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.connectingMaps_mem_radical_of_rightTauSequence_iso_stepComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (R : CategoricalRadical.NilpotentRadicalData C) {ZPrev YPrev ZNext YNext U : C} {bPrev : ZPrev ⟶ YPrev} {bNext : ZNext ⟶ YNext} {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} {S : CategoryTheory.ShortComplex C} (hS : RightTauSequence S) (e : S ≅ stepComplex bPrev bNext f g h comm hzero) : g ∈ R.ideal.hom ZNext ZPrev ∧ h ∈ R.ideal.hom U ZPrev

Both connecting components in an explicit right-ladder step are radical.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.connectingMaps_mem_radical_of_rightTauSequence_nonempty_iso_stepComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (R : CategoricalRadical.NilpotentRadicalData C) {ZPrev YPrev ZNext YNext U : C} {bPrev : ZPrev ⟶ YPrev} {bNext : ZNext ⟶ YNext} {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} {S : CategoryTheory.ShortComplex C} (hS : RightTauSequence S) (e : Nonempty (S ≅ stepComplex bPrev bNext f g h comm hzero)) : g ∈ R.ideal.hom ZNext ZPrev ∧ h ∈ R.ideal.hom U ZPrev

Nonempty form matching the noncanonical mesh isomorphisms stored in Iyama ladder data.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.connectingMaps_mem_radical_of_rightTauSequence_stepFamily {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (R : CategoricalRadical.NilpotentRadicalData C) (S : ℕ → CategoryTheory.ShortComplex C) (Z Y U : ℕ → C) (b : (n : ℕ) → Z n ⟶ Y n) (f : (n : ℕ) → Y (n + 1) ⟶ Y n) (g : (n : ℕ) → Z (n + 1) ⟶ Z n) (h : (n : ℕ) → U (n + 1) ⟶ Z n) (comm : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (b (n + 1)) (f n) = CategoryTheory.CategoryStruct.comp (g n) (b n)) (hzero : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (h n) (b n) = 0) (hS : ∀ (n : ℕ), RightTauSequence (S n)) (e : ∀ (n : ℕ), Nonempty (S n ≅ stepComplex (b n) (b (n + 1)) (f n) (g n) (h n) ⋯ ⋯)) : (∀ (n : ℕ), g n ∈ R.ideal.hom (Z (n + 1)) (Z n)) ∧ ∀ (n : ℕ), h n ∈ R.ideal.hom (U (n + 1)) (Z n)

Family form aligned with the hypotheses of right-ladder radical-power propagation.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.isWeakKernel_stepComplex_of_rightTauSequence_nonempty_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {ZPrev YPrev ZNext YNext U : C} {bPrev : ZPrev ⟶ YPrev} {bNext : ZNext ⟶ YNext} {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} {S : CategoryTheory.ShortComplex C} (hS : RightTauSequence S) (e : Nonempty (S ≅ stepComplex bPrev bNext f g h comm hzero)) : ShortComplex.IsWeakKernel (stepComplex bPrev bNext f g h comm hzero)

A right tau-sequence isomorphic to an explicit right-ladder step makes that step a weak-kernel complex.

def QuotientSubmoduleEquidistribution.Iyama.RightLadder.backwardComposite {C : Type u} [CategoryTheory.Category.{v, u} C] (Z : ℕ → C) (g : (n : ℕ) → Z (n + 1) ⟶ Z n) (n : ℕ) : Z n ⟶ Z 0

The backwards composite of the first n right-ladder connecting maps.

@[simp]

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.backwardComposite_zero {C : Type u} [CategoryTheory.Category.{v, u} C] (Z : ℕ → C) (g : (n : ℕ) → Z (n + 1) ⟶ Z n) : backwardComposite Z g 0 = CategoryTheory.CategoryStruct.id (Z 0)

@[simp]

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.backwardComposite_succ {C : Type u} [CategoryTheory.Category.{v, u} C] (Z : ℕ → C) (g : (n : ℕ) → Z (n + 1) ⟶ Z n) (n : ℕ) : backwardComposite Z g (n + 1) = CategoryTheory.CategoryStruct.comp (g n) (backwardComposite Z g n)

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.backwardComposite_mem_pow {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : CategoricalIdeal.HomIdeal C) (Z : ℕ → C) (g : (n : ℕ) → Z (n + 1) ⟶ Z n) (hg : ∀ (n : ℕ), g n ∈ I.hom (Z (n + 1)) (Z n)) (n : ℕ) : backwardComposite Z g n ∈ (I.pow n).hom (Z n) (Z 0)

A chain of radical connecting maps has its length-n composite in the nth ideal power.

def QuotientSubmoduleEquidistribution.Iyama.RightLadder.HasAnnihilatorPropagation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (Z Y U : ℕ → C) (b : (n : ℕ) → Z n ⟶ Y n) (g : (n : ℕ) → Z (n + 1) ⟶ Z n) (h : (n : ℕ) → U (n + 1) ⟶ Z n) : Prop

The exact abstract output needed from every explicit right-ladder step.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.hasAnnihilatorPropagation_of_weakKernels {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (Z Y U : ℕ → C) (b : (n : ℕ) → Z n ⟶ Y n) (f : (n : ℕ) → Y (n + 1) ⟶ Y n) (g : (n : ℕ) → Z (n + 1) ⟶ Z n) (h : (n : ℕ) → U (n + 1) ⟶ Z n) (comm : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (b (n + 1)) (f n) = CategoryTheory.CategoryStruct.comp (g n) (b n)) (hzero : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (h n) (b n) = 0) (hweak : ∀ (n : ℕ), ShortComplex.IsWeakKernel (stepComplex (b n) (b (n + 1)) (f n) (g n) (h n) ⋯ ⋯)) : HasAnnihilatorPropagation Z Y U b g h

A family of explicit weak-kernel right-ladder steps supplies the abstract annihilator-propagation property.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.hasAnnihilatorPropagation_of_rightTauSequence_stepFamily {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (S : ℕ → CategoryTheory.ShortComplex C) (Z Y U : ℕ → C) (b : (n : ℕ) → Z n ⟶ Y n) (f : (n : ℕ) → Y (n + 1) ⟶ Y n) (g : (n : ℕ) → Z (n + 1) ⟶ Z n) (h : (n : ℕ) → U (n + 1) ⟶ Z n) (comm : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (b (n + 1)) (f n) = CategoryTheory.CategoryStruct.comp (g n) (b n)) (hzero : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (h n) (b n) = 0) (hS : ∀ (n : ℕ), RightTauSequence (S n)) (e : ∀ (n : ℕ), Nonempty (S n ≅ stepComplex (b n) (b (n + 1)) (f n) (g n) (h n) ⋯ ⋯)) : HasAnnihilatorPropagation Z Y U b g h

Right tau-sequence models of all explicit ladder steps supply the annihilator propagation used in radical-power iteration.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.exists_propagated_annihilator {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (Z Y U : ℕ → C) (b : (n : ℕ) → Z n ⟶ Y n) (g : (n : ℕ) → Z (n + 1) ⟶ Z n) (h : (n : ℕ) → U (n + 1) ⟶ Z n) (hstep : HasAnnihilatorPropagation Z Y U b g h) (hkill : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (h n) (backwardComposite Z g n) = 0) {W : C} (s₀ : W ⟶ Z 0) (hs₀ : CategoryTheory.CategoryStruct.comp s₀ (b 0) = 0) (n : ℕ) : ∃ (s : W ⟶ Z n), CategoryTheory.CategoryStruct.comp s (b n) = 0 ∧ s₀ = CategoryTheory.CategoryStruct.comp s (backwardComposite Z g n)

If all complementary terms vanish after composing to the initial source, an initial annihilator propagates through every finite right-ladder prefix.

theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.exists_nonzero_remainder_in_radical_power {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : CategoricalRadical.NilpotentRadicalData C) (Z Y U : ℕ → C) (b : (n : ℕ) → Z n ⟶ Y n) (g : (n : ℕ) → Z (n + 1) ⟶ Z n) (h : (n : ℕ) → U (n + 1) ⟶ Z n) (hstep : HasAnnihilatorPropagation Z Y U b g h) (hg : ∀ (n : ℕ), g n ∈ R.ideal.hom (Z (n + 1)) (Z n)) (hh : ∀ (n : ℕ), h n ∈ R.ideal.hom (U (n + 1)) (Z n)) {W : C} (s₀ : W ⟶ Z 0) (hs₀ : CategoryTheory.CategoryStruct.comp s₀ (b 0) = 0) (hs₀ne : s₀ ≠ 0) : ∃ (n : ℕ), CategoryTheory.CategoryStruct.comp (h n) (backwardComposite Z g n) ∈ (R.ideal.pow (n + 1)).hom (U (n + 1)) (Z 0) ∧ CategoryTheory.CategoryStruct.comp (h n) (backwardComposite Z g n) ≠ 0

Radical-power propagation in the form used in Iyama 6.4.1(1)(i).

Starting from a nonzero annihilator, some complementary morphism hᵢ ≫ gᵢ₋₁ ≫ ⋯ ≫ g₁ is nonzero. It automatically lies in the corresponding radical power. Thus the hypothesis that every Jⁱ(Uᵢ,Z₀) vanishes is incompatible with the initial nonzero annihilator.