The lifted linear action on prestability conditions

Both factors of G̃L⁺(2, ℝ) act at once:

(x • σ).slicing = x.shift • σ.slicing        -- phases relabelled
(x • σ).Z       = actC x.mat ∘ σ.Z           -- charge transformed

The whole point of the Compatible condition in GLTilde is that these two stay in step. compat' demands that a semistable object of phase φ have its charge on the ray ℝ₊ · exp(i π φ); after acting, its phase is φ in the new slicing exactly when it was f⁻¹ φ in the old one, and actC_exp says T carries the old ray to the new one. The positive scalars multiply, so the witness m is replaced by m * r.

This synchronization is precisely the role of Compatible.

Not yet a stability condition

StabilityCondition.WithClassMap additionally carries locallyFinite, and preserving it is a genuine analysis argument, not bookkeeping; the sibling stability-action module supplies it.

Note this file does not need [IsTriangulated C]: PreStabilityCondition.WithClassMap does not depend on it.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.actPre (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 →+ Λ) (x : GLTilde) (σ : PreStabilityCondition.WithClassMap C v) : PreStabilityCondition.WithClassMap C v

x = (T, f) acting on a prestability condition: f relabels the slicing, T transforms the central charge.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.actPre_slicing (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 →+ Λ) (x : GLTilde) (σ : PreStabilityCondition.WithClassMap C v) : (actPre C v x σ).slicing = x • σ.slicing

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.actPre_Z (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 →+ Λ) (x : GLTilde) (σ : PreStabilityCondition.WithClassMap C v) (a : Λ) : (actPre C v x σ).Z a = (actC x.mat) (σ.Z a)

@[implicit_reducible]

noncomputable instance CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.preMulAction (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 →+ Λ) : MulAction GLTilde (PreStabilityCondition.WithClassMap C v)

G̃L⁺(2, ℝ) acts on prestability conditions.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.smul_pre_slicing (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 →+ Λ) (x : GLTilde) (σ : PreStabilityCondition.WithClassMap C v) : (x • σ).slicing = x • σ.slicing

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.smul_pre_Z (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 →+ Λ) (x : GLTilde) (σ : PreStabilityCondition.WithClassMap C v) (a : Λ) : (x • σ).Z a = (actC x.mat) (σ.Z a)