Bridgeland Stability Conditions

13.5. StabilityCondition: LocalHomeomorphism🔗

13.5.1. componentRep🔗

A chosen representative \sigma_0 of a connected component \Sigma \in \pi_0(\operatorname{Stab}_v(\mathcal{D})).

Construction: Obtained via Classical.choose from ConnectedComponents.exists_rep.

🔗def
CategoryTheory.Triangulated.componentRep.{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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C
        v)) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v
CategoryTheory.Triangulated.componentRep.{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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
        C v)) :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap
    C v

Something wrong, better idea? Suggest a change

13.5.2. mk_componentRep🔗

The chosen representative satisfies [\sigma_0] = \Sigma.

Proof: Immediate from Classical.choose_spec.

🔗theorem
CategoryTheory.Triangulated.mk_componentRep.{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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C
        v)) :
  ConnectedComponents.mk
      (CategoryTheory.Triangulated.componentRep C cc) =
    cc
CategoryTheory.Triangulated.mk_componentRep.{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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
        C v)) :
  ConnectedComponents.mk
      (CategoryTheory.Triangulated.componentRep
        C cc) =
    cc

Something wrong, better idea? Suggest a change

13.5.3. componentStabilityCondition🔗

The type of stability conditions in a fixed connected component \Sigma.

Construction: Defined as the subtype \{\, \sigma : \operatorname{Stab}_v(\mathcal{D}) \mid [\sigma] = \Sigma \,\}.

🔗def
CategoryTheory.Triangulated.componentStabilityCondition.{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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C
        v)) :
  Type (max 0 u u')
CategoryTheory.Triangulated.componentStabilityCondition.{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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
        C v)) :
  Type (max 0 u u')

Something wrong, better idea? Suggest a change

13.5.4. componentSeminormSubgroup🔗

Bridgeland's V(\Sigma): the \mathbb{C}-linear subspace of \operatorname{Hom}(\Lambda, \mathbb{C}) consisting of homomorphisms with finite Bridgeland seminorm relative to the chosen representative \sigma_0 \in \Sigma.

Construction: Defined as a Submodule ℂ (Λ →+ ℂ) whose carrier is finiteSeminormSubgroup C (componentRep C cc). Closure under \mathbb{C}-scalar multiplication uses stabSeminorm_smul_complex.

🔗def
CategoryTheory.Triangulated.componentSeminormSubgroup.{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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C
        v)) :
  Submodule ℂ (Λ →+ ℂ)
CategoryTheory.Triangulated.componentSeminormSubgroup.{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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
        C v)) :
  Submodule ℂ (Λ →+ ℂ)

Something wrong, better idea? Suggest a change

13.5.5. componentNorm🔗

The Bridgeland norm \|U\| = (\|U\|_{\sigma_0})_{\text{toReal}} on V(\Sigma), attached to the chosen representative.

Proof: Directly converts the \mathbb{R}_{\geq 0}^\infty-valued seminorm to a real norm via ENNReal.toReal.

🔗def
CategoryTheory.Triangulated.componentNorm.{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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C
        v)) :
  Norm ↥(CategoryTheory.Triangulated.componentSeminormSubgroup C cc)
CategoryTheory.Triangulated.componentNorm.{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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
        C v)) :
  Norm
    ↥(CategoryTheory.Triangulated.componentSeminormSubgroup
        C cc)

Something wrong, better idea? Suggest a change

13.5.6. componentAddGroupNorm🔗

The restricted Bridgeland seminorm is a genuine additive group norm on V(\Sigma): it satisfies the triangle inequality, is symmetric under negation, and the only element with norm zero is the zero homomorphism.

Construction: Constructs an AddGroupNorm from the Bridgeland seminorm, using stabSeminorm_add_le for the triangle inequality, stabSeminorm_neg for negation symmetry, and eq_zero_of_stabSeminorm_toReal_eq_zero for definiteness.

🔗def
CategoryTheory.Triangulated.componentAddGroupNorm.{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 →+ Λ}
  [Fact (Function.Surjective ⇑v)]
  (cc :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C
        v)) :
  AddGroupNorm
    ↥(CategoryTheory.Triangulated.componentSeminormSubgroup C cc)
CategoryTheory.Triangulated.componentAddGroupNorm.{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 →+ Λ}
  [Fact (Function.Surjective ⇑v)]
  (cc :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
        C v)) :
  AddGroupNorm
    ↥(CategoryTheory.Triangulated.componentSeminormSubgroup
        C cc)

