Family Maps for SM with RHN

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.PlusU1.familyUniversalLinear (n : ℕ) : (PlusU1 1).LinSols →ₗ[ℚ] (PlusU1 n).LinSols

The family universal maps on LinSols.

Equations

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

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

The family universal maps on QuadSols.

Equations

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

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

The family universal maps on Sols.

Equations

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