Bridgeland Stability Conditions

14.26. Deformation: WPhase🔗

14.26.1. W_ne_zero_of_seminorm_lt_one🔗

W-nonvanishing. If the seminorm \|W - Z\|_\sigma < 1, then W([E]) \ne 0 for every nonzero \sigma-semistable object E.

Proof: By the triangle inequality, \|W([E])\| \ge \|Z([E])\| - \|(W-Z)([E])\| \ge (1 - M)\|Z([E])\| > 0 where M = \|W - Z\|_\sigma < 1 and \|Z([E])\| > 0 from compatibility.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.W_ne_zero_of_seminorm_lt_one.{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)
  {E : C} {φ : ℝ} (hP : σ.slicing.P φ E)
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  W (CategoryTheory.Triangulated.cl C v E) ≠ 0
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.W_ne_zero_of_seminorm_lt_one.{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)
  {E : C} {φ : ℝ} (hP : σ.slicing.P φ E)
  (hE : ¬CategoryTheory.Limits.IsZero E) :
  W
      (CategoryTheory.Triangulated.cl C v
        E) ≠
    0

Something wrong, better idea? Suggest a change

14.26.2. skewedStabilityFunction_of_near🔗

Node 7.2a. Given a stability condition \sigma and a group homomorphism W with \|W - Z\|_\sigma < 1, W restricts to a skewed stability function on any interval (a, b) with skewing parameter \alpha = (a+b)/2.

Construction: Constructs a SkewedStabilityFunction by setting \alpha = (a+b)/2 and using W_ne_zero_of_seminorm_lt_one for the nonvanishing condition.

🔗def
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near.{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)
  {a b : ℝ} (hab : a < b) :
  CategoryTheory.Triangulated.SkewedStabilityFunction C v σ.slicing a b
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedStabilityFunction_of_near.{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)
  {a b : ℝ} (hab : a < b) :
  CategoryTheory.Triangulated.SkewedStabilityFunction
    C v σ.slicing a b

Something wrong, better idea? Suggest a change

14.26.3. norm_Z_pos_of_intervalProp🔗

Z-nonvanishing for interval objects. For a nonzero object E \in \mathcal{P}((a, b)) with b - a < 1, the central charge satisfies \|Z([E])\| > 0.

Proof: Decompose E via its HN filtration and apply the sector estimate: \cos(\pi(b-a)/2) \cdot \sum \|Z(F_j)\| \le \|Z(E)\|. Since b - a < 1, the cosine is positive, and at least one factor has \|Z(F_j)\| > 0.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.norm_Z_pos_of_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)
  {E : C} (hE : ¬CategoryTheory.Limits.IsZero E) {a b : ℝ}
  (hab : b - a < 1)
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
      E) :
  0 < ‖σ.charge E‖
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.norm_Z_pos_of_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)
  {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  {a b : ℝ} (hab : b - a < 1)
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing a b E) :
  0 < ‖σ.charge E‖

Something wrong, better idea? Suggest a change

14.26.4. W_ne_zero_of_intervalProp🔗

W-nonvanishing for interval objects. If \|W - Z\|_\sigma < \cos(\pi(b-a)/2) and E is nonzero in \mathcal{P}((a, b)) with b - a < 1, then W([E]) \ne 0.

Proof: Combine the Z-nonvanishing bound with the sector bound on W - Z: the ratio M/\cos(\pi(b-a)/2) < 1, so \|(W-Z)(E)\| < \|Z(E)\|, and if W(E) = 0 we get \|Z(E)\| \le \|(W-Z)(E)\|, a contradiction.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.W_ne_zero_of_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 : Λ →+ ℂ) {a b : ℝ} (hab : b - a < 1)
  (hsmall :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.cos (Real.pi * (b - a) / 2)))
  {E : C} (hE : ¬CategoryTheory.Limits.IsZero E)
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b
      E) :
  W (CategoryTheory.Triangulated.cl C v E) ≠ 0
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.W_ne_zero_of_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 : Λ →+ ℂ) {a b : ℝ} (hab : b - a < 1)
  (hsmall :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.cos
          (Real.pi * (b - a) / 2)))
  {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing a b E) :
  W
      (CategoryTheory.Triangulated.cl C v
        E) ≠
    0

