The lifted linear action on stability conditions

This module extends the G̃L⁺(2, ℝ) action from prestability conditions to StabilityCondition.WithClassMap C v.

The additional obligation is that Slicing.IsLocallyFinite survives phase relabelling. It quantifies one radius η over all centres t, while a normalized shift distorts windows.

Three ingredients close it:

1. NormalizedShift.exists_radius (Algebra/Order/NormalizedShift/UniformContinuity.lean) — uniform continuity, giving one radius η' whose every window maps to width < 2η.
2. relabel_intervalProp (CategoryTheory/Triangulated/StabilityCondition/Symmetry/GLTilde/Action/Slicing.lean) — interval subcategories are reindexed exactly, so the relabelled window at (t-η', t+η') is the original at (f⁻¹(t-η'), f⁻¹(t+η')).
3. interval_thinFiniteLength_of_inclusion_strict (WeakStabilityCondition/StabilityCondition/Symmetry/Autoequivalence/Foundations/FiniteLength.lean) — the shrinking lemma. It is stated for two different slicings related by intervalProp ≤ intervalProp, which is exactly the shape (2) produces.

Together these convert a local-finiteness witness for the original slicing into a uniform witness for the relabelled slicing.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.relabel_isLocallyFinite (C : Type u) [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (f : NormalizedShift) (s : Slicing C) (hs : Slicing.IsLocallyFinite C s) : Slicing.IsLocallyFinite C (relabel C f s)

Local finiteness survives phase relabelling.

The window radius changes — η becomes the η' supplied by uniform continuity — but a single radius still works for every centre, which is what IsLocallyFinite demands.

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

x = (T, f) acting on a full stability condition. Slicing and charge are transported by actPre; local finiteness is relabel_isLocallyFinite.

Equations

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

@[simp]

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

@[simp]

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

@[implicit_reducible]

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

The §8 action. G̃L⁺(2, ℝ) acts on stability conditions.

Equations

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

@[simp]

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

@[simp]

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