The Standard Model

This file defines the basic properties of the standard model in particle physics.

@[reducible, inline]

abbrev StandardModel.GaugeGroupI : Type

The global gauge group of the Standard Model with no discrete quotients. The I in the Name is an indication of the statement that this has no discrete quotients.

Equations

• StandardModel.GaugeGroupI = (↥(Matrix.specialUnitaryGroup (Fin 3) ℂ) × ↥(Matrix.specialUnitaryGroup (Fin 2) ℂ) × ↥(unitary ℂ))

def StandardModel.gaugeGroupℤ₂SubGroup : InformalDefinition

The ℤ₂subgroup of the un-quotiented gauge group which acts trivially on all particles in the standard model, i.e., the ℤ₂-subgroup of GaugeGroupI derived from the ℤ₂ subgroup of gaugeGroupℤ₆SubGroup.

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

Equations

• StandardModel.gaugeGroupℤ₂SubGroup = { deps := [`StandardModel.GaugeGroupI], tag := "6V2GH" }

def StandardModel.GaugeGroupℤ₂ : InformalDefinition

The gauge group of the Standard Model with a ℤ₂ quotient, i.e., the quotient of GaugeGroupI by the ℤ₂-subgroup gaugeGroupℤ₂SubGroup.

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

Equations

• StandardModel.GaugeGroupℤ₂ = { deps := [`StandardModel.GaugeGroupI, `StandardModel.gaugeGroupℤ₂SubGroup], tag := "6V2GO" }

def StandardModel.gaugeGroupℤ₃SubGroup : InformalDefinition

The ℤ₃-subgroup of the un-quotiented gauge group which acts trivially on all particles in the standard model, i.e., the ℤ₃-subgroup of GaugeGroupI derived from the ℤ₃ subgroup of gaugeGroupℤ₆SubGroup.

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

Equations

• StandardModel.gaugeGroupℤ₃SubGroup = { deps := [`StandardModel.GaugeGroupI], tag := "6V2GV" }

def StandardModel.GaugeGroupℤ₃ : InformalDefinition

The gauge group of the Standard Model with a ℤ₃-quotient, i.e., the quotient of GaugeGroupI by the ℤ₃-subgroup gaugeGroupℤ₃SubGroup.

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

Equations

• StandardModel.GaugeGroupℤ₃ = { deps := [`StandardModel.GaugeGroupI, `StandardModel.gaugeGroupℤ₃SubGroup], tag := "6V2G3" }

inductive StandardModel.GaugeGroupQuot : Type

Specifies the allowed quotients of SU(3) x SU(2) x U(1) which give a valid gauge group of the Standard Model.

• ℤ₆ : GaugeGroupQuot

  The element of GaugeGroupQuot corresponding to the quotient of the full SM gauge group by the sub-group ℤ₆.

• ℤ₂ : GaugeGroupQuot

  The element of GaugeGroupQuot corresponding to the quotient of the full SM gauge group by the sub-group ℤ₂.

• ℤ₃ : GaugeGroupQuot

  The element of GaugeGroupQuot corresponding to the quotient of the full SM gauge group by the sub-group ℤ₃.

• I : GaugeGroupQuot

  The element of GaugeGroupQuot corresponding to the full SM gauge group.

def StandardModel.GaugeGroup : InformalDefinition

The (global) gauge group of the Standard Model given a choice of quotient, i.e., the map from GaugeGroupQuot to Type which gives the gauge group of the Standard Model for a given choice of quotient.

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

Equations

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

Smoothness structure on the gauge group.

def StandardModel.gaugeGroupI_lie : InformalLemma

The gauge group GaugeGroupI is a Lie group.

Equations

• StandardModel.gaugeGroupI_lie = { deps := [`StandardModel.GaugeGroupI], tag := "6V2HL" }

def StandardModel.gaugeGroup_lie : InformalLemma

For every q in GaugeGroupQuot the group GaugeGroup q is a Lie group.

Equations

• StandardModel.gaugeGroup_lie = { deps := [`StandardModel.GaugeGroup], tag := "6V2HR" }

def StandardModel.gaugeBundleI : InformalDefinition

The trivial principal bundle over SpaceTime with structure group GaugeGroupI.

Equations

• StandardModel.gaugeBundleI = { deps := [`StandardModel.GaugeGroupI, `SpaceTime], tag := "6V2HX" }

def StandardModel.gaugeTransformI : InformalDefinition

A global section of gaugeBundleI.

Equations

• StandardModel.gaugeTransformI = { deps := [`StandardModel.gaugeBundleI], tag := "6V2H5" }