Continuity of each lifted linear action map

Every fixed element of GLTilde acts continuously, hence by a homeomorphism, on the Bridgeland stability space. The proof follows the two coordinates in the definition of basisNhd:

• uniform continuity of NormalizedShift controls slicingDist;
• the operator norms of actC T and actC T⁻¹ control stabSeminorm.

The resulting instance is ContinuousConstSMul: continuity in the stability condition for every fixed group element. The separate, stronger joint statement is proved in CategoryTheory/Triangulated/StabilityCondition/Symmetry/GLTilde/Action/JointContinuous.lean.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.Slicing.relabel_phiPlus {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (f : NormalizedShift) (s : Slicing C) (E : C) (hE : ¬Limits.IsZero E) : Slicing.phiPlus C (relabel C f s) E hE = f.toOrderIso (Slicing.phiPlus C s E hE)

Relabelling applies the normalized shift to the largest HN phase.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.Slicing.relabel_phiMinus {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (f : NormalizedShift) (s : Slicing C) (E : C) (hE : ¬Limits.IsZero E) : Slicing.phiMinus C (relabel C f s) E hE = f.toOrderIso (Slicing.phiMinus C s E hE)

Relabelling applies the normalized shift to the smallest HN phase.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.exists_slicingDist_relabel_control {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (f : NormalizedShift) {e : ℝ} (he : 0 < e) : ∃ (d : ℝ), 0 < d ∧ ∀ (s₁ s₂ : Slicing C), slicingDist C s₁ s₂ < ENNReal.ofReal d → slicingDist C (relabel C f s₁) (relabel C f s₂) < ENNReal.ofReal e

A uniform source radius controlling the slicing distance after a fixed phase relabelling.

Central-charge operator bounds

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.actCCLM (T : ↥(Matrix.GLPos (Fin 2) ℝ)) : ℂ →L[ℝ] ℂ

The real-linear central-charge action as a continuous linear map.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.actCCLM_apply (T : ↥(Matrix.GLPos (Fin 2) ℝ)) (z : ℂ) : (actCCLM T) z = (actC T) z

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.actC_inv_apply (T : ↥(Matrix.GLPos (Fin 2) ℝ)) (z : ℂ) : (actC T⁻¹) ((actC T) z) = z

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.actCCondition (T : ↥(Matrix.GLPos (Fin 2) ℝ)) : ℝ

A deliberately nonzero condition bound. The added 1 avoids a separate positivity proof for the operator norms.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.actCCondition_pos (T : ↥(Matrix.GLPos (Fin 2) ℝ)) : 0 < actCCondition T

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.norm_actC_div_norm_actC_le (T : ↥(Matrix.GLPos (Fin 2) ℝ)) (z w : ℂ) (hw : w ≠ 0) : ‖(actC T) z‖ / ‖(actC T) w‖ ≤ actCCondition T * (‖z‖ / ‖w‖)

The condition-number estimate used by stabSeminorm.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.stabSeminorm_gltilde_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 • σ) ((x • τ).Z - (x • σ).Z) ≤ ENNReal.ofReal (actCCondition x.mat) * Deformation.stabilitySeminorm C σ (τ.Z - σ.Z)

A fixed matrix action expands the stability seminorm by at most its condition bound.

Basic neighborhoods and continuity

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.exists_gltilde_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] (x : GLTilde) {e : ℝ} (he : 0 < e) (he8 : e < 1 / 8) : ∃ (d : ℝ), 0 < d ∧ d < 1 / 8 ∧ ∀ (σ : StabilityCondition.WithClassMap C v), Set.MapsTo (fun (τ : StabilityCondition.WithClassMap C v) => x • τ) (Deformation.basisNhd C σ d) (Deformation.basisNhd C (x • σ) e)

For a fixed GLTilde element, every target radius admits one source radius that works at every centre.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.continuous_const_smul_stability {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) : Continuous fun (σ : StabilityCondition.WithClassMap C v) => x • σ

Every fixed GLTilde element acts continuously on the stability space.

instance CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.gltildeContinuousConstSMulStability {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] : ContinuousConstSMul GLTilde (StabilityCondition.WithClassMap C v)

instance CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.combinedContinuousConstSMulStability {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] : ContinuousConstSMul (GLTilde × AutPairQuot v) (StabilityCondition.WithClassMap C v)

The direct-product symmetry action is continuous in the stability-condition variable for every fixed pair.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.stabilityHomeomorph {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 ≃ₜ StabilityCondition.WithClassMap C v

A named homeomorphism for the action of each fixed lifted matrix.

Equations

• x.stabilityHomeomorph = Homeomorph.smul x

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.combinedStabilityHomeomorph {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] (p : GLTilde × AutPairQuot v) : StabilityCondition.WithClassMap C v ≃ₜ StabilityCondition.WithClassMap C v

A named homeomorphism for each element of the combined symmetry group.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.combinedStabilityHomeomorph p = Homeomorph.smul p