feat: Metric, unit, contract of complex Lorentz vec

HepLean/SpaceTime/LorentzGroup/Basic.lean

@@ -5,6 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.MinkowskiMetric
 import HepLean.SpaceTime.LorentzVector.NormOne
+import LLMLean
 /-!
 # The Lorentz Group
 
@@ -286,5 +287,62 @@ lemma timeComp_mul (Λ Λ' : LorentzGroup d) : timeComp (Λ * Λ') =
   erw [Pi.basisFun_apply, Matrix.mulVec_single_one]
   simp
 
+/-!
+
+## To Complex matrices
+
+-/
+
+/-- The monoid homomorphisms taking the lorentz group to complex matrices. -/
+def toComplex : LorentzGroup d →* Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℂ where
+  toFun Λ := Λ.1.map ofReal
+  map_one' := by
+    ext i j
+    simp
+    simp only [Matrix.one_apply, ofReal_one, ofReal_zero]
+    split_ifs
+    · rfl
+    · rfl
+  map_mul' Λ Λ' := by
+    ext i j
+    simp
+    simp only [← Matrix.map_mul, RingHom.map_matrix_mul]
+    rfl
+
+instance (M : LorentzGroup d ) : Invertible (toComplex M) where
+  invOf := toComplex M⁻¹
+  invOf_mul_self := by
+    rw [← toComplex.map_mul, Group.inv_mul_cancel]
+    simp
+  mul_invOf_self := by
+    rw [← toComplex.map_mul]
+    rw [@mul_inv_cancel]
+    simp
+
+lemma toComplex_inv (Λ : LorentzGroup d) : (toComplex Λ)⁻¹ = toComplex Λ⁻¹  := by
+  refine inv_eq_right_inv ?h
+  rw [← toComplex.map_mul, mul_inv_cancel]
+  simp
+
+@[simp]
+lemma toComplex_mul_minkowskiMatrix_mul_transpose (Λ : LorentzGroup d) :
+    toComplex Λ * minkowskiMatrix.map ofReal * (toComplex Λ)ᵀ = minkowskiMatrix.map ofReal := by
+  simp [toComplex]
+  have h1 : ((Λ.1).map ⇑ofReal)ᵀ = (Λ.1ᵀ).map ofReal := rfl
+  rw [h1]
+  trans (Λ.1 * minkowskiMatrix * Λ.1ᵀ).map ofReal
+  · simp only [Matrix.map_mul]
+  simp only [mul_minkowskiMatrix_mul_transpose]
+
+@[simp]
+lemma toComplex_transpose_mul_minkowskiMatrix_mul_self (Λ : LorentzGroup d) :
+    (toComplex Λ)ᵀ * minkowskiMatrix.map ofReal * toComplex Λ = minkowskiMatrix.map ofReal := by
+  simp [toComplex]
+  have h1 : ((Λ.1).map ⇑ofReal)ᵀ = (Λ.1ᵀ).map ofReal := rfl
+  rw [h1]
+  trans  (Λ.1ᵀ * minkowskiMatrix * Λ.1).map ofReal
+  · simp only [Matrix.map_mul]
+  simp only [transpose_mul_minkowskiMatrix_mul_self]
+
 end
 end LorentzGroup

HepLean/SpaceTime/LorentzVector/Complex.lean

@@ -1,39 +0,0 @@
-/-
-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.Modules
-import HepLean.Meta.Informal
-import Mathlib.RepresentationTheory.Rep
-import HepLean.Tensors.Basic
-/-!
-
-# Complex Lorentz vectors
-
-We define complex Lorentz vectors in 4d space-time as representations of SL(2, C).
-
--/
-
-noncomputable section
-
-open Matrix
-open MatrixGroups
-open Complex
-open TensorProduct
-
-namespace Lorentz
-
-/-- The representation of `SL(2, ℂ)` on complex vectors corresponding to contravariant
-  Lorentz vectors. -/
-def complexContr : Rep ℂ SL(2, ℂ) := Rep.of ContrℂModule.SL2CRep
-
-/-- The representation of `SL(2, ℂ)` on complex vectors corresponding to contravariant
-  Lorentz vectors. -/
-def complexCo : Rep ℂ SL(2, ℂ) := Rep.of CoℂModule.SL2CRep
-
-end Lorentz
-end

