diff --git a/Physlib/Particles/StandardModel/Representations.lean b/Physlib/Particles/StandardModel/Representations.lean index d58482f5b..90b7fd5d5 100644 --- a/Physlib/Particles/StandardModel/Representations.lean +++ b/Physlib/Particles/StandardModel/Representations.lean @@ -7,6 +7,7 @@ module public import Mathlib.Analysis.Complex.Basic public import Mathlib.LinearAlgebra.UnitaryGroup +public import Physlib.Meta.TODO.Basic /-! # Representations appearing in the Standard Model @@ -55,4 +56,10 @@ lemma repU1_fundamentalSU2_commute (u1 : unitary ℂ) (g : specialUnitaryGroup ( apply Subtype.ext simp +TODO "Define a structure capturing the fermionic content of the Standard Model, with all fermions + expressed as left-handed Weyl fermions (`Fermion.LeftHandedWeyl`) and including all three + families. The structure should carry a `Module ℂ` instance together with a representation of the + Lorentz group and a representation of the global gauge group `GaugeGroupI` (built from `repU1` + and `fundamentalSU2`)." + end StandardModel