Something wrong, better idea? Suggest a change

13.5.7. componentNormedAddCommGroup🔗

V(\Sigma) is a normed additive commutative group under the Bridgeland norm.

Proof: Obtained from componentAddGroupNorm via AddGroupNorm.toNormedAddCommGroup.

🔗def
CategoryTheory.Triangulated.componentNormedAddCommGroup.{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 →+ Λ}
  [Fact (Function.Surjective ⇑v)]
  (cc :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C
        v)) :
  NormedAddCommGroup
    ↥(CategoryTheory.Triangulated.componentSeminormSubgroup C cc)
CategoryTheory.Triangulated.componentNormedAddCommGroup.{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 →+ Λ}
  [Fact (Function.Surjective ⇑v)]
  (cc :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
        C v)) :
  NormedAddCommGroup
    ↥(CategoryTheory.Triangulated.componentSeminormSubgroup
        C cc)

Something wrong, better idea? Suggest a change

13.5.8. componentNormedSpace🔗

V(\Sigma) is a \mathbb{C}-normed space under the Bridgeland norm.

Proof: Verifies the NormedSpace.ofCore axioms: nonnegativity (trivial from \mathbb{R}_{\geq 0}^\infty), homogeneity (from stabSeminorm_smul_complex), triangle inequality (from componentAddGroupNorm), and definiteness (from eq_zero_of_stabSeminorm_toReal_eq_zero).

🔗def
CategoryTheory.Triangulated.componentNormedSpace.{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 →+ Λ}
  [Fact (Function.Surjective ⇑v)]
  (cc :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C
        v)) :
  NormedSpace ℂ
    ↥(CategoryTheory.Triangulated.componentSeminormSubgroup C cc)
CategoryTheory.Triangulated.componentNormedSpace.{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 →+ Λ}
  [Fact (Function.Surjective ⇑v)]
  (cc :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
        C v)) :
  NormedSpace ℂ
    ↥(CategoryTheory.Triangulated.componentSeminormSubgroup
        C cc)

Something wrong, better idea? Suggest a change

13.5.9. componentSeminormBall🔗

The seminorm ball in V(\Sigma): \{\, F \in V(\Sigma) : \|F - W\|_{\sigma_0} < r \,\}.

Construction: Defined directly in terms of the \mathbb{R}_{\geq 0}^\infty-valued Bridgeland seminorm.

🔗def
CategoryTheory.Triangulated.componentSeminormBall.{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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v))
  (W : ↥(CategoryTheory.Triangulated.componentSeminormSubgroup C cc))
  (r : ℝ) :
  Set ↥(CategoryTheory.Triangulated.componentSeminormSubgroup C cc)
CategoryTheory.Triangulated.componentSeminormBall.{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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
        C v))
  (W :
    ↥(CategoryTheory.Triangulated.componentSeminormSubgroup
        C cc))
  (r : ℝ) :
  Set
    ↥(CategoryTheory.Triangulated.componentSeminormSubgroup
        C cc)

Something wrong, better idea? Suggest a change

13.5.10. componentSeminormBall_eq_ball🔗

The seminorm balls coincide with the metric balls for the induced norm on V(\Sigma).

Proof: Unfolds both definitions and converts between \mathbb{R}_{\geq 0}^\infty and \mathbb{R} comparisons via ENNReal.ofReal_lt_ofReal_iff and ENNReal.ofReal_toReal.

🔗theorem
CategoryTheory.Triangulated.componentSeminormBall_eq_ball.{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 →+ Λ}
  [Fact (Function.Surjective ⇑v)]
  (cc :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v))
  (W : ↥(CategoryTheory.Triangulated.componentSeminormSubgroup C cc))
  {r : ℝ} (hr : 0 < r) :
  CategoryTheory.Triangulated.componentSeminormBall C cc W r =
    Metric.ball W r
CategoryTheory.Triangulated.componentSeminormBall_eq_ball.{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 →+ Λ}
  [Fact (Function.Surjective ⇑v)]
  (cc :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
        C v))
  (W :
    ↥(CategoryTheory.Triangulated.componentSeminormSubgroup
        C cc))
  {r : ℝ} (hr : 0 < r) :
  CategoryTheory.Triangulated.componentSeminormBall
      C cc W r =
    Metric.ball W r

Something wrong, better idea? Suggest a change

13.5.11. componentSeminormBasis🔗

The basis of seminorm balls defining a topology on V(\Sigma).

