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

Permutations of SM with no RHN.

We define the group of permutations for the SM charges with no RHN.

@[expose] public section

The group of Sₙ permutations for each species.

@[simp]
def PermGroup (n : ℕ) := ∀ (_ : Fin 5), Equiv.Perm (Fin n)

The type PermGroup n inherits the instance of a group from it's target space Equiv.Perm.

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

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

@[simps!]
def chargeMap (f : PermGroup n) : (SMCharges n).Charges →ₗ[ℚ] (SMCharges n).Charges where
  toFun S := toSpeciesEquiv.symm (fun i => toSpecies i S ∘ f i)
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

The representation of (permGroup n) acting on the vector space of charges.


@[simp]
def repCharges {n : ℕ} : Representation ℚ (PermGroup n) (SMCharges n).Charges where
  toFun f := chargeMap f⁻¹
  map_mul' f g := byn✝:ℕn:ℕf:PermGroup ng:PermGroup n⊢ chargeMap (f * g)⁻¹ = chargeMap f⁻¹ * chargeMap g⁻¹
    simp only [PermGroup]n✝:ℕn:ℕf:PermGroup ng:PermGroup n⊢ chargeMap (f * g)⁻¹ = chargeMap f⁻¹ * chargeMap g⁻¹
    apply LinearMap.extn✝:ℕn:ℕf:PermGroup ng:PermGroup n⊢ ∀ (x : (SMCharges n).Charges), (chargeMap (f * g)⁻¹) x = (chargeMap f⁻¹ * chargeMap g⁻¹) x
    intro Sn✝:ℕn:ℕf:PermGroup ng:PermGroup nS:(SMCharges n).Charges⊢ (chargeMap (f * g)⁻¹) S = (chargeMap f⁻¹ * chargeMap g⁻¹) S
    rw [charges_eq_toSpecies_eqn✝:ℕn:ℕf:PermGroup ng:PermGroup nS:(SMCharges n).Charges⊢ ∀ (i : Fin 5), (toSpecies i) ((chargeMap (f * g)⁻¹) S) = (toSpecies i) ((chargeMap f⁻¹ * chargeMap g⁻¹) S)n✝:ℕn:ℕf:PermGroup ng:PermGroup nS:(SMCharges n).Charges⊢ ∀ (i : Fin 5), (toSpecies i) ((chargeMap (f * g)⁻¹) S) = (toSpecies i) ((chargeMap f⁻¹ * chargeMap g⁻¹) S)]n✝:ℕn:ℕf:PermGroup ng:PermGroup nS:(SMCharges n).Charges⊢ ∀ (i : Fin 5), (toSpecies i) ((chargeMap (f * g)⁻¹) S) = (toSpecies i) ((chargeMap f⁻¹ * chargeMap g⁻¹) S)
    intro in✝:ℕn:ℕf:PermGroup ng:PermGroup nS:(SMCharges n).Chargesi:Fin 5⊢ (toSpecies i) ((chargeMap (f * g)⁻¹) S) = (toSpecies i) ((chargeMap f⁻¹ * chargeMap g⁻¹) S)
    simp only [chargeMap_apply, Pi.inv_apply, Module.End.mul_apply]n✝:ℕn:ℕf:PermGroup ng:PermGroup nS:(SMCharges n).Chargesi:Fin 5⊢ (toSpecies i) (toSpeciesEquiv.symm fun i => (toSpecies i) S ∘ ⇑((f * g) i)⁻¹) =
  (toSpecies i)
    (toSpeciesEquiv.symm fun i => (toSpecies i) (toSpeciesEquiv.symm fun i => (toSpecies i) S ∘ ⇑(g i)⁻¹) ∘ ⇑(f i)⁻¹)
    erw [toSMSpecies_toSpecies_inv,n✝:ℕn:ℕf:PermGroup ng:PermGroup nS:(SMCharges n).Chargesi:Fin 5⊢ (toSpecies i) S ∘ ⇑((f * g) i)⁻¹ =
  (toSpecies i)
    (toSpeciesEquiv.symm fun i => (toSpecies i) (toSpeciesEquiv.symm fun i => (toSpecies i) S ∘ ⇑(g i)⁻¹) ∘ ⇑(f i)⁻¹) toSMSpecies_toSpecies_inv,n✝:ℕn:ℕf:PermGroup ng:PermGroup nS:(SMCharges n).Chargesi:Fin 5⊢ (toSpecies i) S ∘ ⇑((f * g) i)⁻¹ = (toSpecies i) (toSpeciesEquiv.symm fun i => (toSpecies i) S ∘ ⇑(g i)⁻¹) ∘ ⇑(f i)⁻¹ toSMSpecies_toSpecies_invn✝:ℕn:ℕf:PermGroup ng:PermGroup nS:(SMCharges n).Chargesi:Fin 5⊢ (toSpecies i) S ∘ ⇑((f * g) i)⁻¹ = ((toSpecies i) S ∘ ⇑(g i)⁻¹) ∘ ⇑(f i)⁻¹]n✝:ℕn:ℕf:PermGroup ng:PermGroup nS:(SMCharges n).Chargesi:Fin 5⊢ (toSpecies i) S ∘ ⇑((f * g) i)⁻¹ = ((toSpecies i) S ∘ ⇑(g i)⁻¹) ∘ ⇑(f i)⁻¹
    rflAll goals completed! 🐙
  map_one' := byn✝:ℕn:ℕ⊢ chargeMap 1⁻¹ = 1
    apply LinearMap.extn✝:ℕn:ℕ⊢ ∀ (x : (SMCharges n).Charges), (chargeMap 1⁻¹) x = 1 x
    intro Sn✝:ℕn:ℕS:(SMCharges n).Charges⊢ (chargeMap 1⁻¹) S = 1 S
    rw [charges_eq_toSpecies_eqn✝:ℕn:ℕS:(SMCharges n).Charges⊢ ∀ (i : Fin 5), (toSpecies i) ((chargeMap 1⁻¹) S) = (toSpecies i) (1 S)n✝:ℕn:ℕS:(SMCharges n).Charges⊢ ∀ (i : Fin 5), (toSpecies i) ((chargeMap 1⁻¹) S) = (toSpecies i) (1 S)]n✝:ℕn:ℕS:(SMCharges n).Charges⊢ ∀ (i : Fin 5), (toSpecies i) ((chargeMap 1⁻¹) S) = (toSpecies i) (1 S)
    intro in✝:ℕn:ℕS:(SMCharges n).Chargesi:Fin 5⊢ (toSpecies i) ((chargeMap 1⁻¹) S) = (toSpecies i) (1 S)
    exact toSMSpecies_toSpecies_inv _ _All goals completed! 🐙

