Radical-power propagation in Iyama left ladders #
This is the categorical dual of the right-ladder calculation in Iyama, Tau-categories I, Lemma 6.4.1(1)(i). The explicit matrix is obtained by opposing the right-ladder matrix and then writing the biproducts back in the original category.
noncomputable def
QuotientSubmoduleEquidistribution.Iyama.LeftLadder.stepComplex
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{YPrev ZPrev YNext ZNext U : 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)
:
CategoryTheory.ShortComplex C
The explicit left-ladder step, dual to Iyama's right-ladder step:
YPrev → YNext ⊞ ZPrev → ZNext ⊞ U,
with first map (f, bPrev) and second-map matrix
[[bNext, -g], [0, h]].
Instances For
theorem
QuotientSubmoduleEquidistribution.Iyama.LeftLadder.exists_next_coannihilator
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts 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}
(hweak : ShortComplex.IsWeakCokernel (stepComplex bPrev bNext f g h comm hzero))
(sPrev : ZPrev ⟶ W)
(hsPrev : CategoryTheory.CategoryStruct.comp bPrev sPrev = 0)
:
∃ (sNext : ZNext ⟶ W) (t : U ⟶ W),
CategoryTheory.CategoryStruct.comp bNext sNext = 0 ∧ sPrev = CategoryTheory.CategoryStruct.comp g sNext + CategoryTheory.CategoryStruct.comp h t
One weak-cokernel left-ladder step propagates a coannihilator across the
step, up to the complementary U-term.
This is the dual identity
sPrev = g ≫ sNext + h ≫ t with bNext ≫ sNext = 0.
theorem
QuotientSubmoduleEquidistribution.Iyama.LeftLadder.stepMaps_mem_radical_of_leftTauSequence_iso_stepComplex
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
(R : CategoricalRadical.NilpotentRadicalData C)
{YPrev ZPrev YNext ZNext U : 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)
:
If an explicit left-ladder step is isomorphic to a left tau-sequence, then all three visible components of its second map belong to the chosen categorical radical ideal.
theorem
QuotientSubmoduleEquidistribution.Iyama.LeftLadder.nextMap_mem_radical_of_leftTauSequence_iso_stepComplex
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
(R : CategoricalRadical.NilpotentRadicalData C)
{YPrev ZPrev YNext ZNext U : 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)
:
The next horizontal arrow in an explicit left-ladder step is radical.
theorem
QuotientSubmoduleEquidistribution.Iyama.LeftLadder.nextMap_mem_radical_of_leftTauSequence_nonempty_iso_stepComplex
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
(R : CategoricalRadical.NilpotentRadicalData C)
{YPrev ZPrev YNext ZNext U : 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 : Nonempty (S ≅ stepComplex bPrev bNext f g h comm hzero))
:
Nonempty form of radicality of the next horizontal arrow.
theorem
QuotientSubmoduleEquidistribution.Iyama.LeftLadder.connectingMaps_mem_radical_of_leftTauSequence_iso_stepComplex
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
(R : CategoricalRadical.NilpotentRadicalData C)
{YPrev ZPrev YNext ZNext U : 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)
:
Both connecting components in an explicit left-ladder step are radical.
theorem
QuotientSubmoduleEquidistribution.Iyama.LeftLadder.connectingMaps_mem_radical_of_leftTauSequence_nonempty_iso_stepComplex
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
(R : CategoricalRadical.NilpotentRadicalData C)
{YPrev ZPrev YNext ZNext U : 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 : Nonempty (S ≅ stepComplex bPrev bNext f g h comm hzero))
:
Nonempty form matching noncanonical mesh isomorphisms.
theorem
QuotientSubmoduleEquidistribution.Iyama.LeftLadder.connectingMaps_mem_radical_of_leftTauSequence_stepFamily
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
(R : CategoricalRadical.NilpotentRadicalData C)
(S : ℕ → CategoryTheory.ShortComplex C)
(Y Z U : ℕ → C)
(b : (n : ℕ) → Y n ⟶ Z n)
(f : (n : ℕ) → Y n ⟶ Y (n + 1))
(g : (n : ℕ) → Z n ⟶ Z (n + 1))
(h : (n : ℕ) → Z n ⟶ U (n + 1))
(comm :
∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (f n) (b (n + 1)) = CategoryTheory.CategoryStruct.comp (b n) (g n))
(hzero : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (b n) (h n) = 0)
(hS : ∀ (n : ℕ), LeftTauSequence (S n))
(e : ∀ (n : ℕ), Nonempty (S n ≅ stepComplex (b n) (b (n + 1)) (f n) (g n) (h n) ⋯ ⋯))
:
Family form aligned with left-ladder radical-power propagation.
theorem
QuotientSubmoduleEquidistribution.Iyama.LeftLadder.isWeakCokernel_stepComplex_of_leftTauSequence_nonempty_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{YPrev ZPrev YNext ZNext U : 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 : Nonempty (S ≅ stepComplex bPrev bNext f g h comm hzero))
:
ShortComplex.IsWeakCokernel (stepComplex bPrev bNext f g h comm hzero)
A left tau-sequence isomorphic to an explicit left-ladder step makes that step a weak-cokernel complex.
def
QuotientSubmoduleEquidistribution.Iyama.LeftLadder.forwardComposite
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(Z : ℕ → C)
(g : (n : ℕ) → Z n ⟶ Z (n + 1))
(n : ℕ)
:
Z 0 ⟶ Z n
The forwards composite of the first n left-ladder connecting maps.
Instances For
@[simp]
theorem
QuotientSubmoduleEquidistribution.Iyama.LeftLadder.forwardComposite_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(Z : ℕ → C)
(g : (n : ℕ) → Z n ⟶ Z (n + 1))
:
forwardComposite Z g 0 = CategoryTheory.CategoryStruct.id (Z 0)
@[simp]
theorem
QuotientSubmoduleEquidistribution.Iyama.LeftLadder.forwardComposite_succ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(Z : ℕ → C)
(g : (n : ℕ) → Z n ⟶ Z (n + 1))
(n : ℕ)
:
forwardComposite Z g (n + 1) = CategoryTheory.CategoryStruct.comp (forwardComposite Z g n) (g n)
theorem
QuotientSubmoduleEquidistribution.Iyama.LeftLadder.forwardComposite_mem_pow
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(I : CategoricalIdeal.HomIdeal C)
(Z : ℕ → C)
(g : (n : ℕ) → Z n ⟶ Z (n + 1))
(hg : ∀ (n : ℕ), g n ∈ I.hom (Z n) (Z (n + 1)))
(n : ℕ)
:
forwardComposite Z g n ∈ (I.pow n).hom (Z 0) (Z n)
A chain of radical connecting maps has its length-n composite in the
nth ideal power.
def
QuotientSubmoduleEquidistribution.Iyama.LeftLadder.HasCoannihilatorPropagation
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(Y Z U : ℕ → C)
(b : (n : ℕ) → Y n ⟶ Z n)
(g : (n : ℕ) → Z n ⟶ Z (n + 1))
(h : (n : ℕ) → Z n ⟶ U (n + 1))
:
The exact abstract output needed from every explicit left-ladder step.
Instances For
theorem
QuotientSubmoduleEquidistribution.Iyama.LeftLadder.hasCoannihilatorPropagation_of_weakCokernels
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
(Y Z U : ℕ → C)
(b : (n : ℕ) → Y n ⟶ Z n)
(f : (n : ℕ) → Y n ⟶ Y (n + 1))
(g : (n : ℕ) → Z n ⟶ Z (n + 1))
(h : (n : ℕ) → Z n ⟶ U (n + 1))
(comm :
∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (f n) (b (n + 1)) = CategoryTheory.CategoryStruct.comp (b n) (g n))
(hzero : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (b n) (h n) = 0)
(hweak : ∀ (n : ℕ), ShortComplex.IsWeakCokernel (stepComplex (b n) (b (n + 1)) (f n) (g n) (h n) ⋯ ⋯))
:
HasCoannihilatorPropagation Y Z U b g h
A family of explicit weak-cokernel left-ladder steps supplies the abstract coannihilator-propagation property.
theorem
QuotientSubmoduleEquidistribution.Iyama.LeftLadder.hasCoannihilatorPropagation_of_leftTauSequence_stepFamily
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
(S : ℕ → CategoryTheory.ShortComplex C)
(Y Z U : ℕ → C)
(b : (n : ℕ) → Y n ⟶ Z n)
(f : (n : ℕ) → Y n ⟶ Y (n + 1))
(g : (n : ℕ) → Z n ⟶ Z (n + 1))
(h : (n : ℕ) → Z n ⟶ U (n + 1))
(comm :
∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (f n) (b (n + 1)) = CategoryTheory.CategoryStruct.comp (b n) (g n))
(hzero : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (b n) (h n) = 0)
(hS : ∀ (n : ℕ), LeftTauSequence (S n))
(e : ∀ (n : ℕ), Nonempty (S n ≅ stepComplex (b n) (b (n + 1)) (f n) (g n) (h n) ⋯ ⋯))
:
HasCoannihilatorPropagation Y Z U b g h
Left tau-sequence models of all explicit ladder steps supply the coannihilator propagation used in radical-power iteration.
theorem
QuotientSubmoduleEquidistribution.Iyama.LeftLadder.exists_propagated_coannihilator
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(Y Z U : ℕ → C)
(b : (n : ℕ) → Y n ⟶ Z n)
(g : (n : ℕ) → Z n ⟶ Z (n + 1))
(h : (n : ℕ) → Z n ⟶ U (n + 1))
(hstep : HasCoannihilatorPropagation Y Z U b g h)
(hkill : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (forwardComposite Z g n) (h n) = 0)
{W : C}
(s₀ : Z 0 ⟶ W)
(hs₀ : CategoryTheory.CategoryStruct.comp (b 0) s₀ = 0)
(n : ℕ)
:
∃ (s : Z n ⟶ W),
CategoryTheory.CategoryStruct.comp (b n) s = 0 ∧ s₀ = CategoryTheory.CategoryStruct.comp (forwardComposite Z g n) s
If all complementary terms vanish after composing from the initial target, an initial coannihilator propagates through every finite left-ladder prefix.
theorem
QuotientSubmoduleEquidistribution.Iyama.LeftLadder.exists_nonzero_coremainder_in_radical_power
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(R : CategoricalRadical.NilpotentRadicalData C)
(Y Z U : ℕ → C)
(b : (n : ℕ) → Y n ⟶ Z n)
(g : (n : ℕ) → Z n ⟶ Z (n + 1))
(h : (n : ℕ) → Z n ⟶ U (n + 1))
(hstep : HasCoannihilatorPropagation Y Z U b g h)
(hg : ∀ (n : ℕ), g n ∈ R.ideal.hom (Z n) (Z (n + 1)))
(hh : ∀ (n : ℕ), h n ∈ R.ideal.hom (Z n) (U (n + 1)))
{W : C}
(s₀ : Z 0 ⟶ W)
(hs₀ : CategoryTheory.CategoryStruct.comp (b 0) s₀ = 0)
(hs₀ne : s₀ ≠ 0)
:
∃ (n : ℕ),
CategoryTheory.CategoryStruct.comp (forwardComposite Z g n) (h n) ∈ (R.ideal.pow (n + 1)).hom (Z 0) (U (n + 1)) ∧ CategoryTheory.CategoryStruct.comp (forwardComposite Z g n) (h n) ≠ 0
Radical-power propagation dual to Iyama 6.4.1(1)(i).
Starting from a nonzero coannihilator, some complementary morphism
g₁ ≫ ⋯ ≫ gᵢ₋₁ ≫ hᵢ is nonzero and lies in the corresponding
radical power.