Joint continuity of the lifted linear action #

This file strengthens the fixed-element continuity proved in CategoryTheory/Triangulated/StabilityCondition/Symmetry/GLTilde/Action/Continuous.lean. The key estimates are local at the identity:

x.shift φ - φ is uniformly small in φ when x is close to 1; integer equivariance reduces this to the compact interval [0, 1];
actCCLM x.mat - 1 is small in operator norm when x is close to 1.

The general case follows from x • τ = x₀ • ((x₀⁻¹ * x) • τ) and the already-proved continuity of the action by the fixed element x₀.

Uniform phase displacement near the identity #

source

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.continuous_shift_displacement :

Continuous fun (p : GLTilde × ℝ) => p.1.shift.toOrderIso p.2 - p.2

Jointly continuous phase displacement.

source

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.eventually_uniform_shift_displacement {a : ℝ} (ha : 0 < a) :

∀ᶠ (x : GLTilde) in nhds 1, ∀ (φ : ℝ), |x.shift.toOrderIso φ - φ| < a

Close to the identity, the lifted phase map is uniformly close to the identity map on all of ℝ.

source

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.slicingDist_smul_le_of_displacement {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} [IsTriangulated C] (x : GLTilde) (σ τ : StabilityCondition.WithClassMap C v) {a d : ℝ} (hdisp : ∀ (φ : ℝ), |x.shift.toOrderIso φ - φ| < a) (hdist : slicingDist C σ.slicing τ.slicing < ENNReal.ofReal d) :

slicingDist C σ.slicing (x • τ).slicing ≤ ENNReal.ofReal (d + a)

Phase displacement of x plus the original slicing distance controls the distance from x • τ back to the fixed slicing σ.

Operator-norm control of the central charge #

source

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.actCCLM_one :

actCCLM 1 = ContinuousLinearMap.id ℝ ℂ

source

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.continuous_actCCLM :

Continuous fun (x : GLTilde) => actCCLM x.mat

The central-charge operator varies continuously in operator norm.

source

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.norm_actC_sub_div_le (T : ↥(Matrix.GLPos (Fin 2) ℝ)) (z w : ℂ) (hw : w ≠ 0) :

‖(actC T) (z + w) - w‖ / ‖w‖ ≤ ‖actCCLM T‖ * (‖z‖ / ‖w‖) + ‖actCCLM T - ContinuousLinearMap.id ℝ ℂ‖

The elementary pointwise estimate behind the stability-seminorm bound.

source

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.stabSeminorm_near_identity_le {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} [IsTriangulated C] (x : GLTilde) (σ τ : StabilityCondition.WithClassMap C v) :

Deformation.stabilitySeminorm C σ ((x • τ).Z - σ.Z) ≤ ENNReal.ofReal ‖actCCLM x.mat‖ * Deformation.stabilitySeminorm C σ (τ.Z - σ.Z) + ENNReal.ofReal ‖actCCLM x.mat - ContinuousLinearMap.id ℝ ℂ‖

Simultaneously moving the group element away from the identity and the stability condition away from σ gives this affine seminorm bound.

A uniform basic-neighborhood estimate at the identity #

source

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.exists_identity_basisNhd_control {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} [IsTriangulated C] (σ : StabilityCondition.WithClassMap C v) {e : ℝ} (he : 0 < e) (he8 : e < 1 / 8) :

∃ (d : ℝ), 0 < d ∧ d < 1 / 8 ∧ ∀ᶠ (x : GLTilde) in nhds 1, Set.MapsTo (fun (τ : StabilityCondition.WithClassMap C v) => x • τ) (Deformation.basisNhd C σ d) (Deformation.basisNhd C σ e)

For a fixed centre σ, group elements sufficiently close to 1 carry one smaller basic neighborhood of σ into any prescribed basic neighborhood of σ. The source radius is independent of the nearby group element.