Nilpotence of the radical from a finite additive generator

If every object is a retract of a finite biproduct of one object G, and End(G) is Artinian, then the categorical radical Hom ideal is nilpotent.

This is a bounded adaptation of QuotientSubmoduleEquidistribution.CategoryTheory.FiniteGeneratorRadicalNilpotence at donor commit d5ba0c48e7a851afd51247ff9cd81fc629e00ed2. Only the finite-generator definitions and nilpotence proof are retained; the donor's wider Auslander-equivalence layer is not imported.

structure MagnitudeConjecture.CategoryTheory.FiniteAddPresentation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (G X : C) : Type v

A witness that X is a retract of a finite biproduct of copies of G.

• n : ℕ
• retract : CategoryTheory.Retract X (⨁ fun (x : Fin self.n) => G)

def MagnitudeConjecture.CategoryTheory.IsFiniteAddGenerator {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (G : C) : Prop

An object is a finite additive generator when every object is a retract of a finite biproduct of copies of it.

theorem MagnitudeConjecture.CategoryTheory.mem_jacobson_of_isRadicalEndomorphism {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X : C} {f : X ⟶ X} (hf : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism f) : CategoryTheory.End.of f ∈ Ring.jacobson (CategoryTheory.End X)

A categorical-radical endomorphism belongs to the ring-theoretic Jacobson radical.

theorem MagnitudeConjecture.CategoryTheory.sandwich_mem_jacobson {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {G X Y : C} {f : X ⟶ Y} (hf : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism f) (a : G ⟶ X) (b : Y ⟶ G) : CategoryTheory.End.of (CategoryTheory.CategoryStruct.comp a (CategoryTheory.CategoryStruct.comp f b)) ∈ Ring.jacobson (CategoryTheory.End G)

Sandwiching a categorical-radical morphism between maps from and to a fixed object gives an element of that object's endomorphism-ring radical.

theorem MagnitudeConjecture.CategoryTheory.sandwich_mem_jacobson_pow {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (G : C) (hG : IsFiniteAddGenerator G) (n : ℕ) {X Y : C} {f : X ⟶ Y} : f ∈ (QuotientSubmoduleEquidistribution.CategoricalRadical.homIdeal.pow n).hom X Y → ∀ (a : G ⟶ X) (b : Y ⟶ G), CategoryTheory.End.of (CategoryTheory.CategoryStruct.comp a (CategoryTheory.CategoryStruct.comp f b)) ∈ Ring.jacobson (CategoryTheory.End G) ^ n

A morphism in the n-th categorical radical power becomes an element of the n-th Jacobson-radical power after sandwiching by maps from and to a finite additive generator.

theorem MagnitudeConjecture.CategoryTheory.eq_zero_of_forall_generator_sandwich_eq_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (G : C) (hG : IsFiniteAddGenerator G) {X Y : C} (f : X ⟶ Y) (hzero : ∀ (a : G ⟶ X) (b : Y ⟶ G), CategoryTheory.CategoryStruct.comp a (CategoryTheory.CategoryStruct.comp f b) = 0) : f = 0

A finite additive generator detects zero morphisms by two-sided sandwiches.

theorem MagnitudeConjecture.CategoryTheory.homIdeal_isNilpotent_of_generator_jacobson {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (G : C) (hG : IsFiniteAddGenerator G) (hJ : IsNilpotent (Ring.jacobson (CategoryTheory.End G))) : QuotientSubmoduleEquidistribution.CategoricalRadical.homIdeal.IsNilpotent

If the Jacobson radical of the endomorphism ring of a finite additive generator is nilpotent, then the categorical radical Hom ideal is nilpotent with the same exponent.

theorem MagnitudeConjecture.CategoryTheory.homIdeal_isNilpotent_of_artinian_generator {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (G : C) (hG : IsFiniteAddGenerator G) [IsArtinianRing (CategoryTheory.End G)] : QuotientSubmoduleEquidistribution.CategoricalRadical.homIdeal.IsNilpotent

Artinianity of the generator endomorphism ring supplies categorical radical nilpotence.

def MagnitudeConjecture.CategoryTheory.nilpotentRadicalDataOfArtinianGenerator {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (G : C) (hG : IsFiniteAddGenerator G) [IsArtinianRing (CategoryTheory.End G)] : QuotientSubmoduleEquidistribution.CategoricalRadical.NilpotentRadicalData C

Canonical nilpotent-radical data for a category with an Artinian finite additive generator.