Something wrong, better idea? Suggest a change

14.26.5. wPhaseOf🔗

The W-phase of a complex number w \ne 0 relative to a skewing parameter \alpha. Defined as \alpha + \arg(w \cdot e^{-i\pi\alpha}) / \pi, giving \psi \in (\alpha - 1, \alpha + 1] satisfying w = \|w\| \cdot e^{i\pi\psi}.

Construction: Computed by rotating w by e^{-i\pi\alpha} to center the branch cut, taking the standard argument in (-\pi, \pi], then rescaling by 1/\pi and shifting by \alpha.

🔗def
CategoryTheory.Triangulated.wPhaseOf (w : ℂ) (α : ℝ) : ℝ
CategoryTheory.Triangulated.wPhaseOf
  (w : ℂ) (α : ℝ) : ℝ

Something wrong, better idea? Suggest a change

14.26.6. wPhaseOf_mem_Ioc🔗

The W-phase lies in the half-open interval (\alpha - 1, \alpha + 1].

Proof: Immediate from \arg(z) \in (-\pi, \pi] after dividing by \pi and adding \alpha.

🔗theorem
CategoryTheory.Triangulated.wPhaseOf_mem_Ioc (w : ℂ) (α : ℝ) :
  CategoryTheory.Triangulated.wPhaseOf w α ∈ Set.Ioc (α - 1) (α + 1)
CategoryTheory.Triangulated.wPhaseOf_mem_Ioc
  (w : ℂ) (α : ℝ) :
  CategoryTheory.Triangulated.wPhaseOf w
      α ∈
    Set.Ioc (α - 1) (α + 1)

Something wrong, better idea? Suggest a change

14.26.7. wPhaseOf_compat🔗

Polar compatibility. A nonzero complex number w equals \|w\| \cdot e^{i\pi \cdot \operatorname{wPhaseOf}(w, \alpha)}.

Proof: Factor w = z \cdot e^{i\pi\alpha} where z = w \cdot e^{-i\pi\alpha}. Apply the standard polar decomposition z = \|z\| \cdot e^{i \arg(z)}, note \|z\| = \|w\|, and reassemble using \arg(z) + \pi\alpha = \pi \cdot \operatorname{wPhaseOf}(w, \alpha).

🔗theorem
CategoryTheory.Triangulated.wPhaseOf_compat (w : ℂ) (α : ℝ) :
  w =
    ↑‖w‖ *
      Complex.exp
        (↑(Real.pi * CategoryTheory.Triangulated.wPhaseOf w α) *
          Complex.I)
CategoryTheory.Triangulated.wPhaseOf_compat
  (w : ℂ) (α : ℝ) :
  w =
    ↑‖w‖ *
      Complex.exp
        (↑(Real.pi *
              CategoryTheory.Triangulated.wPhaseOf
                w α) *
          Complex.I)

Something wrong, better idea? Suggest a change

14.26.8. wPhaseOf_of_exp🔗

The W-phase of m \cdot e^{i\pi\phi} with m > 0 and \phi \in (\alpha - 1, \alpha + 1] equals \phi.

Proof: After rotation by e^{-i\pi\alpha}, the argument of m \cdot e^{i\pi(\phi - \alpha)} is \pi(\phi - \alpha) \in (-\pi, \pi], so dividing by \pi and adding \alpha recovers \phi.

🔗theorem
CategoryTheory.Triangulated.wPhaseOf_of_exp {m φ α : ℝ} (hm : 0 < m)
  (hφ : φ ∈ Set.Ioc (α - 1) (α + 1)) :
  CategoryTheory.Triangulated.wPhaseOf
      (↑m * Complex.exp (↑(Real.pi * φ) * Complex.I)) α =
    φ
