Bridgeland Stability Conditions

13.1. StabilityCondition: Basic🔗

13.1.1. PreStabilityCondition.WithClassMap.ext🔗

Extensionality for prestability conditions: two class-map prestability conditions \sigma and \tau over the same class map v are equal if and only if their slicings agree (\mathcal{P}_\sigma = \mathcal{P}_\tau) and their central charges agree (Z_\sigma = Z_\tau). The compatibility datum is a proposition and hence unique by proof irrelevance.

Proof: Destructs both structures, applies the hypotheses to collapse slicing and charge fields, then uses Subsingleton.elim on the compatibility proof.

🔗theorem
CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.ext.{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.Triangulated.PreStabilityCondition.WithClassMap C v}
  (hs : σ.slicing = τ.slicing) (hZ : σ.Z = τ.Z) : σ = τ
CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.ext.{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.Triangulated.PreStabilityCondition.WithClassMap
      C v}
  (hs : σ.slicing = τ.slicing)
  (hZ : σ.Z = τ.Z) : σ = τ

Something wrong, better idea? Suggest a change

13.1.2. PreStabilityCondition.WithClassMap.ext_iff🔗

🔗theorem
CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.ext_iff.{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.Triangulated.PreStabilityCondition.WithClassMap C
      v} :
  σ = τ ↔ σ.slicing = τ.slicing ∧ σ.Z = τ.Z
CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.ext_iff.{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.Triangulated.PreStabilityCondition.WithClassMap
      C v} :
  σ = τ ↔
    σ.slicing = τ.slicing ∧ σ.Z = τ.Z

Something wrong, better idea? Suggest a change

13.1.3. StabilityCondition.WithClassMap.ext🔗

Extensionality for stability conditions: two class-map stability conditions are equal if and only if their slicings and central charges agree. The local finiteness field is propositional.

Proof: Reduces to PreStabilityCondition.WithClassMap.ext on the parent structure, then uses Subsingleton.elim for the locallyFinite field.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.ext.{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}
  (hs : σ.slicing = τ.slicing) (hZ : σ.Z = τ.Z) : σ = τ
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.ext.{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}
  (hs : σ.slicing = τ.slicing)
  (hZ : σ.Z = τ.Z) : σ = τ

Something wrong, better idea? Suggest a change

13.1.4. StabilityCondition.WithClassMap.ext_iff🔗

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.ext_iff.{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} :
  σ = τ ↔ σ.slicing = τ.slicing ∧ σ.Z = τ.Z
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.ext_iff.{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} :
  σ = τ ↔
    σ.slicing = τ.slicing ∧ σ.Z = τ.Z

Something wrong, better idea? Suggest a change

13.1.5. preStabilityCondition_compat_apply🔗

The compatibility condition for a prestability condition with class map v, simplified: for every nonzero \mathcal{P}(\phi)-semistable object E, Z(\operatorname{cl}_v(E)) = m \cdot e^{i\pi\phi} for some m > 0.

Proof: Immediate simplification of the general compatibility statement.

🔗theorem
CategoryTheory.Triangulated.preStabilityCondition_compat_apply.{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.Triangulated.PreStabilityCondition.WithClassMap C v)
  (φ : ℝ) (E : C) (hE : σ.slicing.P φ E)
  (hNZ : ¬CategoryTheory.Limits.IsZero E) :
  ∃ m,
    0 < m ∧ σ.charge E = ↑m * Complex.exp (↑(Real.pi * φ) * Complex.I)
CategoryTheory.Triangulated.preStabilityCondition_compat_apply.{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.Triangulated.PreStabilityCondition.WithClassMap
      C v)
  (φ : ℝ) (E : C) (hE : σ.slicing.P φ E)
  (hNZ :
    ¬CategoryTheory.Limits.IsZero E) :
  ∃ m,
    0 < m ∧
      σ.charge E =
        ↑m *
          Complex.exp
            (↑(Real.pi * φ) * Complex.I)

Something wrong, better idea? Suggest a change

13.1.6. phase_eq_of_same_Z🔗

Lemma 6.4 sublemma (phase rigidity). If two stability conditions \sigma and \tau share the same central charge Z, and a nonzero object E is \sigma-semistable of phase \phi and \tau-semistable of phase \psi with |\phi - \psi| < 2, then \phi = \psi. This is the key uniqueness ingredient: the central charge determines the phase of any semistable object.

