13.4. StabilityCondition: Defs🔗

13.4.1. PreStabilityCondition.WithClassMap🔗

[Definition 5.1]

A Bridgeland prestability condition on a triangulated category \mathcal{C} with respect to a class map v \colon K_0(\mathcal{C}) \to \Lambda consists of a slicing \mathcal{P} together with a group homomorphism Z \colon \Lambda \to \mathbb{C} (the central charge) such that for every nonzero \mathcal{P}(\phi)-semistable object E, one has Z(v([E])) = m \cdot e^{i\pi\phi} for some m > 0. This is Definition 5.1 of Bridgeland (2007), lifted to an arbitrary class lattice.

Construction: The structure packages the slicing, the central charge on \Lambda, and the compatibility proof that the image of each semistable class lies on the correct ray in \mathbb{C}.

structure

CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.{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 →+ Λ) : Type (max u u')
CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.{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 →+
      Λ) :
  Type (max u u')

Constructor

CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.mk.{v, u, u'}

Fields

slicing : CategoryTheory.Triangulated.Slicing C

The underlying slicing.

Z : Λ →+ ℂ

The central charge on the class lattice Λ.

compat' : ∀ (φ : ℝ) (E : C),
  self.slicing.P φ E →
    ¬CategoryTheory.Limits.IsZero E →
      ∃ m, 0 < m ∧ self.Z (v (CategoryTheory.Triangulated.K₀.of C E)) = ↑m * Complex.exp (↑(Real.pi * φ) * Complex.I)

Compatibility (raw). Use σ.compat instead.

Something wrong, better idea? Suggest a change

13.4.2. charge🔗

def

CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.charge.{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) : ℂ
CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.charge.{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) : ℂ

Something wrong, better idea? Suggest a change

13.4.3. charge_def🔗

theorem

CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.charge_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 →+ Λ}
  (σ :
    CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap C v)
  (E : C) : σ.charge E = σ.Z (CategoryTheory.Triangulated.cl C v E)
CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.charge_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 →+ Λ}
  (σ :
    CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap
      C v)
  (E : C) :
  σ.charge E =
    σ.Z
      (CategoryTheory.Triangulated.cl C v
        E)

Something wrong, better idea? Suggest a change

13.4.4. compat🔗

theorem

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

Something wrong, better idea? Suggest a change

13.4.5. charge_isZero🔗

theorem

CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.charge_isZero.{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 : CategoryTheory.Limits.IsZero E) : σ.charge E = 0
CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.charge_isZero.{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 : CategoryTheory.Limits.IsZero E) :
  σ.charge E = 0

Something wrong, better idea? Suggest a change

13.4.6. charge_congr🔗

theorem

CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.charge_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 →+ Λ}
  {σ τ :
    CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap C v}
  (h : σ.Z = τ.Z) (E : C) : σ.charge E = τ.charge E
CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.charge_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 →+ Λ}
  {σ τ :
    CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap
      C v}
  (h : σ.Z = τ.Z) (E : C) :
  σ.charge E = τ.charge E

Something wrong, better idea? Suggest a change

13.4.7. charge_postnikovTower_eq_sum🔗

theorem

CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.charge_postnikovTower_eq_sum.{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} (P : CategoryTheory.Triangulated.PostnikovTower C E) :
  σ.charge E = ∑ i, σ.charge (P.factor i)
CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.charge_postnikovTower_eq_sum.{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}
  (P :
    CategoryTheory.Triangulated.PostnikovTower
      C E) :
  σ.charge E = ∑ i, σ.charge (P.factor i)

Something wrong, better idea? Suggest a change

13.4.8. PreStabilityCondition🔗

A Bridgeland prestability condition on \mathcal{C}, defined as the specialization of PreStabilityCondition.WithClassMap to the identity class map \operatorname{id} \colon K_0(\mathcal{C}) \to K_0(\mathcal{C}).

Construction: An abbreviation for PreStabilityCondition.WithClassMap C (AddMonoidHom.id (K₀ C)).

def

