Torsion Theory

A torsion theory on an abelian category C is a pair of classes T and F of objects from C such that T is the left orthogonal of F and F is the right orthogonal of T. We call T the torsion class and its objects torsion objects. We call F the torsion-free class and its objects torsion-free objects.

Main definitions

• CategoryTheory.Abelian.TorsionTheory T F: the statement that the pair of object properties T and F is a torsion theory on C.
• CategoryTheory.Abelian.IsTorsionClass P: the statement that P is the torsion class of some torsion theory on C.
• CategoryTheory.Abelian.IsTorsionFreeClass P: the statement that P is the torsion-free class of some torsion theory on C.

Main results

• CategoryTheory.Abelian.isTorsionClass_iff: in a well-powered abelian category with coproducts, P is a torsion class if and only if it is closed under quotients, extensions, and coproducts (a theorem of S. E. Dickson).
• CategoryTheory.Abelian.isTorsionFreeClass_iff: dually, in a well-copowered abelian category with products, P is a torsion-free class if and only if it is closed under subobjects, extensions, and products.

References

• S. E. Dickson, A torsion theory for Abelian categories
• Bo Stenström, Rings and Modules of Quotients
• Bo Stenström, Rings of Quotients

Tags

torsion theory, torsion class, torsion-free class, orthogonal

