Group actions on ACC systems.

We define a group action on an ACC system as a representation on the vector spaces of charges under which the anomaly equations are invariant.

From this we define

• The representation acting on the vector space of solutions to the linear ACCs.
• The group action acting on solutions to the linear + quadratic equations.
• The group action acting on solutions to the anomaly cancellation conditions.

structure ACCSystemGroupAction (χ : ACCSystem) : Type 1

The type of a group action on a system of charges is defined as a representation on the vector spaces of charges under which the anomaly equations are invariant.

• group : Type

  The underlying type of the group.

• groupInst : Group self.group

  An instance given the group component the structure of a Group.

• rep : Representation ℚ self.group χ.Charges

  The representation of group acting on the vector space of charges.

• linearInvariant (i : Fin χ.numberLinear) (g : self.group) (S : χ.Charges) : (χ.linearACCs i) ((self.rep g) S) = (χ.linearACCs i) S

  The invariance of the linear ACCs under the group action.

• quadInvariant (i : Fin χ.numberQuadratic) (g : self.group) (S : χ.Charges) : (χ.quadraticACCs i) ((self.rep g) S) = (χ.quadraticACCs i) S

  The invariance of the quadratic ACCs under the group action.

• cubicInvariant (g : self.group) (S : χ.Charges) : χ.cubicACC ((self.rep g) S) = χ.cubicACC S

  The invariance of the cubic ACC under the group action.

instance ACCSystemGroupAction.instGroupGroup {χ : ACCSystem} (G : ACCSystemGroupAction χ) : Group G.group

The given instance of a group on the group field of a ACCSystemGroupAction.

Equations

• G.instGroupGroup = G.groupInst

def ACCSystemGroupAction.linSolMap {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group) : χ.LinSols →ₗ[ℚ] χ.LinSols

The action of a group element on the vector space of linear solutions.

Equations

• G.linSolMap g = { toFun := fun (S : χ.LinSols) => { val := (G.rep g) S.val, linearSol := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

def ACCSystemGroupAction.linSolRep {χ : ACCSystem} (G : ACCSystemGroupAction χ) : Representation ℚ G.group χ.LinSols

The representation acting on the vector space of solutions to the linear ACCs.

Equations

• G.linSolRep = { toFun := G.linSolMap, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem ACCSystemGroupAction.linSolRep_apply_apply_val {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group) (S : χ.LinSols) : ((G.linSolRep g) S).val = (G.rep g) S.val

theorem ACCSystemGroupAction.rep_linSolRep_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group) (S : χ.LinSols) : χ.linSolsIncl ((G.linSolRep g) S) = (G.rep g) (χ.linSolsIncl S)

The representation on the charges and anomaly free solutions commutes with the inclusion.

instance ACCSystemGroupAction.quadSolAction {χ : ACCSystem} (G : ACCSystemGroupAction χ) : MulAction G.group χ.QuadSols

A multiplicative action of G.group on quadSols.

Equations

• G.quadSolAction = MulAction.mk ⋯ ⋯

theorem ACCSystemGroupAction.linSolRep_quadSolAction_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group) (S : χ.QuadSols) : χ.quadSolsInclLinSols ((MulAction.toFun G.group χ.QuadSols) S g) = (G.linSolRep g) (χ.quadSolsInclLinSols S)

theorem ACCSystemGroupAction.rep_quadSolAction_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group) (S : χ.QuadSols) : χ.quadSolsIncl ((MulAction.toFun G.group χ.QuadSols) S g) = (G.rep g) (χ.quadSolsIncl S)

instance ACCSystemGroupAction.solAction {χ : ACCSystem} (G : ACCSystemGroupAction χ) : MulAction G.group χ.Sols

The group action acting on solutions to the anomaly cancellation conditions.

Equations

• G.solAction = MulAction.mk ⋯ ⋯

theorem ACCSystemGroupAction.quadSolAction_solAction_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group) (S : χ.Sols) : χ.solsInclQuadSols ((MulAction.toFun G.group χ.Sols) S g) = (MulAction.toFun G.group χ.QuadSols) (χ.solsInclQuadSols S) g

theorem ACCSystemGroupAction.linSolRep_solAction_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group) (S : χ.Sols) : χ.solsInclLinSols ((MulAction.toFun G.group χ.Sols) S g) = (G.linSolRep g) (χ.solsInclLinSols S)

theorem ACCSystemGroupAction.rep_solAction_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group) (S : χ.Sols) : χ.solsIncl ((MulAction.toFun G.group χ.Sols) S g) = (G.rep g) (χ.solsIncl S)