Torsion pairs in an abelian category

A torsion pair on an abelian category A is a pair of full subcategories (T, F), closed under isomorphism, such that

• every map from a torsion object to a torsion-free object is zero, and
• every object sits in a short exact sequence 0 → tX → X → fX → 0 with tX ∈ T and fX ∈ F.

Mathlib does not have this at the pin. Every Torsion file in Mathlib is about torsion in algebra — Algebra/Group/Torsion.lean, GroupTheory/Torsion.lean, RingTheory/Flat/TorsionFree.lean and so on. There is no torsion pair, torsion theory, or torsion class for abelian categories. So this is built from scratch rather than wrapped.

Why this is here

A torsion pair in the heart of a t-structure is the input to Happel–Reiten–Smalø tilting, which is in turn the engine behind every construction of stability conditions on a surface. This file is the input datum and its elementary theory; the tilt itself is a separate, much larger obligation and is not formalised here.

Nothing in this file needs algebraic geometry, a triangulated category, or the rest of StabilityCondition/. It is abelian-category theory and imports only Mathlib.

Main results

• tors_iff / free_iff — each class is exactly the orthogonal of the other. This is the standard rigidity of the definition: the decomposition axiom is what upgrades "mutually orthogonal" to "mutually determining".
• free_of_mono / tors_of_epi — F is closed under subobjects, T under quotients. Both fall straight out of tors_iff/free_iff.
• tors_of_shortExact / free_of_shortExact — both classes are closed under extensions.

structure CategoryTheory.Triangulated.Tilting.TorsionPair (A : Type u_1) [Category.{u_2, u_1} A] [Abelian A] : Type u_1

A torsion pair on an abelian category.

• tors : ObjectProperty A

  the torsion class

• free : ObjectProperty A

  the torsion-free class

• tors_isClosedUnderIsomorphisms : self.tors.IsClosedUnderIsomorphisms
• free_isClosedUnderIsomorphisms : self.free.IsClosedUnderIsomorphisms
• hom_eq_zero ⦃X Y : A⦄ : self.tors X → self.free Y → ∀ (f : X ⟶ Y), f = 0

  no nonzero map from a torsion object to a torsion-free one

• exists_shortExact (X : A) : ∃ (T : A) (F : A) (i : T ⟶ X) (p : X ⟶ F) (w : CategoryStruct.comp i p = 0), self.tors T ∧ self.free F ∧ { X₁ := T, X₂ := X, X₃ := F, f := i, g := p, zero := w }.ShortExact

  every object is an extension of a torsion-free object by a torsion one

theorem CategoryTheory.Triangulated.Tilting.TorsionPair.isZero_of_tors_of_free {A : Type u_1} [Category.{u_2, u_1} A] [Abelian A] (P : TorsionPair A) {X : A} (hT : P.tors X) (hF : P.free X) : Limits.IsZero X

An object that is both torsion and torsion-free is zero.

theorem CategoryTheory.Triangulated.Tilting.TorsionPair.tors_iff {A : Type u_1} [Category.{u_2, u_1} A] [Abelian A] (P : TorsionPair A) (X : A) : P.tors X ↔ ∀ ⦃Y : A⦄, P.free Y → ∀ (f : X ⟶ Y), f = 0

The torsion class is exactly the left orthogonal of the torsion-free class. The decomposition axiom is what makes this an iff rather than the one implication hom_eq_zero states.

theorem CategoryTheory.Triangulated.Tilting.TorsionPair.free_iff {A : Type u_1} [Category.{u_2, u_1} A] [Abelian A] (P : TorsionPair A) (Y : A) : P.free Y ↔ ∀ ⦃X : A⦄, P.tors X → ∀ (f : X ⟶ Y), f = 0

The torsion-free class is exactly the right orthogonal of the torsion class.

theorem CategoryTheory.Triangulated.Tilting.TorsionPair.free_of_mono {A : Type u_1} [Category.{u_2, u_1} A] [Abelian A] (P : TorsionPair A) {X Y : A} (i : X ⟶ Y) [Mono i] (hY : P.free Y) : P.free X

The torsion-free class is closed under subobjects.

theorem CategoryTheory.Triangulated.Tilting.TorsionPair.tors_of_epi {A : Type u_1} [Category.{u_2, u_1} A] [Abelian A] (P : TorsionPair A) {X Y : A} (p : X ⟶ Y) [Epi p] (hX : P.tors X) : P.tors Y

The torsion class is closed under quotients.

theorem CategoryTheory.Triangulated.Tilting.TorsionPair.tors_of_shortExact {A : Type u_1} [Category.{u_2, u_1} A] [Abelian A] (P : TorsionPair A) {S : ShortComplex A} (hS : S.ShortExact) (h₁ : P.tors S.X₁) (h₃ : P.tors S.X₃) : P.tors S.X₂

The torsion class is closed under extensions.

theorem CategoryTheory.Triangulated.Tilting.TorsionPair.free_of_shortExact {A : Type u_1} [Category.{u_2, u_1} A] [Abelian A] (P : TorsionPair A) {S : ShortComplex A} (hS : S.ShortExact) (h₁ : P.free S.X₁) (h₃ : P.free S.X₃) : P.free S.X₂

The torsion-free class is closed under extensions.

Uniqueness of the decomposition

The short exact sequence in exists_shortExact is not extra data: its two ends are determined up to isomorphism by X, because each is characterised by an orthogonality condition the other class cannot satisfy. The statement below is the piece that gets used — the torsion end is the largest torsion subobject.

theorem CategoryTheory.Triangulated.Tilting.TorsionPair.exists_factor_of_tors {A : Type u_1} [Category.{u_2, u_1} A] [Abelian A] (P : TorsionPair A) {S : ShortComplex A} (hS : S.ShortExact) (h₃ : P.free S.X₃) {T : A} (hT : P.tors T) (f : T ⟶ S.X₂) : ∃ (g : T ⟶ S.X₁), CategoryStruct.comp g S.f = f

A torsion subobject of X factors through any torsion/torsion-free decomposition of X: the torsion end is maximal among torsion subobjects.

Non-vacuity

A structure with no inhabitant makes every theorem above vacuously true, so the two degenerate torsion pairs are constructed rather than asserted to exist. They are also the extremes the general theory is bracketed by.

def CategoryTheory.Triangulated.Tilting.TorsionPair.allTors (A : Type u_1) [Category.{u_2, u_1} A] [Abelian A] : TorsionPair A

The torsion pair in which every object is torsion and only the zero objects are torsion-free.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Triangulated.Tilting.TorsionPair.allFree (A : Type u_1) [Category.{u_2, u_1} A] [Abelian A] : TorsionPair A

The torsion pair in which only the zero objects are torsion and every object is torsion-free.

Equations

• One or more equations did not get rendered due to their size.