Bridgeland's Theorem 1.2: Central charge is a local homeomorphism #
Following Bridgeland's proof:
- Lemma 6.2 (
stabilitySeminorm_dominated_of_connected): seminorm equivalence on V(Σ). - Prop 6.3: Z continuous into the seminorm topology.
- Lemma 6.4 (
eq_of_same_Z_near): Z locally injective. - Theorem 7.1 (
deformation): Z locally surjective.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.exists_eq_Z_and_mem_basisNhd_of_stabilitySeminorm_lt_sin
(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 →+ Λ}
(σ : WithClassMap C v)
(W : Λ →+ ℂ)
(hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal 1)
(ε₀ : ℝ)
(hε₀ : 0 < ε₀)
(hε₀16 : ε₀ < 1 / 16)
(hWide : WeakStabilityCondition.StabilityCondition.Deformation.WideSectorFiniteLength C σ ε₀)
(ε : ℝ)
(hε : 0 < ε)
(hεε₀ : ε < ε₀ / 2)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
:
∃ (τ : WithClassMap C v), τ.Z = W ∧ τ ∈ WeakStabilityCondition.StabilityCondition.Deformation.basisNhd C σ ε
A small deformation of the central charge lifts directly to a point of basisNhd C σ ε.
This is the form used in the topology arguments for Theorem 1.2: it gives both the
prescribed central charge and the exact basisNhd control, so no radius enlargement
is needed after applying the deformation theorem.
theorem
CategoryTheory.Triangulated.wideSectorFiniteLength_mono
(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 →+ Λ}
(σ : StabilityCondition.WithClassMap C v)
{ε₀ ε₁ : ℝ}
(hε₀ : 0 < ε₀)
(hε₀8 : ε₀ < 1 / 8)
(hWide : WeakStabilityCondition.StabilityCondition.Deformation.WideSectorFiniteLength C σ ε₀)
(hε₁ : 0 < ε₁)
(hε₁8 : ε₁ < 1 / 8)
(hε₁ε₀ : ε₁ ≤ ε₀)
:
Wide-sector finite length is monotone under shrinking ε₀.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.exists_epsilon0_sixteenth
(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 →+ Λ}
(σ : WithClassMap C v)
:
A local ε₀ < 1 / 16 wide-sector witness for deformation.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformation
(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 →+ Λ}
(σ : WithClassMap C v)
:
∃ (ε₀ : ℝ),
0 < ε₀ ∧ ∀ (W : Λ →+ ℂ) (ε : ℝ),
0 < ε →
ε < ε₀ →
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)) →
∃ (τ : WithClassMap C v), τ.Z = W ∧ slicingDist C σ.slicing τ.slicing < ENNReal.ofReal ε
Bridgeland's Theorem 7.1. Let σ be a locally-finite stability condition. Then there is an ε₀ > 0 such that if 0 < ε < ε₀ and W satisfies ‖W − Z‖_σ < sin(πε), then there is a locally-finite stability condition τ = (W, Q) with d(P, Q) < ε.
noncomputable def
CategoryTheory.Triangulated.linearInterpolationZ
(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 →+ Λ}
(σ τ : StabilityCondition.WithClassMap C v)
(t : ℝ)
:
The affine interpolation between the central charges of σ and τ.
Instances For
@[simp]
theorem
CategoryTheory.Triangulated.linearInterpolationZ_zero
(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 →+ Λ}
(σ τ : StabilityCondition.WithClassMap C v)
:
@[simp]
theorem
CategoryTheory.Triangulated.linearInterpolationZ_one
(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 →+ Λ}
(σ τ : StabilityCondition.WithClassMap C v)
:
theorem
CategoryTheory.Triangulated.linearInterpolationZ_sub
(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 →+ Λ}
(σ τ : StabilityCondition.WithClassMap C v)
(t : ℝ)
:
theorem
CategoryTheory.Triangulated.linearInterpolationZ_sub_sub
(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 →+ Λ}
(σ τ : StabilityCondition.WithClassMap C v)
(s t : ℝ)
:
theorem
CategoryTheory.Triangulated.stabilitySeminorm_smul
(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 →+ Λ}
(σ : StabilityCondition.WithClassMap C v)
(U : Λ →+ ℂ)
(t : ℝ)
:
theorem
CategoryTheory.Triangulated.stabilitySeminorm_smul_complex
(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 →+ Λ}
(σ : StabilityCondition.WithClassMap C v)
(U : Λ →+ ℂ)
(t : ℂ)
:
theorem
CategoryTheory.Triangulated.stabilitySeminorm_dominated_of_basisNhd
(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 →+ Λ}
(σ τ : StabilityCondition.WithClassMap C v)
{ε : ℝ}
(hε : 0 < ε)
(hε8 : ε < 1 / 8)
(hτ : τ ∈ WeakStabilityCondition.StabilityCondition.Deformation.basisNhd C σ ε)
:
∃ (K : ENNReal),
K ≠ ⊤ ∧ ∀ (U : Λ →+ ℂ),
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ U ≤ K * WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C τ U
theorem
CategoryTheory.Triangulated.stabilitySeminorm_center_dominates_of_basisNhd
(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 →+ Λ}
(σ τ : StabilityCondition.WithClassMap C v)
{ε : ℝ}
(hε : 0 < ε)
(hε8 : ε < 1 / 8)
(hτ : τ ∈ WeakStabilityCondition.StabilityCondition.Deformation.basisNhd C σ ε)
:
∃ (K : ENNReal),
K ≠ ⊤ ∧ ∀ (U : Λ →+ ℂ),
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C τ U ≤ K * WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ U
Local forward domination inside a Bridgeland basis neighborhood.
theorem
CategoryTheory.Triangulated.basisNhd_self
(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 →+ Λ}
(σ : StabilityCondition.WithClassMap C v)
{ε : ℝ}
(hε : 0 < ε)
(hε8 : ε < 1 / 8)
:
A basis neighborhood contains its center.
theorem
CategoryTheory.Triangulated.basisNhd_mono
(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 →+ Λ}
(σ : StabilityCondition.WithClassMap C v)
{δ ε : ℝ}
(hδ : 0 < δ)
(hδε : δ ≤ ε)
(hε8 : ε < 1 / 8)
:
Shrinking the radius at a fixed center shrinks the Bridgeland basis neighborhood.
theorem
CategoryTheory.Triangulated.exists_basisNhd_subset_basisNhd
(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 →+ Λ}
(σ τ : StabilityCondition.WithClassMap C v)
{ε : ℝ}
(hε : 0 < ε)
(hε8 : ε < 1 / 8)
(hτ : τ ∈ WeakStabilityCondition.StabilityCondition.Deformation.basisNhd C σ ε)
:
∃ (δ : ℝ),
0 < δ ∧ δ < 1 / 8 ∧ WeakStabilityCondition.StabilityCondition.Deformation.basisNhd C τ δ ⊆
WeakStabilityCondition.StabilityCondition.Deformation.basisNhd C σ ε
If τ ∈ B_ε(σ), then some smaller basis neighborhood of τ is contained in B_ε(σ).
This is the local basis-refinement step used later in the local homeomorphism proof. It only needs seminorm domination for nearby stability conditions.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.eq_of_same_Z_near
(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 →+ Λ}
(σ τ : WithClassMap C v)
(hZ : σ.Z = τ.Z)
(hd : slicingDist C σ.slicing τ.slicing < ENNReal.ofReal 1)
:
Two stability conditions with same Z and d < 1 are equal (Lemma 6.4).
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.eq_of_same_Z_of_mem_basisNhd
(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 →+ Λ}
(σ : WithClassMap C v)
{ε : ℝ}
(hε : 0 < ε)
(hε8 : ε < 1 / 8)
{τ₁ τ₂ : WithClassMap C v}
(hτ₁ : τ₁ ∈ WeakStabilityCondition.StabilityCondition.Deformation.basisNhd C σ ε)
(hτ₂ : τ₂ ∈ WeakStabilityCondition.StabilityCondition.Deformation.basisNhd C σ ε)
(hZ : τ₁.Z = τ₂.Z)
:
Two stability conditions lying in the same Bridgeland basis neighborhood of σ
and with the same central charge are equal.
theorem
CategoryTheory.Triangulated.basisNhd_subset_connectedComponent_small
(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 →+ Λ}
(σ : StabilityCondition.WithClassMap C v)
{ε₀ ε : ℝ}
(hε₀ : 0 < ε₀)
(hε₀16 : ε₀ < 1 / 16)
(hWide : WeakStabilityCondition.StabilityCondition.Deformation.WideSectorFiniteLength C σ ε₀)
(hε : 0 < ε)
(hεε₀ : ε < ε₀ / 2)
:
A small Bridgeland basis neighborhood, with radius below the local deformation witness, lies in the connected component of its center. This is the direct straight-line interpolation argument from Bridgeland §7.
theorem
CategoryTheory.Triangulated.exists_local_lift_sameComponent_in_basisNhd
(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 →+ Λ}
(σ τ ρ₀ : StabilityCondition.WithClassMap C v)
{ε t : ℝ}
(hε : 0 < ε)
(hε8 : ε < 1 / 8)
(hτ : τ ∈ WeakStabilityCondition.StabilityCondition.Deformation.basisNhd C σ ε)
(hρ₀mem : ρ₀ ∈ WeakStabilityCondition.StabilityCondition.Deformation.basisNhd C σ ε)
(hρ₀Z : ρ₀.Z = linearInterpolationZ C σ τ t)
:
∃ (η : ℝ),
0 < η ∧ ∀ ⦃s : ℝ⦄,
|s - t| < η →
∃ (ρ : StabilityCondition.WithClassMap C v),
ρ.Z = linearInterpolationZ C σ τ s ∧ ρ ∈ WeakStabilityCondition.StabilityCondition.Deformation.basisNhd C σ ε ∧ ConnectedComponents.mk ρ = ConnectedComponents.mk ρ₀
Local continuation along the straight-line charge interpolation inside a fixed basis
neighborhood. Starting from any lifted point ρ₀ over time t, nearby times also admit lifts
inside the same ambient basis neighborhood and in the same connected component as ρ₀.