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.

def MSSM.PermGroup : Type

The group of family permutations is S₃⁶

Equations

• MSSM.PermGroup = (Fin 6 → Equiv.Perm (Fin 3))

instance MSSM.instGroupPermGroup : Group MSSM.PermGroup

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

Equations

• MSSM.instGroupPermGroup = Pi.group

def MSSM.chargeMap (f : MSSM.PermGroup) : MSSMCharges.Charges →ₗ[ℚ] MSSMCharges.Charges

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

Equations

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

@[simp]

theorem MSSM.chargeMap_apply (f : MSSM.PermGroup) (S : MSSMCharges.Charges) : (MSSM.chargeMap f) S = MSSMCharges.toSMPlusH.symm (MSSMCharges.splitSMPlusH.symm (MSSMCharges.toSpeciesMaps'.symm fun (i : Fin 6) => (MSSMCharges.toSMSpecies i) S ∘ ⇑(f i), MSSMCharges.toSMPlusH S ∘ Sum.inr))

theorem MSSM.chargeMap_toSpecies (f : MSSM.PermGroup) (S : MSSMCharges.Charges) (j : Fin 6) : (MSSMCharges.toSMSpecies j) ((MSSM.chargeMap f) S) = (MSSMCharges.toSMSpecies j) S ∘ ⇑(f j)

def MSSM.repCharges : Representation ℚ MSSM.PermGroup MSSMCharges.Charges

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

Equations

• MSSM.repCharges = { toFun := fun (f : MSSM.PermGroup) => MSSM.chargeMap f⁻¹, map_one' := MSSM.repCharges.proof_1, map_mul' := MSSM.repCharges.proof_2 }

theorem MSSM.repCharges_toSMSpecies (f : MSSM.PermGroup) (S : MSSMCharges.Charges) (j : Fin 6) : (MSSMCharges.toSMSpecies j) ((MSSM.repCharges f) S) = (MSSMCharges.toSMSpecies j) S ∘ ⇑(f⁻¹ j)

theorem MSSM.toSpecies_sum_invariant (m : ℕ) (f : MSSM.PermGroup) (S : MSSMCharges.Charges) (j : Fin 6) : ∑ i : Fin MSSMSpecies.numberCharges, ((fun (a : ℚ) => a ^ m) ∘ (MSSMCharges.toSMSpecies j) ((MSSM.repCharges f) S)) i = ∑ i : Fin MSSMSpecies.numberCharges, ((fun (a : ℚ) => a ^ m) ∘ (MSSMCharges.toSMSpecies j) S) i

theorem MSSM.Hd_invariant (f : MSSM.PermGroup) (S : MSSMCharges.Charges) : MSSMCharges.Hd ((MSSM.repCharges f) S) = MSSMCharges.Hd S

theorem MSSM.Hu_invariant (f : MSSM.PermGroup) (S : MSSMCharges.Charges) : MSSMCharges.Hu ((MSSM.repCharges f) S) = MSSMCharges.Hu S

theorem MSSM.accGrav_invariant (f : MSSM.PermGroup) (S : MSSMCharges.Charges) : MSSMACCs.accGrav ((MSSM.repCharges f) S) = MSSMACCs.accGrav S

theorem MSSM.accSU2_invariant (f : MSSM.PermGroup) (S : MSSMCharges.Charges) : MSSMACCs.accSU2 ((MSSM.repCharges f) S) = MSSMACCs.accSU2 S

theorem MSSM.accSU3_invariant (f : MSSM.PermGroup) (S : MSSMCharges.Charges) : MSSMACCs.accSU3 ((MSSM.repCharges f) S) = MSSMACCs.accSU3 S

theorem MSSM.accYY_invariant (f : MSSM.PermGroup) (S : MSSMCharges.Charges) : MSSMACCs.accYY ((MSSM.repCharges f) S) = MSSMACCs.accYY S

theorem MSSM.accQuad_invariant (f : MSSM.PermGroup) (S : MSSMCharges.Charges) : MSSMACCs.accQuad ((MSSM.repCharges f) S) = MSSMACCs.accQuad S

theorem MSSM.accCube_invariant (f : MSSM.PermGroup) (S : MSSMCharges.Charges) : MSSMACCs.accCube ((MSSM.repCharges f) S) = MSSMACCs.accCube S