The torsion pair at a phase cutoff (display (14.1))

For a slicing s and a cutoff β ∈ [0, 1], the heart P((0, 1]) of the slicing-induced t-structure carries the torsion pair

T = P((β, 1]),      F = P((0, β]),

constructed here as a HeartTorsionPair on s.toTStructure — so the reviewed Happel–Reiten–Smalø tilt applies to it, and with tilt_heart_iff (#106) its tilted heart is identified with the extensions of P((β, 1]) by P((0, β])⟦1⟧, the single-step form of A^{♯β} = ⟨F^β[1], T^β⟩.

Everything is unconditional: the Hom-vanishing is the slicing's own phase-ordered vanishing (zero_of_gtProp_leProp_general), and the decomposition is the Harder–Narasimhan filtration cut at β (exists_split_at_cutoff), with the two interval bounds that the cut does not hand over recovered by rotating the split triangle into the extension closures of the aisle and co-aisle.

Relation to display (14.1), stated for the reviewer

The paper's (14.1) is written in slope language on the heart of a weak stability condition: T^β = {μ⁻ > β}, F^β = {μ⁺ ≤ β}. This file's pair is the same construction in phase language on the slicing heart. The exact finite-slope reparametrisation and equality of the two pairs are formalized downstream in TorsionPair/SourceSlope.lean. The coverage map remains mapped pending its separate source-review protocol.

def CategoryTheory.Triangulated.WeakStabilityCondition.phaseTors {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (β : ℝ) : ObjectProperty C

The torsion class at cutoff β: objects of P((β, 1]).

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.phaseTors s β E = (CategoryTheory.Triangulated.Slicing.gtProp C s β E ∧ CategoryTheory.Triangulated.Slicing.leProp C s 1 E)

def CategoryTheory.Triangulated.WeakStabilityCondition.phaseFree {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (β : ℝ) : ObjectProperty C

The torsion-free class at cutoff β: objects of P((0, β]).

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.phaseFree s β E = (CategoryTheory.Triangulated.Slicing.gtProp C s 0 E ∧ CategoryTheory.Triangulated.Slicing.leProp C s β E)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.leProp_of_iso {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {t : ℝ} {E E' : C} (e : E ≅ E') (h : Slicing.leProp C s t E) : Slicing.leProp C s t E'

leProp is closed under isomorphisms.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.gtProp_of_iso {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {t : ℝ} {E E' : C} (e : E ≅ E') (h : Slicing.gtProp C s t E) : Slicing.gtProp C s t E'

gtProp is closed under isomorphisms.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.mem_heart_of_bounds {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) {E : C} (h0 : Slicing.gtProp C s 0 E) (h1 : Slicing.leProp C s 1 E) : (Slicing.toTStructure C s).heart E

Heart membership from the two interval bounds, through the slicing heart identification Slicing.toTStructure_heart_iff (WeakStabilityCondition/Foundation/Slicing/PhaseTruncation.lean).

def CategoryTheory.Triangulated.WeakStabilityCondition.slicingTorsionPair {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) {β : ℝ} (h0 : 0 ≤ β) (h1 : β ≤ 1) : Tilting.HeartTorsionPair (Slicing.toTStructure C s)

The torsion pair at a phase cutoff — display (14.1) in phase language: (P((β, 1]), P((0, β])) is a torsion pair on the heart P((0, 1]) of the slicing-induced t-structure.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.slicingTorsionPair_tors {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) {β : ℝ} (h0 : 0 ≤ β) (h1 : β ≤ 1) : (slicingTorsionPair s h0 h1).tors = phaseTors s β

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.slicingTorsionPair_free {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) {β : ℝ} (h0 : 0 ≤ β) (h1 : β ≤ 1) : (slicingTorsionPair s h0 h1).free = phaseFree s β

theorem CategoryTheory.Triangulated.WeakStabilityCondition.slicingTilt_heart_iff {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) {β : ℝ} (h0 : 0 ≤ β) (h1 : β ≤ 1) (X : C) : (slicingTorsionPair s h0 h1).tilt.heart X ↔ ∃ (F₀ : C) (T₀ : C) (_ : phaseFree s β F₀) (_ : phaseTors s β T₀) (f : (shiftFunctor C 1).obj F₀ ⟶ X) (g : X ⟶ T₀) (h : T₀ ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj F₀)), Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles

The tilted heart at the cutoff is ⟨P((0, β])⟦1⟧, P((β, 1])⟩ in the single-step form: an object lies in the heart of the tilt of the slicing heart at β iff it is an extension of a P((β, 1])-object by a shifted P((0, β])-object. Direct from tilt_heart_iff (#106). This is the A^{♯β} of display (14.1), up to the unformalized slope–phase reparametrisation.