feat: Add reps to real modules

HepLean/SpaceTime/LorentzVector/Basic.lean

@@ -59,9 +59,9 @@ def time : ℝ := v (Sum.inl 0)
 
 -/
 
-/-- The standard basis of `LorentzVector` indexed by `Fin 1 ⊕ Fin (d)`. -/
+/-- The standard basis of `LorentzVector` indexed by `Fin 1 ⊕ Fin d`. -/
 @[simps!]
-noncomputable def stdBasis : Basis (Fin 1 ⊕ Fin (d)) ℝ (LorentzVector d) := Pi.basisFun ℝ _
+noncomputable def stdBasis : Basis (Fin 1 ⊕ Fin d) ℝ (LorentzVector d) := Pi.basisFun ℝ _
 
 /-- Notation for `stdBasis`. -/
 scoped[LorentzVector] notation "e" => stdBasis

HepLean/SpaceTime/LorentzVector/Complex/Basic.lean

@@ -37,8 +37,8 @@ def complexContr : Rep ℂ SL(2, ℂ) := Rep.of ContrℂModule.SL2CRep
 def complexCo : Rep ℂ SL(2, ℂ) := Rep.of CoℂModule.SL2CRep
 
 /-- The standard basis of complex contravariant Lorentz vectors. -/
-def complexContrBasis : Basis (Fin 1 ⊕ Fin 3) ℂ complexContr := Basis.ofEquivFun
-  (Equiv.linearEquiv ℂ ContrℂModule.toFin13ℂFun)
+def complexContrBasis : Basis (Fin 1 ⊕ Fin 3) ℂ complexContr :=
+  Basis.ofEquivFun ContrℂModule.toFin13ℂEquiv
 
 @[simp]
 lemma complexContrBasis_toFin13ℂ (i :Fin 1 ⊕ Fin 3) :
@@ -65,8 +65,8 @@ def complexContrBasisFin4 : Basis (Fin 4) ℂ complexContr :=
   Basis.reindex complexContrBasis finSumFinEquiv
 
 /-- The standard basis of complex covariant Lorentz vectors. -/
-def complexCoBasis : Basis (Fin 1 ⊕ Fin 3) ℂ complexCo := Basis.ofEquivFun
-  (Equiv.linearEquiv ℂ CoℂModule.toFin13ℂFun)
+def complexCoBasis : Basis (Fin 1 ⊕ Fin 3) ℂ complexCo :=
+  Basis.ofEquivFun CoℂModule.toFin13ℂEquiv
 
 @[simp]
 lemma complexCoBasis_toFin13ℂ (i :Fin 1 ⊕ Fin 3) : (complexCoBasis i).toFin13ℂ = Pi.single i 1 := by

HepLean/SpaceTime/LorentzVector/Complex/Modules.lean

@@ -65,13 +65,8 @@ lemma val_smul (r : ℂ) (ψ : ContrℂModule) : (r • ψ).val = r • ψ.val :
 
 /-- The linear equivalence between `ContrℂModule` and `(Fin 1 ⊕ Fin 3 → ℂ)`. -/
 @[simps!]
-def toFin13ℂEquiv : ContrℂModule ≃ₗ[ℂ] (Fin 1 ⊕ Fin 3 → ℂ) where
-  toFun := toFin13ℂFun
-  map_add' := fun _ _ => rfl
-  map_smul' := fun _ _ => rfl
-  invFun := toFin13ℂFun.symm
-  left_inv := fun _ => rfl
-  right_inv := fun _ => rfl
+def toFin13ℂEquiv : ContrℂModule ≃ₗ[ℂ] (Fin 1 ⊕ Fin 3 → ℂ) :=
+  Equiv.linearEquiv ℂ toFin13ℂFun
 
 /-- The underlying element of `Fin 1 ⊕ Fin 3 → ℂ` of a element in `ContrℂModule` defined
   through the linear equivalence `toFin13ℂEquiv`. -/
@@ -129,13 +124,8 @@ instance : Module ℂ CoℂModule := Equiv.module ℂ toFin13ℂFun
 
 /-- The linear equivalence between `CoℂModule` and `(Fin 1 ⊕ Fin 3 → ℂ)`. -/
 @[simps!]
-def toFin13ℂEquiv : CoℂModule ≃ₗ[ℂ] (Fin 1 ⊕ Fin 3 → ℂ) where
-  toFun := toFin13ℂFun
-  map_add' := fun _ _ => rfl
-  map_smul' := fun _ _ => rfl
-  invFun := toFin13ℂFun.symm
-  left_inv := fun _ => rfl
-  right_inv := fun _ => rfl
+def toFin13ℂEquiv : CoℂModule ≃ₗ[ℂ] (Fin 1 ⊕ Fin 3 → ℂ) :=
+  Equiv.linearEquiv ℂ toFin13ℂFun
 
 /-- The underlying element of `Fin 1 ⊕ Fin 3 → ℂ` of a element in `CoℂModule` defined
   through the linear equivalence `toFin13ℂEquiv`. -/