HepLean/SpaceTime/LorentzVector/Complex/Basic.lean

@@ -0,0 +1,66 @@
+/-
+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.Modules
+import HepLean.Meta.Informal
+import Mathlib.RepresentationTheory.Rep
+import HepLean.Tensors.Basic
+/-!
+
+# Complex Lorentz vectors
+
+We define complex Lorentz vectors in 4d space-time as representations of SL(2, C).
+
+-/
+
+noncomputable section
+
+open Matrix
+open MatrixGroups
+open Complex
+open TensorProduct
+open SpaceTime
+
+namespace Lorentz
+
+/-- The representation of `SL(2, ℂ)` on complex vectors corresponding to contravariant
+  Lorentz vectors. In index notation these have an up index `ψⁱ`. -/
+def complexContr : Rep ℂ SL(2, ℂ) := Rep.of ContrℂModule.SL2CRep
+
+/-- The representation of `SL(2, ℂ)` on complex vectors corresponding to contravariant
+  Lorentz vectors. In index notation these have a down index `ψⁱ`. -/
+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)
+
+@[simp]
+lemma complexContrBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 1 ⊕ Fin 3) :
+    (LinearMap.toMatrix complexContrBasis complexContrBasis) (complexContr.ρ M) i j =
+    (LorentzGroup.toComplex (SL2C.toLorentzGroup M)) i j := by
+  rw [LinearMap.toMatrix_apply]
+  simp only [complexContrBasis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply, transpose_apply]
+  change (((LorentzGroup.toComplex (SL2C.toLorentzGroup M))) *ᵥ (Pi.single j 1)) i = _
+  simp only [mulVec_single, transpose_apply, mul_one]
+
+/-- The standard basis of complex covariant Lorentz vectors. -/
+def complexCoBasis : Basis (Fin 1 ⊕ Fin 3) ℂ complexCo := Basis.ofEquivFun
+  (Equiv.linearEquiv ℂ CoℂModule.toFin13ℂFun)
+
+@[simp]
+lemma complexCoBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 1 ⊕ Fin 3) :
+    (LinearMap.toMatrix complexCoBasis complexCoBasis) (complexCo.ρ M) i j =
+    (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ i j := by
+  rw [LinearMap.toMatrix_apply]
+  simp only [complexCoBasis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply, transpose_apply]
+  change ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ (Pi.single j 1)) i = _
+  simp only [mulVec_single, transpose_apply, mul_one]
+
+end Lorentz
+end

HepLean/SpaceTime/LorentzVector/Complex/Contraction.lean

