From an abelian torsion pair on the heart to the HRS input

TorsionPair/Basic.lean states a torsion pair inside an abelian category; TorsionPair/Heart.lean states one on the heart of a t-structure from inside the ambient triangulated category, and tilts it. Their docstrings say that neither is derived from the other. This file derives the second from the first:

TorsionPair t.heart.FullSubcategory  →  HeartTorsionPair t  →  (tilt) TStructure C

Nothing here is new mathematics. Both halves already exist and are proved generically in t:

• TStructure.heartFullSubcategoryAbelian makes the heart abelian, so a TorsionPair on it can even be stated;
• TStructure.heartFullSubcategory_shortExact_triangle turns a short exact sequence in the heart into a distinguished triangle in C, which is exactly the difference between the two decomposition axioms.

What was missing is the transport of the two classes, which is ambientProperty: a property of heart objects read as a property of ambient objects that happen to lie in the heart.

The payoff

StabilityFunction.hnHeartTorsionPair composes this with hnTorsionPair of TorsionPair/StabilityFunction.lean. A stability function on the heart with the Harder–Narasimhan property and a number β therefore produce, with no further input, a t-structure on C — its tilt. That is the shape of Bridgeland's A(β,ω).

def CategoryTheory.Triangulated.Tilting.ambientProperty {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (P : ObjectProperty t.heart.FullSubcategory) : ObjectProperty C

A property of heart objects, read as a property of ambient objects.

Equations

• CategoryTheory.Triangulated.Tilting.ambientProperty t P X = ∃ (h : t.heart X), P { obj := X, property := h }

theorem CategoryTheory.Triangulated.Tilting.ambientProperty_of_obj {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {P : ObjectProperty t.heart.FullSubcategory} {X : t.heart.FullSubcategory} (hX : P X) : ambientProperty t P X.obj

theorem CategoryTheory.Triangulated.Tilting.heart_of_ambientProperty {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {P : ObjectProperty t.heart.FullSubcategory} {X : C} (hX : ambientProperty t P X) : t.heart X

theorem CategoryTheory.Triangulated.Tilting.isLE_of_ambientProperty {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {P : ObjectProperty t.heart.FullSubcategory} {X : C} (hX : ambientProperty t P X) : t.IsLE X 0

theorem CategoryTheory.Triangulated.Tilting.isGE_of_ambientProperty {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} {P : ObjectProperty t.heart.FullSubcategory} {X : C} (hX : ambientProperty t P X) : t.IsGE X 0

instance CategoryTheory.Triangulated.Tilting.ambientProperty_isClosedUnderIsomorphisms {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} (P : ObjectProperty t.heart.FullSubcategory) [P.IsClosedUnderIsomorphisms] : (ambientProperty t P).IsClosedUnderIsomorphisms

def CategoryTheory.Triangulated.Tilting.HeartTorsionPair.ofTorsionPair {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (P : TorsionPair t.heart.FullSubcategory) : HeartTorsionPair t

A torsion pair on the heart is a HeartTorsionPair. The classes are carried out to C by ambientProperty, and the short exact sequence becomes a distinguished triangle by heartFullSubcategory_shortExact_triangle.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.Tilting.HeartTorsionPair.ofTorsionPair_tors {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (P : TorsionPair t.heart.FullSubcategory) : (ofTorsionPair P).tors = ambientProperty t P.tors

@[simp]

theorem CategoryTheory.Triangulated.Tilting.HeartTorsionPair.ofTorsionPair_free {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (P : TorsionPair t.heart.FullSubcategory) : (ofTorsionPair P).free = ambientProperty t P.free

noncomputable def CategoryTheory.Triangulated.StabilityFunction.hnHeartTorsionPair {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (Z : StabilityFunction t.heart.FullSubcategory) (β : ℝ) (hHN : Z.HasHNProperty) : Tilting.HeartTorsionPair t

A stability function on the heart tilts. Its two classes at a phase cutoff are a torsion pair, hence a HeartTorsionPair, hence — through HeartTorsionPair.tilt — a t-structure on C.

Equations

• Z.hnHeartTorsionPair β hHN = CategoryTheory.Triangulated.Tilting.HeartTorsionPair.ofTorsionPair (Z.hnTorsionPair β hHN)

@[simp]

theorem CategoryTheory.Triangulated.StabilityFunction.hnHeartTorsionPair_tors {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (Z : StabilityFunction t.heart.FullSubcategory) (β : ℝ) (hHN : Z.HasHNProperty) : (Z.hnHeartTorsionPair β hHN).tors = Tilting.ambientProperty t (Z.hnTorsProperty β)

@[simp]

theorem CategoryTheory.Triangulated.StabilityFunction.hnHeartTorsionPair_free {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (Z : StabilityFunction t.heart.FullSubcategory) (β : ℝ) (hHN : Z.HasHNProperty) : (Z.hnHeartTorsionPair β hHN).free = Tilting.ambientProperty t (Z.hnFreeProperty β)

noncomputable def CategoryTheory.Triangulated.StabilityFunction.hnTilt {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (Z : StabilityFunction t.heart.FullSubcategory) (β : ℝ) (hHN : Z.HasHNProperty) : TStructure C

The tilt of a stability function at a cutoff, as a t-structure on the ambient category. This is the whole chain in one declaration: HN filtrations cut at β, the resulting torsion pair, and Happel–Reiten–Smalø.

Equations

• Z.hnTilt β hHN = (Z.hnHeartTorsionPair β hHN).tilt