Radicals

In this file we define what it means for a preradical Φ : Preradical C on an abelian category C to be radical, and we define Radical C as the full subcategory of Preradical C consisting of radicals.

Following Stenström, a preradical Φ is called radical if it coincides with its self colon. We encode this as the property that the natural transformation toColon Φ Φ : Φ ⟶ Φ.colon Φ is an isomorphism, and we prove a basic characterization of radicals in terms of the vanishing of Φ.r on Φ.quotient.

Main definitions

• Preradical.IsRadical : The property that a preradical Φ is radical, i.e. that (Φ.colon Φ) ≅ Φ.

• Radical C : The type of radicals on C, as a full subcategory of Preradical C.

Main results

• Preradical.isRadical_iff_isZero : A preradical Φ is radical if and only if Φ.quotient ⋙ Φ.r is the zero object.

References

• Bo Stenström, Rings and Modules of Quotients
• Bo Stenström, Rings of Quotients

Tags

preradical, radical, torsion theory, abelian

def CategoryTheory.Abelian.Preradical.isRadical (C : Type u_1) [Category.{v_1, u_1} C] [Abelian C] : ObjectProperty (Preradical C)

A preradical Φ is radical if Φ.colon Φ ≅ Φ.

Equations

• CategoryTheory.Abelian.Preradical.isRadical C Φ = CategoryTheory.IsIso (Φ.toColon Φ)

theorem CategoryTheory.Abelian.Preradical.isRadical_iff_isIso (C : Type u_1) [Category.{v_1, u_1} C] [Abelian C] (Φ : Preradical C) : isRadical C Φ ↔ IsIso (Φ.toColon Φ)

theorem CategoryTheory.Abelian.Preradical.isRadical_iff_isZero (C : Type u_1) [Category.{v_1, u_1} C] [Abelian C] (Φ : Preradical C) : isRadical C Φ ↔ Limits.IsZero (Φ.quotient.comp Φ.r)

A preradical Φ is radical if and only if it Φ vanishes on the quotient Φ.quotient.

@[reducible, inline]

abbrev CategoryTheory.Abelian.Radical (C : Type u_1) [Category.{v_1, u_1} C] [Abelian C] : Type (max u_1 v_1)

The category of radicals on C, defined as the full subcategory of Preradical C consisting of preradicals Φ such that toColon Φ Φ is an isomorphism.

Equations

• CategoryTheory.Abelian.Radical C = (CategoryTheory.Abelian.Preradical.isRadical C).FullSubcategory

instance CategoryTheory.Abelian.Radical.instIsIsoPreradicalToColonObjIsRadical {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (Φ : Radical C) : IsIso (Φ.obj.toColon Φ.obj)

theorem CategoryTheory.Abelian.Radical.isZero {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (Φ : Radical C) : Limits.IsZero (Φ.obj.quotient.comp Φ.obj.r)