Local Homeomorphism of the Central Charge #
Component normed space construction, charge map structure, and the proof of Bridgeland's Theorem 1.2: the central charge map is a local homeomorphism on each connected component of Stab(D).
noncomputable def
CategoryTheory.Triangulated.componentRep
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
(cc : ConnectedComponents (StabilityCondition.WithClassMap C v))
:
A chosen representative of a connected component of StabilityCondition.WithClassMap C v.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Triangulated.mk_componentRep
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
(cc : ConnectedComponents (StabilityCondition.WithClassMap C v))
:
@[reducible, inline]
abbrev
CategoryTheory.Triangulated.componentStabilityCondition
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
(cc : ConnectedComponents (StabilityCondition.WithClassMap C v))
:
Type (max 0 u u')
The component of stability conditions with connected-component label cc.
Equations
Instances For
def
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.CentralChargeIsLocalHomeomorphOnConnectedComponents
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
:
The owner-native local-homeomorphism statement for the central charge on every connected component of the stability space.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Triangulated.componentSeminormSubgroup
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
(cc : ConnectedComponents (StabilityCondition.WithClassMap C v))
:
Bridgeland's V(Σ), implemented using a chosen representative of the component.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[implicit_reducible]
noncomputable instance
CategoryTheory.Triangulated.componentNorm
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
(cc : ConnectedComponents (StabilityCondition.WithClassMap C v))
:
Norm ↥(componentSeminormSubgroup C cc)
The Bridgeland norm on V(Σ) attached to a chosen representative of the component.
Equations
- One or more equations did not get rendered due to their size.
noncomputable def
CategoryTheory.Triangulated.componentAddGroupNorm
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
[Fact (Function.Surjective ⇑v)]
(cc : ConnectedComponents (StabilityCondition.WithClassMap C v))
:
The restricted Bridgeland seminorm is a genuine additive norm on V(Σ).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[implicit_reducible]
noncomputable instance
CategoryTheory.Triangulated.componentNormedAddCommGroup
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
[Fact (Function.Surjective ⇑v)]
(cc : ConnectedComponents (StabilityCondition.WithClassMap C v))
:
@[implicit_reducible]
noncomputable instance
CategoryTheory.Triangulated.componentNormedSpace
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
[Fact (Function.Surjective ⇑v)]
(cc : ConnectedComponents (StabilityCondition.WithClassMap C v))
:
NormedSpace ℂ ↥(componentSeminormSubgroup C cc)
Equations
def
CategoryTheory.Triangulated.componentSeminormBall
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
(cc : ConnectedComponents (StabilityCondition.WithClassMap C v))
(W : ↥(componentSeminormSubgroup C cc))
(r : ℝ)
:
Set ↥(componentSeminormSubgroup C cc)
The seminorm balls in V(Σ) coming from the representative σ₀ ∈ Σ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Triangulated.componentSeminormBall_eq_ball
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
[Fact (Function.Surjective ⇑v)]
(cc : ConnectedComponents (StabilityCondition.WithClassMap C v))
(W : ↥(componentSeminormSubgroup C cc))
{r : ℝ}
(hr : 0 < r)
:
The old seminorm balls are exactly the metric balls for the induced norm on V(Σ).
def
CategoryTheory.Triangulated.componentSeminormBasis
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
(cc : ConnectedComponents (StabilityCondition.WithClassMap C v))
:
Set (Set ↥(componentSeminormSubgroup C cc))
The basis of seminorm balls defining the topology on V(Σ).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
CategoryTheory.Triangulated.componentSeminormTopology
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
(cc : ConnectedComponents (StabilityCondition.WithClassMap C v))
:
The linear topology on V(Σ) generated by seminorm balls for one representative.
Equations
Instances For
theorem
CategoryTheory.Triangulated.isTopologicalBasis_componentSeminormBasis
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
[Fact (Function.Surjective ⇑v)]
(cc : ConnectedComponents (StabilityCondition.WithClassMap C v))
:
The old seminorm-ball basis is a genuine topological basis for the norm topology on V(Σ).
theorem
CategoryTheory.Triangulated.componentSeminormTopology_eq_normTopology
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
[Fact (Function.Surjective ⇑v)]
(cc : ConnectedComponents (StabilityCondition.WithClassMap C v))
:
The ad hoc generated topology on V(Σ) agrees with the topology induced by the Bridgeland
norm defined above.
theorem
CategoryTheory.Triangulated.componentSeminorm_lt_top_of_mem_component
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
(cc : ConnectedComponents (StabilityCondition.WithClassMap C v))
(σ : StabilityCondition.WithClassMap C v)
(hσ : ConnectedComponents.mk σ = cc)
(U : ↥(componentSeminormSubgroup C cc))
:
Any element of the chosen V(Σ) has finite Bridgeland seminorm with respect to any
stability condition in the same connected component.
theorem
CategoryTheory.Triangulated.componentNorm_equivalent_of_mem_component
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
[Fact (Function.Surjective ⇑v)]
(cc : ConnectedComponents (StabilityCondition.WithClassMap C v))
(σ : StabilityCondition.WithClassMap C v)
(hσ : ConnectedComponents.mk σ = cc)
:
The chosen norm on V(Σ) is equivalent to the Bridgeland norm coming from any
representative σ ∈ Σ. This is the formal version of Bridgeland's statement that the norms
‖·‖_σ on a connected component are equivalent.
theorem
CategoryTheory.Triangulated.componentZ_mem
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
(cc : ConnectedComponents (StabilityCondition.WithClassMap C v))
(σ : StabilityCondition.WithClassMap C v)
(hσ : ConnectedComponents.mk σ = cc)
:
For σ ∈ Σ, its central charge lies in V(Σ).
def
CategoryTheory.Triangulated.componentZMap
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
(cc : ConnectedComponents (StabilityCondition.WithClassMap C v))
:
componentStabilityCondition C cc → ↥(componentSeminormSubgroup C cc)
The central charge map restricted to a connected component and landing in V(Σ).
Instances For
Canonical component local model #
structure
CategoryTheory.Triangulated.ComponentTopologicalLinearLocalModel
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
(cc : ConnectedComponents (StabilityCondition.WithClassMap C v))
:
Type u'
A reusable non-existential package for the current formalization of Bridgeland's Theorem 1.2 on a fixed connected component.
The chosen complex-linear charge space
V(Σ)for this connected component.- instNormedAddCommGroup : NormedAddCommGroup ↥self.V
- instNormedSpace : NormedSpace ℂ ↥self.V
- mem_charge (σ : StabilityCondition.WithClassMap C v) : ConnectedComponents.mk σ = cc → σ.Z ∈ self.V
- isLocalHomeomorph_chargeMap : IsLocalHomeomorph fun (x : { σ : StabilityCondition.WithClassMap C v // ConnectedComponents.mk σ = cc }) => match x with | ⟨σ, hσ⟩ => ⟨σ.Z, ⋯⟩
Instances For
def
CategoryTheory.Triangulated.ComponentTopologicalLinearLocalModel.chargeMap
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
{cc : ConnectedComponents (StabilityCondition.WithClassMap C v)}
(M : ComponentTopologicalLinearLocalModel C cc)
:
componentStabilityCondition C cc → ↥M.V
The restricted central charge map attached to a component local model.
Equations
Instances For
Theorem 1.2 #
noncomputable def
CategoryTheory.Triangulated.componentTopologicalLinearLocalModel
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
[Fact (Function.Surjective ⇑v)]
(cc : ConnectedComponents (StabilityCondition.WithClassMap C v))
:
The canonical componentwise local linear model used to state Bridgeland's
Theorem 1.2 in terms of an explicit normed complex vector space V(Σ).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Triangulated.centralChargeIsLocalHomeomorphOnConnectedComponents
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
[Fact (Function.Surjective ⇑v)]
:
Bridgeland's Theorem 1.2. For each connected component Σ of the stability space, there is a linear subspace V(Σ) ⊂ Hom(Λ, ℂ) with a normed topology and a local homeomorphism Z : Σ → V(Σ) mapping each stability condition to its central charge.