Bridgeland Stability Conditions

14.17. Deformation: PhiPlusHN🔗

14.17.1. wPhaseOf_lt_of_phiPlus_lt🔗

W-phase upper bound from \varphi^+ bound. If E \in \mathcal{P}((a, b)) with \varphi^+(E) < b - 4\varepsilon and the interval is wide enough (6\varepsilon \le b - a), then \psi(E) < b - 3\varepsilon. This key estimate propagates through the HN recursion.

Proof: From \varphi^+(E) < b - 4\varepsilon and \varphi^-(E) > a, deduce E \in \mathcal{P}((a, b - 4\varepsilon)). Apply wPhaseOf_lt_of_intervalProp with the narrower interval (a, b - 4\varepsilon) and perturbation \varepsilon. The condition (a+b)/2 \le (b-4\varepsilon) + \varepsilon = b - 3\varepsilon follows from 6\varepsilon \le b - a.

🔗theorem
CategoryTheory.Triangulated.wPhaseOf_lt_of_phiPlus_lt.{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) {ε : ℝ} (hε : 0 < ε) (hε2 : ε < 1 / 4)
  (hthin : b - a + 2 * ε < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε)))
  (h_wide : 6 * ε ≤ b - a) {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b E)
  (hphiPlus :
    CategoryTheory.Triangulated.Slicing.phiPlus C σ.slicing E hE <
      b - 4 * ε) :
  CategoryTheory.Triangulated.wPhaseOf
      ((CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
            C σ W hW hab).W
        (CategoryTheory.Triangulated.cl C v E))
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
          C σ W hW hab).α <
    b - 3 * ε
CategoryTheory.Triangulated.wPhaseOf_lt_of_phiPlus_lt.{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) {ε : ℝ}
  (hε : 0 < ε) (hε2 : ε < 1 / 4)
  (hthin : b - a + 2 * ε < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε)))
  (h_wide : 6 * ε ≤ b - a) {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing a b E)
  (hphiPlus :
    CategoryTheory.Triangulated.Slicing.phiPlus
        C σ.slicing E hE <
      b - 4 * ε) :
  CategoryTheory.Triangulated.wPhaseOf
      ((CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
            C σ W hW hab).W
        (CategoryTheory.Triangulated.cl C
          v E))
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
          C σ W hW hab).α <
    b - 3 * ε

Something wrong, better idea? Suggest a change

14.17.2. hn_exists_with_phiPlus_reduction🔗

HN existence with \varphi^+ reduction (Bridgeland p.23--24). Drops both hHom and hDestabBound from the older HN existence theorem. Instead takes perturbation data and a quotient lower bound t \ge a + \varepsilon. At each step: (1) call exists_strictMDQ_with_quotient_bound, (2) extract the kernel and lift to a smaller strict subobject, (3) recurse with the MDQ phase as new lower bound. The \varphi^+ invariant (\varphi^+(Y) < b - 4\varepsilon) is propagated through kernels via phiPlus_triangle_le.

Proof: Well-founded induction on the strict-subobject poset. Semistable case: single-factor filtration. Non-semistable case: derive \psi(Y) < b - 3\varepsilon from \varphi^+(Y) < b - 4\varepsilon via wPhaseOf_lt_of_phiPlus_lt. Call exists_strictMDQ_with_quotient_bound (which handles Hom vanishing and destabilizing bounds internally). Extract kernel K, lift to T < S, propagate \varphi^+(K) \le \varphi^+(Y) < b - 4\varepsilon via phiPlus_triangle_le, then recurse on T.

