feat: add properties of spacetime

HepLean/StandardModel/Basic.lean

@@ -10,6 +10,7 @@ import Mathlib.Geometry.Manifold.Instances.Real
 import Mathlib.RepresentationTheory.Basic
 import Mathlib.LinearAlgebra.Matrix.ToLin
 import Mathlib.Analysis.InnerProductSpace.Adjoint
+import Mathlib.LinearAlgebra.CliffordAlgebra.Basic
 /-!
 # The Standard Model
 
@@ -29,8 +30,86 @@ open Matrix
 open Complex
 open ComplexConjugate
 
-/-- The space-time (TODO: Change to Minkowski.) -/
+noncomputable section spaceTime
-abbrev spaceTime := EuclideanSpace ℝ (Fin 4)
+
+/-- The space-time -/
+def spaceTime : Type := Fin 4 → ℝ
+
+/-- Give spacetime the structure of an additive commutative monoid. -/
+instance : AddCommMonoid spaceTime := Pi.addCommMonoid
+
+/-- Give spacetime the structure of a module over the reals. -/
+instance : Module ℝ spaceTime := Pi.module _ _ _
+
+instance euclideanNormedAddCommGroup : NormedAddCommGroup spaceTime := Pi.normedAddCommGroup
+
+instance euclideanNormedSpace : NormedSpace ℝ spaceTime := Pi.normedSpace
+
+
+namespace spaceTime
+
+def asSmoothManifold : ModelWithCorners ℝ spaceTime spaceTime := 𝓘(ℝ, spaceTime)
+
+@[simp]
+def η : Matrix (Fin 4) (Fin 4) ℝ :=
+  ![![1, 0, 0, 0], ![0, -1, 0, 0], ![0, 0, -1, 0], ![0, 0, 0, -1]]
+
+lemma η_symmetric (μ ν : Fin 4) : η μ ν = η ν μ := by
+  fin_cases μ <;>
+    fin_cases ν <;>
+    simp only [η, Fin.zero_eta, Matrix.cons_val', Matrix.cons_val_fin_one, Matrix.cons_val_one,
+      Matrix.cons_val_succ', Matrix.cons_val_zero, Matrix.empty_val', Matrix.head_cons,
+      Matrix.head_fin_const, Matrix.head_cons, Matrix.vecCons_const, Fin.mk_one, Fin.mk_one]
+
+@[simps!]
+def linearMapForSpaceTime (x : spaceTime) : spaceTime →ₗ[ℝ] ℝ where
+  toFun y := x ⬝ᵥ (η *ᵥ y)
+  map_add' y z := by
+    simp only
+    rw [mulVec_add, dotProduct_add]
+  map_smul' c y := by
+    simp only
+    rw [mulVec_smul, dotProduct_smul]
+    rfl
+
+def ηLin : LinearMap.BilinForm ℝ spaceTime where
+  toFun x := linearMapForSpaceTime x
+  map_add' x y := by
+    apply LinearMap.ext
+    intro z
+    simp only [linearMapForSpaceTime_apply, LinearMap.add_apply]
+    rw [add_dotProduct]
+  map_smul' c x := by
+    apply LinearMap.ext
+    intro z
+    simp only [linearMapForSpaceTime_apply, RingHom.id_apply, LinearMap.smul_apply, smul_eq_mul]
+    rw [smul_dotProduct]
+    rfl
+
+def quadraticForm : QuadraticForm ℝ spaceTime := ηLin.toQuadraticForm
+
+def lorentzGroup : Subgroup (GeneralLinearGroup (Fin 4) ℝ) where
+  carrier := {Λ | ∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y}
+  mul_mem' {a b} := by
+    intros ha hb x y
+    simp
+    rw [← mulVec_mulVec, ← mulVec_mulVec, ha, hb]
+  one_mem' := by
+    intros x y
+    simp
+  inv_mem' {a} := by
+    intros ha x y
+    simp only [coe_units_inv, ← ha ((a.1⁻¹) *ᵥ x) ((a.1⁻¹) *ᵥ y), mulVec_mulVec]
+    have hx : (a.1 * (a.1)⁻¹) = 1 := by
+      simp only [@Units.mul_eq_one_iff_inv_eq, coe_units_inv]
+    simp [hx]
+
+
+abbrev cliffordAlgebra := CliffordAlgebra quadraticForm
+
+end spaceTime
+
+end spaceTime
 
 /-- The global gauge group of the standard model. TODO: Generalize to quotient. -/
 abbrev gaugeGroup : Type :=

HepLean/StandardModel/CliffordAlgebra.lean

@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.StandardModel.Basic
+/-!
+# The Clifford Algebra
+
+This file defines the Gamma matrices.
+
+## TODO
+
+- Prove that the algebra generated by the gamma matrices is ismorphic to the
+  Clifford algebra assocaited with spacetime.
+-
+-/
+
+namespace StandardModel
+open Complex
+
+noncomputable section diracRepresentation
+
+def γ0 : Matrix (Fin 4) (Fin 4) ℂ :=
+  ![![1, 0, 0, 0], ![0, 1, 0, 0], ![0, 0, -1, 0], ![0, 0, 0, -1]]
+
+def γ1 : Matrix (Fin 4) (Fin 4) ℂ :=
+  ![![0, 0, 0, 1], ![0, 0, 1, 0], ![0, -1, 0, 0], ![-1, 0, 0, 0]]
+
+def γ2 : Matrix (Fin 4) (Fin 4) ℂ :=
+  ![![0, 0, 0, - I], ![0, 0, I, 0], ![0, I, 0, 0], ![-I, 0, 0, 0]]
+
+def γ3 : Matrix (Fin 4) (Fin 4) ℂ :=
+  ![![0, 0, 1, 0], ![0, 0, 0, -1], ![-1, 0, 0, 0], ![0, 1, 0, 0]]
+
+def γ5 : Matrix (Fin 4) (Fin 4) ℂ := I • (γ0 * γ1 * γ2 * γ3)
+
+@[simp]
+def γ : Fin 4 → Matrix (Fin 4) (Fin 4) ℂ := ![γ0, γ1, γ2, γ3]
+
+
+namespace γ
+
+variable (μ : Fin 4)
+
+
+
+
+/-- The trace of the gamma matrices is zero. -/
+lemma trace_eq_zero (μ : Fin 4) : Matrix.trace (γ μ) = 0 := by
+  fin_cases μ
+    <;> simp [γ, γ0, γ1, γ2, γ3]
+    <;> rw [Matrix.trace, Fin.sum_univ_four]
+    <;> simp
+  any_goals rfl
+  change 0 + 0 = 0
+  simp [add_zero]
+
+
+
+@[simp]
+def γSet : Set (Matrix (Fin 4) (Fin 4) ℂ) := {γ i | i : Fin 4}
+
+lemma γ_in_γSet (μ : Fin 4) : γ μ ∈ γSet := by
+  simp [γSet]
+
+def diracAlgebra : Subalgebra ℝ (Matrix (Fin 4) (Fin 4) ℂ) :=
+  Algebra.adjoin ℝ γSet
+
+lemma γSet_subset_diracAlgebra : γSet ⊆ diracAlgebra :=
+  Algebra.subset_adjoin
+
+lemma γ_in_diracAlgebra (μ : Fin 4) : γ μ ∈ diracAlgebra :=
+  γSet_subset_diracAlgebra (γ_in_γSet μ)
+
+end γ
+
+end diracRepresentation
+end StandardModel