Preradicals

A preradical on an abelian category C is a monomorphism in the functor category C ⥤ C with codomain 𝟭 C, i.e. an element of MonoOver (𝟭 C).

Main definitions

• Preradical C: The type of preradicals on C.
• Preradical.r: The underlying endofunctor of a Preradical.
• Preradical.ι: The structure morphism of a Preradical.
• Preradical.IsIdempotent: The predicate expressing idempotence.

References

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

Tags

category theory, preradical, torsion theory

@[reducible, inline]

abbrev CategoryTheory.Abelian.Preradical (C : Type u) [Category.{v, u} C] : Type (max u v)

A preradical on an abelian category C is a monomorphism in C ⥤ C with codomain 𝟭 C.

Equations

• CategoryTheory.Abelian.Preradical C = CategoryTheory.MonoOver (CategoryTheory.Functor.id C)

@[reducible, inline]

abbrev CategoryTheory.Abelian.Preradical.r {C : Type u} [Category.{v, u} C] (Φ : Preradical C) : Functor C C

The underlying endofunctor r : C ⥤ C of a preradical Φ.

Equations

• Φ.r = Φ.obj.left

@[reducible, inline]

abbrev CategoryTheory.Abelian.Preradical.ι {C : Type u} [Category.{v, u} C] (Φ : Preradical C) : Φ.r ⟶ Functor.id C

The structure morphism Φ.r ⟶ 𝟭 C of a preradical Φ.

Equations

• Φ.ι = Φ.obj.hom

@[simp]

theorem CategoryTheory.Abelian.Preradical.r_map_ι_app {C : Type u} [Category.{v, u} C] [Abelian C] (Φ : Preradical C) (X : C) : Φ.r.map (Φ.ι.app X) = Φ.ι.app (Φ.r.obj X)

class CategoryTheory.Abelian.Preradical.IsIdempotent {C : Type u} [Category.{v, u} C] (Φ : Preradical C) : Prop

A preradical Φ is idempotent if Φ.r ⋙ Φ.r ≅ Φ.r.

• isIso_whiskerLeft_r_ι : IsIso (Φ.r.whiskerLeft Φ.ι)

instance CategoryTheory.Abelian.Preradical.instIsIsoAppιObjROfIsIdempotent {C : Type u} [Category.{v, u} C] (Φ : Preradical C) [Φ.IsIdempotent] (X : C) : IsIso (Φ.ι.app (Φ.r.obj X))

instance CategoryTheory.Abelian.Preradical.instIsIsoMapRAppιOfIsIdempotent {C : Type u} [Category.{v, u} C] [Abelian C] (Φ : Preradical C) [Φ.IsIdempotent] (X : C) : IsIso (Φ.r.map (Φ.ι.app X))