Physlib.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.Permutations

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.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.Basic
public import Mathlib.RepresentationTheory.Basic

Permutations of MSSM charges and solutions

The three family MSSM charges has a family permutation of S₃⁶. This file defines this group and its action on the MSSM.

@[expose] public section

The group of family permutations is S₃⁶

@[simp]
def PermGroup := Fin 6 → Equiv.Perm (Fin 3)

The type PermGroup has a group instances derived from the group instance of it's target.

@[simp]
instance : Group PermGroup := Pi.group

The image of an element of permGroup under the representation on charges.


@[simps!]
def chargeMap (f : PermGroup) : MSSMCharges.Charges →ₗ[ℚ] MSSMCharges.Charges where
  toFun S := toSpecies.symm (fun i => toSMSpecies i S ∘ f i, Prod.snd (toSpecies S))
  map_add' S T := byf:PermGroupS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ toSpecies.symm (fun i => (toSMSpecies i) (S + T) ∘ ⇑(f i), (toSpecies (S + T)).2) =
  toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2) +
    toSpecies.symm (fun i => (toSMSpecies i) T ∘ ⇑(f i), (toSpecies T).2)
    rw [charges_eq_toSpecies_eqf:PermGroupS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ (∀ (i : Fin 6),
    (toSMSpecies i) (toSpecies.symm (fun i => (toSMSpecies i) (S + T) ∘ ⇑(f i), (toSpecies (S + T)).2)) =
      (toSMSpecies i)
        (toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2) +
          toSpecies.symm (fun i => (toSMSpecies i) T ∘ ⇑(f i), (toSpecies T).2))) ∧
  Hd (toSpecies.symm (fun i => (toSMSpecies i) (S + T) ∘ ⇑(f i), (toSpecies (S + T)).2)) =
      Hd
        (toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2) +
          toSpecies.symm (fun i => (toSMSpecies i) T ∘ ⇑(f i), (toSpecies T).2)) ∧
    Hu (toSpecies.symm (fun i => (toSMSpecies i) (S + T) ∘ ⇑(f i), (toSpecies (S + T)).2)) =
      Hu
        (toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2) +
          toSpecies.symm (fun i => (toSMSpecies i) T ∘ ⇑(f i), (toSpecies T).2))f:PermGroupS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ (∀ (i : Fin 6),
    (toSMSpecies i) (toSpecies.symm (fun i => (toSMSpecies i) (S + T) ∘ ⇑(f i), (toSpecies (S + T)).2)) =
      (toSMSpecies i)
        (toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2) +
          toSpecies.symm (fun i => (toSMSpecies i) T ∘ ⇑(f i), (toSpecies T).2))) ∧
  Hd (toSpecies.symm (fun i => (toSMSpecies i) (S + T) ∘ ⇑(f i), (toSpecies (S + T)).2)) =
      Hd
        (toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2) +
          toSpecies.symm (fun i => (toSMSpecies i) T ∘ ⇑(f i), (toSpecies T).2)) ∧
    Hu (toSpecies.symm (fun i => (toSMSpecies i) (S + T) ∘ ⇑(f i), (toSpecies (S + T)).2)) =
      Hu
        (toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2) +
          toSpecies.symm (fun i => (toSMSpecies i) T ∘ ⇑(f i), (toSpecies T).2))]f:PermGroupS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ (∀ (i : Fin 6),
    (toSMSpecies i) (toSpecies.symm (fun i => (toSMSpecies i) (S + T) ∘ ⇑(f i), (toSpecies (S + T)).2)) =
      (toSMSpecies i)
        (toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2) +
          toSpecies.symm (fun i => (toSMSpecies i) T ∘ ⇑(f i), (toSpecies T).2))) ∧
  Hd (toSpecies.symm (fun i => (toSMSpecies i) (S + T) ∘ ⇑(f i), (toSpecies (S + T)).2)) =
      Hd
        (toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2) +
          toSpecies.symm (fun i => (toSMSpecies i) T ∘ ⇑(f i), (toSpecies T).2)) ∧
    Hu (toSpecies.symm (fun i => (toSMSpecies i) (S + T) ∘ ⇑(f i), (toSpecies (S + T)).2)) =
      Hu
        (toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2) +
          toSpecies.symm (fun i => (toSMSpecies i) T ∘ ⇑(f i), (toSpecies T).2))
    refine And.intro ?_ $ Prod.mk_inj.mp rflf:PermGroupS:MSSMCharges.ChargesT:MSSMCharges.Charges⊢ ∀ (i : Fin 6),
  (toSMSpecies i) (toSpecies.symm (fun i => (toSMSpecies i) (S + T) ∘ ⇑(f i), (toSpecies (S + T)).2)) =
    (toSMSpecies i)
      (toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2) +
        toSpecies.symm (fun i => (toSMSpecies i) T ∘ ⇑(f i), (toSpecies T).2))
    intro if:PermGroupS:MSSMCharges.ChargesT:MSSMCharges.Chargesi:Fin 6⊢ (toSMSpecies i) (toSpecies.symm (fun i => (toSMSpecies i) (S + T) ∘ ⇑(f i), (toSpecies (S + T)).2)) =
  (toSMSpecies i)
    (toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2) +
      toSpecies.symm (fun i => (toSMSpecies i) T ∘ ⇑(f i), (toSpecies T).2))
    rw [(toSMSpecies i).map_addf:PermGroupS:MSSMCharges.ChargesT:MSSMCharges.Chargesi:Fin 6⊢ (toSMSpecies i) (toSpecies.symm (fun i => (toSMSpecies i) (S + T) ∘ ⇑(f i), (toSpecies (S + T)).2)) =
  (toSMSpecies i) (toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2)) +
    (toSMSpecies i) (toSpecies.symm (fun i => (toSMSpecies i) T ∘ ⇑(f i), (toSpecies T).2))f:PermGroupS:MSSMCharges.ChargesT:MSSMCharges.Chargesi:Fin 6⊢ (toSMSpecies i) (toSpecies.symm (fun i => (toSMSpecies i) (S + T) ∘ ⇑(f i), (toSpecies (S + T)).2)) =
  (toSMSpecies i) (toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2)) +
    (toSMSpecies i) (toSpecies.symm (fun i => (toSMSpecies i) T ∘ ⇑(f i), (toSpecies T).2))]f:PermGroupS:MSSMCharges.ChargesT:MSSMCharges.Chargesi:Fin 6⊢ (toSMSpecies i) (toSpecies.symm (fun i => (toSMSpecies i) (S + T) ∘ ⇑(f i), (toSpecies (S + T)).2)) =
  (toSMSpecies i) (toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2)) +
    (toSMSpecies i) (toSpecies.symm (fun i => (toSMSpecies i) T ∘ ⇑(f i), (toSpecies T).2))
    rw [toSMSpecies_toSpecies_inv,f:PermGroupS:MSSMCharges.ChargesT:MSSMCharges.Chargesi:Fin 6⊢ (fun i => (toSMSpecies i) (S + T) ∘ ⇑(f i), (toSpecies (S + T)).2).1 i =
  (toSMSpecies i) (toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2)) +
    (toSMSpecies i) (toSpecies.symm (fun i => (toSMSpecies i) T ∘ ⇑(f i), (toSpecies T).2))f:PermGroupS:MSSMCharges.ChargesT:MSSMCharges.Chargesi:Fin 6⊢ (fun i => (toSMSpecies i) (S + T) ∘ ⇑(f i), (toSpecies (S + T)).2).1 i =
  (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2).1 i +
    (fun i => (toSMSpecies i) T ∘ ⇑(f i), (toSpecies T).2).1 i toSMSpecies_toSpecies_inv,f:PermGroupS:MSSMCharges.ChargesT:MSSMCharges.Chargesi:Fin 6⊢ (fun i => (toSMSpecies i) (S + T) ∘ ⇑(f i), (toSpecies (S + T)).2).1 i =
  (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2).1 i +
    (toSMSpecies i) (toSpecies.symm (fun i => (toSMSpecies i) T ∘ ⇑(f i), (toSpecies T).2))f:PermGroupS:MSSMCharges.ChargesT:MSSMCharges.Chargesi:Fin 6⊢ (fun i => (toSMSpecies i) (S + T) ∘ ⇑(f i), (toSpecies (S + T)).2).1 i =
  (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2).1 i +
    (fun i => (toSMSpecies i) T ∘ ⇑(f i), (toSpecies T).2).1 i toSMSpecies_toSpecies_invf:PermGroupS:MSSMCharges.ChargesT:MSSMCharges.Chargesi:Fin 6⊢ (fun i => (toSMSpecies i) (S + T) ∘ ⇑(f i), (toSpecies (S + T)).2).1 i =
  (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2).1 i +
    (fun i => (toSMSpecies i) T ∘ ⇑(f i), (toSpecies T).2).1 if:PermGroupS:MSSMCharges.ChargesT:MSSMCharges.Chargesi:Fin 6⊢ (fun i => (toSMSpecies i) (S + T) ∘ ⇑(f i), (toSpecies (S + T)).2).1 i =
  (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2).1 i +
    (fun i => (toSMSpecies i) T ∘ ⇑(f i), (toSpecies T).2).1 i]f:PermGroupS:MSSMCharges.ChargesT:MSSMCharges.Chargesi:Fin 6⊢ (fun i => (toSMSpecies i) (S + T) ∘ ⇑(f i), (toSpecies (S + T)).2).1 i =
  (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2).1 i +
    (fun i => (toSMSpecies i) T ∘ ⇑(f i), (toSpecies T).2).1 i
    rflAll goals completed! 🐙
  map_smul' a S := byf:PermGroupa:ℚS:MSSMCharges.Charges⊢ toSpecies.symm (fun i => (toSMSpecies i) (a • S) ∘ ⇑(f i), (toSpecies (a • S)).2) =
  (RingHom.id ℚ) a • toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2)
    rw [charges_eq_toSpecies_eqf:PermGroupa:ℚS:MSSMCharges.Charges⊢ (∀ (i : Fin 6),
    (toSMSpecies i) (toSpecies.symm (fun i => (toSMSpecies i) (a • S) ∘ ⇑(f i), (toSpecies (a • S)).2)) =
      (toSMSpecies i) ((RingHom.id ℚ) a • toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2))) ∧
  Hd (toSpecies.symm (fun i => (toSMSpecies i) (a • S) ∘ ⇑(f i), (toSpecies (a • S)).2)) =
      Hd ((RingHom.id ℚ) a • toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2)) ∧
    Hu (toSpecies.symm (fun i => (toSMSpecies i) (a • S) ∘ ⇑(f i), (toSpecies (a • S)).2)) =
      Hu ((RingHom.id ℚ) a • toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2))f:PermGroupa:ℚS:MSSMCharges.Charges⊢ (∀ (i : Fin 6),
    (toSMSpecies i) (toSpecies.symm (fun i => (toSMSpecies i) (a • S) ∘ ⇑(f i), (toSpecies (a • S)).2)) =
      (toSMSpecies i) ((RingHom.id ℚ) a • toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2))) ∧
  Hd (toSpecies.symm (fun i => (toSMSpecies i) (a • S) ∘ ⇑(f i), (toSpecies (a • S)).2)) =
      Hd ((RingHom.id ℚ) a • toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2)) ∧
    Hu (toSpecies.symm (fun i => (toSMSpecies i) (a • S) ∘ ⇑(f i), (toSpecies (a • S)).2)) =
      Hu ((RingHom.id ℚ) a • toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2))]f:PermGroupa:ℚS:MSSMCharges.Charges⊢ (∀ (i : Fin 6),
    (toSMSpecies i) (toSpecies.symm (fun i => (toSMSpecies i) (a • S) ∘ ⇑(f i), (toSpecies (a • S)).2)) =
      (toSMSpecies i) ((RingHom.id ℚ) a • toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2))) ∧
  Hd (toSpecies.symm (fun i => (toSMSpecies i) (a • S) ∘ ⇑(f i), (toSpecies (a • S)).2)) =
      Hd ((RingHom.id ℚ) a • toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2)) ∧
    Hu (toSpecies.symm (fun i => (toSMSpecies i) (a • S) ∘ ⇑(f i), (toSpecies (a • S)).2)) =
      Hu ((RingHom.id ℚ) a • toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2))
    apply And.intro ?_ $ Prod.mk_inj.mp rflf:PermGroupa:ℚS:MSSMCharges.Charges⊢ ∀ (i : Fin 6),
  (toSMSpecies i) (toSpecies.symm (fun i => (toSMSpecies i) (a • S) ∘ ⇑(f i), (toSpecies (a • S)).2)) =
    (toSMSpecies i) ((RingHom.id ℚ) a • toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2))
    intro if:PermGroupa:ℚS:MSSMCharges.Chargesi:Fin 6⊢ (toSMSpecies i) (toSpecies.symm (fun i => (toSMSpecies i) (a • S) ∘ ⇑(f i), (toSpecies (a • S)).2)) =
  (toSMSpecies i) ((RingHom.id ℚ) a • toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2))
    rw [(toSMSpecies i).map_smul,f:PermGroupa:ℚS:MSSMCharges.Chargesi:Fin 6⊢ (toSMSpecies i) (toSpecies.symm (fun i => (toSMSpecies i) (a • S) ∘ ⇑(f i), (toSpecies (a • S)).2)) =
  (RingHom.id ℚ) a • (toSMSpecies i) (toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2))f:PermGroupa:ℚS:MSSMCharges.Chargesi:Fin 6⊢ (fun i => (toSMSpecies i) (a • S) ∘ ⇑(f i), (toSpecies (a • S)).2).1 i =
  (RingHom.id ℚ) a • (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2).1 i toSMSpecies_toSpecies_inv,f:PermGroupa:ℚS:MSSMCharges.Chargesi:Fin 6⊢ (fun i => (toSMSpecies i) (a • S) ∘ ⇑(f i), (toSpecies (a • S)).2).1 i =
  (RingHom.id ℚ) a • (toSMSpecies i) (toSpecies.symm (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2))f:PermGroupa:ℚS:MSSMCharges.Chargesi:Fin 6⊢ (fun i => (toSMSpecies i) (a • S) ∘ ⇑(f i), (toSpecies (a • S)).2).1 i =
  (RingHom.id ℚ) a • (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2).1 i toSMSpecies_toSpecies_invf:PermGroupa:ℚS:MSSMCharges.Chargesi:Fin 6⊢ (fun i => (toSMSpecies i) (a • S) ∘ ⇑(f i), (toSpecies (a • S)).2).1 i =
  (RingHom.id ℚ) a • (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2).1 if:PermGroupa:ℚS:MSSMCharges.Chargesi:Fin 6⊢ (fun i => (toSMSpecies i) (a • S) ∘ ⇑(f i), (toSpecies (a • S)).2).1 i =
  (RingHom.id ℚ) a • (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2).1 i]f:PermGroupa:ℚS:MSSMCharges.Chargesi:Fin 6⊢ (fun i => (toSMSpecies i) (a • S) ∘ ⇑(f i), (toSpecies (a • S)).2).1 i =
  (RingHom.id ℚ) a • (fun i => (toSMSpecies i) S ∘ ⇑(f i), (toSpecies S).2).1 i
    rflAll goals completed! 🐙