CategoryTheory.Triangulated.wPhaseOf_of_exp
  {m φ α : ℝ} (hm : 0 < m)
  (hφ : φ ∈ Set.Ioc (α - 1) (α + 1)) :
  CategoryTheory.Triangulated.wPhaseOf
      (↑m *
        Complex.exp
          (↑(Real.pi * φ) * Complex.I))
      α =
    φ

Something wrong, better idea? Suggest a change

14.26.9. wPhaseOf_zero🔗

The W-phase of zero is \alpha, since \arg(0) = 0.

Proof: Direct computation: \arg(0) = 0, so \alpha + 0/\pi = \alpha.

🔗theorem
CategoryTheory.Triangulated.wPhaseOf_zero (α : ℝ) :
  CategoryTheory.Triangulated.wPhaseOf 0 α = α
CategoryTheory.Triangulated.wPhaseOf_zero
  (α : ℝ) :
  CategoryTheory.Triangulated.wPhaseOf 0
      α =
    α

Something wrong, better idea? Suggest a change

14.26.10. wPhaseOf_neg🔗

Negation shifts W-phase by 1. For nonzero w, \operatorname{wPhaseOf}(-w, \alpha + 1) = \operatorname{wPhaseOf}(w, \alpha) + 1. Since e^{i\pi} = -1, negating w shifts the argument by \pi, hence the phase by 1.

Proof: Write -w = \|w\| \cdot e^{i\pi(\phi + 1)} where \phi = \operatorname{wPhaseOf}(w, \alpha). Since \phi + 1 \in (\alpha, \alpha + 2] = ((\alpha+1) - 1, (\alpha+1) + 1], apply wPhaseOf_of_exp to get \operatorname{wPhaseOf}(-w, \alpha + 1) = \phi + 1.

🔗theorem
CategoryTheory.Triangulated.wPhaseOf_neg {w : ℂ} (hw : w ≠ 0) (α : ℝ) :
  CategoryTheory.Triangulated.wPhaseOf (-w) (α + 1) =
    CategoryTheory.Triangulated.wPhaseOf w α + 1
CategoryTheory.Triangulated.wPhaseOf_neg
  {w : ℂ} (hw : w ≠ 0) (α : ℝ) :
  CategoryTheory.Triangulated.wPhaseOf
      (-w) (α + 1) =
    CategoryTheory.Triangulated.wPhaseOf w
        α +
      1

Something wrong, better idea? Suggest a change

14.26.11. wPhaseOf_add_two🔗

Shifting \alpha by 2 shifts wPhaseOf by 2. For nonzero w, \operatorname{wPhaseOf}(w, \alpha + 2) = \operatorname{wPhaseOf}(w, \alpha) + 2.

Proof: Apply wPhaseOf_neg twice: once for w \mapsto -w and once for -w \mapsto w.

🔗theorem
CategoryTheory.Triangulated.wPhaseOf_add_two {w : ℂ} (hw : w ≠ 0)
  (α : ℝ) :
  CategoryTheory.Triangulated.wPhaseOf w (α + 2) =
    CategoryTheory.Triangulated.wPhaseOf w α + 2
CategoryTheory.Triangulated.wPhaseOf_add_two
  {w : ℂ} (hw : w ≠ 0) (α : ℝ) :
  CategoryTheory.Triangulated.wPhaseOf w
      (α + 2) =
    CategoryTheory.Triangulated.wPhaseOf w
        α +
      2

Something wrong, better idea? Suggest a change

14.26.12. wPhase🔗

The W-phase of an object E with respect to a skewed stability function \mathtt{ssf}, defined as \mathrm{wPhaseOf}(W([E]), \alpha). This is the unique real number \psi \in (\alpha - 1, \alpha + 1] satisfying W([E]) = \|W([E])\| \cdot e^{i\pi\psi} (when W([E]) \ne 0; otherwise it equals \alpha by convention). The parameter \alpha \in (a, b) is the skewing center of \mathtt{ssf}.