The species charges of a set of charges acted on by a family permutation is the permutation of those species charges with the corresponding part of the family permutation.

lemma repCharges_toSpecies (f : PermGroup n) (S : (SMCharges n).Charges) (j : Fin 5) :
    toSpecies j (repCharges f S) = toSpecies j S ∘ f⁻¹ j :=
  toSMSpecies_toSpecies_inv _ _

The sum over every charge in any species to some power m is invariant under the group action.


lemma toSpecies_sum_invariant (m : ℕ) (f : PermGroup n) (S : (SMCharges n).Charges) (j : Fin 5) :
    ∑ i, ((fun a => a ^ m) ∘ toSpecies j (repCharges f S)) i =
    ∑ i, ((fun a => a ^ m) ∘ toSpecies j S) i := byn:ℕm:ℕf:PermGroup nS:(SMCharges n).Chargesj:Fin 5⊢ ∑ i, ((fun a => a ^ m) ∘ (toSpecies j) ((repCharges f) S)) i = ∑ i, ((fun a => a ^ m) ∘ (toSpecies j) S) i
  rw [repCharges_toSpeciesn:ℕm:ℕf:PermGroup nS:(SMCharges n).Chargesj:Fin 5⊢ ∑ i, ((fun a => a ^ m) ∘ (toSpecies j) S ∘ ⇑(f⁻¹ j)) i = ∑ i, ((fun a => a ^ m) ∘ (toSpecies j) S) in:ℕm:ℕf:PermGroup nS:(SMCharges n).Chargesj:Fin 5⊢ ∑ i, ((fun a => a ^ m) ∘ (toSpecies j) S ∘ ⇑(f⁻¹ j)) i = ∑ i, ((fun a => a ^ m) ∘ (toSpecies j) S) i]n:ℕm:ℕf:PermGroup nS:(SMCharges n).Chargesj:Fin 5⊢ ∑ i, ((fun a => a ^ m) ∘ (toSpecies j) S ∘ ⇑(f⁻¹ j)) i = ∑ i, ((fun a => a ^ m) ∘ (toSpecies j) S) i
  exact Equiv.sum_comp (f⁻¹ j) ((fun a => a ^ m) ∘ toSpecies j S)All goals completed! 🐙

