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.GaugeGroupI.toSU3 : GaugeGroupI →* ↥(Matrix.specialUnitaryGroup (Fin 3) ℂ)

The underlying element of SU(3) of an element in GaugeGroupI.

Equations

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

def StandardModel.GaugeGroupI.toSU2 : GaugeGroupI →* ↥(Matrix.specialUnitaryGroup (Fin 2) ℂ)

The underlying element of SU(2) of an element in GaugeGroupI.

Equations

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

def StandardModel.GaugeGroupI.toU1 : GaugeGroupI →* ↥(unitary ℂ)

The underlying element of U(1) of an element in GaugeGroupI.

Equations

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

theorem StandardModel.GaugeGroupI.ext {g g' : GaugeGroupI} (hSU3 : toSU3 g = toSU3 g') (hSU2 : toSU2 g = toSU2 g') (hU1 : toU1 g = toU1 g') : g = g'

theorem StandardModel.GaugeGroupI.ext_iff {g g' : GaugeGroupI} : g = g' ↔ toSU3 g = toSU3 g' ∧ toSU2 g = toSU2 g' ∧ toU1 g = toU1 g'

instance StandardModel.GaugeGroupI.instStar : Star GaugeGroupI

Equations

• StandardModel.GaugeGroupI.instStar = { star := fun (g : StandardModel.GaugeGroupI) => (star g.1, star g.2.1, star g.2.2) }

theorem StandardModel.GaugeGroupI.star_eq (g : GaugeGroupI) : star g = (star g.1, star g.2.1, star g.2.2)

@[simp]

theorem StandardModel.GaugeGroupI.star_toSU3 (g : GaugeGroupI) : toSU3 (star g) = star (toSU3 g)

@[simp]

theorem StandardModel.GaugeGroupI.star_toSU2 (g : GaugeGroupI) : toSU2 (star g) = star (toSU2 g)

@[simp]

theorem StandardModel.GaugeGroupI.star_toU1 (g : GaugeGroupI) : toU1 (star g) = star (toU1 g)

instance StandardModel.GaugeGroupI.instInvolutiveStar : InvolutiveStar GaugeGroupI

Equations

• StandardModel.GaugeGroupI.instInvolutiveStar = { toStar := StandardModel.GaugeGroupI.instStar, star_involutive := ⋯ }

def StandardModel.GaugeGroupI.ofU1Subgroup (u1 : ↥(unitary ℂ)) : GaugeGroupI

The inclusion of a U(1) subgroup.

Equations

• StandardModel.GaugeGroupI.ofU1Subgroup u1 = (1, ⟨!![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)], ⋯⟩, u1)

@[simp]

theorem StandardModel.GaugeGroupI.ofU1Subgroup_toSU3 (u1 : ↥(unitary ℂ)) : toSU3 (ofU1Subgroup u1) = 1

@[simp]

theorem StandardModel.GaugeGroupI.ofU1Subgroup_toSU2 (u1 : ↥(unitary ℂ)) : toSU2 (ofU1Subgroup u1) = ⟨!![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)], ⋯⟩

@[simp]

theorem StandardModel.GaugeGroupI.ofU1Subgroup_toU1 (u1 : ↥(unitary ℂ)) : toU1 (ofU1Subgroup u1) = u1

def StandardModel.gaugeGroupℤ₆SubGroup [inst : Group GaugeGroupI] : Subgroup GaugeGroupI

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 = sorry

def StandardModel.GaugeGroupℤ₆ : Type

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ℤ₆ = sorry

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