@@ -0,0 +1,101 @@
+/-
+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 HepLean.SpaceTime.LorentzVector.Complex.Basic
+/-!
+
+# Contraction of Lorentz vectors
+
+
+-/
+
+noncomputable section
+
+open Matrix
+open MatrixGroups
+open Complex
+open TensorProduct
+open SpaceTime
+open CategoryTheory.MonoidalCategory
+namespace Lorentz
+
+/-- The bi-linear map corresponding to contraction of a contravariant Lorentz vector with a
+  covariant Lorentz vector. -/
+def contrCoContrBi : complexContr →ₗ[ℂ] complexCo →ₗ[ℂ] ℂ where
+  toFun ψ := {
+    toFun := fun φ => ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ,
+    map_add' := by
+      intro φ φ'
+      simp only [map_add]
+      rw [dotProduct_add]
+    map_smul' := by
+      intro r φ
+      simp only [LinearEquiv.map_smul]
+      rw [dotProduct_smul]
+      rfl}
+  map_add' ψ ψ':= by
+    refine LinearMap.ext (fun φ => ?_)
+    simp only [map_add, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply]
+    rw [add_dotProduct]
+  map_smul' r ψ := by
+    refine LinearMap.ext (fun φ => ?_)
+    simp only [LinearEquiv.map_smul, LinearMap.coe_mk, AddHom.coe_mk]
+    rw [smul_dotProduct]
+    rfl
+
+/-- The bi-linear map corresponding to contraction of a covariant Lorentz vector with a
+  contravariant Lorentz vector. -/
+def contrContrCoBi : complexCo →ₗ[ℂ] complexContr →ₗ[ℂ] ℂ where
+  toFun φ := {
+    toFun := fun ψ => φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ,
+    map_add' := by
+      intro ψ ψ'
+      simp only [map_add]
+      rw [dotProduct_add]
+    map_smul' := by
+      intro r ψ
+      simp only [LinearEquiv.map_smul]
+      rw [dotProduct_smul]
+      rfl}
+  map_add' φ φ' := by
+    refine LinearMap.ext (fun ψ => ?_)
+    simp only [map_add, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply]
+    rw [add_dotProduct]
+  map_smul' r φ := by
+    refine LinearMap.ext (fun ψ => ?_)
+    simp only [LinearEquiv.map_smul, LinearMap.coe_mk, AddHom.coe_mk]
+    rw [smul_dotProduct]
+    rfl
+
+/-- The linear map from complexContr ⊗ complexCo to ℂ given by
+    summing over components of contravariant Lorentz vector and
+    covariant Lorentz vector in the
+    standard basis (i.e. the dot product).
+    In terms of index notation this is the contraction is ψⁱ φᵢ. -/
+def contrCoContraction : complexContr ⊗ complexCo ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where
+  hom := TensorProduct.lift contrCoContrBi
+  comm M := TensorProduct.ext' fun ψ φ => by
+    change ((LorentzGroup.toComplex (SL2C.toLorentzGroup M)) *ᵥ ψ.toFin13ℂ) ⬝ᵥ
+      ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ φ.toFin13ℂ) = ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ
+    rw [dotProduct_mulVec, vecMul_transpose, mulVec_mulVec]
+    rw [inv_mul_of_invertible (LorentzGroup.toComplex (SL2C.toLorentzGroup M))]
+    simp
+
+/-- The linear map from complexCo ⊗ complexContr to ℂ given by
+    summing over components of covariant Lorentz vector and
+    contravariant Lorentz vector in the
+    standard basis (i.e. the dot product).
+    In terms of index notation this is the contraction is φᵢ ψⁱ. -/
+def coContrContraction : complexCo ⊗ complexContr ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where
+  hom := TensorProduct.lift contrContrCoBi
+  comm M := TensorProduct.ext' fun φ ψ => by
+    change ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ  *ᵥ φ.toFin13ℂ) ⬝ᵥ
+      ((LorentzGroup.toComplex (SL2C.toLorentzGroup M)) *ᵥ ψ.toFin13ℂ) = φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ
+    rw [dotProduct_mulVec, mulVec_transpose, vecMul_vecMul]
+    rw [inv_mul_of_invertible (LorentzGroup.toComplex (SL2C.toLorentzGroup M))]
+    simp
+
+end Lorentz
+end

HepLean/SpaceTime/LorentzVector/Complex/Metric.lean

