Permutations of SM charges with RHN.

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

def SMRHN.PermGroup (n : ℕ) : Type

The group of Sₙ permutations for each species.

Equations

• SMRHN.PermGroup n = (Fin 6 → Equiv.Perm (Fin n))

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

The instance of a group on PermGroup n through the target space Equiv.Perm (Fin n).

Equations

• SMRHN.instGroupPermGroup = Pi.group

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

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

Equations

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

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

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

theorem SMRHN.accGrav_invariant {n : ℕ} (f : PermGroup n) (S : (SMνCharges n).Charges) : SMνACCs.accGrav ((repCharges f) S) = SMνACCs.accGrav S

theorem SMRHN.accSU2_invariant {n : ℕ} (f : PermGroup n) (S : (SMνCharges n).Charges) : SMνACCs.accSU2 ((repCharges f) S) = SMνACCs.accSU2 S

theorem SMRHN.accSU3_invariant {n : ℕ} (f : PermGroup n) (S : (SMνCharges n).Charges) : SMνACCs.accSU3 ((repCharges f) S) = SMνACCs.accSU3 S

theorem SMRHN.accYY_invariant {n : ℕ} (f : PermGroup n) (S : (SMνCharges n).Charges) : SMνACCs.accYY ((repCharges f) S) = SMνACCs.accYY S

theorem SMRHN.accQuad_invariant {n : ℕ} (f : PermGroup n) (S : (SMνCharges n).Charges) : SMνACCs.accQuad ((repCharges f) S) = SMνACCs.accQuad S

theorem SMRHN.accCube_invariant {n : ℕ} (f : PermGroup n) (S : (SMνCharges n).Charges) : SMνACCs.accCube ((repCharges f) S) = SMνACCs.accCube S