Stability functions on weak HN tilts from generator positivity

An HRS-tilted heart is generated under extensions by the HN-torsion objects and the shifts of HN-free objects. Consequently, an additive ambient charge is a strict stability function on the tilt as soon as it lies in the semi-closed upper half-plane on every nonzero generator of those two kinds.

This assembly is independent of how generator positivity is proved. In particular, Mukai-square and support-dimension arguments belong in a Mukai consumer, not in this generic weak-tilting module.

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.mem_semiClosedUpperHalfPlane_of_mem_hnTilt_heart {C : Type u} [Category.{u_1, u} 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) (Z : K₀ C →+ ℂ) (hTors : ∀ (T₀ : t.heart.FullSubcategory), ¬Limits.IsZero T₀ → T₀ ∈ W.hnTors μ₀ → Z (K₀.of C T₀.obj) ∈ semiClosedUpperHalfPlane) (hFree : ∀ (F₀ : t.heart.FullSubcategory), ¬Limits.IsZero F₀ → F₀ ∈ W.hnFree μ₀ → Z (K₀.of C ((shiftFunctor C 1).obj F₀.obj)) ∈ semiClosedUpperHalfPlane) {X : C} (hX : (W.hnTilt μ₀ hHN).heart X) (hX0 : ¬Limits.IsZero X) : Z (K₀.of C X) ∈ semiClosedUpperHalfPlane

An additive ambient charge is positive on a nonzero object of the HN tilt when it is positive on every nonzero torsion generator and shifted free generator.

def CategoryTheory.Triangulated.WeakStabilityFunctionOn.hnTiltStabilityFunction {C : Type u} [Category.{u_1, u} 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) (Z : K₀ C →+ ℂ) (hTors : ∀ (T₀ : t.heart.FullSubcategory), ¬Limits.IsZero T₀ → T₀ ∈ W.hnTors μ₀ → Z (K₀.of C T₀.obj) ∈ semiClosedUpperHalfPlane) (hFree : ∀ (F₀ : t.heart.FullSubcategory), ¬Limits.IsZero F₀ → F₀ ∈ W.hnFree μ₀ → Z (K₀.of C ((shiftFunctor C 1).obj F₀.obj)) ∈ semiClosedUpperHalfPlane) : WeakStabilityCondition.StabilityFunction (W.hnTilt μ₀ hHN)

Build a strict stability function on the HN-tilted heart from positivity on its two kinds of nonzero generators.

Equations

• W.hnTiltStabilityFunction μ₀ hHN Z hTors hFree = { Z := Z, nonzero_mem := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.hnTiltStabilityFunction_Z {C : Type u} [Category.{u_1, u} 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) (Z : K₀ C →+ ℂ) (hTors : ∀ (T₀ : t.heart.FullSubcategory), ¬Limits.IsZero T₀ → T₀ ∈ W.hnTors μ₀ → Z (K₀.of C T₀.obj) ∈ semiClosedUpperHalfPlane) (hFree : ∀ (F₀ : t.heart.FullSubcategory), ¬Limits.IsZero F₀ → F₀ ∈ W.hnFree μ₀ → Z (K₀.of C ((shiftFunctor C 1).obj F₀.obj)) ∈ semiClosedUpperHalfPlane) : (W.hnTiltStabilityFunction μ₀ hHN Z hTors hFree).Z = Z