🔗theorem
CategoryTheory.Triangulated.hn_exists_with_phiPlus_reduction.{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ε2 : ε < 1 / 4) (hε8 : ε < 1 / 8)
  (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)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F →
          (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
                  C σ W hW hab).W
              (CategoryTheory.Triangulated.cl C v F) ≠
            0)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F →
          L <
              CategoryTheory.Triangulated.wPhaseOf
                ((CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
                      C σ W hW hab).W
                  (CategoryTheory.Triangulated.cl C v F))
                (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
                    C σ W hW hab).α ∧
            CategoryTheory.Triangulated.wPhaseOf
                ((CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
                      C σ W hW hab).W
                  (CategoryTheory.Triangulated.cl C v F))
                (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
                    C σ W hW hab).α <
              U)
  (hWidth : U - L < 1) (t : ℝ) (ht : a + ε ≤ t)
  (X : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b)
  (hX : ¬CategoryTheory.Limits.IsZero X)
  (hquot :
    ∀
      {B :
        CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
      (q : X ⟶ B),
      CategoryTheory.IsStrictEpi q →
        ¬CategoryTheory.Limits.IsZero B.obj →
          t <
            CategoryTheory.Triangulated.wPhaseOf
              ((CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
                    C σ W hW hab).W
                (CategoryTheory.Triangulated.cl C v B.obj))
              (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
                  C σ W hW hab).α)
  (hL_a : a ≤ L + ε) (h_wide : 6 * ε ≤ b - a)
  (hphiPlus_X :
    ∀ (hXne : ¬CategoryTheory.Limits.IsZero X.obj),
      CategoryTheory.Triangulated.Slicing.phiPlus C σ.slicing X.obj
          hXne <
        b - 4 * ε) :
  have ssf :=
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
      C σ W hW hab;
  have Psem := fun ψ F =>
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf
      F ψ;
  ∃ G, ∀ (j : Fin G.n), t < G.φ j ∧ G.φ j < U
CategoryTheory.Triangulated.hn_exists_with_phiPlus_reduction.{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ε2 : ε < 1 / 4) (hε8 : ε < 1 / 8)
  (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)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
                  C σ W hW hab).W
              (CategoryTheory.Triangulated.cl
                C v F) ≠
            0)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          L <
              CategoryTheory.Triangulated.wPhaseOf
                ((CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
                      C σ W hW hab).W
                  (CategoryTheory.Triangulated.cl
                    C v F))
                (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
                    C σ W hW hab).α ∧
            CategoryTheory.Triangulated.wPhaseOf
                ((CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
                      C σ W hW hab).W
                  (CategoryTheory.Triangulated.cl
                    C v F))
                (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
                    C σ W hW hab).α <
              U)
  (hWidth : U - L < 1) (t : ℝ)
  (ht : a + ε ≤ t)
  (X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b)
  (hX : ¬CategoryTheory.Limits.IsZero X)
  (hquot :
    ∀
      {B :
        CategoryTheory.Triangulated.Slicing.IntervalCat
          C σ.slicing a b}
      (q : X ⟶ B),
      CategoryTheory.IsStrictEpi q →
        ¬CategoryTheory.Limits.IsZero
              B.obj →
          t <
            CategoryTheory.Triangulated.wPhaseOf
              ((CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
                    C σ W hW hab).W
                (CategoryTheory.Triangulated.cl
                  C v B.obj))
              (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
                  C σ W hW hab).α)
  (hL_a : a ≤ L + ε)
  (h_wide : 6 * ε ≤ b - a)
  (hphiPlus_X :
    ∀
      (hXne :
        ¬CategoryTheory.Limits.IsZero
            X.obj),
      CategoryTheory.Triangulated.Slicing.phiPlus
          C σ.slicing X.obj hXne <
        b - 4 * ε) :
  have ssf :=
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
      C σ W hW hab;
  have Psem := fun ψ F =>
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C ssf F ψ;
  ∃ G,
    ∀ (j : Fin G.n), t < G.φ j ∧ G.φ j < U

  1. Call exists_strictMDQ_with_quotient_bound (which handles hHom and hDestabBound internally)

  2. Extract kernel, lift to smaller strict subobject

  3. Recurse with the MDQ phase as new lower bound

Something wrong, better idea? Suggest a change