Representations appearing in the Standard Model

This file defines the basic representations which appear in the Standard Model.

@[simp]

theorem StandardModel.repU1Map_coe (g : ↥(unitary ℂ)) : ↑(StandardModel.repU1Map g) = g ^ 3 • 1

noncomputable def StandardModel.repU1Map (g : ↥(unitary ℂ)) : ↥(Matrix.unitaryGroup (Fin 2) ℂ)

The 2d representation of U(1) with charge 3 as a map from U(1) to unitaryGroup (Fin 2) ℂ.

Equations

• StandardModel.repU1Map g = ⟨g ^ 3 • 1, ⋯⟩

@[simp]

theorem StandardModel.repU1_apply_coe (g : ↥(unitary ℂ)) : ↑(StandardModel.repU1 g) = g ^ 3 • 1

noncomputable def StandardModel.repU1 : ↥(unitary ℂ) →* ↥(Matrix.unitaryGroup (Fin 2) ℂ)

The 2d representation of U(1) with charge 3 as a homomorphism from U(1) to unitaryGroup (Fin 2) ℂ.

Equations

• StandardModel.repU1 = { toFun := fun (g : ↥(unitary ℂ)) => StandardModel.repU1Map g, map_one' := StandardModel.repU1.proof_1, map_mul' := StandardModel.repU1.proof_2 }

@[simp]

theorem StandardModel.fundamentalSU2_apply_coe (g : ↥(Matrix.specialUnitaryGroup (Fin 2) ℂ)) : ↑(StandardModel.fundamentalSU2 g) = ↑g

def StandardModel.fundamentalSU2 : ↥(Matrix.specialUnitaryGroup (Fin 2) ℂ) →* ↥(Matrix.unitaryGroup (Fin 2) ℂ)

The fundamental representation of SU(2) as a homomorphism to unitaryGroup (Fin 2) ℂ.

Equations

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

theorem StandardModel.repU1_fundamentalSU2_commute (u1 : ↥(unitary ℂ)) (g : ↥(Matrix.specialUnitaryGroup (Fin 2) ℂ)) : StandardModel.repU1 u1 * StandardModel.fundamentalSU2 g = StandardModel.fundamentalSU2 g * StandardModel.repU1 u1