@@ -0,0 +1,88 @@
+/-
+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 HepLean.SpaceTime.LorentzVector.Complex.Two
+import HepLean.SpaceTime.MinkowskiMetric
+/-!
+
+# Metric for complex Lorentz vectors
+
+-/
+noncomputable section
+
+open Matrix
+open MatrixGroups
+open Complex
+open TensorProduct
+open SpaceTime
+open CategoryTheory.MonoidalCategory
+namespace Lorentz
+
+/-- The metric `ηᵃᵃ` as an element of `(complexContr ⊗ complexContr).V`. -/
+def contrMetricVal : (complexContr ⊗ complexContr).V :=
+  contrContrToMatrix.symm ((@minkowskiMatrix 3).map ofReal)
+
+/-- The metric `ηᵃᵃ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexContr`,
+  making its invariance under the action of `SL(2,ℂ)`. -/
+def contrMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexContr where
+  hom := {
+    toFun := fun a =>
+      let a' : ℂ := a
+      a' • contrMetricVal,
+    map_add' := fun x y => by
+      simp only [add_smul],
+    map_smul' := fun m x => by
+      simp only [smul_smul]
+      rfl}
+  comm M := by
+    ext x : 2
+    simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+      Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.coe_comp,
+      Function.comp_apply]
+    let x' : ℂ := x
+    change x' • contrMetricVal =
+      (TensorProduct.map (complexContr.ρ M) (complexContr.ρ M)) (x' • contrMetricVal)
+    simp only [Action.instMonoidalCategory_tensorObj_V, _root_.map_smul]
+    apply congrArg
+    simp only [Action.instMonoidalCategory_tensorObj_V, contrMetricVal]
+    erw [contrContrToMatrix_ρ_symm]
+    apply congrArg
+    simp only [LorentzGroup.toComplex_mul_minkowskiMatrix_mul_transpose]
+
+/-- The metric `ηᵢᵢ` as an element of `(complexCo ⊗ complexCo).V`. -/
+def coMetricVal : (complexCo ⊗ complexCo).V :=
+  coCoToMatrix.symm ((@minkowskiMatrix 3).map ofReal)
+
+/-- The metric `ηᵢᵢ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexCo`,
+  making its invariance under the action of `SL(2,ℂ)`. -/
+def coMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexCo where
+  hom := {
+    toFun := fun a =>
+      let a' : ℂ := a
+      a' • coMetricVal,
+    map_add' := fun x y => by
+      simp only [add_smul],
+    map_smul' := fun m x => by
+      simp only [smul_smul]
+      rfl}
+  comm M := by
+    ext x : 2
+    simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+      Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.coe_comp,
+      Function.comp_apply]
+    let x' : ℂ := x
+    change x' • coMetricVal =
+      (TensorProduct.map (complexCo.ρ M) (complexCo.ρ M)) (x' • coMetricVal)
+    simp only [Action.instMonoidalCategory_tensorObj_V, _root_.map_smul]
+    apply congrArg
+    simp only [Action.instMonoidalCategory_tensorObj_V, coMetricVal]
+    erw [coCoToMatrix_ρ_symm]
+    apply congrArg
+    rw [LorentzGroup.toComplex_inv]
+    simp only [lorentzGroupIsGroup_inv, SL2C.toLorentzGroup_apply_coe,
+      LorentzGroup.toComplex_transpose_mul_minkowskiMatrix_mul_self]
+
+end Lorentz
+end

HepLean/SpaceTime/LorentzVector/Complex/Two.lean

@@ -0,0 +1,271 @@
+/-
+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 HepLean.SpaceTime.LorentzVector.Complex.Basic
+import Mathlib.LinearAlgebra.TensorProduct.Matrix
+/-!
+
+# Tensor products of two complex Lorentz vectors
+
+-/
+noncomputable section
+
+open Matrix
+open MatrixGroups
+open Complex
+open TensorProduct
+open SpaceTime
+open CategoryTheory.MonoidalCategory
+namespace Lorentz
+
+/-- Equivalence of `complexContr ⊗ complexContr` to `4 x 4` complex matrices. -/
+def contrContrToMatrix : (complexContr ⊗ complexContr).V ≃ₗ[ℂ]
+    Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ :=
+  (Basis.tensorProduct complexContrBasis complexContrBasis).repr ≪≫ₗ
+  Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)) ≪≫ₗ
+  LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)
+
+/-- Equivalence of `complexCo ⊗ complexCo` to `4 x 4` complex matrices. -/
+def coCoToMatrix : (complexCo ⊗ complexCo).V ≃ₗ[ℂ]
+    Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ :=
+  (Basis.tensorProduct complexCoBasis complexCoBasis).repr ≪≫ₗ
+  Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)) ≪≫ₗ
+  LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)
+
+/-- Equivalence of `complexContr ⊗ complexCo` to `4 x 4` complex matrices. -/
+def contrCoToMatrix : (complexContr ⊗ complexCo).V ≃ₗ[ℂ]
+    Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ :=
+  (Basis.tensorProduct complexContrBasis complexCoBasis).repr ≪≫ₗ
+  Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)) ≪≫ₗ
+  LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)
+
+/-- Equivalence of `complexCo ⊗ complexContr` to `4 x 4` complex matrices. -/
+def coContrToMatrix : (complexCo ⊗ complexContr).V ≃ₗ[ℂ]
+    Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ :=
+  (Basis.tensorProduct complexCoBasis complexContrBasis).repr ≪≫ₗ
+  Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)) ≪≫ₗ
+  LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)
+
+/-!
+
+## Group actions
+
+-/
+
+lemma contrContrToMatrix_ρ (v : (complexContr ⊗ complexContr).V) (M : SL(2,ℂ)) :
+    contrContrToMatrix (TensorProduct.map (complexContr.ρ M) (complexContr.ρ M) v) =
+    (LorentzGroup.toComplex (SL2C.toLorentzGroup M)) * contrContrToMatrix v *
+    (LorentzGroup.toComplex (SL2C.toLorentzGroup M))ᵀ := by
+  nth_rewrite 1 [contrContrToMatrix]
+  simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.trans_apply]
+  trans (LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)) ((LinearMap.toMatrix
+      (complexContrBasis.tensorProduct complexContrBasis)
+      (complexContrBasis.tensorProduct complexContrBasis)
+      (TensorProduct.map (complexContr.ρ M) (complexContr.ρ M)))
+      *ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)))
+      ((complexContrBasis.tensorProduct complexContrBasis).repr v)))
+  · apply congrArg
+    have h1 := (LinearMap.toMatrix_mulVec_repr (complexContrBasis.tensorProduct complexContrBasis)
+      (complexContrBasis.tensorProduct complexContrBasis)
+      (TensorProduct.map (complexContr.ρ M) (complexContr.ρ M)) v)
+    erw [h1]
+    rfl
+  rw [TensorProduct.toMatrix_map]
+  funext i j
+  change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
+        ((LinearMap.toMatrix complexContrBasis complexContrBasis) (complexContr.ρ M))
+        ((LinearMap.toMatrix complexContrBasis complexContrBasis) (complexContr.ρ M)) (i, j) k)
+        * contrContrToMatrix v k.1 k.2) = _
+  erw [Finset.sum_product]
+  simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
+  have h1 : ∑ x, (∑ x1 , LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 *
+      contrContrToMatrix v x1 x) * LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x
+      = ∑ x , ∑ x1 , (LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1
+      * contrContrToMatrix v x1 x) * LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x := by
+    congr
+    funext x
+    rw [Finset.sum_mul]
+  erw [h1]
+  rw [Finset.sum_comm]
+  congr
+  funext x
+  congr
+  funext x1
+  simp only [complexContrBasis_ρ_apply, transpose_apply, Action.instMonoidalCategory_tensorObj_V]
+  ring
+
+lemma coCoToMatrix_ρ (v : (complexCo ⊗ complexCo).V) (M : SL(2,ℂ)) :
+    coCoToMatrix (TensorProduct.map (complexCo.ρ M) (complexCo.ρ M) v) =
+    (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ * coCoToMatrix v *
+    (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ := by
+  nth_rewrite 1 [coCoToMatrix]
+  simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.trans_apply]
+  trans (LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)) ((LinearMap.toMatrix
+      (complexCoBasis.tensorProduct complexCoBasis)
+      (complexCoBasis.tensorProduct complexCoBasis)
+      (TensorProduct.map (complexCo.ρ M) (complexCo.ρ M))
+      *ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)))
+      ((complexCoBasis.tensorProduct complexCoBasis).repr v))))
+  · apply congrArg
+    have h1 := (LinearMap.toMatrix_mulVec_repr (complexCoBasis.tensorProduct complexCoBasis)
+      (complexCoBasis.tensorProduct complexCoBasis)
+      (TensorProduct.map (complexCo.ρ M) (complexCo.ρ M)) v)
+    erw [h1]
+    rfl
+  rw [TensorProduct.toMatrix_map]
+  funext i j
+  change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
+        ((LinearMap.toMatrix complexCoBasis complexCoBasis) (complexCo.ρ M))
+        ((LinearMap.toMatrix complexCoBasis complexCoBasis) (complexCo.ρ M)) (i, j) k)
+        * coCoToMatrix v k.1 k.2) = _
+  erw [Finset.sum_product]
+  simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
+  have h1 : ∑ x, (∑ x1 , (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i *
+      coCoToMatrix v x1 x) * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j
+      = ∑ x , ∑ x1 , ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i
+      * coCoToMatrix v x1 x) * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j := by
+    congr
+    funext x
+    rw [Finset.sum_mul]
+  erw [h1]
+  rw [Finset.sum_comm]
+  congr
+  funext x
+  congr
+  funext x1
+  simp only [complexCoBasis_ρ_apply, transpose_apply, Action.instMonoidalCategory_tensorObj_V]
+  ring
+
+lemma contrCoToMatrix_ρ (v : (complexContr ⊗ complexCo).V) (M : SL(2,ℂ)) :
+    contrCoToMatrix (TensorProduct.map (complexContr.ρ M) (complexCo.ρ M) v) =
+    (LorentzGroup.toComplex (SL2C.toLorentzGroup M)) * contrCoToMatrix v *
+    (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ := by
+  nth_rewrite 1 [contrCoToMatrix]
+  simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.trans_apply]
+  trans (LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)) ((LinearMap.toMatrix
+      (complexContrBasis.tensorProduct complexCoBasis)
+      (complexContrBasis.tensorProduct complexCoBasis)
+      (TensorProduct.map (complexContr.ρ M) (complexCo.ρ M))
+      *ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)))
+      ((complexContrBasis.tensorProduct complexCoBasis).repr v))))
+  · apply congrArg
+    have h1 := (LinearMap.toMatrix_mulVec_repr (complexContrBasis.tensorProduct complexCoBasis)
+      (complexContrBasis.tensorProduct complexCoBasis)
+      (TensorProduct.map (complexContr.ρ M) (complexCo.ρ M)) v)
+    erw [h1]
+    rfl
+  rw [TensorProduct.toMatrix_map]
+  funext i j
+  change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
+        ((LinearMap.toMatrix complexContrBasis complexContrBasis) (complexContr.ρ M))
+        ((LinearMap.toMatrix complexCoBasis complexCoBasis) (complexCo.ρ M)) (i, j) k)
+        * contrCoToMatrix v k.1 k.2) = _
+  erw [Finset.sum_product]
+  simp_rw [kroneckerMap_apply, Matrix.mul_apply]
+  have h1 : ∑ x, (∑ x1 , LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 *
+      contrCoToMatrix v x1 x) * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j
+      = ∑ x , ∑ x1 , (LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1
+      * contrCoToMatrix v x1 x) * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j := by
+    congr
+    funext x
+    rw [Finset.sum_mul]
+  erw [h1]
+  rw [Finset.sum_comm]
+  congr
+  funext x
+  congr
+  funext x1
+  simp only [complexContrBasis_ρ_apply, complexCoBasis_ρ_apply, transpose_apply,
+    Action.instMonoidalCategory_tensorObj_V]
+  ring
+
+lemma coContrToMatrix_ρ (v : (complexCo ⊗ complexContr).V) (M : SL(2,ℂ)) :
+    coContrToMatrix (TensorProduct.map (complexCo.ρ M) (complexContr.ρ M) v) =
+    (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ * coContrToMatrix v *
+    (LorentzGroup.toComplex (SL2C.toLorentzGroup M))ᵀ := by
+  nth_rewrite 1 [coContrToMatrix]
+  simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.trans_apply]
+  trans (LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)) ((LinearMap.toMatrix
+      (complexCoBasis.tensorProduct complexContrBasis)
+      (complexCoBasis.tensorProduct complexContrBasis)
+      (TensorProduct.map (complexCo.ρ M) (complexContr.ρ M))
+      *ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)))
+      ((complexCoBasis.tensorProduct complexContrBasis).repr v))))
+  · apply congrArg
+    have h1 := (LinearMap.toMatrix_mulVec_repr (complexCoBasis.tensorProduct complexContrBasis)
+      (complexCoBasis.tensorProduct complexContrBasis)
+      (TensorProduct.map (complexCo.ρ M) (complexContr.ρ M)) v)
+    erw [h1]
+    rfl
+  rw [TensorProduct.toMatrix_map]
+  funext i j
+  change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
+        ((LinearMap.toMatrix complexCoBasis complexCoBasis) (complexCo.ρ M))
+        ((LinearMap.toMatrix complexContrBasis complexContrBasis) (complexContr.ρ M)) (i, j) k)
+        * coContrToMatrix v k.1 k.2) = _
+  erw [Finset.sum_product]
+  simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
+  have h1 : ∑ x, (∑ x1 , (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i *
+      coContrToMatrix v x1 x) * (LorentzGroup.toComplex (SL2C.toLorentzGroup M)) j x
+      = ∑ x , ∑ x1 , ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i
+      * coContrToMatrix v x1 x) * (LorentzGroup.toComplex (SL2C.toLorentzGroup M)) j x := by
+    congr
+    funext x
+    rw [Finset.sum_mul]
+  erw [h1]
+  rw [Finset.sum_comm]
+  congr
+  funext x
+  congr
+  funext x1
+  simp only [complexCoBasis_ρ_apply, complexContrBasis_ρ_apply, transpose_apply,
+    Action.instMonoidalCategory_tensorObj_V]
+  ring
+
+/-!
+
+## The symm version of the group actions.
+
+
+-/
+
+lemma contrContrToMatrix_ρ_symm (v : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) (M : SL(2,ℂ)) :
+    TensorProduct.map (complexContr.ρ M) (complexContr.ρ M) (contrContrToMatrix.symm v) =
+    contrContrToMatrix.symm ((LorentzGroup.toComplex (SL2C.toLorentzGroup M)) * v *
+    (LorentzGroup.toComplex (SL2C.toLorentzGroup M))ᵀ) := by
+  have h1 := contrContrToMatrix_ρ (contrContrToMatrix.symm v) M
+  simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.apply_symm_apply] at h1
+  rw [← h1]
+  simp
+
+lemma coCoToMatrix_ρ_symm (v : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) (M : SL(2,ℂ)) :
+    TensorProduct.map (complexCo.ρ M) (complexCo.ρ M) (coCoToMatrix.symm v) =
+    coCoToMatrix.symm ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ * v *
+    (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹) := by
+  have h1 := coCoToMatrix_ρ (coCoToMatrix.symm v) M
+  simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.apply_symm_apply] at h1
+  rw [← h1]
+  simp
+
+lemma contrCoToMatrix_ρ_symm (v : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) (M : SL(2,ℂ)) :
+    TensorProduct.map (complexContr.ρ M) (complexCo.ρ M) (contrCoToMatrix.symm v) =
+    contrCoToMatrix.symm ((LorentzGroup.toComplex (SL2C.toLorentzGroup M)) * v *
+    (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹) := by
+  have h1 := contrCoToMatrix_ρ (contrCoToMatrix.symm v) M
+  simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.apply_symm_apply] at h1
+  rw [← h1]
+  simp
+
+lemma coContrToMatrix_ρ_symm (v : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) (M : SL(2,ℂ)) :
+    TensorProduct.map (complexCo.ρ M) (complexContr.ρ M) (coContrToMatrix.symm v) =
+    coContrToMatrix.symm ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ * v *
+    (LorentzGroup.toComplex (SL2C.toLorentzGroup M))ᵀ) := by
+  have h1 := coContrToMatrix_ρ (coContrToMatrix.symm v) M
+  simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.apply_symm_apply] at h1
+  rw [← h1]
+  simp
+
+end Lorentz
+end

