Equivariance of period coordinates

The symmetry action on a stability condition has a corresponding action on its central charge. This file packages that charge action as additive equivalences of Λ →+ ℂ and proves the equivariance square both on the full stability space and on each connected component.

The GLTilde factor postcomposes by its real-linear action on ℂ; the autoequivalence factor precomposes by its compatible lattice automorphism. These operations are additive equivalences even though the first one need not be complex-linear.

Additive equivalences of the charge space

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.chargeAddEquiv {Λ : Type u'} [AddCommGroup Λ] (x : GLTilde) : (Λ →+ ℂ) ≃+ (Λ →+ ℂ)

Postcomposition of a charge by the real-linear action of a lifted matrix.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.chargeAddEquiv_apply {Λ : Type u'} [AddCommGroup Λ] (x : GLTilde) (Z : Λ →+ ℂ) (a : Λ) : (x.chargeAddEquiv Z) a = (actC x.mat) (Z a)

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPair.chargeAddEquiv {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 →+ Λ} (a : AutPair v) : (Λ →+ ℂ) ≃+ (Λ →+ ℂ)

Precomposition of a charge by the lattice automorphism carried by an autoequivalence pair.

Equations

• a.chargeAddEquiv = { toFun := fun (Z : Λ →+ ℂ) => Z.comp a.lam.toAddMonoidHom, invFun := fun (Z : Λ →+ ℂ) => Z.comp a.lam.symm.toAddMonoidHom, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPair.chargeAddEquiv_apply {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 →+ Λ} (a : AutPair v) (Z : Λ →+ ℂ) (y : Λ) : (a.chargeAddEquiv Z) y = Z (a.lam y)

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPairQuot.chargeAddEquiv {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 →+ Λ} (q : AutPairQuot v) : (Λ →+ ℂ) ≃+ (Λ →+ ℂ)

The charge-space equivalence descends to AutPairQuot, since its setoid fixes the lattice automorphism on the nose.

Equations

• q.chargeAddEquiv = Quotient.liftOn q CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPair.chargeAddEquiv ⋯

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPairQuot.chargeAddEquiv_mk {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 →+ Λ} (a : AutPair v) : (mk a).chargeAddEquiv = a.chargeAddEquiv

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.combinedChargeAddEquiv {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 →+ Λ} (p : GLTilde × AutPairQuot v) : (Λ →+ ℂ) ≃+ (Λ →+ ℂ)

The combined charge action: precompose by the lattice automorphism, then postcompose by the lifted real matrix.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.combinedChargeAddEquiv p = p.2.chargeAddEquiv.trans p.1.chargeAddEquiv

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.combinedChargeAddEquiv_mk_apply {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) (a : AutPair v) (Z : Λ →+ ℂ) (y : Λ) : ((combinedChargeAddEquiv (x, AutPairQuot.mk a)) Z) y = (actC x.mat) (Z (a.lam y))

Equivariance of the full period map

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.centralCharge_equivariant {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) : (x • σ).Z = x.chargeAddEquiv σ.Z

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPairQuot.centralCharge_equivariant {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] (q : AutPairQuot v) (σ : StabilityCondition.WithClassMap C v) : (q • σ).Z = q.chargeAddEquiv σ.Z

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.combinedCentralCharge_equivariant {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) : (p • σ).Z = (combinedChargeAddEquiv p) σ.Z

The central-charge map is equivariant for the combined symmetry action.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.combinedCentralCharge_equivariant_apply {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))

The connected-component square

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.componentCentralCharge_equivariant {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) (cc : ConnectedComponents (StabilityCondition.WithClassMap C v)) (σ : { τ : StabilityCondition.WithClassMap C v // ConnectedComponents.mk τ = cc }) : (↑((componentHomeomorph p cc) σ)).Z = (combinedChargeAddEquiv p) (↑σ).Z

On component subtypes, symmetry transport and the central-charge map form the expected equivariant square.