Pointwise perturbation of semistable charges

This module connects the pure relative-phase estimates to owner stability conditions. It packages the pointwise relative norm bound that a future stability seminorm will supply, proves nonvanishing below one, and constructs the skewed stability data used on thin intervals.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SemistableChargeBound (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C κ) (W : Λ →+ ℂ) (r : ℝ) : Prop

A uniform pointwise relative norm bound on all nonzero semistable objects. The bound is deliberately independent of any chosen global norm on the target lattice.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.relativePhase_charge_eq (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C κ) {E : C} {φ α : ℝ} (hP : σ.slicing.P φ E) (hE : ¬Limits.IsZero E) (hφ : φ ∈ Set.Ioc (α - 1) (α + 1)) : relativePhase (σ.charge E) α = φ

The old central charge has the selected relative phase of a semistable object on every compatible branch.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.perturbedCharge_ne_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 Λ] {κ : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C κ) (W : Λ →+ ℂ) {r φ : ℝ} (hr : r < 1) (hbound : SemistableChargeBound C σ W r) {E : C} (hP : σ.slicing.P φ E) (hE : ¬Limits.IsZero E) : W (classOf C κ E) ≠ 0

A pointwise norm bound below one prevents the perturbed charge of a nonzero semistable object from vanishing.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfBound (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C κ) (W : Λ →+ ℂ) {r a b : ℝ} (hr : r < 1) (hbound : SemistableChargeBound C σ W r) (hab : a < b) : SkewedStabilityFunction C κ σ.slicing a b

A pointwise semistable-charge bound below one induces owner skewed stability data on every nonempty interval.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.relativePhase_perturbation_of_charge (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C κ) (W : Λ →+ ℂ) {E : C} {φ α ε : ℝ} (hP : σ.slicing.P φ E) (hE : ¬Limits.IsZero E) (hφα : φ ∈ Set.Ioo (α - 1 / 2) (α + 1 / 2)) (hε : 0 < ε) (hε2 : ε ≤ 1 / 2) (hbd : ‖(W - σ.Z) (classOf C κ E)‖ < Real.sin (Real.pi * ε) * ‖σ.charge E‖) : |relativePhase (W (classOf C κ E)) α - φ| < ε

Pointwise charge control by sin (π ε) gives the corresponding strict phase control for an old semistable object.