14.18. Deformation: PhiPlusMDQ🔗

14.18.1. wPhaseOf_gt_of_narrow_interval🔗

Phase lower bound via Im argument (generalized). If E \in \mathcal{P}((c, d)) and every \sigma-semistable factor of phase \phi \in (c, d) has W-phase strictly between \psi and \psi + 1, then \operatorname{wPhaseOf}(W(E), \alpha) > \psi. Replaces the older h\alpha\_ge condition with a direct width bound.

Proof: The imaginary part of W(E) \cdot e^{-i\pi\psi} is positive: each \sigma-semistable factor contributes a positive imaginary part (from the phase gap hypothesis), and positivity is additive over the HN filtration. If \operatorname{wPhaseOf}(W(E), \alpha) \le \psi, then \sin(\pi(\theta - \psi)) \le 0, contradicting positivity of the imaginary part.

theorem

CategoryTheory.Triangulated.wPhaseOf_gt_of_narrow_interval.{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] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {E : C} (hE : ¬CategoryTheory.Limits.IsZero E) (W : Λ →+ ℂ)
  {α ψ c d : ℝ}
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing c d E)
  (hE_width :
    ψ - 1 <
      CategoryTheory.Triangulated.wPhaseOf
        (W (CategoryTheory.Triangulated.cl C v E)) α)
  (hW_ne :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          c < φ → φ < d → W (CategoryTheory.Triangulated.cl C v F) ≠ 0)
  (hfactors :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          c < φ →
            φ < d →
              ψ <
                  CategoryTheory.Triangulated.wPhaseOf
                    (W (CategoryTheory.Triangulated.cl C v F)) α ∧
                CategoryTheory.Triangulated.wPhaseOf
                    (W (CategoryTheory.Triangulated.cl C v F)) α <
                  ψ + 1) :
  ψ <
    CategoryTheory.Triangulated.wPhaseOf
      (W (CategoryTheory.Triangulated.cl C v E)) α
CategoryTheory.Triangulated.wPhaseOf_gt_of_narrow_interval.{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]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (W : Λ →+ ℂ) {α ψ c d : ℝ}
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing c d E)
  (hE_width :
    ψ - 1 <
      CategoryTheory.Triangulated.wPhaseOf
        (W
          (CategoryTheory.Triangulated.cl
            C v E))
        α)
  (hW_ne :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          c < φ →
            φ < d →
              W
                  (CategoryTheory.Triangulated.cl
                    C v F) ≠
                0)
  (hfactors :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          c < φ →
            φ < d →
              ψ <
                  CategoryTheory.Triangulated.wPhaseOf
                    (W
                      (CategoryTheory.Triangulated.cl
                        C v F))
                    α ∧
                CategoryTheory.Triangulated.wPhaseOf
                    (W
                      (CategoryTheory.Triangulated.cl
                        C v F))
                    α <
                  ψ + 1) :
  ψ <
    CategoryTheory.Triangulated.wPhaseOf
      (W
        (CategoryTheory.Triangulated.cl C
          v E))
      α

Something wrong, better idea? Suggest a change

14.18.2. exists_strictMDQ_with_quotient_bound🔗

MDQ existence with \varphi^+ case split (Bridgeland p.23). Same recursion as exists_strictMDQ_of_finiteLength but replaces hHom with perturbation data and a quotient lower bound, and replaces hDestabBound with phiPlus_bound_of_destabilizing_subobject when \varphi^+(Q_S) \le \psi(Q_S) + \varepsilon. When \varphi^+(Q_S) > \psi(Q_S) + \varepsilon, a \sigma-phase split branch applies.

Proof: Noetherian induction on the strict-subobject poset. Case 1 (semistable): identity MDQ. Case 2 (\varphi^+ \le \psi + \varepsilon): find a destabilizing strict subobject via the first strict SES, bound its phase by b - \varepsilon using phiPlus_bound_of_destabilizing_subobject, pull back, recurse, and compose via comp_of_destabilizing_with_quotient_bound. Case 3 (\varphi^+ > \psi + \varepsilon): extract the \sigma-HN filtration, split at cutoff \psi + \varepsilon, get the high-phase part X_{\mathrm{hi}} and low part Q_{S,\mathrm{lo}}, find an MDQ on \operatorname{coker}(A_{\mathrm{hi}}) via recursion, then compose via mdq_of_sigma_phase_split.