The gravitational anomaly equations is invariant under family permutations.

lemma accGrav_invariant (f : PermGroup n) (S : (SMCharges n).Charges) :
    accGrav (repCharges f S) = accGrav S := accGrav_ext
  (byn:ℕf:PermGroup nS:(SMCharges n).Charges⊢ ∀ (j : Fin 5), ∑ i, (toSpecies j) ((repCharges f) S) i = ∑ i, (toSpecies j) S i simpa using toSpecies_sum_invariant 1 f SAll goals completed! 🐙)

The SU(2) anomaly equation is invariant under family permutations.

lemma accSU2_invariant (f : PermGroup n) (S : (SMCharges n).Charges) :
    accSU2 (repCharges f S) = accSU2 S := accSU2_ext
  (byn:ℕf:PermGroup nS:(SMCharges n).Charges⊢ ∀ (j : Fin 5), ∑ i, (toSpecies j) ((repCharges f) S) i = ∑ i, (toSpecies j) S i simpa using toSpecies_sum_invariant 1 f SAll goals completed! 🐙)

The SU(3) anomaly equation is invariant under family permutations.

lemma accSU3_invariant (f : PermGroup n) (S : (SMCharges n).Charges) :
    accSU3 (repCharges f S) = accSU3 S :=
  accSU3_ext
    (byn:ℕf:PermGroup nS:(SMCharges n).Charges⊢ ∀ (j : Fin 5), ∑ i, (toSpecies j) ((repCharges f) S) i = ∑ i, (toSpecies j) S i simpa using toSpecies_sum_invariant 1 f SAll goals completed! 🐙)

The Y² anomaly equation is invariant under family permutations.

lemma accYY_invariant (f : PermGroup n) (S : (SMCharges n).Charges) :
    accYY (repCharges f S) = accYY S :=
  accYY_ext
    (byn:ℕf:PermGroup nS:(SMCharges n).Charges⊢ ∀ (j : Fin 5), ∑ i, (toSpecies j) ((repCharges f) S) i = ∑ i, (toSpecies j) S i simpa using toSpecies_sum_invariant 1 f SAll goals completed! 🐙)

The quadratic anomaly equation is invariant under family permutations.

lemma accQuad_invariant (f : PermGroup n) (S : (SMCharges n).Charges) :
    accQuad (repCharges f S) = accQuad S :=
  accQuad_ext
    (toSpecies_sum_invariant 2 f S)

The cubic anomaly equation is invariant under family permutations.

lemma accCube_invariant (f : PermGroup n) (S : (SMCharges n).Charges) :
    accCube (repCharges f S) = accCube S :=
  accCube_ext (toSpecies_sum_invariant 3 f S)