lemma chargeMap_toSpecies (f : PermGroup) (S : MSSMCharges.Charges) (j : Fin 6) :
    toSMSpecies j (chargeMap f S) = toSMSpecies j S ∘ f j :=
  toSMSpecies_toSpecies_inv _ _

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


@[simp]
def repCharges : Representation ℚ PermGroup (MSSMCharges).Charges where
  toFun f := chargeMap f⁻¹
  map_mul' f g := byf:PermGroupg:PermGroup⊢ chargeMap (f * g)⁻¹ = chargeMap f⁻¹ * chargeMap g⁻¹
    simp only [PermGroup]f:PermGroupg:PermGroup⊢ chargeMap (f * g)⁻¹ = chargeMap f⁻¹ * chargeMap g⁻¹
    apply LinearMap.extf:PermGroupg:PermGroup⊢ ∀ (x : MSSMCharges.Charges), (chargeMap (f * g)⁻¹) x = (chargeMap f⁻¹ * chargeMap g⁻¹) x
    intro Sf:PermGroupg:PermGroupS:MSSMCharges.Charges⊢ (chargeMap (f * g)⁻¹) S = (chargeMap f⁻¹ * chargeMap g⁻¹) S
    rw [charges_eq_toSpecies_eqf:PermGroupg:PermGroupS:MSSMCharges.Charges⊢ (∀ (i : Fin 6), (toSMSpecies i) ((chargeMap (f * g)⁻¹) S) = (toSMSpecies i) ((chargeMap f⁻¹ * chargeMap g⁻¹) S)) ∧
  Hd ((chargeMap (f * g)⁻¹) S) = Hd ((chargeMap f⁻¹ * chargeMap g⁻¹) S) ∧
    Hu ((chargeMap (f * g)⁻¹) S) = Hu ((chargeMap f⁻¹ * chargeMap g⁻¹) S)f:PermGroupg:PermGroupS:MSSMCharges.Charges⊢ (∀ (i : Fin 6), (toSMSpecies i) ((chargeMap (f * g)⁻¹) S) = (toSMSpecies i) ((chargeMap f⁻¹ * chargeMap g⁻¹) S)) ∧
  Hd ((chargeMap (f * g)⁻¹) S) = Hd ((chargeMap f⁻¹ * chargeMap g⁻¹) S) ∧
    Hu ((chargeMap (f * g)⁻¹) S) = Hu ((chargeMap f⁻¹ * chargeMap g⁻¹) S)]f:PermGroupg:PermGroupS:MSSMCharges.Charges⊢ (∀ (i : Fin 6), (toSMSpecies i) ((chargeMap (f * g)⁻¹) S) = (toSMSpecies i) ((chargeMap f⁻¹ * chargeMap g⁻¹) S)) ∧
  Hd ((chargeMap (f * g)⁻¹) S) = Hd ((chargeMap f⁻¹ * chargeMap g⁻¹) S) ∧
    Hu ((chargeMap (f * g)⁻¹) S) = Hu ((chargeMap f⁻¹ * chargeMap g⁻¹) S)
    refine And.intro ?_ $ Prod.mk_inj.mp rflf:PermGroupg:PermGroupS:MSSMCharges.Charges⊢ ∀ (i : Fin 6), (toSMSpecies i) ((chargeMap (f * g)⁻¹) S) = (toSMSpecies i) ((chargeMap f⁻¹ * chargeMap g⁻¹) S)
    intro if:PermGroupg:PermGroupS:MSSMCharges.Chargesi:Fin 6⊢ (toSMSpecies i) ((chargeMap (f * g)⁻¹) S) = (toSMSpecies i) ((chargeMap f⁻¹ * chargeMap g⁻¹) S)
    simp only [Module.End.mul_apply]f:PermGroupg:PermGroupS:MSSMCharges.Chargesi:Fin 6⊢ (toSMSpecies i) ((chargeMap (f * g)⁻¹) S) = (toSMSpecies i) ((chargeMap f⁻¹) ((chargeMap g⁻¹) S))
    rw [chargeMap_toSpecies,f:PermGroupg:PermGroupS:MSSMCharges.Chargesi:Fin 6⊢ (toSMSpecies i) S ∘ ⇑((f * g)⁻¹ i) = (toSMSpecies i) ((chargeMap f⁻¹) ((chargeMap g⁻¹) S))f:PermGroupg:PermGroupS:MSSMCharges.Chargesi:Fin 6⊢ (toSMSpecies i) S ∘ ⇑((f * g)⁻¹ i) = (toSMSpecies i) ((chargeMap g⁻¹) S) ∘ ⇑(f⁻¹ i) chargeMap_toSpeciesf:PermGroupg:PermGroupS:MSSMCharges.Chargesi:Fin 6⊢ (toSMSpecies i) S ∘ ⇑((f * g)⁻¹ i) = (toSMSpecies i) ((chargeMap g⁻¹) S) ∘ ⇑(f⁻¹ i)f:PermGroupg:PermGroupS:MSSMCharges.Chargesi:Fin 6⊢ (toSMSpecies i) S ∘ ⇑((f * g)⁻¹ i) = (toSMSpecies i) ((chargeMap g⁻¹) S) ∘ ⇑(f⁻¹ i)]f:PermGroupg:PermGroupS:MSSMCharges.Chargesi:Fin 6⊢ (toSMSpecies i) S ∘ ⇑((f * g)⁻¹ i) = (toSMSpecies i) ((chargeMap g⁻¹) S) ∘ ⇑(f⁻¹ i)
    simp only [Pi.inv_apply]f:PermGroupg:PermGroupS:MSSMCharges.Chargesi:Fin 6⊢ (toSMSpecies i) S ∘ ⇑((f * g) i)⁻¹ = (toSMSpecies i) ((chargeMap g⁻¹) S) ∘ ⇑(f i)⁻¹
    rw [chargeMap_toSpeciesf:PermGroupg:PermGroupS:MSSMCharges.Chargesi:Fin 6⊢ (toSMSpecies i) S ∘ ⇑((f * g) i)⁻¹ = ((toSMSpecies i) S ∘ ⇑(g⁻¹ i)) ∘ ⇑(f i)⁻¹f:PermGroupg:PermGroupS:MSSMCharges.Chargesi:Fin 6⊢ (toSMSpecies i) S ∘ ⇑((f * g) i)⁻¹ = ((toSMSpecies i) S ∘ ⇑(g⁻¹ i)) ∘ ⇑(f i)⁻¹]f:PermGroupg:PermGroupS:MSSMCharges.Chargesi:Fin 6⊢ (toSMSpecies i) S ∘ ⇑((f * g) i)⁻¹ = ((toSMSpecies i) S ∘ ⇑(g⁻¹ i)) ∘ ⇑(f i)⁻¹
    rflAll goals completed! 🐙
  map_one' := by⊢ chargeMap 1⁻¹ = 1
    apply LinearMap.ext⊢ ∀ (x : MSSMCharges.Charges), (chargeMap 1⁻¹) x = 1 x
    intro SS:MSSMCharges.Charges⊢ (chargeMap 1⁻¹) S = 1 S
    rw [charges_eq_toSpecies_eqS:MSSMCharges.Charges⊢ (∀ (i : Fin 6), (toSMSpecies i) ((chargeMap 1⁻¹) S) = (toSMSpecies i) (1 S)) ∧
  Hd ((chargeMap 1⁻¹) S) = Hd (1 S) ∧ Hu ((chargeMap 1⁻¹) S) = Hu (1 S)S:MSSMCharges.Charges⊢ (∀ (i : Fin 6), (toSMSpecies i) ((chargeMap 1⁻¹) S) = (toSMSpecies i) (1 S)) ∧
  Hd ((chargeMap 1⁻¹) S) = Hd (1 S) ∧ Hu ((chargeMap 1⁻¹) S) = Hu (1 S)]S:MSSMCharges.Charges⊢ (∀ (i : Fin 6), (toSMSpecies i) ((chargeMap 1⁻¹) S) = (toSMSpecies i) (1 S)) ∧
  Hd ((chargeMap 1⁻¹) S) = Hd (1 S) ∧ Hu ((chargeMap 1⁻¹) S) = Hu (1 S)
    refine And.intro ?_ $ Prod.mk_inj.mp rflS:MSSMCharges.Charges⊢ ∀ (i : Fin 6), (toSMSpecies i) ((chargeMap 1⁻¹) S) = (toSMSpecies i) (1 S)
    intro iS:MSSMCharges.Chargesi:Fin 6⊢ (toSMSpecies i) ((chargeMap 1⁻¹) S) = (toSMSpecies i) (1 S)
    exact toSMSpecies_toSpecies_inv _ _All goals completed! 🐙

              lemma repCharges_toSMSpecies (f : PermGroup) (S : MSSMCharges.Charges) (j : Fin 6) :
    toSMSpecies j (repCharges f S) = toSMSpecies j S ∘ f⁻¹ j :=
  toSMSpecies_toSpecies_inv _ _

