Local central-charge lifts

The deformation theorem constructs a stability condition with a prescribed nearby central charge. This file puts that construction into the topology on the stability space: using a slightly smaller deformation radius places the result in any specified larger basic neighborhood.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.exists_with_Z_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 Λ] {κ : K₀ C →+ Λ} (σ : WithClassMap C κ) (W : Λ →+ ℂ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r) {ε₀ : ℝ} (hε₀ : 0 < ε₀) (hε₀16 : ε₀ < 1 / 16) (hWide : WeakStabilityCondition.StabilityCondition.Deformation.WideSectorFiniteLength C σ ε₀) {δ ε : ℝ} (hδ : 0 < δ) (hδhalf : δ < ε₀ / 2) (hδ2 : δ ≤ 1 / 2) (hδ8 : δ < 1 / 8) (hδε : δ < ε) (hε8 : ε < 1 / 8) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * δ))) : ∃ (τ : WithClassMap C κ), τ.Z = W ∧ τ ∈ WeakStabilityCondition.StabilityCondition.Deformation.basisNhd C σ ε

A charge satisfying the deformation estimate at radius δ lifts to a stability condition in every larger basic neighborhood of radius ε.

The returned point is the canonical repository-owned deformation, so the central-charge equality is definitional.