Construction: The set of sets of the form componentSeminormBall C cc W r with r > 0.

🔗def
CategoryTheory.Triangulated.componentSeminormBasis.{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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C
        v)) :
  Set
    (Set ↥(CategoryTheory.Triangulated.componentSeminormSubgroup C cc))
CategoryTheory.Triangulated.componentSeminormBasis.{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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
        C v)) :
  Set
    (Set
      ↥(CategoryTheory.Triangulated.componentSeminormSubgroup
          C cc))

Something wrong, better idea? Suggest a change

13.5.12. componentSeminormTopology🔗

The topology on V(\Sigma) generated by seminorm balls for one representative.

Construction: Defined as TopologicalSpace.generateFrom (componentSeminormBasis C cc).

🔗def
CategoryTheory.Triangulated.componentSeminormTopology.{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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C
        v)) :
  TopologicalSpace
    ↥(CategoryTheory.Triangulated.componentSeminormSubgroup C cc)
CategoryTheory.Triangulated.componentSeminormTopology.{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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
        C v)) :
  TopologicalSpace
    ↥(CategoryTheory.Triangulated.componentSeminormSubgroup
        C cc)

Something wrong, better idea? Suggest a change

13.5.13. isTopologicalBasis_componentSeminormBasis🔗

The seminorm-ball basis is a genuine topological basis for the norm topology on V(\Sigma).

Proof: Verifies that each seminorm ball is open in the norm topology (since it equals a metric ball) and that every neighborhood contains a seminorm ball (since metric balls are seminorm balls).

🔗theorem
CategoryTheory.Triangulated.isTopologicalBasis_componentSeminormBasis.{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 →+ Λ}
  [Fact (Function.Surjective ⇑v)]
  (cc :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C
        v)) :
  TopologicalSpace.IsTopologicalBasis
    (CategoryTheory.Triangulated.componentSeminormBasis C cc)
CategoryTheory.Triangulated.isTopologicalBasis_componentSeminormBasis.{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 →+ Λ}
  [Fact (Function.Surjective ⇑v)]
  (cc :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
        C v)) :
  TopologicalSpace.IsTopologicalBasis
    (CategoryTheory.Triangulated.componentSeminormBasis
      C cc)

Something wrong, better idea? Suggest a change

13.5.14. componentSeminormTopology_eq_normTopology🔗

The topology generated by seminorm balls agrees with the topology induced by the Bridgeland norm on V(\Sigma).

Proof: Follows from isTopologicalBasis_componentSeminormBasis and the characterization of a topology by its topological basis.

🔗theorem
CategoryTheory.Triangulated.componentSeminormTopology_eq_normTopology.{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 →+ Λ}
  [Fact (Function.Surjective ⇑v)]
  (cc :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C
        v)) :
  CategoryTheory.Triangulated.componentSeminormTopology C cc =
    inferInstance
CategoryTheory.Triangulated.componentSeminormTopology_eq_normTopology.{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 →+ Λ}
  [Fact (Function.Surjective ⇑v)]
  (cc :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
        C v)) :
  CategoryTheory.Triangulated.componentSeminormTopology
      C cc =
    inferInstance

Something wrong, better idea? Suggest a change

13.5.15. componentSeminorm_lt_top_of_mem_component🔗

Any element of V(\Sigma) has finite Bridgeland seminorm with respect to any stability condition in the same connected component.

Proof: Uses finiteSeminormSubgroup_eq_of_connected to transfer the finiteness from the chosen representative to any other member of the component.

🔗theorem
CategoryTheory.Triangulated.componentSeminorm_lt_top_of_mem_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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v))
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (hσ : ConnectedComponents.mk σ = cc)
  (U : ↥(CategoryTheory.Triangulated.componentSeminormSubgroup C cc)) :
  CategoryTheory.Triangulated.stabSeminorm C σ ↑U < ⊤
CategoryTheory.Triangulated.componentSeminorm_lt_top_of_mem_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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
        C v))
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (hσ : ConnectedComponents.mk σ = cc)
  (U :
    ↥(CategoryTheory.Triangulated.componentSeminormSubgroup
        C cc)) :
  CategoryTheory.Triangulated.stabSeminorm
      C σ ↑U <
    ⊤

Something wrong, better idea? Suggest a change

13.5.16. componentNorm_equivalent_of_mem_component🔗

