The Spin(10) Model

Note: By physicists this is usually called SO(10). However, the true gauge group involved is Spin(10).

def Spin10Model.GaugeGroupI : InformalDefinition

The gauge group of the Spin(10) model, i.e., the group Spin(10).

Equations

• Spin10Model.GaugeGroupI = { deps := [], tag := "6V2X7" }

def Spin10Model.inclPatiSalam : InformalDefinition

The inclusion of the Pati-Salam gauge group into Spin(10), i.e., the lift of the embedding SO(6) × SO(4) → SO(10) to universal covers, giving a homomorphism Spin(6) × Spin(4) → Spin(10). Precomposed with the isomorphism, PatiSalam.gaugeGroupISpinEquiv, between SU(4) × SU(2) × SU(2) and Spin(6) × Spin(4).

See page 56 of https://math.ucr.edu/home/baez/guts.pdf

Equations

• Spin10Model.inclPatiSalam = { deps := [`Spin10Model.GaugeGroupI, `PatiSalam.GaugeGroupI, `PatiSalam.gaugeGroupISpinEquiv], tag := "6V2YG" }

def Spin10Model.inclSM : InformalDefinition

The inclusion of the Standard Model gauge group into Spin(10), i.e., the composition of embedPatiSalam and PatiSalam.inclSM.

See page 56 of https://math.ucr.edu/home/baez/guts.pdf

Equations

• Spin10Model.inclSM = { deps := [`Spin10Model.inclPatiSalam, `PatiSalam.inclSM], tag := "6V2YO" }

def Spin10Model.inclGeorgiGlashow : InformalDefinition

The inclusion of the Georgi-Glashow gauge group into Spin(10), i.e., the Lie group homomorphism from SU(n) → Spin(2n) discussed on page 46 of https://math.ucr.edu/home/baez/guts.pdf for n = 5.

Equations

• Spin10Model.inclGeorgiGlashow = { deps := [`Spin10Model.GaugeGroupI, `GeorgiGlashow.GaugeGroupI], tag := "6V2YU" }

def Spin10Model.inclSMThruGeorgiGlashow : InformalDefinition

The inclusion of the Standard Model gauge group into Spin(10), i.e., the composition of inclGeorgiGlashow and GeorgiGlashow.inclSM.

Equations

• Spin10Model.inclSMThruGeorgiGlashow = { deps := [`Spin10Model.inclGeorgiGlashow, `GeorgiGlashow.inclSM], tag := "6V2YZ" }

def Spin10Model.inclSM_eq_inclSMThruGeorgiGlashow : InformalLemma

The inclusion inclSM is equal to the inclusion inclSMThruGeorgiGlashow.

Equations

• Spin10Model.inclSM_eq_inclSMThruGeorgiGlashow = { deps := [`Spin10Model.inclSM, `Spin10Model.inclSMThruGeorgiGlashow], tag := "6V2Y6" }