The tilt of a weak stability function at a slope cutoff #

TorsionPair/WeakStabilityFunction.lean produces hnTorsionPair, the torsion pair cut out of an abelian category by a slope μ₀ : WithTop ℝ. This file feeds it through the Happel–Reiten–Smalø machinery that HeartAdapter.lean and HnTiltHeart.lean already set up for the strict case, and describes the resulting heart.

Nothing here is new mathematics. Every declaration is one composition, exactly as in the strict HeartAdapter.lean / HnTiltHeart.lean pair. The chain

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

is generic in the torsion pair, so once the weak pair exists — which is what took the work, and what needed the charge-free subobject correspondence behind it — the tilt is immediate.

The one difference that matters #

The strict hnTilt cuts by a phase β : ℝ. This one cuts by a slope in WithTop ℝ, and that is not cosmetic: on a surface a skyscraper has charge 0 and no phase at all, so no phase cutoff can place it, while every finite slope cutoff puts it in T μ₀ (WeakSlopeData.mem_hnTors_of_rank_zero). The tilted heart here therefore contains the objects that the strict construction cannot even speak about, which is the entire reason the weak lane exists.

Both are at abelianDatum of the heart, so they are strictly parallel: the strict StabilityFunction t.heart.FullSubcategory is StabilityFunctionOn (abelianDatum …), and this is WeakStabilityFunctionOn at the same datum. Neither is at heartDatum t, whose classes live in the ambient K₀ C.

What this is still not #

It is not Bridgeland's Lemma 6.2. This says what the tilted heart is; Lemma 6.2 says that Z(β,ω) is a stability function on it, which is the four-case positivity argument and needs the real part as well as the imaginary one. StabilityCondition/Mukai/Slope.lean supplies the imaginary half against the untilted classes; nothing here closes the gap.

source

noncomputable def CategoryTheory.Triangulated.WeakStabilityFunctionOn.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} (W : WeakStabilityFunctionOn (abelianDatum t.heart.FullSubcategory)) (μ₀ : WithTop ℝ) (hHN : W.HasHNProperty) :

Tilting.HeartTorsionPair t

The weak cutoff pair, transported to the heart-torsion-pair form Happel–Reiten–Smalø consumes.

Equations

W.hnHeartTorsionPair μ₀ hHN = CategoryTheory.Triangulated.Tilting.HeartTorsionPair.ofTorsionPair (W.hnTorsionPair μ₀ hHN)

Instances For

source

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.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} (W : WeakStabilityFunctionOn (abelianDatum t.heart.FullSubcategory)) (μ₀ : WithTop ℝ) (hHN : W.HasHNProperty) :

(W.hnHeartTorsionPair μ₀ hHN).tors = Tilting.ambientProperty t (W.hnTorsProperty μ₀)

source

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.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} (W : WeakStabilityFunctionOn (abelianDatum t.heart.FullSubcategory)) (μ₀ : WithTop ℝ) (hHN : W.HasHNProperty) :

(W.hnHeartTorsionPair μ₀ hHN).free = Tilting.ambientProperty t (W.hnFreeProperty μ₀)

source

noncomputable def CategoryTheory.Triangulated.WeakStabilityFunctionOn.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} (W : WeakStabilityFunctionOn (abelianDatum t.heart.FullSubcategory)) (μ₀ : WithTop ℝ) (hHN : W.HasHNProperty) :

TStructure C

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

Equations