CategoryTheory.Triangulated.PreStabilityCondition.{v, 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
CategoryTheory.Triangulated.PreStabilityCondition.{v,
    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

Something wrong, better idea? Suggest a change

13.4.9. StabilityCondition.WithClassMap🔗

[Definition 5.7]

A Bridgeland stability condition on a triangulated category \mathcal{C} with respect to a class map v \colon K_0(\mathcal{C}) \to \Lambda is a prestability condition whose underlying slicing is locally finite: for every \phi \in \mathbb{R} and every bounded interval of phases, every object in the corresponding quasi-abelian category has finite length. This is Definition 5.3 of Bridgeland (2007).

Construction: Extends PreStabilityCondition.WithClassMap with a proof that the slicing satisfies the IsLocallyFinite condition.

structure

CategoryTheory.Triangulated.StabilityCondition.WithClassMap.{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 →+ Λ) : Type (max u u')
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.{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 →+
      Λ) :
  Type (max u u')

Constructor

CategoryTheory.Triangulated.StabilityCondition.WithClassMap.mk.{v, u, u'}

Extends

CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap C v

Fields

slicing : CategoryTheory.Triangulated.Slicing C

Inherited from

CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap C v

Z : Λ →+ ℂ

Inherited from

CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap C v

compat' : ∀ (φ : ℝ) (E : C),
  self.slicing.P φ E →
    ¬CategoryTheory.Limits.IsZero E →
      ∃ m, 0 < m ∧ self.Z (v (CategoryTheory.Triangulated.K₀.of C E)) = ↑m * Complex.exp (↑(Real.pi * φ) * Complex.I)

Inherited from

CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap C v

locallyFinite : CategoryTheory.Triangulated.Slicing.IsLocallyFinite C self.slicing

The slicing is locally finite.

Something wrong, better idea? Suggest a change

13.4.10. StabilityCondition🔗

A Bridgeland stability condition on \mathcal{C}, the specialization of StabilityCondition.WithClassMap to the identity class map. This is the classical object \operatorname{Stab}(\mathcal{C}) from Bridgeland (2007).

Construction: An abbreviation for StabilityCondition.WithClassMap C (AddMonoidHom.id (K₀ C)).

def

CategoryTheory.Triangulated.StabilityCondition.{v, 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
CategoryTheory.Triangulated.StabilityCondition.{v,
    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

Something wrong, better idea? Suggest a change

13.4.11. stabilityCondition_compat_apply🔗

The compatibility condition for a stability condition with identity class map: for every nonzero \mathcal{P}(\phi)-semistable object E, the central charge satisfies Z([E]) = m \cdot e^{i\pi\phi} for some m > 0.

Proof: Immediate by simplifying the general compatibility statement when v = \operatorname{id}.

theorem

CategoryTheory.Triangulated.stabilityCondition_compat_apply.{v, 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]
  (σ : CategoryTheory.Triangulated.StabilityCondition C) (φ : ℝ) (E : C)
  (hE : σ.slicing.P φ E) (hNZ : ¬CategoryTheory.Limits.IsZero E) :
  ∃ m,
    0 < m ∧
      σ.Z (CategoryTheory.Triangulated.K₀.of C E) =
        ↑m * Complex.exp (↑(Real.pi * φ) * Complex.I)
CategoryTheory.Triangulated.stabilityCondition_compat_apply.{v,
    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]
  (σ :
    CategoryTheory.Triangulated.StabilityCondition
      C)
  (φ : ℝ) (E : C) (hE : σ.slicing.P φ E)
  (hNZ :
    ¬CategoryTheory.Limits.IsZero E) :
  ∃ m,
    0 < m ∧
      σ.Z
          (CategoryTheory.Triangulated.K₀.of
            C E) =
        ↑m *
          Complex.exp
            (↑(Real.pi * φ) * Complex.I)

Something wrong, better idea? Suggest a change

13.4.12. im_ofReal_mul_exp_mul_exp_neg🔗

The phase rotation identity: \operatorname{Im}(m \cdot e^{i\pi\psi} \cdot e^{-i\pi\phi}) = m \cdot \sin(\pi(\psi - \phi)). This factorization underlies all sign arguments in Bridgeland's deformation theory (Lemmas 6.1--6.4).

Proof: Combines the exponentials via e^{i\pi\psi} \cdot e^{-i\pi\phi} = e^{i\pi(\psi - \phi)}, then extracts the imaginary part using Euler's formula.

theorem

CategoryTheory.Triangulated.im_ofReal_mul_exp_mul_exp_neg (m ψ φ : ℝ) :
  (↑m * Complex.exp (↑(Real.pi * ψ) * Complex.I) *
        Complex.exp (-(↑(Real.pi * φ) * Complex.I))).im =
    m * Real.sin (Real.pi * (ψ - φ))
CategoryTheory.Triangulated.im_ofReal_mul_exp_mul_exp_neg
  (m ψ φ : ℝ) :
  (↑m *
          Complex.exp
            (↑(Real.pi * ψ) * Complex.I) *
        Complex.exp
          (-(↑(Real.pi * φ) *
              Complex.I))).im =
    m * Real.sin (Real.pi * (ψ - φ))

Something wrong, better idea? Suggest a change

13.4.13. slicingDist🔗

The Bridgeland generalized metric on slicings. For slicings \mathcal{P}_1 and \mathcal{P}_2, this is d(\mathcal{P}_1, \mathcal{P}_2) = \sup_{E \neq 0} \max(|\phi_1^+(E) - \phi_2^+(E)|,\, |\phi_1^-(E) - \phi_2^-(E)|) where \phi^{\pm} denote the maximum/minimum HN phases.

Construction: Defined as an \mathbb{R}_{\geq 0}^{\infty}-valued supremum over all nonzero objects of the maximum of the absolute phase differences.

def

CategoryTheory.Triangulated.slicingDist.{v, 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]
  (s₁ s₂ : CategoryTheory.Triangulated.Slicing C) : ENNReal
CategoryTheory.Triangulated.slicingDist.{v,
    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]
  (s₁ s₂ :
    CategoryTheory.Triangulated.Slicing
      C) :
  ENNReal

Something wrong, better idea? Suggest a change

13.4.14. stabSeminorm🔗

The Bridgeland seminorm \|U\|_\sigma on \operatorname{Hom}(\Lambda, \mathbb{C}). For a stability condition \sigma = (Z, \mathcal{P}) with class map v and a group homomorphism U \colon \Lambda \to \mathbb{C}, this is \|U\|_\sigma = \sup \{\, |U(v[E])| / |Z(v[E])| : E \text{ is } \sigma\text{-semistable and nonzero}\,\}.

Construction: Defined as an \mathbb{R}_{\geq 0}^{\infty}-valued supremum indexed over objects, phases, semistability witnesses, and nonzero witnesses.

def

CategoryTheory.Triangulated.stabSeminorm.{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)
  (U : Λ →+ ℂ) : ENNReal
CategoryTheory.Triangulated.stabSeminorm.{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)
  (U : Λ →+ ℂ) : ENNReal

Something wrong, better idea? Suggest a change

13.4.15. basisNhd🔗

The basis neighborhood B_\varepsilon(\sigma) for the Bridgeland topology on \operatorname{Stab}_v(\mathcal{D}): B_\varepsilon(\sigma) = \{\, \tau : \|\tau.Z - \sigma.Z\|_\sigma < \sin(\pi\varepsilon) \text{ and } d(\mathcal{P}_\sigma, \mathcal{P}_\tau) < \varepsilon \,\}.

Construction: Defined as the set of stability conditions satisfying both the seminorm bound on the central charge difference and the slicing distance bound.

def

CategoryTheory.Triangulated.basisNhd.{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)
  (ε : ℝ) :
  Set (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
CategoryTheory.Triangulated.basisNhd.{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)
  (ε : ℝ) :
  Set
    (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)

Something wrong, better idea? Suggest a change

13.4.16. topologicalSpace🔗

The Bridgeland topology on \operatorname{Stab}_v(\mathcal{D}), generated by \{\, B_\varepsilon(\sigma) : \sigma \in \operatorname{Stab}_v(\mathcal{D}),\, 0 < \varepsilon < 1/8 \,\}. This is the BLMNPS topology: the coarsest making both the charge map \sigma \mapsto \sigma.Z and the slicing map continuous.

Proof: Constructed via TopologicalSpace.generateFrom applied to the family of basis neighborhoods.

def

CategoryTheory.Triangulated.StabilityCondition.WithClassMap.topologicalSpace.{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 →+ Λ} :
  TopologicalSpace
    (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.topologicalSpace.{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 →+
      Λ} :
  TopologicalSpace
    (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)

Something wrong, better idea? Suggest a change

13.4.17. ComponentIndex🔗

The set of connected components of \operatorname{Stab}_v(\mathcal{D}), i.e., the quotient \pi_0(\operatorname{Stab}_v(\mathcal{D})).

Construction: An abbreviation for ConnectedComponents (StabilityCondition.WithClassMap C v).

def

CategoryTheory.Triangulated.StabilityCondition.WithClassMap.ComponentIndex.{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 →+ Λ) : Type (max u' u)
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.ComponentIndex.{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 →+
      Λ) :
  Type (max u' u)

Something wrong, better idea? Suggest a change

13.4.18. Component🔗

The type of stability conditions in a fixed connected component \Sigma of \operatorname{Stab}_v(\mathcal{D}).

Construction: Defined as the subtype of stability conditions whose ConnectedComponents.mk equals the given component index.

def

CategoryTheory.Triangulated.StabilityCondition.WithClassMap.Component.{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 →+ Λ)
  (cc :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.ComponentIndex
      C v) :
  Type (max 0 u u')
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.Component.{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 →+ Λ)
  (cc :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.ComponentIndex
      C v) :
  Type (max 0 u u')

Something wrong, better idea? Suggest a change

13.4.19. CentralChargeIsLocalHomeomorphOnConnectedComponents🔗

[Theorem 1.2] statement only; proof is componentTopologicalLinearLocalModel

The Bridgeland Theorem 1.2 statement in existential form: for every connected component \Sigma of \operatorname{Stab}_v(\mathcal{D}), there exists a complex normed subspace V(\Sigma) \subseteq \operatorname{Hom}(\Lambda, \mathbb{C}) such that every central charge in \Sigma lies in V(\Sigma), and the restricted central charge map \sigma \mapsto Z(\sigma) is a local homeomorphism from \Sigma onto V(\Sigma).

Construction: A proposition quantifying over component indices, asserting existence of a \mathbb{C}-normed submodule and an IsLocalHomeomorph instance.

def

CategoryTheory.Triangulated.StabilityCondition.WithClassMap.CentralChargeIsLocalHomeomorphOnConnectedComponents.{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 →+ Λ} : Prop
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.CentralChargeIsLocalHomeomorphOnConnectedComponents.{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 →+
      Λ} :
  Prop

Something wrong, better idea? Suggest a change