Bridgeland Stability Conditions — Ext Theorems and Phase Rigidity

Extensionality theorems for stability conditions, phase rigidity (Lemma 6.4 sublemma), and the exponential decomposition impossibility lemmas. The core structures, topology, and seminorm are in StabilityCondition.Defs.

References

• Bridgeland, "Stability conditions on triangulated categories", Annals of Math. 2007

Ext theorems

theorem CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.ext (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} {σ τ : WithClassMap C v} (hs : σ.slicing = τ.slicing) (hZ : σ.Z = τ.Z) : σ = τ

theorem CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.ext_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} {σ τ : WithClassMap C v} : σ = τ ↔ σ.slicing = τ.slicing ∧ σ.Z = τ.Z

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.ext (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} {σ τ : WithClassMap C v} (hs : σ.slicing = τ.slicing) (hZ : σ.Z = τ.Z) : σ = τ

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.ext_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} {σ τ : WithClassMap C v} : σ = τ ↔ σ.slicing = τ.slicing ∧ σ.Z = τ.Z

theorem CategoryTheory.Triangulated.preStabilityCondition_compat_apply (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : PreStabilityCondition.WithClassMap C v) (φ : ℝ) (E : C) (hE : σ.slicing.P φ E) (hNZ : ¬Limits.IsZero E) : ∃ (m : ℝ), 0 < m ∧ σ.charge E = ↑m * Complex.exp (↑(Real.pi * φ) * Complex.I)

The ordinary compatibility statement for a prestability condition, with the identity class map simplified away.

Phase rigidity for same central charge

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.phase_eq_of_same_Z (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ τ : WithClassMap C v) (hZ : σ.Z = τ.Z) {E : C} {φ ψ : ℝ} (hσ : σ.slicing.P φ E) (hτ : τ.slicing.P ψ E) (hE : ¬Limits.IsZero E) (habs : |φ - ψ| < 2) : φ = ψ

Lemma 6.4 sublemma. If two stability conditions σ and τ have the same central charge Z, and a nonzero object E is σ-semistable of phase φ and τ-semistable of phase ψ with |φ - ψ| < 2, then φ = ψ.

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 : Fin n, ↑(b i) * Complex.exp (↑(Real.pi * θ i) * Complex.I)) : False

A real multiple of exp(iπψ) cannot equal a sum of positive real multiples of exp(iπθⱼ) where all θⱼ lie strictly below ψ and above ψ - 1. The proof takes the imaginary part after dividing by exp(iπψ): since sin(π(θⱼ - ψ)) < 0 for all j, the imaginary part of the sum is strictly negative, contradicting 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 : Fin n, ↑(b i) * Complex.exp (↑(Real.pi * θ i) * Complex.I)) : False

Symmetric version: a real multiple of exp(iπψ) cannot equal a sum of positive real multiples of exp(iπθⱼ) where all θⱼ lie strictly above ψ and below ψ + 1.