Construction: An abbreviation for \mathrm{wPhaseOf}(\mathtt{ssf}.W(\mathrm{cl}(E)),\ \mathtt{ssf}.\alpha), the W-phase of the deformed charge W([E]) computed relative to the skewing parameter \alpha.

🔗def
CategoryTheory.Triangulated.SkewedStabilityFunction.wPhase.{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 →+ Λ}
  {s : CategoryTheory.Triangulated.Slicing C} {a b : ℝ}
  (ssf : CategoryTheory.Triangulated.SkewedStabilityFunction C v s a b)
  (E : C) : ℝ
CategoryTheory.Triangulated.SkewedStabilityFunction.wPhase.{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 →+ Λ}
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {a b : ℝ}
  (ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v s a b)
  (E : C) : ℝ

Something wrong, better idea? Suggest a change

14.26.13. wNe🔗

The nonvanishing condition for the deformed central charge: \mathrm{wNe}(E) holds when W([E]) \ne 0 in \mathbb{C}. This ensures that the W-phase \mathrm{wPhaseOf}(W([E]), \alpha) is well-defined (for zero input \mathrm{wPhaseOf} returns \alpha by convention, so the phase is only geometrically meaningful when W([E]) \ne 0).

Construction: An abbreviation for W(\mathrm{cl}(E)) \ne 0, where \mathrm{cl}(E) \in K_0 is the class of E.

🔗def
CategoryTheory.Triangulated.SkewedStabilityFunction.wNe.{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 →+ Λ}
  {s : CategoryTheory.Triangulated.Slicing C} {a b : ℝ}
  (ssf : CategoryTheory.Triangulated.SkewedStabilityFunction C v s a b)
  (E : C) : Prop
CategoryTheory.Triangulated.SkewedStabilityFunction.wNe.{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 →+ Λ}
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {a b : ℝ}
  (ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v s a b)
  (E : C) : Prop

Something wrong, better idea? Suggest a change

14.26.14. wPhase_def🔗

The W-phase of E unfolds as \mathrm{wPhaseOf}(W([E]), \alpha), where \alpha is the reference phase of the skewed stability function.

Proof: This is true by reflexivity (definitional unfolding).

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.wPhase_def.{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 →+ Λ}
  {s : CategoryTheory.Triangulated.Slicing C} {a b : ℝ}
  (ssf : CategoryTheory.Triangulated.SkewedStabilityFunction C v s a b)
  (E : C) :
  ssf.wPhase E =
    CategoryTheory.Triangulated.wPhaseOf
      (ssf.W (CategoryTheory.Triangulated.cl C v E)) ssf.α
CategoryTheory.Triangulated.SkewedStabilityFunction.wPhase_def.{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 →+ Λ}
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {a b : ℝ}
  (ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v s a b)
  (E : C) :
  ssf.wPhase E =
    CategoryTheory.Triangulated.wPhaseOf
      (ssf.W
        (CategoryTheory.Triangulated.cl C
          v E))
      ssf.α

Something wrong, better idea? Suggest a change

14.26.15. wNe_def🔗

Unfolds the definition of wNe: ssf.wNe E is definitionally equal to the proposition W([E]) \ne 0. This lemma is used to convert between the abstract predicate and the explicit nonvanishing condition.

Proof: This is a rfl proof: both sides are definitionally equal by the abbreviation wNe.

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.wNe_def.{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 →+ Λ}
  {s : CategoryTheory.Triangulated.Slicing C} {a b : ℝ}
  (ssf : CategoryTheory.Triangulated.SkewedStabilityFunction C v s a b)
  (E : C) :
  ssf.wNe E = (ssf.W (CategoryTheory.Triangulated.cl C v E) ≠ 0)
CategoryTheory.Triangulated.SkewedStabilityFunction.wNe_def.{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 →+ Λ}
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {a b : ℝ}
  (ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v s a b)
  (E : C) :
  ssf.wNe E =
    (ssf.W
        (CategoryTheory.Triangulated.cl C
          v E) ≠
      0)

