The MSSM with 3 families and RHNs #

We define the system of ACCs for the MSSM with 3 families and RHNs. We define the system of charges for 1-species. We prove some basic lemmas about them.

source

def MSSMCharges :

ACCSystemCharges

The vector space of charges corresponding to the MSSM fermions.

Equations

MSSMCharges = ACCSystemChargesMk 20

Instances For

source

@[simp]

theorem MSSMCharges_numberCharges :

MSSMCharges.numberCharges = 20

source

def MSSMSpecies :

ACCSystemCharges

The vector spaces of charges of one species of fermions in the MSSM.

Equations

MSSMSpecies = ACCSystemChargesMk 3

Instances For

source

@[simp]

theorem MSSMSpecies_numberCharges :

MSSMSpecies.numberCharges = 3

source

def MSSMCharges.toSMPlusH :

MSSMCharges.Charges ≃ (Fin 18 ⊕ Fin 2 → ℚ)

An equivalence between MSSMCharges.charges and the space of maps (Fin 18 ⊕ Fin 2 → ℚ). The first 18 factors corresponds to the SM fermions, while the last two are the higgsions.

Equations

MSSMCharges.toSMPlusH = (finSumFinEquiv.arrowCongr (Equiv.refl ℚ)).symm

Instances For

source

@[simp]

theorem MSSMCharges.toSMPlusH_symm_apply (a✝ : Fin 18 ⊕ Fin 2 → ℚ) (a✝¹ : Fin (18 + 2)) :

toSMPlusH.symm a✝ a✝¹ = a✝ (finSumFinEquiv.symm a✝¹)

source

@[simp]

theorem MSSMCharges.toSMPlusH_apply (a✝ : Fin (18 + 2) → ℚ) (a✝¹ : Fin 18 ⊕ Fin 2) :

toSMPlusH a✝ a✝¹ = a✝ (finSumFinEquiv a✝¹)

source

def MSSMCharges.splitSMPlusH :

(Fin 18 ⊕ Fin 2 → ℚ) ≃ (Fin 18 → ℚ) × (Fin 2 → ℚ)

An equivalence between Fin 18 ⊕ Fin 2 → ℚ and (Fin 18 → ℚ) × (Fin 2 → ℚ).

Equations

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

Instances For

source

@[simp]

theorem MSSMCharges.splitSMPlusH_apply (f : Fin 18 ⊕ Fin 2 → ℚ) :

splitSMPlusH f = (f ∘ Sum.inl , f ∘ Sum.inr )

source

@[simp]

theorem MSSMCharges.splitSMPlusH_symm_apply (f : (Fin 18 → ℚ) × (Fin 2 → ℚ)) (a✝ : Fin 18 ⊕ Fin 2) :

splitSMPlusH.symm f a✝ = Sum.elim f.1 f.2 a✝

source

def MSSMCharges.toSplitSMPlusH :

MSSMCharges.Charges ≃ (Fin 18 → ℚ) × (Fin 2 → ℚ)

An equivalence between MSSMCharges.charges and (Fin 18 → ℚ) × (Fin 2 → ℚ). This splits the charges up into the SM and the additional ones for the MSSM.

Equations

MSSMCharges.toSplitSMPlusH = MSSMCharges.toSMPlusH.trans MSSMCharges.splitSMPlusH

Instances For

source

@[simp]

theorem MSSMCharges.toSplitSMPlusH_apply (a✝ : MSSMCharges.Charges) :

toSplitSMPlusH a✝ = (toSMPlusH a✝ ∘ Sum.inl , toSMPlusH a✝ ∘ Sum.inr )

source

@[simp]

theorem MSSMCharges.toSplitSMPlusH_symm_apply (a✝ : (Fin 18 → ℚ) × (Fin 2 → ℚ)) :

toSplitSMPlusH.symm a✝ = toSMPlusH.symm (splitSMPlusH.symm a✝)

source

def MSSMCharges.toSpeciesMaps' :

(Fin 18 → ℚ) ≃ (Fin 6 → Fin 3 → ℚ)

An equivalence between (Fin 18 → ℚ) and (Fin 6 → Fin 3 → ℚ).

Equations

MSSMCharges.toSpeciesMaps' = ((Equiv.curry (Fin 6) (Fin 3) ℚ).symm.trans (finProdFinEquiv.arrowCongr (Equiv.refl ℚ))).symm

Instances For

source

@[simp]

theorem MSSMCharges.toSpeciesMaps'_apply (a✝ : Fin (6 * 3) → ℚ) (a✝¹ : Fin 6) (a✝² : Fin 3) :

toSpeciesMaps' a✝ a✝¹ a✝² = a✝ (finProdFinEquiv (a✝¹, a✝²))

source

@[simp]

theorem MSSMCharges.toSpeciesMaps'_symm_apply (a✝ : Fin 6 → Fin 3 → ℚ) (a✝¹ : Fin (6 * 3)) :

toSpeciesMaps'.symm a✝ a✝¹ = a✝ a✝¹.divNat a✝¹.modNat

source

def MSSMCharges.toSpecies :

MSSMCharges.Charges ≃ (Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ)

An equivalence between MSSMCharges.charges and (Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ)). This splits charges up into the SM and additional fermions, and further splits the SM into species.

Equations