HepLean/SpaceTime/LorentzVector/Real/Modules.lean

@@ -68,18 +68,24 @@ lemma val_smul (r : ℝ) (ψ : ContrℝModule d) : (r • ψ).val = r • ψ.val
 
 /-- The linear equivalence between `ContrℝModule` and `(Fin 1 ⊕ Fin d → ℝ)`. -/
 @[simps!]
-def toFin1dℝEquiv : ContrℝModule d ≃ₗ[ℝ] (Fin 1 ⊕ Fin d → ℝ) where
-  toFun := toFin1dℝFun
-  map_add' := fun _ _ => rfl
-  map_smul' := fun _ _ => rfl
-  invFun := toFin1dℝFun.symm
-  left_inv := fun _ => rfl
-  right_inv := fun _ => rfl
+def toFin1dℝEquiv : ContrℝModule d ≃ₗ[ℝ] (Fin 1 ⊕ Fin d → ℝ) :=
+  Equiv.linearEquiv ℝ toFin1dℝFun
 
 /-- The underlying element of `Fin 1 ⊕ Fin d → ℝ` of a element in `ContrℝModule` defined
   through the linear equivalence `toFin1dℝEquiv`. -/
 abbrev toFin1dℝ (ψ : ContrℝModule d) := toFin1dℝEquiv ψ
 
+/-- The standard basis of `ContrℝModule` indexed by `Fin 1 ⊕ Fin d`. -/
+@[simps!]
+def stdBasis : Basis (Fin 1 ⊕ Fin d) ℝ (ContrℝModule d) := Basis.ofEquivFun toFin1dℝEquiv
+
+/-- The representation of the Lorentz group acting on `ContrℝModule d`. -/
+def rep : Representation ℝ (LorentzGroup d) (ContrℝModule d) where
+  toFun g := Matrix.toLinAlgEquiv stdBasis g
+  map_one' := (MulEquivClass.map_eq_one_iff (Matrix.toLinAlgEquiv stdBasis)).mpr rfl
+  map_mul' x y := by
+    simp only [lorentzGroupIsGroup_mul_coe, _root_.map_mul]
+
 end ContrℝModule
 
 /-- The module for covariant (up-index) complex Lorentz vectors. -/
@@ -112,18 +118,26 @@ instance : Module ℝ (CoℝModule d) := Equiv.module ℝ toFin1dℝFun
 
 /-- The linear equivalence between `CoℝModule` and `(Fin 1 ⊕ Fin d → ℝ)`. -/
 @[simps!]
-def toFin1dℝEquiv : CoℝModule d ≃ₗ[ℝ] (Fin 1 ⊕ Fin d → ℝ) where
-  toFun := toFin1dℝFun
-  map_add' := fun _ _ => rfl
-  map_smul' := fun _ _ => rfl
-  invFun := toFin1dℝFun.symm
-  left_inv := fun _ => rfl
-  right_inv := fun _ => rfl
+def toFin1dℝEquiv : CoℝModule d ≃ₗ[ℝ] (Fin 1 ⊕ Fin d → ℝ) :=
+  Equiv.linearEquiv ℝ toFin1dℝFun
 
 /-- The underlying element of `Fin 1 ⊕ Fin d → ℝ` of a element in `CoℝModule` defined
   through the linear equivalence `toFin1dℝEquiv`. -/
 abbrev toFin1dℝ (ψ : CoℝModule d) := toFin1dℝEquiv ψ
 
+/-- The standard basis of `CoℝModule` indexed by `Fin 1 ⊕ Fin d`. -/
+@[simps!]
+def stdBasis : Basis (Fin 1 ⊕ Fin d) ℝ (CoℝModule d) := Basis.ofEquivFun toFin1dℝEquiv
+
+/-- The representation of the Lorentz group acting on `CoℝModule d`. -/
+def rep : Representation ℝ (LorentzGroup d) (CoℝModule d) where
+  toFun g := Matrix.toLinAlgEquiv stdBasis (LorentzGroup.transpose g⁻¹)
+  map_one' := by
+    simp only [inv_one, LorentzGroup.transpose_one, lorentzGroupIsGroup_one_coe, _root_.map_one]
+  map_mul' x y := by
+    simp only [_root_.mul_inv_rev, lorentzGroupIsGroup_inv, LorentzGroup.transpose_mul,
+      lorentzGroupIsGroup_mul_coe, _root_.map_mul]
+
 end CoℝModule
 
 end