lemma toSpecies_sum_invariant (m : ℕ) (f : PermGroup) (S : MSSMCharges.Charges) (j : Fin 6) :
    ∑ i, ((fun a => a ^ m) ∘ toSMSpecies j (repCharges f S)) i =
    ∑ i, ((fun a => a ^ m) ∘ toSMSpecies j S) i := bym:ℕf:PermGroupS:MSSMCharges.Chargesj:Fin 6⊢ ∑ i, ((fun a => a ^ m) ∘ (toSMSpecies j) ((repCharges f) S)) i = ∑ i, ((fun a => a ^ m) ∘ (toSMSpecies j) S) i
  rw [repCharges_toSMSpeciesm:ℕf:PermGroupS:MSSMCharges.Chargesj:Fin 6⊢ ∑ i, ((fun a => a ^ m) ∘ (toSMSpecies j) S ∘ ⇑(f⁻¹ j)) i = ∑ i, ((fun a => a ^ m) ∘ (toSMSpecies j) S) im:ℕf:PermGroupS:MSSMCharges.Chargesj:Fin 6⊢ ∑ i, ((fun a => a ^ m) ∘ (toSMSpecies j) S ∘ ⇑(f⁻¹ j)) i = ∑ i, ((fun a => a ^ m) ∘ (toSMSpecies j) S) i]m:ℕf:PermGroupS:MSSMCharges.Chargesj:Fin 6⊢ ∑ i, ((fun a => a ^ m) ∘ (toSMSpecies j) S ∘ ⇑(f⁻¹ j)) i = ∑ i, ((fun a => a ^ m) ∘ (toSMSpecies j) S) i
  exact Equiv.sum_comp (f⁻¹ j) ((fun a => a ^ m) ∘ (toSMSpecies j) S)All goals completed! 🐙lemma Hd_invariant (f : PermGroup) (S : MSSMCharges.Charges) :
    Hd (repCharges f S) = Hd S := rfllemma Hu_invariant (f : PermGroup) (S : MSSMCharges.Charges) :
    Hu (repCharges f S) = Hu S := rfllemma accGrav_invariant (f : PermGroup) (S : MSSMCharges.Charges) :
    accGrav (repCharges f S) = accGrav S :=
  accGrav_ext
    (byf:PermGroupS:MSSMCharges.Charges⊢ ∀ (j : Fin 6), ∑ i, (toSMSpecies j) ((repCharges f) S) i = ∑ i, (toSMSpecies j) S i simpa using toSpecies_sum_invariant 1 f SAll goals completed! 🐙)
    (Hd_invariant f S)
    (Hu_invariant f S)lemma accSU2_invariant (f : PermGroup) (S : MSSMCharges.Charges) :
    accSU2 (repCharges f S) = accSU2 S :=
  accSU2_ext
    (byf:PermGroupS:MSSMCharges.Charges⊢ ∀ (j : Fin 6), ∑ i, (toSMSpecies j) ((repCharges f) S) i = ∑ i, (toSMSpecies j) S i simpa using toSpecies_sum_invariant 1 f SAll goals completed! 🐙)
    (Hd_invariant f S)
    (Hu_invariant f S)lemma accSU3_invariant (f : PermGroup) (S : MSSMCharges.Charges) :
    accSU3 (repCharges f S) = accSU3 S :=
  accSU3_ext
    (byf:PermGroupS:MSSMCharges.Charges⊢ ∀ (j : Fin 6), ∑ i, (toSMSpecies j) ((repCharges f) S) i = ∑ i, (toSMSpecies j) S i simpa using toSpecies_sum_invariant 1 f SAll goals completed! 🐙)lemma accYY_invariant (f : PermGroup) (S : MSSMCharges.Charges) :
    accYY (repCharges f S) = accYY S :=
  accYY_ext
    (byf:PermGroupS:MSSMCharges.Charges⊢ ∀ (j : Fin 6), ∑ i, (toSMSpecies j) ((repCharges f) S) i = ∑ i, (toSMSpecies j) S i simpa using toSpecies_sum_invariant 1 f SAll goals completed! 🐙)
    (Hd_invariant f S)
    (Hu_invariant f S)lemma accQuad_invariant (f : PermGroup) (S : MSSMCharges.Charges) :
    accQuad (repCharges f S) = accQuad S :=
  accQuad_ext
    (toSpecies_sum_invariant 2 f S)
    (Hd_invariant f S)
    (Hu_invariant f S)lemma accCube_invariant (f : PermGroup) (S : MSSMCharges.Charges) :
    accCube (repCharges f S) = accCube S :=
  accCube_ext
    (toSpecies_sum_invariant 3 f S)
    (Hd_invariant f S)
    (Hu_invariant f S)