14.25. Deformation: Theorem🔗

14.25.1. deformed🔗

The canonical deformed stability condition attached to a nearby central charge W. This packages the actual object constructed in the deformation proof as a StabilityCondition.WithClassMap, rather than hiding it behind an existential.

Construction: Constructs the deformed slicing Q via deformedSlicing, pairs it with W as the central charge, verifies compatibility, then establishes local finite length by showing each deformed interval Q((t - \varepsilon_0, t + \varepsilon_0)) embeds into the \sigma-interval \mathcal{P}((t - 2\varepsilon_0, t + 2\varepsilon_0)) which has sector finite length.

def

CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformed.{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)
  (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 * ε))) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformed.{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)
  (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 * ε))) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap
    C v

Something wrong, better idea? Suggest a change

14.25.2. deformed_Z🔗

The central charge of the deformed stability condition is W: \tau.Z = W.

Proof: Definitional: deformed stores W as its central charge component.

theorem

CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformed_Z.{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)
  (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 * ε))) :
  (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformed
        C σ W hW ε₀ hε₀ hε₀10 hWide ε hε hεε₀ hsin).Z =
    W
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformed_Z.{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)
  (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 * ε))) :
  (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformed
        C σ W hW ε₀ hε₀ hε₀10 hWide ε hε
        hεε₀ hsin).Z =
    W

Something wrong, better idea? Suggest a change

14.25.3. slicingDist_deformed_le🔗

The canonical deformation has slicing distance at most \varepsilon from the original: d(P, Q) \le \varepsilon.

Proof: Apply slicingDist_le_of_phase_bounds: show |\varphi^+(E; P) - \varphi^+(E; Q)| \le \varepsilon and |\varphi^-(E; P) - \varphi^-(E; Q)| \le \varepsilon for all nonzero E. Forward direction (sigma to Q): Q-HN factors are deformedPred, so phase confinement gives \sigma-phases within \varepsilon of Q-phases. Reverse direction (Q \to \sigma): \sigma-HN factors are mapped into Q(> t) and Q(< t) predicates, giving Q-phases within \varepsilon of \sigma-phases.

theorem

CategoryTheory.Triangulated.StabilityCondition.WithClassMap.slicingDist_deformed_le.{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)
  (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 * ε))) :
  CategoryTheory.Triangulated.slicingDist C σ.slicing
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformed
          C σ W hW ε₀ hε₀ hε₀10 hWide ε hε hεε₀ hsin).slicing ≤
    ENNReal.ofReal ε
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.slicingDist_deformed_le.{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)
  (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 * ε))) :
  CategoryTheory.Triangulated.slicingDist
      C σ.slicing
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformed
          C σ W hW ε₀ hε₀ hε₀10 hWide ε hε
          hεε₀ hsin).slicing ≤
    ENNReal.ofReal ε

Something wrong, better idea? Suggest a change

14.25.4. exists_eq_Z_and_slicingDist_lt_of_stabSeminorm_lt_sin🔗

Bridgeland's Theorem 7.1 (deformation of stability conditions). Under the small-deformation hypothesis \|W - Z\|_\sigma < \sin(\pi\varepsilon), there exists a locally-finite stability condition \tau = (W, Q) with d(P, Q) < \varepsilon.

Proof: The strict hypothesis \|W - Z\|_\sigma < \sin(\pi\varepsilon) allows shrinking: find \varepsilon' < \varepsilon with \|W - Z\|_\sigma < \sin(\pi\varepsilon') via the intermediate value theorem (more precisely, by taking \varepsilon' = \operatorname{arcsin}(y)/\pi where y is the midpoint between the seminorm and \sin(\pi\varepsilon)). Apply slicingDist_deformed_le at \varepsilon' to get d(P, Q) \le \varepsilon' < \varepsilon.

theorem

CategoryTheory.Triangulated.StabilityCondition.WithClassMap.exists_eq_Z_and_slicingDist_lt_of_stabSeminorm_lt_sin.{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)
  (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 * ε))) :
  ∃ τ,
    τ.Z = W ∧
      CategoryTheory.Triangulated.slicingDist C σ.slicing τ.slicing <
        ENNReal.ofReal ε
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.exists_eq_Z_and_slicingDist_lt_of_stabSeminorm_lt_sin.{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)
  (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 * ε))) :
  ∃ τ,
    τ.Z = W ∧
      CategoryTheory.Triangulated.slicingDist
          C σ.slicing τ.slicing <
        ENNReal.ofReal ε

Something wrong, better idea? Suggest a change