HepLean/SpaceTime/LorentzVector/Complex/Unit.lean

@@ -0,0 +1,89 @@
+/-
+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 HepLean.SpaceTime.LorentzVector.Complex.Two
+/-!
+
+# Unit for complex Lorentz vectors
+
+-/
+noncomputable section
+
+open Matrix
+open MatrixGroups
+open Complex
+open TensorProduct
+open SpaceTime
+open CategoryTheory.MonoidalCategory
+namespace Lorentz
+
+/-- The contra-co unit for complex lorentz vectors. Usually denoted `δⁱᵢ`. -/
+def contrCoUnitVal : (complexContr ⊗ complexCo).V :=
+  contrCoToMatrix.symm 1
+
+/-- The contra-co unit for complex lorentz vectors as a morphism
+  `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexCo`, manifesting the invaraince under
+  the `SL(2, ℂ)` action. -/
+def contrCoUnit :  𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexCo where
+  hom := {
+    toFun := fun a =>
+      let a' : ℂ := a
+      a' • contrCoUnitVal,
+    map_add' := fun x y => by
+      simp only [add_smul],
+    map_smul' := fun m x => by
+      simp only [smul_smul]
+      rfl}
+  comm M := by
+    ext x : 2
+    simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+      Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.coe_comp,
+      Function.comp_apply]
+    let x' : ℂ := x
+    change x' • contrCoUnitVal =
+      (TensorProduct.map (complexContr.ρ M) (complexCo.ρ M)) (x' • contrCoUnitVal)
+    simp only [Action.instMonoidalCategory_tensorObj_V, _root_.map_smul]
+    apply congrArg
+    simp only [Action.instMonoidalCategory_tensorObj_V, contrCoUnitVal]
+    erw [contrCoToMatrix_ρ_symm]
+    apply congrArg
+    simp
+
+/-- The co-contra unit for complex lorentz vectors. Usually denoted `δᵢⁱ`. -/
+def coContrUnitVal : (complexCo ⊗ complexContr).V :=
+  coContrToMatrix.symm 1
+
+/-- The co-contra unit for complex lorentz vectors as a morphism
+  `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexContr`, manifesting the invaraince under
+  the `SL(2, ℂ)` action. -/
+def coContrUnit :  𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexContr where
+  hom := {
+    toFun := fun a =>
+      let a' : ℂ := a
+      a' • coContrUnitVal,
+    map_add' := fun x y => by
+      simp only [add_smul],
+    map_smul' := fun m x => by
+      simp only [smul_smul]
+      rfl}
+  comm M := by
+    ext x : 2
+    simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+      Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.coe_comp,
+      Function.comp_apply]
+    let x' : ℂ := x
+    change x' • coContrUnitVal =
+      (TensorProduct.map (complexCo.ρ M) (complexContr.ρ M)) (x' • coContrUnitVal)
+    simp only [Action.instMonoidalCategory_tensorObj_V, _root_.map_smul]
+    apply congrArg
+    simp only [Action.instMonoidalCategory_tensorObj_V, coContrUnitVal]
+    erw [coContrToMatrix_ρ_symm]
+    apply congrArg
+    symm
+    refine transpose_eq_one.mp ?h.h.h.a
+    simp
+
+end Lorentz
+end

HepLean/SpaceTime/LorentzVector/Modules.lean

@@ -68,7 +68,7 @@ abbrev toFin13ℂ (ψ : ContrℂModule) := toFin13ℂEquiv ψ
 /-- The representation of the Lorentz group on `ContrℂModule`. -/
 def lorentzGroupRep : Representation ℂ (LorentzGroup 3) ContrℂModule where
   toFun M := {
-      toFun := fun v => toFin13ℂEquiv.symm ((M.1.map ofReal) *ᵥ v.toFin13ℂ),
+      toFun := fun v => toFin13ℂEquiv.symm (LorentzGroup.toComplex M *ᵥ v.toFin13ℂ),
       map_add' := by
         intro ψ ψ'
         simp [mulVec_add]
@@ -132,7 +132,7 @@ abbrev toFin13ℂ (ψ : CoℂModule) := toFin13ℂEquiv ψ
 /-- The representation of the Lorentz group on `CoℂModule`. -/
 def lorentzGroupRep : Representation ℂ (LorentzGroup 3) CoℂModule where
   toFun M := {
-      toFun := fun v => toFin13ℂEquiv.symm ((M.1.map ofReal)⁻¹ᵀ *ᵥ v.toFin13ℂ),
+      toFun := fun v => toFin13ℂEquiv.symm ((LorentzGroup.toComplex M)⁻¹ᵀ *ᵥ v.toFin13ℂ),
       map_add' := by
         intro ψ ψ'
         simp [mulVec_add]
@@ -147,7 +147,7 @@ def lorentzGroupRep : Representation ℂ (LorentzGroup 3) CoℂModule where
     simp only [SpecialLinearGroup.coe_mul, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.mul_apply,
       LinearEquiv.apply_symm_apply, mulVec_mulVec, EmbeddingLike.apply_eq_iff_eq]
     refine (congrFun (congrArg _ ?_) _)
-    simp only [lorentzGroupIsGroup_mul_coe, Matrix.map_mul]
+    simp only [_root_.map_mul]
     rw [Matrix.mul_inv_rev]
     exact transpose_mul _ _