A nilpotent categorical radical as Hom-ideal data

The current categorical-radical predicate is morphismwise. Iyama's ladder argument also needs powers of that radical. This file gives the exact bridge: a two-sided additive Hom ideal whose membership predicate is the categorical radical, together with a nilpotence exponent.

Nilpotence is stronger than Iyama's general J^∞ = 0 hypothesis, but is the appropriate finite condition for the acyclic word mesh categories used in the manuscript.

structure QuotientSubmoduleEquidistribution.CategoricalRadical.NilpotentRadicalData (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : Type (max u v)

A realization of the categorical radical as a nilpotent two-sided additive Hom ideal.

• ideal : CategoricalIdeal.HomIdeal C
• mem_iff {X Y : C} (f : X ⟶ Y) : f ∈ self.ideal.hom X Y ↔ IsRadicalMorphism f
• nilpotent : self.ideal.IsNilpotent

theorem QuotientSubmoduleEquidistribution.CategoricalRadical.NilpotentRadicalData.mem_ideal_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : NilpotentRadicalData C) {X Y : C} (f : X ⟶ Y) : f ∈ R.ideal.hom X Y ↔ IsRadicalMorphism f

Radical membership may be converted to membership in the chosen Hom ideal.

theorem QuotientSubmoduleEquidistribution.CategoricalRadical.NilpotentRadicalData.eq_zero_of_mem_every_power {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : NilpotentRadicalData C) {X Y : C} {f : X ⟶ Y} (hf : ∀ (n : ℕ), f ∈ (R.ideal.pow n).hom X Y) : f = 0

A morphism lying in every power of a nilpotent categorical radical is zero.

theorem QuotientSubmoduleEquidistribution.CategoricalRadical.NilpotentRadicalData.isNilpotent_end_of_mem_ideal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : NilpotentRadicalData C) {X : C} {f : X ⟶ X} (hf : f ∈ R.ideal.hom X X) : IsNilpotent (CategoryTheory.End.of f)

A radical endomorphism is nilpotent when the categorical radical Hom ideal is nilpotent.