structure CategoryTheory.Abelian.TorsionTheory {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (T F : ObjectProperty C) : Prop

A torsion theory in an abelian category consists of two classes, T and F, of torsion and torsion-free objects, respectively, such that T is the left orthogonal of F and F is the right orthogonal of T.

• leftOrthogonal_eq : F.leftOrthogonal = T
• rightOrthogonal_eq : T.rightOrthogonal = F

class CategoryTheory.Abelian.IsTorsionClass {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (P : ObjectProperty C) : Prop

A property of objects P is a torsion class if P is the left orthogonal of its right orthogonal, i.e. P.rightOrthogonal.leftOrthogonal = P. Equivalently, P is the torsion class of some torsion theory, namely TorsionTheory P P.rightOrthogonal; see IsTorsionClass.torsionTheory.

This is a typeclass, on the model of Functor.IsLeftAdjoint: every construction of a torsion theory registers an instance for its torsion class, and the closure properties of torsion classes are then available by instance search. See IsTorsionClass.torsionTheory for the torsion theory itself.

• leftOrthogonal_rightOrthogonal_eq : P.rightOrthogonal.leftOrthogonal = P

theorem CategoryTheory.Abelian.isTorsionClass_iff {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (P : ObjectProperty C) : IsTorsionClass P ↔ autoParam (P.rightOrthogonal.leftOrthogonal = P) IsTorsionClass.leftOrthogonal_rightOrthogonal_eq._autoParam

class CategoryTheory.Abelian.IsTorsionFreeClass {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (P : ObjectProperty C) : Prop

A property of objects P is a torsion-free class if P is the right orthogonal of its left orthogonal, i.e. P.leftOrthogonal.rightOrthogonal = P. Equivalently, P is the torsion-free class of some torsion theory, namely TorsionTheory P.leftOrthogonal P; see IsTorsionFreeClass.torsionTheory. This is a typeclass; see IsTorsionClass for the design.

• rightOrthogonal_leftOrthogonal_eq : P.leftOrthogonal.rightOrthogonal = P

theorem CategoryTheory.Abelian.isTorsionFreeClass_iff {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (P : ObjectProperty C) : IsTorsionFreeClass P ↔ autoParam (P.leftOrthogonal.rightOrthogonal = P) IsTorsionFreeClass.rightOrthogonal_leftOrthogonal_eq._autoParam

theorem CategoryTheory.Abelian.TorsionTheory.torsion_iff {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {T F : ObjectProperty C} (hTF : TorsionTheory T F) (X : C) : T X ↔ ∀ ⦃Y : C⦄ (f : X ⟶ Y), F Y → f = 0

An object of a torsion theory is torsion iff every morphism from it to a torsion-free object vanishes.

theorem CategoryTheory.Abelian.TorsionTheory.torsionFree_iff {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {T F : ObjectProperty C} (hTF : TorsionTheory T F) (Y : C) : F Y ↔ ∀ ⦃X : C⦄ (f : X ⟶ Y), T X → f = 0

An object of a torsion theory is torsion-free iff every morphism to it from a torsion object vanishes.

theorem CategoryTheory.Abelian.TorsionTheory.generated_by {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (P : ObjectProperty C) : TorsionTheory P.rightOrthogonal.leftOrthogonal P.rightOrthogonal

The torsion theory generated by a property of objects P: the torsion-free class is the right orthogonal of P, and the torsion class is the left orthogonal of that.

theorem CategoryTheory.Abelian.TorsionTheory.cogenerated_by {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (P : ObjectProperty C) : TorsionTheory P.leftOrthogonal P.leftOrthogonal.rightOrthogonal

The torsion theory cogenerated by a property of objects P: the torsion class is the left orthogonal of P, and the torsion-free class is the right orthogonal of that.

theorem CategoryTheory.Abelian.TorsionTheory.op {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {T F : ObjectProperty C} (hTF : TorsionTheory T F) : TorsionTheory F.op T.op

A torsion theory on C induces a torsion theory on Cᵒᵖ with the roles of the torsion and torsion-free classes exchanged.

theorem CategoryTheory.Abelian.TorsionTheory.unop {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {T F : ObjectProperty Cᵒᵖ} (hTF : TorsionTheory T F) : TorsionTheory F.unop T.unop

A torsion theory on Cᵒᵖ induces a torsion theory on C with the roles of the torsion and torsion-free classes exchanged.

theorem CategoryTheory.Abelian.TorsionTheory.isTorsionClass {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {T F : ObjectProperty C} (hTF : TorsionTheory T F) : IsTorsionClass T

A torsion theory exhibits its torsion class as a torsion class.

theorem CategoryTheory.Abelian.TorsionTheory.isTorsionFreeClass {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {T F : ObjectProperty C} (hTF : TorsionTheory T F) : IsTorsionFreeClass F

A torsion theory exhibits its torsion-free class as a torsion-free class.

instance CategoryTheory.Abelian.instIsTorsionClassLeftOrthogonal {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (P : ObjectProperty C) : IsTorsionClass P.leftOrthogonal

A left orthogonal is the torsion class of the torsion theory it cogenerates.

instance CategoryTheory.Abelian.instIsTorsionFreeClassRightOrthogonal {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (P : ObjectProperty C) : IsTorsionFreeClass P.rightOrthogonal

A right orthogonal is the torsion-free class of the torsion theory it generates.

theorem CategoryTheory.Abelian.IsTorsionClass.torsionTheory {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (P : ObjectProperty C) [IsTorsionClass P] : TorsionTheory P P.rightOrthogonal

The torsion theory whose torsion class is P; its torsion-free class is necessarily P.rightOrthogonal.

instance CategoryTheory.Abelian.IsTorsionClass.instIsClosedUnderQuotients {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (P : ObjectProperty C) [IsTorsionClass P] : P.IsClosedUnderQuotients

A torsion class is closed under quotients.

instance CategoryTheory.Abelian.IsTorsionClass.instIsClosedUnderExtensions {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (P : ObjectProperty C) [IsTorsionClass P] : P.IsClosedUnderExtensions

A torsion class is closed under extensions.

instance CategoryTheory.Abelian.IsTorsionClass.instIsClosedUnderColimitsOfShape {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (P : ObjectProperty C) [IsTorsionClass P] {J : Type u_2} [Category.{v_2, u_2} J] : P.IsClosedUnderColimitsOfShape J

A torsion class is closed under colimits of any shape.

instance CategoryTheory.Abelian.IsTorsionClass.instIsTorsionFreeClassOppositeOp {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (P : ObjectProperty C) [IsTorsionClass P] : IsTorsionFreeClass P.op

The opposite of a torsion class is a torsion-free class.

instance CategoryTheory.Abelian.IsTorsionClass.instIsTorsionFreeClassUnopOfOpposite {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {Q : ObjectProperty Cᵒᵖ} [IsTorsionClass Q] : IsTorsionFreeClass Q.unop

The unopposite of a torsion class in Cᵒᵖ is a torsion-free class in C.

theorem CategoryTheory.Abelian.IsTorsionFreeClass.torsionTheory {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (P : ObjectProperty C) [IsTorsionFreeClass P] : TorsionTheory P.leftOrthogonal P

The torsion theory whose torsion-free class is P; its torsion class is necessarily P.leftOrthogonal.

instance CategoryTheory.Abelian.IsTorsionFreeClass.instIsClosedUnderSubobjects {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (P : ObjectProperty C) [IsTorsionFreeClass P] : P.IsClosedUnderSubobjects

A torsion-free class is closed under subobjects.

instance CategoryTheory.Abelian.IsTorsionFreeClass.instIsClosedUnderExtensions {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (P : ObjectProperty C) [IsTorsionFreeClass P] : P.IsClosedUnderExtensions

A torsion-free class is closed under extensions.

instance CategoryTheory.Abelian.IsTorsionFreeClass.instIsClosedUnderLimitsOfShape {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (P : ObjectProperty C) [IsTorsionFreeClass P] {J : Type u_2} [Category.{v_2, u_2} J] : P.IsClosedUnderLimitsOfShape J

A torsion-free class is closed under limits of any shape.

instance CategoryTheory.Abelian.IsTorsionFreeClass.instIsTorsionClassOppositeOp {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (P : ObjectProperty C) [IsTorsionFreeClass P] : IsTorsionClass P.op

The opposite of a torsion-free class is a torsion class.

instance CategoryTheory.Abelian.IsTorsionFreeClass.instIsTorsionClassUnopOfOpposite {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {Q : ObjectProperty Cᵒᵖ} [IsTorsionFreeClass Q] : IsTorsionClass Q.unop

The unopposite of a torsion-free class is a torsion class.

theorem CategoryTheory.Abelian.isTorsionClass_iff_of_wellPowered {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (P : ObjectProperty C) [LocallySmall.{w, v_1, u_1} C] [WellPowered.{w, v_1, u_1} C] [Limits.HasCoproducts C] : IsTorsionClass P ↔ P.IsClosedUnderQuotients ∧ P.IsClosedUnderExtensions ∧ ∀ (J : Type w), P.IsClosedUnderColimitsOfShape (Discrete J)

In a well-powered abelian category with coproducts, a property of objects P is a torsion class if and only if it is closed under quotients, extensions, and coproducts. This is a theorem of S. E. Dickson; see also Bo Stenström, Rings of Quotients, Chapter VI.

theorem CategoryTheory.Abelian.isTorsionFreeClass_iff_isTorsionClass_op {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (P : ObjectProperty C) : IsTorsionFreeClass P ↔ IsTorsionClass P.op

A property of objects is a torsion-free class if and only if its opposite is a torsion class in the opposite category.

theorem CategoryTheory.Abelian.isTorsionClass_iff_isTorsionFreeClass_op {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (P : ObjectProperty C) : IsTorsionClass P ↔ IsTorsionFreeClass P.op

A property of objects is a torsion class if and only if its opposite is a torsion-free class in the opposite category.

theorem CategoryTheory.Abelian.isTorsionFreeClass_iff_of_wellPowered {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (P : ObjectProperty C) [LocallySmall.{w, v_1, u_1} C] [WellPowered.{w, v_1, u_1} Cᵒᵖ] [Limits.HasProducts C] : IsTorsionFreeClass P ↔ P.IsClosedUnderSubobjects ∧ P.IsClosedUnderExtensions ∧ ∀ (J : Type w), P.IsClosedUnderLimitsOfShape (Discrete J)

In a well-copowered abelian category with products, a property of objects P is a torsion-free class if and only if it is closed under subobjects, extensions, and products. This is the dual of isTorsionClass_iff, obtained by transporting it through the opposite category.