Bridgeland Stability Conditions

14.7. Deformation: HNExistence🔗

14.7.1. interior_has_enveloped_HN_ssf🔗

Lemma 7.7 interior HN (ssf version, Bridgeland p.23). Every nonzero object E in the interior \mathcal{P}((a + 2\varepsilon, b - 4\varepsilon)) of a thin finite-length interval \mathcal{P}((a,b)) admits an HN filtration whose factors are \operatorname{ssf}-semistable in \mathcal{P}((a,b)) with phases in (a + \varepsilon, b - \varepsilon).

Proof: Part A: Apply the \varphi^+ reduction recursion (hn_exists_with_phiPlus_reduction) to obtain an HN filtration with phases in (a+\varepsilon, U). Part B: Establish a tight upper bound \psi(F_1) < b - 3\varepsilon on the first (largest-phase) factor by backward induction on the Postnikov chain: \varphi^+(\operatorname{chain}(k)) \le \varphi^+(E) < b - 4\varepsilon combined with phase confinement \psi_1 - \varepsilon < \varphi^-(F_1) \le \varphi^+(F_1) gives \psi_1 < b - 3\varepsilon. Since phases are decreasing, all phases are < b - \varepsilon.

🔗theorem
CategoryTheory.Triangulated.interior_has_enveloped_HN_ssf.{v, u, u'}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a b : ℝ} (hab : a < b) [Fact (a < b)] [Fact (b - a ≤ 1)] {ε : ℝ}
  (hε : 0 < ε) (hε10 : ε < 1 / 10) (hthin : b - a + 2 * ε < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε)))
  (hFL : CategoryTheory.Triangulated.ThinFiniteLengthInInterval C σ a b)
  {E : C} (hE : ¬CategoryTheory.Limits.IsZero E)
  (hInt :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing
      (a + 2 * ε) (b - 4 * ε) E) :
  have ssf :=
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
      C σ W hW hab;
  ∃ G, ∀ (j : Fin G.n), a + ε < G.φ j ∧ G.φ j < b - ε
CategoryTheory.Triangulated.interior_has_enveloped_HN_ssf.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a b : ℝ} (hab : a < b) [Fact (a < b)]
  [Fact (b - a ≤ 1)] {ε : ℝ} (hε : 0 < ε)
  (hε10 : ε < 1 / 10)
  (hthin : b - a + 2 * ε < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε)))
  (hFL :
    CategoryTheory.Triangulated.ThinFiniteLengthInInterval
      C σ a b)
  {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hInt :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing (a + 2 * ε) (b - 4 * ε)
      E) :
  have ssf :=
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
      C σ W hW hab;
  ∃ G,
    ∀ (j : Fin G.n),
      a + ε < G.φ j ∧ G.φ j < b - ε

Something wrong, better idea? Suggest a change

14.7.2. interior_has_enveloped_HN🔗

Lemma 7.7 interior HN (deformedPred version). Derives a deformedPred-typed HN filtration from interior_has_enveloped_HN_ssf by wrapping each \operatorname{ssf}-semistable factor with the enveloping interval (a, b) as the deformedPred witness. Phase bounds are (a + \varepsilon, b - \varepsilon) matching the paper.

Proof: Apply interior_has_enveloped_HN_ssf to get an ssf-typed filtration G. Retype each factor: since G.\phi(j) \in (a + \varepsilon, b - \varepsilon), the interval (a, b) with a + \varepsilon \le G.\phi(j) \le b - \varepsilon witnesses \operatorname{deformedPred}.

🔗theorem
CategoryTheory.Triangulated.interior_has_enveloped_HN.{v, u, u'}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a b : ℝ} (hab : a < b) [Fact (a < b)] [Fact (b - a ≤ 1)] {ε : ℝ}
  (hε : 0 < ε) (hε10 : ε < 1 / 10) (hthin : b - a + 2 * ε < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε)))
  (hFL : CategoryTheory.Triangulated.ThinFiniteLengthInInterval C σ a b)
  {E : C} (hE : ¬CategoryTheory.Limits.IsZero E)
  (hInt :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing
      (a + 2 * ε) (b - 4 * ε) E) :
  ∃ G, ∀ (j : Fin G.n), a + ε < G.φ j ∧ G.φ j < b - ε
CategoryTheory.Triangulated.interior_has_enveloped_HN.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a b : ℝ} (hab : a < b) [Fact (a < b)]
  [Fact (b - a ≤ 1)] {ε : ℝ} (hε : 0 < ε)
  (hε10 : ε < 1 / 10)
  (hthin : b - a + 2 * ε < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε)))
  (hFL :
    CategoryTheory.Triangulated.ThinFiniteLengthInInterval
      C σ a b)
  {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hInt :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing (a + 2 * ε) (b - 4 * ε)
      E) :
  ∃ G,
    ∀ (j : Fin G.n),
      a + ε < G.φ j ∧ G.φ j < b - ε

Something wrong, better idea? Suggest a change

14.7.3. sigmaSemistable_hasDeformedHN🔗

\sigma-semistable objects have Q-HN filtrations (Bridgeland p.24). For E \in \mathcal{P}(\phi), embed E in \mathcal{P}((\phi - 3\varepsilon, \phi + 5\varepsilon)) and apply interior_has_enveloped_HN. The Q-HN phases lie in (\phi - 2\varepsilon, \phi + 4\varepsilon). Two parameters: \varepsilon_0 (local finiteness, < 1/10) and \varepsilon (perturbation, \varepsilon < \varepsilon_0). ThinFiniteLengthInInterval is derived from WideSectorFiniteLength via of_wide.

Proof: Set a = \phi - 3\varepsilon, b = \phi + 5\varepsilon. Derive thin finite length from wide-sector finite length. Embed E \in \mathcal{P}(\phi) \subset \mathcal{P}((\phi - \varepsilon, \phi + \varepsilon)) = \mathcal{P}((a + 2\varepsilon, b - 4\varepsilon)). Apply interior_has_enveloped_HN and translate phase bounds.

🔗theorem
CategoryTheory.Triangulated.sigmaSemistable_hasDeformedHN.{v, u, u'}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ : ℝ} (hε₀ : 0 < ε₀) (hε₀10 : ε₀ < 1 / 10)
  (hWide :
    CategoryTheory.Triangulated.WideSectorFiniteLength C σ ε₀ hε₀ ⋯)
  {ε : ℝ} (hε : 0 < ε) (hεε₀ : ε < ε₀)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε)))
  {E : C} {φ : ℝ} (hP : σ.slicing.P φ E)
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  ∃ G, ∀ (j : Fin G.n), φ - 2 * ε < G.φ j ∧ G.φ j < φ + 4 * ε
CategoryTheory.Triangulated.sigmaSemistable_hasDeformedHN.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  [CategoryTheory.IsTriangulated C]
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε₀ : ℝ} (hε₀ : 0 < ε₀)
  (hε₀10 : ε₀ < 1 / 10)
  (hWide :
    CategoryTheory.Triangulated.WideSectorFiniteLength
      C σ ε₀ hε₀ ⋯)
  {ε : ℝ} (hε : 0 < ε) (hεε₀ : ε < ε₀)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε)))
  {E : C} {φ : ℝ} (hP : σ.slicing.P φ E)
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  ∃ G,
    ∀ (j : Fin G.n),
      φ - 2 * ε < G.φ j ∧
        G.φ j < φ + 4 * ε

Something wrong, better idea? Suggest a change