The repository-owned deformation theorem

This packages the deformed slicing with its perturbed central charge and proves local finiteness by embedding each small deformed interval into a uniformly finite old interval.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformed_intervalProp_subset_old_wide (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) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) (t : ℝ) : Slicing.intervalProp C (deformedSlicing C σ W hr0 hr1 hW hε₀ hε₀16 hWide hε hεhalf hε2 hε8 hsin) (t - ε₀) (t + ε₀) ≤ Slicing.intervalProp C σ.slicing (t - 4 * ε₀) (t + 4 * ε₀)

A small interval for the deformed slicing lies in the corresponding uniformly wide interval for the old slicing.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedSlicing_isLocallyFinite (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) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) : Slicing.IsLocallyFinite C (deformedSlicing C σ W hr0 hr1 hW hε₀ hε₀16 hWide hε hεhalf hε2 hε8 hsin)

The repository-owned deformed slicing is locally finite.

def CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformed (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) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) : WithClassMap C κ

The canonical stability condition with perturbed central charge and the repository-owned deformed slicing.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformed_Z (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) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) : (deformed C σ W hr0 hr1 hW hε₀ hε₀16 hWide hε hεhalf hε2 hε8 hsin).Z = W

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.slicingDist_deformed_le (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) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) : slicingDist C σ.slicing (deformed C σ W hr0 hr1 hW hε₀ hε₀16 hWide hε hεhalf hε2 hε8 hsin).slicing ≤ ENNReal.ofReal ε

The canonical deformed slicing is at distance at most the deformation radius from the original slicing.