The torsion pair of an abelian stability function at a phase cutoff

For a stability function Z on an abelian category with the Harder–Narasimhan property, and a number β, the two classes of Abelian/Stability/Cutoff.lean

T β = {E | every HN phase of E exceeds β}      F β = {E | every HN phase is at most β}

are a TorsionPair. Both axioms are already proved:

• hom_eq_zero is hom_eq_zero_of_mem_hnTors_of_mem_hnFree — the image of a map is a quotient of the source and a subobject of the target, so the monotonicity of PhaseMonotone.lean traps its phases in the empty interval (β, β];
• exists_shortExact is exists_shortExact_hnTors_hnFree — the HN chain cut at the index where its phases cross β.

Relation to the slicing torsion pair

TorsionPair/Slope.lean builds the same display (14.1) pair on the heart of a slicing in a triangulated category, from the slicing's own phase-ordered vanishing. This file is the abelian statement, for an object-level stability function and its own HN filtrations, which is the form Bridgeland's §6 uses on Coh X: with the charge -degree + i·rank of Slope.lean, T β and F β are the μ-slope classes {μ⁻ > β} and {μ⁺ ≤ β}. Neither pair is derived from the other here.

def CategoryTheory.Triangulated.StabilityFunction.hnTorsProperty {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (β : ℝ) : ObjectProperty A

The torsion class at a cutoff, as an ObjectProperty.

Equations

• Z.hnTorsProperty β E = (E ∈ Z.hnTors β)

def CategoryTheory.Triangulated.StabilityFunction.hnFreeProperty {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (β : ℝ) : ObjectProperty A

The torsion-free class at a cutoff, as an ObjectProperty.

Equations

• Z.hnFreeProperty β E = (E ∈ Z.hnFree β)

instance CategoryTheory.Triangulated.StabilityFunction.hnTorsProperty_isClosedUnderIsomorphisms {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (β : ℝ) : (Z.hnTorsProperty β).IsClosedUnderIsomorphisms

instance CategoryTheory.Triangulated.StabilityFunction.hnFreeProperty_isClosedUnderIsomorphisms {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (β : ℝ) : (Z.hnFreeProperty β).IsClosedUnderIsomorphisms

def CategoryTheory.Triangulated.StabilityFunction.hnTorsionPair {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (β : ℝ) (hHN : Z.HasHNProperty) : Tilting.TorsionPair A

The two classes at a phase cutoff are a torsion pair.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.StabilityFunction.hnTorsionPair_tors {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (β : ℝ) (hHN : Z.HasHNProperty) : (Z.hnTorsionPair β hHN).tors = Z.hnTorsProperty β

@[simp]

theorem CategoryTheory.Triangulated.StabilityFunction.hnTorsionPair_free {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (β : ℝ) (hHN : Z.HasHNProperty) : (Z.hnTorsionPair β hHN).free = Z.hnFreeProperty β