The chosen norm on V(\Sigma) is equivalent to the Bridgeland norm coming from any representative \sigma \in \Sigma: there exist K, L > 0 with \|U\| \leq K \cdot \|U\|_\sigma and \|U\|_\sigma \leq L \cdot \|U\|.

Proof: Obtains domination constants from stabSeminorm_dominated_of_connected in both directions, then converts the \mathbb{R}_{\geq 0}^\infty bounds to real inequalities.

🔗theorem
CategoryTheory.Triangulated.componentNorm_equivalent_of_mem_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 →+ Λ}
  [Fact (Function.Surjective ⇑v)]
  (cc :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v))
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (hσ : ConnectedComponents.mk σ = cc) :
  ∃ K L,
    0 < K ∧
      0 < L ∧
        ∀
          (U :
            ↥(CategoryTheory.Triangulated.componentSeminormSubgroup C
                cc)),
          ‖U‖ ≤
              K *
                (CategoryTheory.Triangulated.stabSeminorm C σ
                    ↑U).toReal ∧
            (CategoryTheory.Triangulated.stabSeminorm C σ ↑U).toReal ≤
              L * ‖U‖
CategoryTheory.Triangulated.componentNorm_equivalent_of_mem_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 →+ Λ}
  [Fact (Function.Surjective ⇑v)]
  (cc :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
        C v))
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (hσ : ConnectedComponents.mk σ = cc) :
  ∃ K L,
    0 < K ∧
      0 < L ∧
        ∀
          (U :
            ↥(CategoryTheory.Triangulated.componentSeminormSubgroup
                C cc)),
          ‖U‖ ≤
              K *
                (CategoryTheory.Triangulated.stabSeminorm
                    C σ ↑U).toReal ∧
            (CategoryTheory.Triangulated.stabSeminorm
                  C σ ↑U).toReal ≤
              L * ‖U‖

Something wrong, better idea? Suggest a change

13.5.17. componentZ_mem🔗

For \sigma \in \Sigma, its central charge Z(\sigma) lies in V(\Sigma).

Proof: Uses finiteSeminormSubgroup_eq_of_connected to transfer Z_mem_finiteSeminormSubgroup from \sigma to the chosen representative.

🔗theorem
CategoryTheory.Triangulated.componentZ_mem.{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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v))
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (hσ : ConnectedComponents.mk σ = cc) :
  σ.Z ∈ CategoryTheory.Triangulated.componentSeminormSubgroup C cc
CategoryTheory.Triangulated.componentZ_mem.{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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
        C v))
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (hσ : ConnectedComponents.mk σ = cc) :
  σ.Z ∈
    CategoryTheory.Triangulated.componentSeminormSubgroup
      C cc

Something wrong, better idea? Suggest a change

13.5.18. componentZMap🔗

The central charge map restricted to a connected component and landing in V(\Sigma): \sigma \mapsto Z(\sigma) \in V(\Sigma).

Construction: Defined by \langle \sigma, h_\sigma \rangle \mapsto \langle \sigma.Z, \text{componentZ\_mem}(\sigma, h_\sigma) \rangle.

🔗def
CategoryTheory.Triangulated.componentZMap.{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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C
        v)) :
  CategoryTheory.Triangulated.componentStabilityCondition C cc →
    ↥(CategoryTheory.Triangulated.componentSeminormSubgroup C cc)
CategoryTheory.Triangulated.componentZMap.{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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
        C v)) :
  CategoryTheory.Triangulated.componentStabilityCondition
      C cc →
    ↥(CategoryTheory.Triangulated.componentSeminormSubgroup
        C cc)

Something wrong, better idea? Suggest a change

13.5.19. ComponentTopologicalLinearLocalModel🔗

A reusable non-existential package for Bridgeland's Theorem 1.2 on a fixed connected component \Sigma. Bundles: (1) the complex-linear charge space V(\Sigma), (2) a NormedAddCommGroup and NormedSpace \mathbb{C} instance on it, (3) the proof that all central charges in \Sigma lie in V(\Sigma), and (4) the proof that the restricted charge map is a local homeomorphism.

Construction: A structure with fields V, instNormedAddCommGroup, instNormedSpace, mem_charge, and isLocalHomeomorph_chargeMap.

🔗structure
CategoryTheory.Triangulated.ComponentTopologicalLinearLocalModel.{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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C
        v)) :
  Type u'
CategoryTheory.Triangulated.ComponentTopologicalLinearLocalModel.{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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
        C v)) :
  Type u'

Constructor

