9. StabilityCondition.Defs
Module BridgelandStability.StabilityCondition.Defs — 9 declarations (Structure, Definition)
9.1. CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap
Structure | BridgelandStability.StabilityCondition.Defs | Source | Open Issue
/-- A Bridgeland prestability condition with respect to a class map
`v : K₀(C) → Λ`. The central charge lives on `Λ`, and the ordinary ambient
charge is recovered by precomposition with `v`. -/
@[informal "Definition 1.1" "restated as Def 5.1" complete, informal "Definition 5.1" complete]
structure WithClassMap (v : K₀ C →+ Λ) where
/-- The underlying slicing. -/
slicing : Slicing C
/-- The central charge on the class lattice `Λ`. -/
Z : Λ →+ ℂ
/-- Compatibility (raw). Use `σ.compat` instead. -/
compat' : ∀ (φ : ℝ) (E : C), slicing.P φ E → ¬IsZero E →
∃ (m : ℝ), 0 < m ∧
Z (v (K₀.of C E)) = ↑m * Complex.exp (↑(Real.pi * φ) * Complex.I)
9.2. CategoryTheory.Triangulated.slicingDist
Definition | BridgelandStability.StabilityCondition.Defs | Source | Open Issue
/-- The Bridgeland generalized metric on slicings. For slicings `s₁` and `s₂`,
this is the supremum over all nonzero objects `E` of
`max(|φ₁⁺(E) - φ₂⁺(E)|, |φ₁⁻(E) - φ₂⁻(E)|)`. -/
def slicingDist (s₁ s₂ : Slicing C) : ℝ≥0∞ :=
⨆ (E : C) (hE : ¬IsZero E),
ENNReal.ofReal (max |s₁.phiPlus C E hE - s₂.phiPlus C E hE|
|s₁.phiMinus C E hE - s₂.phiMinus C E hE|)
9.3. CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.charge
Definition | BridgelandStability.StabilityCondition.Defs | Source | Open Issue
/-- The central charge evaluated at the class of `E`. This is `Z(v[E])`. -/
noncomputable abbrev WithClassMap.charge {v : K₀ C →+ Λ}
(σ : WithClassMap C v) (E : C) : ℂ :=
σ.Z (cl C v E)
9.4. CategoryTheory.Triangulated.StabilityCondition.WithClassMap
Structure | BridgelandStability.StabilityCondition.Defs | Source | Open Issue
/-- A Bridgeland stability condition with respect to a class map `v : K₀(C) → Λ`.
This is the locally-finite refinement of `PreStabilityCondition.WithClassMap`. -/
@[informal "Definition 5.7" complete]
structure WithClassMap (v : K₀ C →+ Λ)
extends PreStabilityCondition.WithClassMap C v where
/-- The slicing is locally finite. -/
locallyFinite : slicing.IsLocallyFinite C
9.5. CategoryTheory.Triangulated.stabSeminorm
Definition | BridgelandStability.StabilityCondition.Defs | Source | Open Issue
/-- The Bridgeland seminorm `‖U‖_σ` on `Hom(Λ, ℂ)`. For a class-map stability
condition `σ = (Z, P)` with class map `v : K₀(D) → Λ` and a group homomorphism
`U : Λ → ℂ`, this is `sup { |U(v[E])| / |Z(v[E])| : E is σ-semistable and nonzero }`.
When `v = id` (i.e., `Λ = K₀(D)`), this recovers Bridgeland's original seminorm. -/
def stabSeminorm {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v)
(U : Λ →+ ℂ) : ℝ≥0∞ :=
⨆ (E : C) (φ : ℝ) (_ : σ.slicing.P φ E) (_ : ¬IsZero E),
ENNReal.ofReal (‖U (cl C v E)‖ / ‖σ.charge E‖)
9.6. CategoryTheory.Triangulated.basisNhd
Definition | BridgelandStability.StabilityCondition.Defs | Source | Open Issue
/-- The basis neighborhood `B_ε(σ)` for the Bridgeland topology on `Stab_v(D)`. -/
def basisNhd {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) (ε : ℝ) :
Set (StabilityCondition.WithClassMap C v) :=
{τ | stabSeminorm C σ (τ.Z - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)) ∧
slicingDist C σ.slicing τ.slicing < ENNReal.ofReal ε}
9.7. CategoryTheory.Triangulated.StabilityCondition.WithClassMap.topologicalSpace
Definition | BridgelandStability.StabilityCondition.Defs | Source | Open Issue
/-- The Bridgeland topology on `Stab_v(D)`, generated by the basis neighborhoods
`B_ε(σ)` for all stability conditions `σ` and all `ε ∈ (0, 1/8)`.
This is the BLMNPS topology: the coarsest making both the charge map `σ ↦ σ.Z`
and the slicing map continuous. When `v = id`, this recovers Bridgeland's original
topology on `Stab(D)`. -/
instance StabilityCondition.WithClassMap.topologicalSpace {v : K₀ C →+ Λ} :
TopologicalSpace (StabilityCondition.WithClassMap C v) :=
TopologicalSpace.generateFrom
{U | ∃ (σ : StabilityCondition.WithClassMap C v) (ε : ℝ), 0 < ε ∧ ε < 1 / 8 ∧
U = basisNhd C σ ε}
9.8. CategoryTheory.Triangulated.StabilityCondition.WithClassMap.ComponentIndex
Definition | BridgelandStability.StabilityCondition.Defs | Source | Open Issue
/-- The connected-component index set for `Stab_v(D)`. -/
abbrev ComponentIndex (v : K₀ C →+ Λ) :=
_root_.ConnectedComponents (StabilityCondition.WithClassMap C v)
9.9. CategoryTheory.Triangulated.StabilityCondition.WithClassMap.Component
Definition | BridgelandStability.StabilityCondition.Defs | Source | Open Issue
/-- The type of `v`-relative stability conditions in a fixed connected component. -/
abbrev Component (v : K₀ C →+ Λ) (cc : StabilityCondition.WithClassMap.ComponentIndex C v) :=
{σ : StabilityCondition.WithClassMap C v // _root_.ConnectedComponents.mk σ = cc}