Family Maps for SM with RHN (no hypercharge)

We give some propererties of the family maps for the SM with RHN, in particular, we define family universal maps in the case of LinSols, QuadSols, and Sols.

def SMRHN.SM.familyUniversalLinear (n : ℕ) : (SM 1).LinSols →ₗ[ℚ] (SM n).LinSols

The family universal maps on LinSols.

Equations

• SMRHN.SM.familyUniversalLinear n = { toFun := fun (S : (SMRHN.SM 1).LinSols) => SMRHN.SM.chargeToLinear ((SMRHN.familyUniversal n) S.val) ⋯ ⋯ ⋯, map_add' := ⋯, map_smul' := ⋯ }

def SMRHN.SM.familyUniversalQuad (n : ℕ) : (SM 1).QuadSols → (SM n).QuadSols

The family universal maps on QuadSols.

Equations

• SMRHN.SM.familyUniversalQuad n S = SMRHN.SM.chargeToQuad ((SMRHN.familyUniversal n) S.val) ⋯ ⋯ ⋯

def SMRHN.SM.familyUniversalAF (n : ℕ) : (SM 1).Sols → (SM n).Sols

The family universal maps on Sols.

Equations

• SMRHN.SM.familyUniversalAF n S = SMRHN.SM.chargeToAF ((SMRHN.familyUniversal n) S.val) ⋯ ⋯ ⋯ ⋯