HepLean Documentation

HepLean.StandardModel.Representations

Representations appearing in the Standard Model #

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

noncomputable def StandardModel.repU1Map (g : (unitary )) :

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

Equations
Instances For
    @[simp]
    noncomputable def StandardModel.repU1 :

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

    Equations
    Instances For
      @[simp]
      theorem StandardModel.repU1_apply_coe (g : (unitary )) :
      (StandardModel.repU1 g) = g ^ 3 1

      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.
      Instances For
        @[simp]
        theorem StandardModel.fundamentalSU2_apply_coe (g : (Matrix.specialUnitaryGroup (Fin 2) )) :
        (StandardModel.fundamentalSU2 g) = g
        theorem StandardModel.repU1_fundamentalSU2_commute (u1 : (unitary )) (g : (Matrix.specialUnitaryGroup (Fin 2) )) :
        StandardModel.repU1 u1 * StandardModel.fundamentalSU2 g = StandardModel.fundamentalSU2 g * StandardModel.repU1 u1