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 with elements (α^2 * I₃, α^(-3) * I₂, α), where α is a sixth complex root of unity.

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

Equations

• StandardModel.gaugeGroupℤ₆SubGroup = { deps := [`StandardModel.GaugeGroupI] }

def StandardModel.GaugeGroupℤ₆ : InformalDefinition

The smallest possible gauge group of the Standard Model, 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] }

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, `StandardModel.gaugeGroupℤ₆SubGroup] }

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] }

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, `StandardModel.gaugeGroupℤ₆SubGroup] }

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] }

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] }

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] }

def StandardModel.gaugeBundleI : InformalDefinition

The trivial principal bundle over SpaceTime with structure group GaugeGroupI.

Equations

• StandardModel.gaugeBundleI = { deps := [`StandardModel.GaugeGroupI, `SpaceTime] }

def StandardModel.gaugeTransformI : InformalDefinition

A global section of gaugeBundleI.

Equations

• StandardModel.gaugeTransformI = { deps := [`StandardModel.gaugeBundleI] }