The two classes at a phase cutoff

Bridgeland's torsion pair is cut from Coh X by a slope, and #709 turned the slope order into the phase order, so the cut is by a phase. This file defines the two classes and proves what follows from the Harder–Narasimhan machinery already in Uniqueness/:

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

• mem_hnTors_iff_forall, mem_hnFree_iff_forall — the classes are well defined: φ⁻ and φ⁺ are intrinsic (phiMinus_eq, phiPlus_eq), so "some filtration" and "every filtration" agree. The HN property is a hypothesis of these two and of nothing else: without a filtration to exhibit, the universally quantified form is vacuous while membership asks for a witness.
• isZero_of_mem_hnTors_of_mem_hnFree — the two classes meet only in zero, which is φ⁻ ≤ φ⁺ and nothing else.
• hom_eq_zero_of_mem_hnTors_of_semistable — the Hom-vanishing, for a semistable target.
• hom_eq_zero_of_mem_hnTors_of_mem_hnFree — the Hom-vanishing, for a general target. The image of a map is a quotient of the source and a subobject of the target, so the monotonicity of PhaseMonotone.lean traps it: β < φ⁻(image) ≤ φ⁺(image) ≤ β, which leaves the image zero.

What is deliberately not here

One step still stands between this and a torsion pair, and it is not implied by anything below.

• The splitting. Every object sitting in a short exact sequence with a torsion sub and a torsion-free quotient, obtained by cutting the HN chain at the crossing index. Uniqueness/Tail.lean removes one factor at a time and is the machinery this would induct over.

Until it exists, these are two classes with a Hom-vanishing property, not a torsion pair, and nothing here calls them one.

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

The torsion class at a cutoff: the zero object, and the objects whose Harder–Narasimhan phases all exceed β.

Equations

• Z.hnTors β = {E : A | CategoryTheory.Limits.IsZero E ∨ ∃ (F : CategoryTheory.Triangulated.AbelianHNFiltration Z E), β < F.phiMinus}

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

The torsion-free class at a cutoff: the zero object, and the objects whose Harder–Narasimhan phases are all at most β.

Equations

• Z.hnFree β = {E : A | CategoryTheory.Limits.IsZero E ∨ ∃ (F : CategoryTheory.Triangulated.AbelianHNFiltration Z E), F.phiPlus ≤ β}

theorem CategoryTheory.Triangulated.StabilityFunction.isZero_mem_hnTors {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {β : ℝ} {E : A} (hE : Limits.IsZero E) : E ∈ Z.hnTors β

theorem CategoryTheory.Triangulated.StabilityFunction.isZero_mem_hnFree {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {β : ℝ} {E : A} (hE : Limits.IsZero E) : E ∈ Z.hnFree β

theorem CategoryTheory.Triangulated.StabilityFunction.mem_hnTors_iff_forall {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {β : ℝ} (hHN : Z.HasHNProperty) {E : A} (hE : ¬Limits.IsZero E) : E ∈ Z.hnTors β ↔ ∀ (F : AbelianHNFiltration Z E), β < F.phiMinus

Membership is independent of the filtration chosen, because φ⁻ is.

The HN property is needed for the reverse direction only: without a filtration to exhibit, the universally quantified condition is vacuous while membership asks for a witness.

theorem CategoryTheory.Triangulated.StabilityFunction.mem_hnFree_iff_forall {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {β : ℝ} (hHN : Z.HasHNProperty) {E : A} (hE : ¬Limits.IsZero E) : E ∈ Z.hnFree β ↔ ∀ (F : AbelianHNFiltration Z E), F.phiPlus ≤ β

Membership is independent of the filtration chosen, because φ⁺ is.

theorem CategoryTheory.Triangulated.StabilityFunction.isZero_of_mem_hnTors_of_mem_hnFree {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {β : ℝ} {E : A} (hT : E ∈ Z.hnTors β) (hF : E ∈ Z.hnFree β) : Limits.IsZero E

The two classes meet only in zero. An object in both would have β < φ⁻ ≤ φ⁺ ≤ β.

theorem CategoryTheory.Triangulated.StabilityFunction.hom_eq_zero_of_mem_hnTors_of_semistable {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {β : ℝ} {E B : A} (hE : ¬Limits.IsZero E) (hT : E ∈ Z.hnTors β) (hB : Z.IsSemistable B) (hphase : Z.phase B ≤ β) (f : E ⟶ B) : f = 0

Hom-vanishing, for a semistable target. A map from an object whose HN phases all exceed β to a semistable object of phase at most β is zero.

theorem CategoryTheory.Triangulated.StabilityFunction.hom_eq_zero_of_mem_hnTors_of_mem_hnFree {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {β : ℝ} (hHN : Z.HasHNProperty) {E B : A} (hT : E ∈ Z.hnTors β) (hFr : B ∈ Z.hnFree β) (f : E ⟶ B) : f = 0

Hom-vanishing. A map from an object whose HN phases all exceed β to an object whose HN phases are all at most β is zero: its image is a quotient of the source and a subobject of the target, so β < φ⁻(image) and φ⁺(image) ≤ β, which phiMinus_le_phiPlus contradicts unless the image is zero.

The HN property is needed for the image, which is neither of the two given objects.