Proof: Obtains Z([E]) = m_1 e^{i\pi\phi} = m_2 e^{i\pi\psi} from both compatibility conditions, then applies the uniqueness lemma eq_of_pos_mul_exp_eq for positive real multiples of exponentials.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.phase_eq_of_same_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)
  (hZ : σ.Z = τ.Z) {E : C} {φ ψ : ℝ} (hσ : σ.slicing.P φ E)
  (hτ : τ.slicing.P ψ E) (hE : ¬CategoryTheory.Limits.IsZero E)
  (habs : |φ - ψ| < 2) : φ = ψ
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.phase_eq_of_same_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)
  (hZ : σ.Z = τ.Z) {E : C} {φ ψ : ℝ}
  (hσ : σ.slicing.P φ E)
  (hτ : τ.slicing.P ψ E)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (habs : |φ - ψ| < 2) : φ = ψ

Something wrong, better idea? Suggest a change

13.1.7. no_exp_decomp_below🔗

A real multiple of e^{i\pi\psi} cannot equal a sum \sum_j b_j \, e^{i\pi\theta_j} with all b_j > 0 and all \theta_j strictly below \psi (and above \psi - 1). The proof divides by e^{i\pi\psi} and takes imaginary parts: each term contributes b_j \sin(\pi(\theta_j - \psi)) < 0, so the total imaginary part is strictly negative, contradicting the real LHS.

Proof: Divides by e^{i\pi\psi} to reduce to a real vs. negative-imaginary-part contradiction. Uses sin_neg_of_neg_of_neg_pi_lt to show each divided term has strictly negative imaginary part, then Finset.sum_neg for the sum.

🔗theorem
CategoryTheory.Triangulated.no_exp_decomp_below {ψ : ℝ} {n : ℕ}
  (hn : 0 < n) {m : ℝ} {b : Fin n → ℝ} (hb : ∀ (i : Fin n), 0 < b i)
  {θ : Fin n → ℝ} (hθ_lt : ∀ (i : Fin n), θ i < ψ)
  (hθ_gt : ∀ (i : Fin n), ψ - 1 < θ i)
  (heq :
    ↑m * Complex.exp (↑(Real.pi * ψ) * Complex.I) =
      ∑ i, ↑(b i) * Complex.exp (↑(Real.pi * θ i) * Complex.I)) :
  False
CategoryTheory.Triangulated.no_exp_decomp_below
  {ψ : ℝ} {n : ℕ} (hn : 0 < n) {m : ℝ}
  {b : Fin n → ℝ}
  (hb : ∀ (i : Fin n), 0 < b i)
  {θ : Fin n → ℝ}
  (hθ_lt : ∀ (i : Fin n), θ i < ψ)
  (hθ_gt : ∀ (i : Fin n), ψ - 1 < θ i)
  (heq :
    ↑m *
        Complex.exp
          (↑(Real.pi * ψ) * Complex.I) =
      ∑ i,
        ↑(b i) *
          Complex.exp
            (↑(Real.pi * θ i) *
              Complex.I)) :
  False

Something wrong, better idea? Suggest a change

13.1.8. no_exp_decomp_above🔗

Symmetric version: a real multiple of e^{i\pi\psi} cannot equal a sum of positive real multiples of e^{i\pi\theta_j} where all \theta_j lie strictly above \psi and below \psi + 1.

Proof: Identical structure to no_exp_decomp_below with reversed sign: each divided term has strictly positive imaginary part via sin_pos_of_pos_of_lt_pi, giving a positive sum that contradicts the real LHS.

🔗theorem
CategoryTheory.Triangulated.no_exp_decomp_above {ψ : ℝ} {n : ℕ}
  (hn : 0 < n) {m : ℝ} {b : Fin n → ℝ} (hb : ∀ (i : Fin n), 0 < b i)
  {θ : Fin n → ℝ} (hθ_gt : ∀ (i : Fin n), ψ < θ i)
  (hθ_lt : ∀ (i : Fin n), θ i < ψ + 1)
  (heq :
    ↑m * Complex.exp (↑(Real.pi * ψ) * Complex.I) =
      ∑ i, ↑(b i) * Complex.exp (↑(Real.pi * θ i) * Complex.I)) :
  False
CategoryTheory.Triangulated.no_exp_decomp_above
  {ψ : ℝ} {n : ℕ} (hn : 0 < n) {m : ℝ}
  {b : Fin n → ℝ}
  (hb : ∀ (i : Fin n), 0 < b i)
  {θ : Fin n → ℝ}
  (hθ_gt : ∀ (i : Fin n), ψ < θ i)
  (hθ_lt : ∀ (i : Fin n), θ i < ψ + 1)
  (heq :
    ↑m *
        Complex.exp
          (↑(Real.pi * ψ) * Complex.I) =
      ∑ i,
        ↑(b i) *
          Complex.exp
            (↑(Real.pi * θ i) *
              Complex.I)) :
  False

Something wrong, better idea? Suggest a change