The combined symmetry action

The two halves of Bridgeland's section 8 action commute. GLTilde changes phases and postcomposes the central charge by a real-linear automorphism of ℂ; AutPairQuot v changes objects and precomposes the charge by an automorphism of the class lattice. These operations are independent:

• phase relabelling commutes with transport of a slicing along an autoequivalence;
• postcomposition on ℂ commutes with precomposition on Λ.

This gives both the SMulCommClass recording that independence and the product action

MulAction (GLTilde × AutPairQuot v)
  (StabilityCondition.WithClassMap C v).

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.relabel_mapEquiv {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (x : GLTilde) (Φ : TriEquiv C) (s : Slicing C) : x • s.mapEquiv Φ.e = (x • s).mapEquiv Φ.e

Relabelling phases commutes with transporting a slicing along an autoequivalence.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.gltilde_autPair_smul_comm {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) (a : AutPair v) (σ : StabilityCondition.WithClassMap C v) : x • a.act σ = a.act (x • σ)

A concrete compatible autoequivalence and GLTilde commute on stability conditions. Quotient descent is handled below.

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

The two section 8 actions commute after quotienting the autoequivalence component by natural isomorphism.

@[implicit_reducible]

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

The combined section 8 symmetry action.

The product acts by the autoequivalence first and GLTilde second. The commutation theorem above makes this a genuine action of the direct product.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.prod_mk_smul_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 →+ Λ} [IsTriangulated C] (x : GLTilde) (a : AutPair v) (σ : StabilityCondition.WithClassMap C v) : ((x, AutPairQuot.mk a) • σ).slicing = x • σ.slicing.mapEquiv a.Φ.e

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.prod_mk_smul_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 →+ Λ} [IsTriangulated C] (x : GLTilde) (a : AutPair v) (σ : StabilityCondition.WithClassMap C v) (y : Λ) : ((x, AutPairQuot.mk a) • σ).Z y = (actC x.mat) (σ.Z (a.lam y))