Physlib.QFT.AnomalyCancellation.GroupActions

Imports

/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.QFT.AnomalyCancellation.Basic
public import Mathlib.RepresentationTheory.Basic

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.

@[expose] public section

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.

The underlying type of the group.

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

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

The invariance of the linear ACCs under the group action.

The invariance of the quadratic ACCs under the group action.

The invariance of the cubic ACC under the group action.

              structure ACCSystemGroupAction (χ : ACCSystem) where  group : Type  groupInst : Group group  rep : Representation ℚ group χ.Charges  linearInvariant : ∀ i g S, χ.linearACCs i (rep g S) = χ.linearACCs i S  quadInvariant : ∀ i g S, (χ.quadraticACCs i) (rep g S) = (χ.quadraticACCs i) S  cubicInvariant : ∀ g S, χ.cubicACC (rep g S) = χ.cubicACC S

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

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

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


def linSolMap {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group) :
    χ.LinSols →ₗ[ℚ] χ.LinSols where
  toFun S := ⟨G.rep g S.val, byχ:ACCSystemG:ACCSystemGroupAction χg:G.groupS:χ.LinSols⊢ ∀ (i : Fin χ.numberLinear), (χ.linearACCs i) ((G.rep g) S.val) = 0
    intro iχ:ACCSystemG:ACCSystemGroupAction χg:G.groupS:χ.LinSolsi:Fin χ.numberLinear⊢ (χ.linearACCs i) ((G.rep g) S.val) = 0
    rw [G.linearInvariant,χ:ACCSystemG:ACCSystemGroupAction χg:G.groupS:χ.LinSolsi:Fin χ.numberLinear⊢ (χ.linearACCs i) S.val = 0All goals completed! 🐙 S.linearSolχ:ACCSystemG:ACCSystemGroupAction χg:G.groupS:χ.LinSolsi:Fin χ.numberLinear⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙⟩
  map_add' S T := ACCSystemLinear.LinSols.ext ((G.rep g).map_add' _ _)
  map_smul' a S := ACCSystemLinear.LinSols.ext ((G.rep g).map_smul' _ _)

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


