feat: Add representations for real Lorentz vecs

HepLean.lean

@@ -90,6 +90,7 @@ import HepLean.SpaceTime.LorentzVector.Complex.Unit
 import HepLean.SpaceTime.LorentzVector.Covariant
 import HepLean.SpaceTime.LorentzVector.LorentzAction
 import HepLean.SpaceTime.LorentzVector.NormOne
+import HepLean.SpaceTime.LorentzVector.Real.Basic
 import HepLean.SpaceTime.LorentzVector.Real.Modules
 import HepLean.SpaceTime.MinkowskiMetric
 import HepLean.SpaceTime.PauliMatrices.AsTensor

HepLean/SpaceTime/LorentzVector/Real/Basic.lean

@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import Mathlib.Data.Complex.Exponential
+import Mathlib.Analysis.InnerProductSpace.PiL2
+import HepLean.SpaceTime.SL2C.Basic
+import HepLean.SpaceTime.LorentzVector.Complex.Modules
+import HepLean.Meta.Informal
+import Mathlib.RepresentationTheory.Rep
+import HepLean.SpaceTime.LorentzVector.Real.Modules
+/-!
+
+# Real Lorentz vectors
+
+We define real Lorentz vectors in as representations of the Lorentz group.
+
+-/
+
+noncomputable section
+
+open Matrix
+open MatrixGroups
+open Complex
+open TensorProduct
+open SpaceTime
+
+namespace Lorentz
+
+/-- The representation of `LorentzGroup d` on real vectors corresponding to contravariant
+  Lorentz vectors. In index notation these have an up index `ψⁱ`. -/
+def Contr (d : ℕ) : Rep ℝ (LorentzGroup d) := Rep.of ContrℝModule.rep
+
+/-- The representation of `LorentzGroup d` on real vectors corresponding to covariant
+  Lorentz vectors. In index notation these have an up index `ψⁱ`. -/
+def Co (d : ℕ) : Rep ℝ (LorentzGroup d) := Rep.of CoℝModule.rep
+
+end Lorentz
+end

HepLean/SpaceTime/LorentzVector/Real/Modules.lean

@@ -35,7 +35,7 @@ namespace ContrℝModule
 variable {d : ℕ}
 
 /-- The equivalence between `ContrℝModule` and `Fin 1 ⊕ Fin d → ℂ`. -/
-def toFin1dℝFun : ContrℝModule d  ≃ (Fin 1 ⊕ Fin d → ℝ) where
+def toFin1dℝFun : ContrℝModule d ≃ (Fin 1 ⊕ Fin d → ℝ) where
   toFun v := v.val
   invFun f := ⟨f⟩
   left_inv _ := rfl