Bridgeland Stability Conditions

11. NumericalStabilityManifold🔗

11.1. classMapChargeSpace_finiteDimensional🔗

When the class lattice \Lambda is finitely generated as an abelian group, the charge space \operatorname{Hom}_{\mathbb{Z}}(\Lambda, \mathbb{C}) is finite-dimensional over \mathbb{C}.

Proof: Chooses a surjection \mathbb{Z}^n \twoheadrightarrow \Lambda from the finite generation hypothesis. Precomposition gives an injection \operatorname{Hom}(\Lambda, \mathbb{C}) \hookrightarrow operatorname(Hom)(mathbb(Z)^n, mathbb(C)) cong mathbb(C)^n$, and finite-dimensionality follows from FiniteDimensional.of_injective.

🔗theorem
CategoryTheory.Triangulated.classMapChargeSpace_finiteDimensional.{u'}
  (Λ : Type u') [AddCommGroup Λ] [AddGroup.FG Λ] :
  FiniteDimensional ℂ (Λ →+ ℂ)
CategoryTheory.Triangulated.classMapChargeSpace_finiteDimensional.{u'}
  (Λ : Type u') [AddCommGroup Λ]
  [AddGroup.FG Λ] :
  FiniteDimensional ℂ (Λ →+ ℂ)

Something wrong, better idea? Suggest a change

11.2. exists_chartedSpace_and_hasGroupoid_idRestr_of_isLocalHomeomorph_to_complex_model🔗

If f : M \to E is a local homeomorphism into a normed space, then M admits a charted space structure modeled on E whose transition maps lie in the identity-restriction groupoid.

Proof: For each x \in M, Classical.choose extracts a chart from the local homeomorphism hypothesis. The atlas is the range of these charts. Since all charts agree with f, the transition maps e_y^{-1} \circ e_x are the identity on their domain, hence belong to idRestrGroupoid.

🔗theorem
CategoryTheory.Triangulated.exists_chartedSpace_and_hasGroupoid_idRestr_of_isLocalHomeomorph_to_complex_model.{u_1,
    u_2}
  {E : Type u_1} {M : Type u_2} [NormedAddCommGroup E]
  [TopologicalSpace M] (f : M → E) (hf : IsLocalHomeomorph f) :
  ∃ x, HasGroupoid M idRestrGroupoid
CategoryTheory.Triangulated.exists_chartedSpace_and_hasGroupoid_idRestr_of_isLocalHomeomorph_to_complex_model.{u_1,
    u_2}
  {E : Type u_1} {M : Type u_2}
  [NormedAddCommGroup E]
  [TopologicalSpace M] (f : M → E)
  (hf : IsLocalHomeomorph f) :
  ∃ x, HasGroupoid M idRestrGroupoid

Something wrong, better idea? Suggest a change

11.3. isManifold_of_hasGroupoid_idRestr🔗

A charted space whose structure groupoid is contained in the identity-restriction groupoid is automatically a smooth (in fact C^\infty) complex manifold.

Proof: The identity-restriction groupoid is contained in \operatorname{contDiff}^\infty by closedUnderRestriction_iff_id_le. The result follows from hasGroupoid_of_le and IsManifold.mk'.

🔗theorem
CategoryTheory.Triangulated.isManifold_of_hasGroupoid_idRestr.{u_1, u_2}
  {E : Type u_1} {M : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E]
  [TopologicalSpace M] [ChartedSpace E M]
  [HasGroupoid M idRestrGroupoid] :
  IsManifold (modelWithCornersSelf ℂ E) ⊤ M
CategoryTheory.Triangulated.isManifold_of_hasGroupoid_idRestr.{u_1,
    u_2}
  {E : Type u_1} {M : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℂ E]
  [TopologicalSpace M] [ChartedSpace E M]
  [HasGroupoid M idRestrGroupoid] :
  IsManifold (modelWithCornersSelf ℂ E) ⊤
    M

Something wrong, better idea? Suggest a change

11.4. exists_chartedSpace_and_complexManifold_of_isLocalHomeomorph_to_complex_model🔗

If f : M \to E is a local homeomorphism into a finite-dimensional complex normed space, then M admits the structure of a complex manifold modeled on E. This is the abstract topological-to-manifold bridge for Corollary 1.3.

Proof: Combines exists_chartedSpace_and_hasGroupoid_idRestr_of_isLocalHomeomorph_to_complex_model with isManifold_of_hasGroupoid_idRestr.

🔗theorem
CategoryTheory.Triangulated.exists_chartedSpace_and_complexManifold_of_isLocalHomeomorph_to_complex_model.{u_1,
    u_2}
  {E : Type u_1} {M : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E]
  [TopologicalSpace M] (f : M → E) (hf : IsLocalHomeomorph f) :
  ∃ x, IsManifold (modelWithCornersSelf ℂ E) ⊤ M
CategoryTheory.Triangulated.exists_chartedSpace_and_complexManifold_of_isLocalHomeomorph_to_complex_model.{u_1,
    u_2}
  {E : Type u_1} {M : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℂ E]
  [TopologicalSpace M] (f : M → E)
  (hf : IsLocalHomeomorph f) :
  ∃ x,
    IsManifold (modelWithCornersSelf ℂ E)
      ⊤ M

Something wrong, better idea? Suggest a change

11.5. WithClassMap.existsComplexManifoldOnConnectedComponent🔗

[Corollary 1.3] class-map generalization; manifold consequence only

Bridgeland's Corollary 1.3 for \operatorname{Stab}_v(\mathcal{D}). Each connected component of the class-map stability space carries the structure of a complex manifold modeled on a finite-dimensional complex normed space, provided v is surjective and \Lambda is finitely generated.

Proof: The local model from Theorem 1.2 (componentTopologicalLinearLocalModel) gives a local homeomorphism into V(\Sigma). Since \Lambda has finite rank, \operatorname{Hom}(\Lambda, \mathbb{C}) is finite-dimensional (classMapChargeSpace_finiteDimensional), hence so is the submodule V(\Sigma). Feeding this into exists_chartedSpace_and_complexManifold_of_isLocalHomeomorph_to_complex_model completes the proof.

🔗theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.existsComplexManifoldOnConnectedComponent.{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 Λ] [AddGroup.FG Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  [Fact (Function.Surjective ⇑v)]
  (cc :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.ComponentIndex
      C v) :
  ∃ E x x_1,
    ∃ (_ : FiniteDimensional ℂ E),
      ∃ x_3,
        IsManifold (modelWithCornersSelf ℂ E) ⊤
          (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.Component
            C v cc)
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.existsComplexManifoldOnConnectedComponent.{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 Λ]
  [AddGroup.FG Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  [Fact (Function.Surjective ⇑v)]
  (cc :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.ComponentIndex
      C v) :
  ∃ E x x_1,
    ∃ (_ : FiniteDimensional ℂ E),
      ∃ x_3,
        IsManifold
          (modelWithCornersSelf ℂ E) ⊤
          (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.Component
            C v cc)

Something wrong, better idea? Suggest a change

11.6. NumericalStabilityCondition.existsComplexManifoldOnConnectedComponent🔗

[Corollary 1.3] complex manifold conclusion only

Corollary 1.3 (Bridgeland 2007). Each connected component of the space of numerical stability conditions on a triangulated category \mathcal{C} is a finite-dimensional complex manifold. Here \mathcal{C} is a k-linear triangulated category of finite type that is numerically finite, and the stability conditions are numerical in the sense that they factor through the numerical Grothendieck group.

Proof: The proof (currently sorry) should construct local charts by showing that the forgetful map from stability conditions to the space of central charges (a finite-dimensional complex vector space) is a local homeomorphism on each connected component, using the deformation result (Theorem 1.2) and the support property.

🔗theorem
CategoryTheory.Triangulated.NumericalStabilityCondition.existsComplexManifoldOnConnectedComponent.{w,
    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]
  (k : Type w) [Field k] [CategoryTheory.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType k C]
  [CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C 1)]
  [CategoryTheory.Triangulated.NumericallyFinite k C]
  (cc :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.ComponentIndex
      C (CategoryTheory.Triangulated.numericalQuotientMap k C)) :
  ∃ E x x_1,
    ∃ (_ : FiniteDimensional ℂ E),
      ∃ x_3,
        IsManifold (modelWithCornersSelf ℂ E) ⊤
          (CategoryTheory.Triangulated.NumericalComponent k C cc)
CategoryTheory.Triangulated.NumericalStabilityCondition.existsComplexManifoldOnConnectedComponent.{w,
    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]
  (k : Type w) [Field k]
  [CategoryTheory.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType
      k C]
  [CategoryTheory.Functor.Linear k
      (CategoryTheory.shiftFunctor C 1)]
  [CategoryTheory.Triangulated.NumericallyFinite
      k C]
  (cc :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.ComponentIndex
      C
      (CategoryTheory.Triangulated.numericalQuotientMap
        k C)) :
  ∃ E x x_1,
    ∃ (_ : FiniteDimensional ℂ E),
      ∃ x_3,
        IsManifold
          (modelWithCornersSelf ℂ E) ⊤
          (CategoryTheory.Triangulated.NumericalComponent
            k C cc)

Something wrong, better idea? Suggest a change