Something wrong, better idea? Suggest a change

14.26.16. wPhase_congr🔗

If two objects E and E' have the same deformed charge, W([E]) = W([E']), then they have the same W-phase, \mathrm{wPhase}(E) = \mathrm{wPhase}(E'). This is the congruence lemma for the W-phase under equality of charges.

Proof: Immediate from unfolding wPhase and rewriting with the hypothesis W([E]) = W([E']).

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.wPhase_congr.{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 →+ Λ}
  {s : CategoryTheory.Triangulated.Slicing C} {a b : ℝ}
  (ssf : CategoryTheory.Triangulated.SkewedStabilityFunction C v s a b)
  {E E' : C}
  (h :
    ssf.W (CategoryTheory.Triangulated.cl C v E) =
      ssf.W (CategoryTheory.Triangulated.cl C v E')) :
  ssf.wPhase E = ssf.wPhase E'
CategoryTheory.Triangulated.SkewedStabilityFunction.wPhase_congr.{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 →+ Λ}
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {a b : ℝ}
  (ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v s a b)
  {E E' : C}
  (h :
    ssf.W
        (CategoryTheory.Triangulated.cl C
          v E) =
      ssf.W
        (CategoryTheory.Triangulated.cl C
          v E')) :
  ssf.wPhase E = ssf.wPhase E'

Something wrong, better idea? Suggest a change

14.26.17. wPhase_iso🔗

Isomorphic objects have equal W-phases: if E \cong E', then \psi_W(E) = \psi_W(E').

Proof: Since the central charge W factors through K_0, an isomorphism E \cong E' implies [E] = [E'] in K_0, hence W([E]) = W([E']), and the W-phases agree by wPhase_congr.

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.wPhase_iso.{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 →+ Λ}
  {s : CategoryTheory.Triangulated.Slicing C} {a b : ℝ}
  (ssf : CategoryTheory.Triangulated.SkewedStabilityFunction C v s a b)
  {E E' : C} (e : E ≅ E') : ssf.wPhase E = ssf.wPhase E'
CategoryTheory.Triangulated.SkewedStabilityFunction.wPhase_iso.{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 →+ Λ}
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {a b : ℝ}
  (ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v s a b)
  {E E' : C} (e : E ≅ E') :
  ssf.wPhase E = ssf.wPhase E'

Something wrong, better idea? Suggest a change

14.26.18. wPhase_seesaw🔗

A phase seesaw inequality: if W([E_1]) + W([E_2]) = W([E]), the W-phase of E equals \psi, the W-phase of E_1 lies in (\psi-1, \psi], W([E_2]) \neq 0, and the W-phase of E_2 lies in (\psi-1, \psi+1), then \psi \leq \psi_W(E_2).

Proof: By contradiction, assume \psi_W(E_2) < \psi. Rotating by e^{-i\pi\psi} and taking imaginary parts, \mathrm{Im}(W([E]) \cdot e^{-i\pi\psi}) = 0 (since \psi_W(E) = \psi), \mathrm{Im}(W([E_1]) \cdot e^{-i\pi\psi}) \geq 0 (since \psi_W(E_1) \leq \psi), and \mathrm{Im}(W([E_2]) \cdot e^{-i\pi\psi}) < 0 (since \psi_W(E_2) < \psi). The additivity W([E_1]) + W([E_2]) = W([E]) then yields a sign contradiction.

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.wPhase_seesaw.{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 →+ Λ}
  {s : CategoryTheory.Triangulated.Slicing C} {a b : ℝ}
  (ssf : CategoryTheory.Triangulated.SkewedStabilityFunction C v s a b)
  {E E₁ E₂ : C} {ψ : ℝ}
  (hsum :
    ssf.W (CategoryTheory.Triangulated.cl C v E₁) +
        ssf.W (CategoryTheory.Triangulated.cl C v E₂) =
      ssf.W (CategoryTheory.Triangulated.cl C v E))
  (hψ : ssf.wPhase E = ψ)
  (hE₁_range : ssf.wPhase E₁ ∈ Set.Ioc (ψ - 1) ψ) (hE₂_ne : ssf.wNe E₂)
  (hE₂_range : ssf.wPhase E₂ ∈ Set.Ioo (ψ - 1) (ψ + 1)) :
  ψ ≤ ssf.wPhase E₂
CategoryTheory.Triangulated.SkewedStabilityFunction.wPhase_seesaw.{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 →+ Λ}
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {a b : ℝ}
  (ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v s a b)
  {E E₁ E₂ : C} {ψ : ℝ}
  (hsum :
    ssf.W
          (CategoryTheory.Triangulated.cl
            C v E₁) +
        ssf.W
          (CategoryTheory.Triangulated.cl
            C v E₂) =
      ssf.W
        (CategoryTheory.Triangulated.cl C
          v E))
  (hψ : ssf.wPhase E = ψ)
  (hE₁_range :
    ssf.wPhase E₁ ∈ Set.Ioc (ψ - 1) ψ)
  (hE₂_ne : ssf.wNe E₂)
  (hE₂_range :
    ssf.wPhase E₂ ∈
      Set.Ioo (ψ - 1) (ψ + 1)) :
  ψ ≤ ssf.wPhase E₂

Something wrong, better idea? Suggest a change

14.26.19. Semistable🔗

W-semistability. An object E in \mathcal{P}((a, b)) is W-semistable of W-phase \psi if: (1) E \in \mathcal{P}((a,b)) and E \ne 0, (2) W([E]) \ne 0, (3) \operatorname{wPhaseOf}(W([E]), \alpha) = \psi, and (4) for every distinguished triangle K \to E \to Q \to K[1] with K, Q \in \mathcal{P}((a,b)) and K \ne 0, we have \operatorname{wPhaseOf}(W([K]), \alpha) \le \psi.

Construction: A structure bundling the interval membership, nonzero witness, W-nonvanishing, phase equality, and the subobject phase inequality.

🔗structure
CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable.{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 →+ Λ}
  {s : CategoryTheory.Triangulated.Slicing C} {a b : ℝ}
  (ssf : CategoryTheory.Triangulated.SkewedStabilityFunction C v s a b)
  (E : C) (ψ : ℝ) : Prop
CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable.{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 →+ Λ}
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {a b : ℝ}
  (ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v s a b)
  (E : C) (ψ : ℝ) : Prop

  1. E is in the interval P((a, b)) and is nonzero,

  2. W([E]) ≠ 0 (so the W-phase is well-defined),

  3. The W-phase of E equals ψ,

  4. For every distinguished triangle K → E → Q → K[1] with both K, Q ∈ P((a, b)) and K nonzero, the W-phase of K is at most ψ.

Constructor

CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable.mk.{v, u, u'}

Fields

intervalProp : CategoryTheory.Triangulated.Slicing.intervalProp C s a b E
nonzero : ¬CategoryTheory.Limits.IsZero E
wNe : ssf.wNe E
phase_eq : ssf.wPhase E = ψ
le_of_distTriang : ∀ ⦃K Q : C⦄ ⦃f₁ : K ⟶ E⦄ ⦃f₂ : E ⟶ Q⦄ ⦃f₃ : Q ⟶ (CategoryTheory.shiftFunctor C 1).obj K⦄,
  CategoryTheory.Pretriangulated.Triangle.mk f₁ f₂ f₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
    CategoryTheory.Triangulated.Slicing.intervalProp C s a b K →
      CategoryTheory.Triangulated.Slicing.intervalProp C s a b Q → ¬CategoryTheory.Limits.IsZero K → ssf.wPhase K ≤ ψ

Something wrong, better idea? Suggest a change

14.26.20. wPhaseOf_indep🔗

\alpha-independence of wPhaseOf. For nonzero w, if \operatorname{wPhaseOf}(w, \alpha_1) \in (\alpha_2 - 1, \alpha_2 + 1], then \operatorname{wPhaseOf}(w, \alpha_1) = \operatorname{wPhaseOf}(w, \alpha_2). This shows the W-phase is intrinsic, provided the branch cuts are compatible.

Proof: Write w = \|w\| \cdot e^{i\pi\phi} where \phi = \operatorname{wPhaseOf}(w, \alpha_1). Since \phi \in (\alpha_2 - 1, \alpha_2 + 1], apply wPhaseOf_of_exp with parameter \alpha_2 to get \operatorname{wPhaseOf}(w, \alpha_2) = \phi.

🔗theorem
CategoryTheory.Triangulated.wPhaseOf_indep {w : ℂ} (hw : w ≠ 0)
  (α₁ α₂ : ℝ)
  (h :
    CategoryTheory.Triangulated.wPhaseOf w α₁ ∈
      Set.Ioc (α₂ - 1) (α₂ + 1)) :
  CategoryTheory.Triangulated.wPhaseOf w α₁ =
    CategoryTheory.Triangulated.wPhaseOf w α₂
CategoryTheory.Triangulated.wPhaseOf_indep
  {w : ℂ} (hw : w ≠ 0) (α₁ α₂ : ℝ)
  (h :
    CategoryTheory.Triangulated.wPhaseOf w
        α₁ ∈
      Set.Ioc (α₂ - 1) (α₂ + 1)) :
  CategoryTheory.Triangulated.wPhaseOf w
      α₁ =
    CategoryTheory.Triangulated.wPhaseOf w
      α₂

Something wrong, better idea? Suggest a change

14.26.21. phase_mem_Ioc🔗

The W-phase of a W-semistable object lies in (\alpha - 1, \alpha + 1].

Proof: Substitute the phase equality into wPhaseOf_mem_Ioc.

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable.phase_mem_Ioc.{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 →+ Λ}
  {s : CategoryTheory.Triangulated.Slicing C} {a b : ℝ}
  {ssf : CategoryTheory.Triangulated.SkewedStabilityFunction C v s a b}
  {E : C} {ψ : ℝ}
  (h :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf
      E ψ) :
  ψ ∈ Set.Ioc (ssf.α - 1) (ssf.α + 1)
CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable.phase_mem_Ioc.{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 →+ Λ}
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v s a b}
  {E : C} {ψ : ℝ}
  (h :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C ssf E ψ) :
  ψ ∈ Set.Ioc (ssf.α - 1) (ssf.α + 1)

Something wrong, better idea? Suggest a change

14.26.22. polar🔗

The W-value of a W-semistable object satisfies the polar decomposition W([E]) = \|W([E])\| \cdot e^{i\pi\psi}.

Proof: Substitute the phase equality into wPhaseOf_compat.

🔗theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable.polar.{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 →+ Λ}
  {s : CategoryTheory.Triangulated.Slicing C} {a b : ℝ}
  {ssf : CategoryTheory.Triangulated.SkewedStabilityFunction C v s a b}
  {E : C} {ψ : ℝ}
  (h :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable C ssf
      E ψ) :
  ssf.W (CategoryTheory.Triangulated.cl C v E) =
    ↑‖ssf.W (CategoryTheory.Triangulated.cl C v E)‖ *
      Complex.exp (↑(Real.pi * ψ) * Complex.I)
CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable.polar.{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 →+ Λ}
  {s :
    CategoryTheory.Triangulated.Slicing C}
  {a b : ℝ}
  {ssf :
    CategoryTheory.Triangulated.SkewedStabilityFunction
      C v s a b}
  {E : C} {ψ : ℝ}
  (h :
    CategoryTheory.Triangulated.SkewedStabilityFunction.Semistable
      C ssf E ψ) :
  ssf.W
      (CategoryTheory.Triangulated.cl C v
        E) =
    ↑‖ssf.W
            (CategoryTheory.Triangulated.cl
              C v E)‖ *
      Complex.exp
        (↑(Real.pi * ψ) * Complex.I)

Something wrong, better idea? Suggest a change