Permutations of SM with no RHN.

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

def SM.PermGroup (n : ℕ) : Type

The group of Sₙ permutations for each species.

Equations

• SM.PermGroup n = (Fin 5 → Equiv.Perm (Fin n))

instance SM.instGroupPermGroup {n : ℕ} : Group (PermGroup n)

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

Equations

• SM.instGroupPermGroup = Pi.group

def SM.chargeMap {n : ℕ} (f : PermGroup n) : (SMCharges n).Charges →ₗ[ℚ] (SMCharges n).Charges

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

Equations

• SM.chargeMap f = { toFun := fun (S : (SMCharges n).Charges) => SMCharges.toSpeciesEquiv.symm fun (i : Fin 5) => (SMCharges.toSpecies i) S ∘ ⇑(f i), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem SM.chargeMap_apply {n : ℕ} (f : PermGroup n) (S : (SMCharges n).Charges) : (chargeMap f) S = SMCharges.toSpeciesEquiv.symm fun (i : Fin 5) => (SMCharges.toSpecies i) S ∘ ⇑(f i)

def SM.repCharges {n : ℕ} : Representation ℚ (PermGroup n) (SMCharges n).Charges

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

Equations

• SM.repCharges = { toFun := fun (f : SM.PermGroup n) => SM.chargeMap f⁻¹, map_one' := ⋯, map_mul' := ⋯ }

theorem SM.repCharges_toSpecies {n : ℕ} (f : PermGroup n) (S : (SMCharges n).Charges) (j : Fin 5) : (SMCharges.toSpecies j) ((repCharges f) S) = (SMCharges.toSpecies j) S ∘ ⇑(f⁻¹ j)

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.

theorem SM.toSpecies_sum_invariant {n : ℕ} (m : ℕ) (f : PermGroup n) (S : (SMCharges n).Charges) (j : Fin 5) : ∑ i : Fin (SMSpecies n).numberCharges, ((fun (a : ℚ) => a ^ m) ∘ (SMCharges.toSpecies j) ((repCharges f) S)) i = ∑ i : Fin (SMSpecies n).numberCharges, ((fun (a : ℚ) => a ^ m) ∘ (SMCharges.toSpecies j) S) i

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

theorem SM.accGrav_invariant {n : ℕ} (f : PermGroup n) (S : (SMCharges n).Charges) : SMACCs.accGrav ((repCharges f) S) = SMACCs.accGrav S

The gravitational anomaly equations is invariant under family permutations.

theorem SM.accSU2_invariant {n : ℕ} (f : PermGroup n) (S : (SMCharges n).Charges) : SMACCs.accSU2 ((repCharges f) S) = SMACCs.accSU2 S

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

theorem SM.accSU3_invariant {n : ℕ} (f : PermGroup n) (S : (SMCharges n).Charges) : SMACCs.accSU3 ((repCharges f) S) = SMACCs.accSU3 S

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

theorem SM.accYY_invariant {n : ℕ} (f : PermGroup n) (S : (SMCharges n).Charges) : SMACCs.accYY ((repCharges f) S) = SMACCs.accYY S

The Y² anomaly equation is invariant under family permutations.

theorem SM.accQuad_invariant {n : ℕ} (f : PermGroup n) (S : (SMCharges n).Charges) : SMACCs.accQuad ((repCharges f) S) = SMACCs.accQuad S

The quadratic anomaly equation is invariant under family permutations.

theorem SM.accCube_invariant {n : ℕ} (f : PermGroup n) (S : (SMCharges n).Charges) : SMACCs.accCube ((repCharges f) S) = SMACCs.accCube S

The cubic anomaly equation is invariant under family permutations.