BridgelandStability Comparator Manual

10.Β StabilityCondition.DefsπŸ”—

Module BridgelandStability.StabilityCondition.Defs β€” 9 declarations (Structure, Definition)

10.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 5.1"] 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)

10.2.Β 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)

10.3.Β 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|)

10.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"] structure WithClassMap (v : Kβ‚€ C β†’+ Ξ›) extends PreStabilityCondition.WithClassMap C v where /-- The slicing is locally finite. -/ locallyFinite : slicing.IsLocallyFinite C

10.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β€–)

10.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 Ξ΅}

10.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 Οƒ Ξ΅}

10.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)

10.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}