14.3. Deformation: DeformedSlicing🔗

14.3.1. deformedSlicing🔗

Deformed slicing (Nodes 7.Q + 7.6 + 7.7). The slicing Q with Q(\psi) = \operatorname{deformedPred}(\sigma, W, \varepsilon, \psi), where \varepsilon < \varepsilon_0 < 1/10 is the perturbation parameter.

Construction: Constructed as a Slicing whose predicate is deformedPred. The closedUnderIso field transports W-semistability across isomorphisms. The shift_iff field uses deformedPred_shift_one and its converse. The hom_vanishing field is Lemma 7.6 via hom_eq_zero_of_deformedPred. The hn_exists field delegates to deformedSlicing_hn_exists.

def

CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedSlicing.{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 * ε))) :
  CategoryTheory.Triangulated.Slicing C
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedSlicing.{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 * ε))) :
  CategoryTheory.Triangulated.Slicing C

Something wrong, better idea? Suggest a change

14.3.2. deformedSlicing_compat🔗

W-compatibility of the deformed slicing. For every nonzero Q-semistable object E of Q-phase \psi, the central charge W([E]) lies on the ray \mathbb{R}_+ \cdot e^{i\pi\psi}.

Proof: The Semistable structure stores \operatorname{wPhaseOf}(W([E]), \alpha) = \psi, which by wPhaseOf_compat gives W([E]) = \|W([E])\| \cdot e^{i\pi\psi} with \|W([E])\| > 0.

theorem

CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedSlicing_compat.{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 * ε)))
  (ψ : ℝ) (E : C)
  (hQ :
    (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedSlicing
          C σ W hW ε₀ hε₀ hε₀10 hWide ε hε hεε₀ hsin).P
      ψ E)
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  ∃ m,
    0 < m ∧
      W (CategoryTheory.Triangulated.cl C v E) =
        ↑m * Complex.exp (↑(Real.pi * ψ) * Complex.I)
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedSlicing_compat.{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 * ε)))
  (ψ : ℝ) (E : C)
  (hQ :
    (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedSlicing
          C σ W hW ε₀ hε₀ hε₀10 hWide ε hε
          hεε₀ hsin).P
      ψ E)
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  ∃ m,
    0 < m ∧
      W
          (CategoryTheory.Triangulated.cl
            C v E) =
        ↑m *
          Complex.exp
            (↑(Real.pi * ψ) * Complex.I)

Something wrong, better idea? Suggest a change

14.3.3. sigma_semistable_intervalProp🔗

Reverse phase confinement. If E is \sigma-semistable of phase \phi and \|W - Z\|_\sigma < \sin(\pi\varepsilon), then E lies in the Q-interval \mathcal{Q}((\phi - 2\varepsilon - \delta, \phi + 4\varepsilon + \delta)) for any \delta > 0.

Proof: Apply sigmaSemistable_hasDeformedHN to obtain a Q-HN filtration with phases in (\phi - 2\varepsilon, \phi + 4\varepsilon), then widen by \delta.

theorem

CategoryTheory.Triangulated.sigma_semistable_intervalProp.{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 * ε)))
  {E : C} {φ : ℝ} (hP : σ.slicing.P φ E)
  (hE : ¬CategoryTheory.Limits.IsZero E) {δ : ℝ} (hδ : 0 < δ) :
  CategoryTheory.Triangulated.Slicing.intervalProp C
    (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedSlicing
      C σ W hW ε₀ hε₀ hε₀10 hWide ε hε hεε₀ hsin)
    (φ - 2 * ε - δ) (φ + 4 * ε + δ) E
CategoryTheory.Triangulated.sigma_semistable_intervalProp.{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 * ε)))
  {E : C} {φ : ℝ} (hP : σ.slicing.P φ E)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  {δ : ℝ} (hδ : 0 < δ) :
  CategoryTheory.Triangulated.Slicing.intervalProp
    C
    (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedSlicing
      C σ W hW ε₀ hε₀ hε₀10 hWide ε hε
      hεε₀ hsin)
    (φ - 2 * ε - δ) (φ + 4 * ε + δ) E

Something wrong, better idea? Suggest a change

14.3.4. deformed_intervalProp_subset_sigma_intervalProp🔗

A Q-interval of radius \varepsilon_0 is contained in a \sigma-interval of radius 2\varepsilon_0: \mathcal{Q}((t - \varepsilon_0, t + \varepsilon_0)) \subseteq \mathcal{P}((t - 2\varepsilon_0, t + 2\varepsilon_0)).

Proof: For each Q-HN factor of an object in \mathcal{Q}((t - \varepsilon_0, t + \varepsilon_0)), phase confinement gives \sigma-phases within \varepsilon of the Q-phase, which lies in (t - \varepsilon_0, t + \varepsilon_0). Since \varepsilon < \varepsilon_0, the \sigma-phases lie in (t - 2\varepsilon_0, t + 2\varepsilon_0).

theorem

CategoryTheory.Triangulated.deformed_intervalProp_subset_sigma_intervalProp.{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 * ε)))
  (t : ℝ) :
  CategoryTheory.Triangulated.Slicing.intervalProp C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedSlicing
        C σ W hW ε₀ hε₀ hε₀10 hWide ε hε hεε₀ hsin)
      (t - ε₀) (t + ε₀) ≤
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing
      (t - 2 * ε₀) (t + 2 * ε₀)
CategoryTheory.Triangulated.deformed_intervalProp_subset_sigma_intervalProp.{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 * ε)))
  (t : ℝ) :
  CategoryTheory.Triangulated.Slicing.intervalProp
      C
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedSlicing
        C σ W hW ε₀ hε₀ hε₀10 hWide ε hε
        hεε₀ hsin)
      (t - ε₀) (t + ε₀) ≤
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing (t - 2 * ε₀)
      (t + 2 * ε₀)

Something wrong, better idea? Suggest a change