Merge pull request #16 from HEPLean/SM/Higgs-field

Higgs Field

HepLean.lean

@@ -54,3 +54,5 @@ import HepLean.FlavorPhysics.CKMMatrix.Relations
 import HepLean.FlavorPhysics.CKMMatrix.Rows
 import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.Basic
 import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters
+import HepLean.StandardModel.Basic
+import HepLean.StandardModel.HiggsField

HepLean/StandardModel/Basic.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import Mathlib.Data.Complex.Exponential
+import Mathlib.Geometry.Manifold.VectorBundle.Basic
+import Mathlib.Geometry.Manifold.VectorBundle.SmoothSection
+import Mathlib.Geometry.Manifold.Instances.Real
+import Mathlib.RepresentationTheory.Basic
+/-!
+# The Standard Model
+
+This file defines the basic properties of the standard model in particle physics.
+
+-/
+universe v u
+namespace StandardModel
+
+open Manifold
+open Matrix
+open Complex
+open ComplexConjugate
+
+/-- The space-time (TODO: Change to Minkowski.) -/
+abbrev spaceTime := EuclideanSpace ℝ (Fin 4)
+
+/-- The global gauge group of the standard model. -/
+abbrev guageGroup : Type := specialUnitaryGroup (Fin 3) ℂ ×
+  specialUnitaryGroup (Fin 2) ℂ × unitary ℂ
+
+end StandardModel