theorem

CategoryTheory.Triangulated.exists_strictMDQ_with_quotient_bound.{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] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction C v σ.slicing a
      b}
  [Fact (a < b)] [Fact (b - a ≤ 1)]
  (hFiniteLength :
    CategoryTheory.Triangulated.ThinFiniteLengthInInterval C σ a b)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F → ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
          F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧ ssf.wPhase F < U)
  (hWidth : U - L < 1) (W : Λ →+ ℂ)
  (hW_stab :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε : ℝ} (hε : 0 < ε) (hε2 : ε < 1 / 4) (hε8 : ε < 1 / 8) (hab : a < b)
  (hthin : b - a + 2 * ε < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε)))
  (hssf :
    ssf =
      CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW_stab hab)
  (hL_a : a ≤ L + ε) {t_lo : ℝ} (ht_lo : a + ε ≤ t_lo)
  {X : CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
  (hX : ¬CategoryTheory.Limits.IsZero X)
  (hQuotLo_ss :
    ∀
      {B' :
        CategoryTheory.Triangulated.Slicing.IntervalCat C σ.slicing a b}
      (q' : X ⟶ B'),
      CategoryTheory.IsStrictEpi q' →
        ¬CategoryTheory.Limits.IsZero B'.obj →
          CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
              C ssf B'.obj (ssf.wPhase B'.obj) →
            t_lo < ssf.wPhase B'.obj)
  (hψ_X_lo : t_lo < ssf.wPhase X.obj)
  (hψ_X_upper : ssf.wPhase X.obj < b - 3 * ε) :
  ∃ B q, CategoryTheory.Triangulated.IsStrictMDQ C σ ssf q
CategoryTheory.Triangulated.exists_strictMDQ_with_quotient_bound.{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]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v σ.slicing a b}
  [Fact (a < b)] [Fact (b - a ≤ 1)]
  (hFiniteLength :
    CategoryTheory.Triangulated.ThinFiniteLengthInInterval
      C σ a b)
  (hW_interval :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          ssf.wNe F)
  {L U : ℝ}
  (hWindow :
    ∀ {F : C},
      CategoryTheory.Triangulated.Slicing.intervalProp
          C σ.slicing a b F →
        ¬CategoryTheory.Limits.IsZero F →
          L < ssf.wPhase F ∧
            ssf.wPhase F < U)
  (hWidth : U - L < 1) (W : Λ →+ ℂ)
  (hW_stab :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {ε : ℝ} (hε : 0 < ε) (hε2 : ε < 1 / 4)
  (hε8 : ε < 1 / 8) (hab : a < b)
  (hthin : b - a + 2 * ε < 1)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε)))
  (hssf :
    ssf =
      CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near
        C σ W hW_stab hab)
  (hL_a : a ≤ L + ε) {t_lo : ℝ}
  (ht_lo : a + ε ≤ t_lo)
  {X :
    CategoryTheory.Triangulated.Slicing.IntervalCat
      C σ.slicing a b}
  (hX : ¬CategoryTheory.Limits.IsZero X)
  (hQuotLo_ss :
    ∀
      {B' :
        CategoryTheory.Triangulated.Slicing.IntervalCat
          C σ.slicing a b}
      (q' : X ⟶ B'),
      CategoryTheory.IsStrictEpi q' →
        ¬CategoryTheory.Limits.IsZero
              B'.obj →
          CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
              C ssf B'.obj
              (ssf.wPhase B'.obj) →
            t_lo < ssf.wPhase B'.obj)
  (hψ_X_lo : t_lo < ssf.wPhase X.obj)
  (hψ_X_upper :
    ssf.wPhase X.obj < b - 3 * ε) :
  ∃ B q,
    CategoryTheory.Triangulated.IsStrictMDQ
      C σ ssf q

hHom → perturbation data + W-semistable quotient lower bound
hDestabBound → phiPlus_bound_of_destabilizing_subobject (when φ⁺ ≤ ψ + ε)

Something wrong, better idea? Suggest a change