CategoryTheory.Triangulated.ComponentTopologicalLinearLocalModel.mk.{v, u, u'}

Fields

V : Submodule ℂ (Λ →+ ℂ)

The chosen complex-linear charge space V(Σ) for this connected component.

instNormedAddCommGroup : NormedAddCommGroup ↥self.V
instNormedSpace : NormedSpace ℂ ↥self.V
mem_charge : ∀ (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v), ConnectedComponents.mk σ = cc → σ.Z ∈ self.V
isLocalHomeomorph_chargeMap : IsLocalHomeomorph fun x =>
  match x with
  | ⟨σ, hσ⟩ => ⟨σ.Z, ⋯⟩

Something wrong, better idea? Suggest a change

13.5.20. chargeMap🔗

The restricted central charge map attached to a component local model: \sigma \mapsto Z(\sigma) \in V.

Construction: Defined by \langle \sigma, h_\sigma \rangle \mapsto \langle \sigma.Z, M.\text{mem\_charge}(\sigma, h_\sigma) \rangle.

🔗def
CategoryTheory.Triangulated.ComponentTopologicalLinearLocalModel.chargeMap.{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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)}
  (M :
    CategoryTheory.Triangulated.ComponentTopologicalLinearLocalModel C
      cc) :
  CategoryTheory.Triangulated.componentStabilityCondition C cc → ↥M.V
CategoryTheory.Triangulated.ComponentTopologicalLinearLocalModel.chargeMap.{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 :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
        C v)}
  (M :
    CategoryTheory.Triangulated.ComponentTopologicalLinearLocalModel
      C cc) :
  CategoryTheory.Triangulated.componentStabilityCondition
      C cc →
    ↥M.V

Something wrong, better idea? Suggest a change

13.5.21. componentTopologicalLinearLocalModel🔗

Bridgeland's Theorem 1.2: the canonical componentwise local linear model. For each connected component \Sigma of \operatorname{Stab}_v(\mathcal{D}), the central charge map \sigma \mapsto Z(\sigma) is a local homeomorphism from \Sigma to the complex normed space V(\Sigma). Specializing to v = \operatorname{id} recovers Bridgeland's Theorem 1.2; specializing to the numerical quotient recovers Corollary 1.3.

Construction: Constructs a ComponentTopologicalLinearLocalModel by assembling the seminorm topology agreement (componentSeminormTopology_eq_normTopology), continuity of the charge map (Proposition 6.3 + Lemma 6.2), injectivity (Lemma 6.4), and openness (Theorem 7.1 + Lemma 6.2 reverse comparison).

🔗def
CategoryTheory.Triangulated.componentTopologicalLinearLocalModel.{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 →+ Λ}
  [Fact (Function.Surjective ⇑v)]
  (cc :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C
        v)) :
  CategoryTheory.Triangulated.ComponentTopologicalLinearLocalModel C cc
CategoryTheory.Triangulated.componentTopologicalLinearLocalModel.{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 →+ Λ}
  [Fact (Function.Surjective ⇑v)]
  (cc :
    ConnectedComponents
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
        C v)) :
  CategoryTheory.Triangulated.ComponentTopologicalLinearLocalModel
    C cc

Something wrong, better idea? Suggest a change

13.5.22. centralChargeIsLocalHomeomorphOnConnectedComponents🔗

[Theorem 1.2]

Bridgeland's Theorem 1.2: for each connected component \Sigma of the stability space \mathrm{Stab}(\mathcal{C}), the central charge map Z : \Sigma \to V(\Sigma) is a local homeomorphism onto a linear subspace V(\Sigma) \subset \mathrm{Hom}(\Lambda, \mathbb{C}) equipped with a natural normed topology.

Proof: The proof assembles the ComponentTopologicalLinearLocalModel for each connected component, which packages: the normed subspace V(\Sigma), the fact that every central charge lands in V(\Sigma), and the local homeomorphism property of the charge map (proved via a seminorm ball argument showing openness and continuity of Z).

🔗theorem
CategoryTheory.Triangulated.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 →+ Λ}
  [Fact (Function.Surjective ⇑v)] :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.CentralChargeIsLocalHomeomorphOnConnectedComponents
    C
CategoryTheory.Triangulated.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 →+ Λ}
  [Fact (Function.Surjective ⇑v)] :
  CategoryTheory.Triangulated.StabilityCondition.WithClassMap.CentralChargeIsLocalHomeomorphOnConnectedComponents
    C

Something wrong, better idea? Suggest a change