@[simps!]
def linSolRep {χ : ACCSystem} (G : ACCSystemGroupAction χ) :
    Representation ℚ G.group χ.LinSols where
  toFun := G.linSolMap
  map_mul' g1 g2 := byχ:ACCSystemG:ACCSystemGroupAction χg1:G.groupg2:G.group⊢ G.linSolMap (g1 * g2) = G.linSolMap g1 * G.linSolMap g2
    refine LinearMap.ext fun S ↦ ACCSystemLinear.LinSols.ext ?_χ:ACCSystemG:ACCSystemGroupAction χg1:G.groupg2:G.groupS:χ.LinSols⊢ ((G.linSolMap (g1 * g2)) S).val = ((G.linSolMap g1 * G.linSolMap g2) S).val
    change (G.rep (g1 * g2)) S.val = _χ:ACCSystemG:ACCSystemGroupAction χg1:G.groupg2:G.groupS:χ.LinSols⊢ (G.rep (g1 * g2)) S.val = ((G.linSolMap g1 * G.linSolMap g2) S).val
    rw [G.rep.map_mulχ:ACCSystemG:ACCSystemGroupAction χg1:G.groupg2:G.groupS:χ.LinSols⊢ (G.rep g1 * G.rep g2) S.val = ((G.linSolMap g1 * G.linSolMap g2) S).valχ:ACCSystemG:ACCSystemGroupAction χg1:G.groupg2:G.groupS:χ.LinSols⊢ (G.rep g1 * G.rep g2) S.val = ((G.linSolMap g1 * G.linSolMap g2) S).val]χ:ACCSystemG:ACCSystemGroupAction χg1:G.groupg2:G.groupS:χ.LinSols⊢ (G.rep g1 * G.rep g2) S.val = ((G.linSolMap g1 * G.linSolMap g2) S).val
    rflAll goals completed! 🐙
  map_one' := byχ:ACCSystemG:ACCSystemGroupAction χ⊢ G.linSolMap 1 = 1
    refine LinearMap.ext fun S ↦ ACCSystemLinear.LinSols.ext ?_χ:ACCSystemG:ACCSystemGroupAction χS:χ.LinSols⊢ ((G.linSolMap 1) S).val = (1 S).val
    change (G.rep.toFun 1) S.val = _χ:ACCSystemG:ACCSystemGroupAction χS:χ.LinSols⊢ ((↑G.rep).toFun 1) S.val = (1 S).val
    rw [G.rep.map_one'χ:ACCSystemG:ACCSystemGroupAction χS:χ.LinSols⊢ 1 S.val = (1 S).valχ:ACCSystemG:ACCSystemGroupAction χS:χ.LinSols⊢ 1 S.val = (1 S).val]χ:ACCSystemG:ACCSystemGroupAction χS:χ.LinSols⊢ 1 S.val = (1 S).val
    rflAll goals completed! 🐙

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

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

A multiplicative action of G.group on quadSols.

set_option backward.isDefEq.respectTransparency false in


instance quadSolAction {χ : ACCSystem} (G : ACCSystemGroupAction χ) :
    MulAction G.group χ.QuadSols where
  smul f S := ⟨G.linSolRep f S.1, byχ:ACCSystemG:ACCSystemGroupAction χf:G.groupS:χ.QuadSols⊢ ∀ (i : Fin χ.numberQuadratic), (χ.quadraticACCs i) ((G.linSolRep f) S.toLinSols).val = 0 simp [linSolRep_apply_apply_val, G.quadInvariant, S.quadSol]All goals completed! 🐙⟩
  mul_smul f1 f2 S := byχ:ACCSystemG:ACCSystemGroupAction χf1:G.groupf2:G.groupS:χ.QuadSols⊢ (f1 * f2) • S = f1 • f2 • S
    apply ACCSystemQuad.QuadSols.extχ:ACCSystemG:ACCSystemGroupAction χf1:G.groupf2:G.groupS:χ.QuadSols⊢ ((f1 * f2) • S).val = (f1 • f2 • S).val
    change (G.rep.toFun (f1 * f2)) S.val = _χ:ACCSystemG:ACCSystemGroupAction χf1:G.groupf2:G.groupS:χ.QuadSols⊢ ((↑G.rep).toFun (f1 * f2)) S.val = (f1 • f2 • S).val
    rw [G.rep.map_mul'χ:ACCSystemG:ACCSystemGroupAction χf1:G.groupf2:G.groupS:χ.QuadSols⊢ ((↑G.rep).toFun f1 * (↑G.rep).toFun f2) S.val = (f1 • f2 • S).valχ:ACCSystemG:ACCSystemGroupAction χf1:G.groupf2:G.groupS:χ.QuadSols⊢ ((↑G.rep).toFun f1 * (↑G.rep).toFun f2) S.val = (f1 • f2 • S).val]χ:ACCSystemG:ACCSystemGroupAction χf1:G.groupf2:G.groupS:χ.QuadSols⊢ ((↑G.rep).toFun f1 * (↑G.rep).toFun f2) S.val = (f1 • f2 • S).val
    rflAll goals completed! 🐙
  one_smul S := byχ:ACCSystemG:ACCSystemGroupAction χS:χ.QuadSols⊢ 1 • S = S
    apply ACCSystemQuad.QuadSols.extχ:ACCSystemG:ACCSystemGroupAction χS:χ.QuadSols⊢ (1 • S).val = S.val
    change (G.rep.toFun 1) S.val = _χ:ACCSystemG:ACCSystemGroupAction χS:χ.QuadSols⊢ ((↑G.rep).toFun 1) S.val = S.val
    rw [G.rep.map_one'χ:ACCSystemG:ACCSystemGroupAction χS:χ.QuadSols⊢ 1 S.val = S.valχ:ACCSystemG:ACCSystemGroupAction χS:χ.QuadSols⊢ 1 S.val = S.val]χ:ACCSystemG:ACCSystemGroupAction χS:χ.QuadSols⊢ 1 S.val = S.val
    rflAll goals completed! 🐙

lemma linSolRep_quadSolAction_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group)
    (S : χ.QuadSols) : χ.quadSolsInclLinSols (G.quadSolAction.toFun _ _ S g) =
    G.linSolRep g (χ.quadSolsInclLinSols S) := rfl

lemma rep_quadSolAction_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group)
    (S : χ.QuadSols) : χ.quadSolsIncl (G.quadSolAction.toFun _ _ S g) =
    G.rep g (χ.quadSolsIncl S) := rfl

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


instance solAction {χ : ACCSystem} (G : ACCSystemGroupAction χ) : MulAction G.group χ.Sols where
  smul g S := ⟨G.quadSolAction.toFun _ _ S.1 g, byχ:ACCSystemG:ACCSystemGroupAction χg:G.groupS:χ.Sols⊢ χ.cubicACC ((MulAction.toFun G.group χ.QuadSols) S.toQuadSols g).val = 0
    simp only [MulAction.toFun_apply]χ:ACCSystemG:ACCSystemGroupAction χg:G.groupS:χ.Sols⊢ χ.cubicACC (g • S.toQuadSols).val = 0
    change χ.cubicACC (G.rep g S.val) = 0χ:ACCSystemG:ACCSystemGroupAction χg:G.groupS:χ.Sols⊢ χ.cubicACC ((G.rep g) S.val) = 0
    rw [G.cubicInvariant,χ:ACCSystemG:ACCSystemGroupAction χg:G.groupS:χ.Sols⊢ χ.cubicACC S.val = 0All goals completed! 🐙 S.cubicSolχ:ACCSystemG:ACCSystemGroupAction χg:G.groupS:χ.Sols⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙⟩
  mul_smul f1 f2 S := byχ:ACCSystemG:ACCSystemGroupAction χf1:G.groupf2:G.groupS:χ.Sols⊢ (f1 * f2) • S = f1 • f2 • S
    apply ACCSystem.Sols.extχ:ACCSystemG:ACCSystemGroupAction χf1:G.groupf2:G.groupS:χ.Sols⊢ ((f1 * f2) • S).val = (f1 • f2 • S).val
    change (G.rep.toFun (f1 * f2)) S.val = _χ:ACCSystemG:ACCSystemGroupAction χf1:G.groupf2:G.groupS:χ.Sols⊢ ((↑G.rep).toFun (f1 * f2)) S.val = (f1 • f2 • S).val
    rw [G.rep.map_mul'χ:ACCSystemG:ACCSystemGroupAction χf1:G.groupf2:G.groupS:χ.Sols⊢ ((↑G.rep).toFun f1 * (↑G.rep).toFun f2) S.val = (f1 • f2 • S).valχ:ACCSystemG:ACCSystemGroupAction χf1:G.groupf2:G.groupS:χ.Sols⊢ ((↑G.rep).toFun f1 * (↑G.rep).toFun f2) S.val = (f1 • f2 • S).val]χ:ACCSystemG:ACCSystemGroupAction χf1:G.groupf2:G.groupS:χ.Sols⊢ ((↑G.rep).toFun f1 * (↑G.rep).toFun f2) S.val = (f1 • f2 • S).val
    rflAll goals completed! 🐙
  one_smul S := byχ:ACCSystemG:ACCSystemGroupAction χS:χ.Sols⊢ 1 • S = S
    apply ACCSystem.Sols.extχ:ACCSystemG:ACCSystemGroupAction χS:χ.Sols⊢ (1 • S).val = S.val
    change (G.rep.toFun 1) S.val = _χ:ACCSystemG:ACCSystemGroupAction χS:χ.Sols⊢ ((↑G.rep).toFun 1) S.val = S.val
    rw [G.rep.map_one'χ:ACCSystemG:ACCSystemGroupAction χS:χ.Sols⊢ 1 S.val = S.valχ:ACCSystemG:ACCSystemGroupAction χS:χ.Sols⊢ 1 S.val = S.val]χ:ACCSystemG:ACCSystemGroupAction χS:χ.Sols⊢ 1 S.val = S.val
    rflAll goals completed! 🐙

              lemma quadSolAction_solAction_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group)
    (S : χ.Sols) : χ.solsInclQuadSols (G.solAction.toFun _ _ S g) =
    G.quadSolAction.toFun _ _ (χ.solsInclQuadSols S) g := rfllemma linSolRep_solAction_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group)
    (S : χ.Sols) : χ.solsInclLinSols (G.solAction.toFun _ _ S g) =
    G.linSolRep g (χ.solsInclLinSols S) := rfllemma rep_solAction_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group)
    (S : χ.Sols) : χ.solsIncl (G.solAction.toFun _ _ S g) = G.rep g (χ.solsIncl S) := rfl