From 8b2c853fd83b3a044c157ad02e961449d371dd67 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 31 Jul 2024 07:29:59 -0400
Subject: [PATCH 1/2] feat: equivariance of rising and lowering indices

---
 .../SpaceTime/LorentzTensor/Contraction.lean  |  4 +-
 .../LorentzTensor/MulActionTensor.lean        | 66 +++++++++++++++----
 .../LorentzTensor/RisingLowering.lean         | 62 ++++++++++++++++-
 3 files changed, 115 insertions(+), 17 deletions(-)

diff --git a/HepLean/SpaceTime/LorentzTensor/Contraction.lean b/HepLean/SpaceTime/LorentzTensor/Contraction.lean
index fed8eab..e08da05 100644
--- a/HepLean/SpaceTime/LorentzTensor/Contraction.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Contraction.lean
@@ -287,9 +287,9 @@ lemma contrAll_rep {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (
   simp only [mk_apply]
   apply congrArg
   funext x
-  rw [← repColorModule_colorModuleCast_apply]
+  rw [← colorModuleCast_equivariant_apply]
   nth_rewrite 2 [← contrDual_inv (c x) g]
-  rfl
+  simp
 
 @[simp]
 lemma contrAll_rep_apply {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = 𝓣.τ ∘ d ∘ e)
diff --git a/HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean b/HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean
index 46e9f14..c5de9da 100644
--- a/HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean
+++ b/HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean
@@ -27,6 +27,9 @@ class MulActionTensor (G : Type) [Monoid G] (𝓣 : TensorStructure R) where
   /-- The contraction of a vector with its dual is invariant under the group action. -/
   contrDual_inv : ∀ μ g, 𝓣.contrDual μ ∘ₗ
     TensorProduct.map (repColorModule μ g) (repColorModule (𝓣.τ μ) g) = 𝓣.contrDual μ
+  /-- The invariance of the metric under the group action. -/
+  metric_inv : ∀ μ g, (TensorProduct.map (repColorModule μ g) (repColorModule μ g)) (𝓣.metric μ) =
+    𝓣.metric μ
 
 namespace MulActionTensor
 
@@ -50,6 +53,9 @@ def compHom (f : H →* G) : MulActionTensor H 𝓣 where
   contrDual_inv μ h := by
     simp only [MonoidHom.coe_comp, Function.comp_apply]
     rw [contrDual_inv]
+  metric_inv μ h := by
+    simp only [MonoidHom.coe_comp, Function.comp_apply]
+    rw [metric_inv]
 
 /-- The trivial `MulActionTensor` defined via trivial representations. -/
 def trivial : MulActionTensor G 𝓣 where
@@ -57,6 +63,9 @@ def trivial : MulActionTensor G 𝓣 where
   contrDual_inv μ g := by
     simp only [Representation.trivial, MonoidHom.one_apply, TensorProduct.map_one]
     rfl
+  metric_inv μ g := by
+    simp only [Representation.trivial, MonoidHom.one_apply, TensorProduct.map_one]
+    rfl
 
 end MulActionTensor
 
@@ -74,6 +83,40 @@ variable {d : ℕ} {X Y Y' Z : Type} [Fintype X] [DecidableEq X] [Fintype Y] [De
 
 /-!
 
+# Equivariance properties involving modules
+
+-/
+
+@[simp]
+lemma contrDual_equivariant_tmul (g : G) (x : 𝓣.ColorModule μ) (y : 𝓣.ColorModule (𝓣.τ μ)) :
+    (𝓣.contrDual μ ((repColorModule μ g x) ⊗ₜ[R] (repColorModule (𝓣.τ μ) g y))) =
+    𝓣.contrDual μ (x ⊗ₜ[R] y) := by
+  trans (𝓣.contrDual μ ∘ₗ
+      TensorProduct.map (repColorModule μ g) (repColorModule (𝓣.τ μ) g)) (x ⊗ₜ[R] y)
+  rfl
+  rw [contrDual_inv]
+
+@[simp]
+lemma colorModuleCast_equivariant_apply (h : μ = ν) (g : G) (x : 𝓣.ColorModule μ) :
+    (𝓣.colorModuleCast h) (repColorModule μ g x) =
+    (repColorModule ν g) (𝓣.colorModuleCast h x) := by
+  subst h
+  simp [colorModuleCast]
+
+@[simp]
+lemma contrRightAux_contrDual_equivariant_tmul (g : G) (m : 𝓣.ColorModule ν ⊗[R] 𝓣.ColorModule μ)
+    (x : 𝓣.ColorModule (𝓣.τ μ)) : (contrRightAux (𝓣.contrDual μ))
+    ((TensorProduct.map (repColorModule ν g) (repColorModule μ g) m) ⊗ₜ[R]
+    (repColorModule (𝓣.τ μ) g x)) =
+    repColorModule ν g ((contrRightAux (𝓣.contrDual μ)) (m ⊗ₜ[R] x)) := by
+  refine TensorProduct.induction_on m (by simp) ?_ ?_
+  · intro y z
+    simp [contrRightAux]
+  · intro x z h1 h2
+    simp [add_tmul, LinearMap.map_add, h1, h2]
+
+/-!
+
 ## Representation of tensor products
 
 -/
@@ -89,19 +132,13 @@ def rep : Representation R G (𝓣.Tensor cX) where
 
 local infixl:101 " • " => 𝓣.rep
 
-lemma repColorModule_colorModuleCast_apply (h : μ = ν) (g : G) (x : 𝓣.ColorModule μ) :
-    (repColorModule ν g) (𝓣.colorModuleCast h x) =
-    (𝓣.colorModuleCast h) (repColorModule μ g x) := by
-  subst h
-  simp [colorModuleCast]
-
 @[simp]
 lemma repColorModule_colorModuleCast (h : μ = ν) (g : G) :
     (repColorModule ν g) ∘ₗ (𝓣.colorModuleCast h).toLinearMap =
     (𝓣.colorModuleCast h).toLinearMap ∘ₗ (repColorModule μ g) := by
   apply LinearMap.ext
   intro x
-  simp [repColorModule_colorModuleCast_apply]
+  simp [colorModuleCast_equivariant_apply]
 
 @[simp]
 lemma rep_mapIso (e : X ≃ Y) (h : cX = cY ∘ e) (g : G) :
@@ -112,7 +149,7 @@ lemma rep_mapIso (e : X ≃ Y) (h : cX = cY ∘ e) (g : G) :
   simp only [LinearMap.compMultilinearMap_apply, LinearMap.coe_comp, LinearEquiv.coe_coe,
     Function.comp_apply]
   erw [mapIso_tprod]
-  simp [rep, repColorModule_colorModuleCast_apply]
+  simp [rep, colorModuleCast_equivariant_apply]
   change (PiTensorProduct.map fun x => (repColorModule (cY x)) g)
     ((PiTensorProduct.tprod R) fun i => (𝓣.colorModuleCast _) (x (e.symm i))) =
     (𝓣.mapIso e h) ((PiTensorProduct.map _) ((PiTensorProduct.tprod R) x))
@@ -120,7 +157,7 @@ lemma rep_mapIso (e : X ≃ Y) (h : cX = cY ∘ e) (g : G) :
   apply congrArg
   funext i
   subst h
-  simp [repColorModule_colorModuleCast_apply]
+  simp [colorModuleCast_equivariant_apply]
 
 @[simp]
 lemma rep_mapIso_apply (e : X ≃ Y) (h : cX = cY ∘ e) (g : G) (x : 𝓣.Tensor cX) :
@@ -143,7 +180,7 @@ lemma rep_tprod (g : G) (f : (i : X) → 𝓣.ColorModule (cX i)) :
 
 -/
 
-lemma rep_tensoratorEquiv (g : G) :
+lemma tensoratorEquiv_equivariant (g : G) :
     (𝓣.tensoratorEquiv cX cY) ∘ₗ (TensorProduct.map (𝓣.rep g) (𝓣.rep g)) = 𝓣.rep g ∘ₗ
     (𝓣.tensoratorEquiv cX cY).toLinearMap := by
   apply tensorProd_piTensorProd_ext
@@ -156,18 +193,19 @@ lemma rep_tensoratorEquiv (g : G) :
   | Sum.inl x => rfl
   | Sum.inr x => rfl
 
-lemma rep_tensoratorEquiv_apply (g : G) (x : 𝓣.Tensor cX ⊗[R] 𝓣.Tensor cY) :
+@[simp]
+lemma tensoratorEquiv_equivariant_apply (g : G) (x : 𝓣.Tensor cX ⊗[R] 𝓣.Tensor cY) :
     (𝓣.tensoratorEquiv cX cY) ((TensorProduct.map (𝓣.rep g) (𝓣.rep g)) x)
     = (𝓣.rep g) ((𝓣.tensoratorEquiv cX cY) x) := by
   trans ((𝓣.tensoratorEquiv cX cY) ∘ₗ (TensorProduct.map (𝓣.rep g) (𝓣.rep g))) x
   rfl
-  rw [rep_tensoratorEquiv]
+  rw [tensoratorEquiv_equivariant]
   rfl
 
 lemma rep_tensoratorEquiv_tmul (g : G) (x : 𝓣.Tensor cX) (y : 𝓣.Tensor cY) :
     (𝓣.tensoratorEquiv cX cY) ((g • x) ⊗ₜ[R] (g • y)) =
     g • ((𝓣.tensoratorEquiv cX cY) (x ⊗ₜ[R] y)) := by
-  nth_rewrite 1 [← rep_tensoratorEquiv_apply]
+  nth_rewrite 1 [← tensoratorEquiv_equivariant_apply]
   rfl
 
 lemma rep_tensoratorEquiv_symm (g : G) :
@@ -175,7 +213,7 @@ lemma rep_tensoratorEquiv_symm (g : G) :
     (𝓣.tensoratorEquiv cX cY).symm.toLinearMap := by
   rw [LinearEquiv.eq_comp_toLinearMap_symm, LinearMap.comp_assoc,
     LinearEquiv.toLinearMap_symm_comp_eq]
-  exact Eq.symm (rep_tensoratorEquiv 𝓣 g)
+  exact Eq.symm (tensoratorEquiv_equivariant 𝓣 g)
 
 @[simp]
 lemma rep_tensoratorEquiv_symm_apply (g : G) (x : 𝓣.Tensor (Sum.elim cX cY)) :
diff --git a/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean b/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean
index 450b099..ed869d9 100644
--- a/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean
+++ b/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean
@@ -3,7 +3,7 @@ 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.LorentzTensor.Basic
+import HepLean.SpaceTime.LorentzTensor.MulActionTensor
 /-!
 
 # Rising and Lowering of indices
@@ -31,6 +31,9 @@ variable {d : ℕ} {X Y Y' Z W C P : Type} [Fintype X] [DecidableEq X] [Fintype
   {cX cX2 : X → 𝓣.Color} {cY : Y → 𝓣.Color} {cZ : Z → 𝓣.Color}
   {cW : W → 𝓣.Color} {cY' : Y' → 𝓣.Color} {μ ν: 𝓣.Color}
 
+variable {G H : Type} [Group G] [Group H] [MulActionTensor G 𝓣]
+local infixl:101 " • " => 𝓣.rep
+
 /-!
 
 ## Properties of the unit
@@ -120,6 +123,27 @@ def dualizeModule (μ : 𝓣.Color) : 𝓣.ColorModule μ ≃ₗ[R] 𝓣.ColorMo
       Function.comp_apply, lTensorHomToHomLTensor_apply, LinearMap.id_coe, id_eq,
       metric_contrRight_unit]
 
+@[simp]
+lemma dualizeModule_equivariant (g : G) :
+    (𝓣.dualizeModule μ) ∘ₗ ((MulActionTensor.repColorModule μ) g) =
+    (MulActionTensor.repColorModule (𝓣.τ μ) g) ∘ₗ (𝓣.dualizeModule μ) := by
+  apply LinearMap.ext
+  intro x
+  simp only [dualizeModule, dualizeFun, dualizeSymm, LinearEquiv.ofLinear_toLinearMap,
+    LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, colorModuleCast_equivariant_apply,
+    lTensorHomToHomLTensor_apply, LinearMap.id_coe, id_eq]
+  nth_rewrite 1 [← MulActionTensor.metric_inv (𝓣.τ μ) g]
+  simp
+
+@[simp]
+lemma dualizeModule_equivariant_apply (g : G) (x : 𝓣.ColorModule μ) :
+    (𝓣.dualizeModule μ) ((MulActionTensor.repColorModule μ) g x) =
+    (MulActionTensor.repColorModule (𝓣.τ μ) g) (𝓣.dualizeModule μ x) := by
+  trans ((𝓣.dualizeModule μ) ∘ₗ ((MulActionTensor.repColorModule μ) g)) x
+  rfl
+  rw [dualizeModule_equivariant]
+  rfl
+
 /-- Dualizes the color of all indicies of a tensor by contraction with the metric. -/
 def dualizeAll : 𝓣.Tensor cX ≃ₗ[R] 𝓣.Tensor (𝓣.τ ∘ cX) := by
   refine LinearEquiv.ofLinear
@@ -141,6 +165,24 @@ def dualizeAll : 𝓣.Tensor cX ≃ₗ[R] 𝓣.Tensor (𝓣.τ ∘ cX) := by
     apply congrArg
     simp
 
+@[simp]
+lemma dualizeAll_equivariant (g : G) : (𝓣.dualizeAll.toLinearMap) ∘ₗ (@rep R _ G _ 𝓣 _ X cX g)
+    = 𝓣.rep g ∘ₗ (𝓣.dualizeAll.toLinearMap) := by
+  apply LinearMap.ext
+  intro x
+  simp [dualizeAll]
+  refine PiTensorProduct.induction_on' x ?_ (by
+      intro a b hx a
+      simp [map_add, add_tmul, hx]
+      simp_all only [Function.comp_apply, LinearMap.coe_comp, LinearMap.id_coe, id_eq])
+  intro rx fx
+  simp
+  apply congrArg
+  change (PiTensorProduct.map _) ((PiTensorProduct.tprod R) _) =
+    (𝓣.rep g) ((PiTensorProduct.map _) ((PiTensorProduct.tprod R) fx))
+  rw [PiTensorProduct.map_tprod, PiTensorProduct.map_tprod]
+  simp
+
 lemma dualize_cond (e : C ⊕ P ≃ X) :
     cX = Sum.elim (cX ∘ e ∘ Sum.inl) (cX ∘ e ∘ Sum.inr) ∘ e.symm := by
   rw [Equiv.eq_comp_symm]
@@ -169,6 +211,24 @@ def dualize (e : C ⊕ P ≃ X) : 𝓣.Tensor cX ≃ₗ[R]
   (𝓣.tensoratorEquiv _ _) ≪≫ₗ
   𝓣.mapIso e (𝓣.dualize_cond' e)
 
+/-- Dualizing indices is equivariant with respect to the group action. This is the
+  applied version of this statement. -/
+@[simp]
+lemma dualize_equivariant_apply (e : C ⊕ P ≃ X) (g : G) (x : 𝓣.Tensor cX) :
+    𝓣.dualize e (g • x) = g • (𝓣.dualize e x) := by
+  simp only [dualize, TensorProduct.congr, LinearEquiv.refl_toLinearMap, LinearEquiv.refl_symm,
+    LinearEquiv.trans_apply, rep_mapIso_apply, rep_tensoratorEquiv_symm_apply,
+    LinearEquiv.ofLinear_apply]
+  rw [← LinearMap.comp_apply (TensorProduct.map _ _), ← TensorProduct.map_comp]
+  simp only [dualizeAll_equivariant, LinearMap.id_comp]
+  have h1 {M N A B C : Type} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid A]
+      [AddCommMonoid B] [AddCommMonoid C] [Module R M] [Module R N] [Module R A] [Module R B]
+      [Module R C] (f : M →ₗ[R] N) (g : A →ₗ[R] B) (h : B →ₗ[R] C) : TensorProduct.map (h ∘ₗ g) f
+      = TensorProduct.map h f ∘ₗ TensorProduct.map g (LinearMap.id) :=
+    ext rfl
+  rw [h1, LinearMap.coe_comp, Function.comp_apply]
+  simp only [tensoratorEquiv_equivariant_apply, rep_mapIso_apply]
+
 end TensorStructure
 
 end

From 7b0b979d51cceb4c96a445d2f78e43d69d510b60 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 31 Jul 2024 08:52:09 -0400
Subject: [PATCH 2/2] feat: Add metric invariance for Real Lorentz Tensors

---
 HepLean/SpaceTime/LorentzGroup/Basic.lean     |  21 +++
 .../SpaceTime/LorentzTensor/Real/Basic.lean   |  13 +-
 .../LorentzTensor/RisingLowering.lean         |   2 +-
 .../SpaceTime/LorentzVector/Contraction.lean  | 139 +++++++++++++++---
 .../SpaceTime/LorentzVector/Covariant.lean    |  10 ++
 .../LorentzVector/LorentzAction.lean          |   8 +
 HepLean/SpaceTime/MinkowskiMetric.lean        |   6 +
 7 files changed, 175 insertions(+), 24 deletions(-)

diff --git a/HepLean/SpaceTime/LorentzGroup/Basic.lean b/HepLean/SpaceTime/LorentzGroup/Basic.lean
index 98a12f5..5adf6fb 100644
--- a/HepLean/SpaceTime/LorentzGroup/Basic.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean
@@ -167,6 +167,27 @@ lemma subtype_mul_inv : (Subtype.val Λ) * (Subtype.val Λ)⁻¹ = 1 := by
   rw [mul_inv_self Λ]
   simp only [lorentzGroupIsGroup_one_coe]
 
+@[simp]
+lemma mul_minkowskiMatrix_mul_transpose :
+    (Subtype.val Λ) * minkowskiMatrix * (Subtype.val Λ).transpose = minkowskiMatrix := by
+  have h2 := Λ.prop
+  rw [LorentzGroup.mem_iff_self_mul_dual] at h2
+  simp [minkowskiMetric.dual] at h2
+  symm
+  refine right_inv_eq_left_inv minkowskiMatrix.sq ?_
+  rw [← h2]
+  noncomm_ring
+
+@[simp]
+lemma transpose_mul_minkowskiMatrix_mul_self :
+    (Subtype.val Λ).transpose * minkowskiMatrix * (Subtype.val Λ) = minkowskiMatrix := by
+  have h2 := Λ.prop
+  rw [LorentzGroup.mem_iff_dual_mul_self] at h2
+  simp [minkowskiMetric.dual] at h2
+  refine right_inv_eq_left_inv ?_ minkowskiMatrix.sq
+  rw [← h2]
+  noncomm_ring
+
 /-- The transpose of a matrix in the Lorentz group is an element of the Lorentz group. -/
 def transpose (Λ : LorentzGroup d) : LorentzGroup d :=
   ⟨Λ.1ᵀ, mem_iff_transpose.mp Λ.2⟩
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
index 745565e..dbf3abb 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
@@ -81,12 +81,12 @@ def realLorentzTensor (d : ℕ) : TensorStructure ℝ where
     | .down => LorentzVector.unitDown_rid
   metric μ :=
     match μ with
-    | realTensor.ColorType.up => asProdLorentzVector
-    | realTensor.ColorType.down => asProdCovariantLorentzVector
+    | realTensor.ColorType.up => asTenProd
+    | realTensor.ColorType.down => asCoTenProd
   metric_dual μ :=
     match μ with
-    | realTensor.ColorType.up => asProdLorentzVector_contr_asCovariantProdLorentzVector
-    | realTensor.ColorType.down => asProdCovariantLorentzVector_contr_asProdLorentzVector
+    | realTensor.ColorType.up => asTenProd_contr_asCoTenProd
+    | realTensor.ColorType.down => asCoTenProd_contr_asTenProd
 
 /-- The action of the Lorentz group on real Lorentz tensors. -/
 instance : MulActionTensor (LorentzGroup d) (realLorentzTensor d) where
@@ -98,5 +98,8 @@ instance : MulActionTensor (LorentzGroup d) (realLorentzTensor d) where
     match μ with
     | .up => TensorProduct.ext' (fun _ _ => LorentzVector.contrUpDown_invariant_lorentzAction)
     | .down => TensorProduct.ext' (fun _ _ => LorentzVector.contrDownUp_invariant_lorentzAction)
-
+  metric_inv μ g :=
+    match μ with
+    | .up => asTenProd_invariant g
+    | .down => asCoTenProd_invariant g
 end
diff --git a/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean b/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean
index ed869d9..7a95683 100644
--- a/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean
+++ b/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean
@@ -176,7 +176,7 @@ lemma dualizeAll_equivariant (g : G) : (𝓣.dualizeAll.toLinearMap) ∘ₗ (@re
       simp [map_add, add_tmul, hx]
       simp_all only [Function.comp_apply, LinearMap.coe_comp, LinearMap.id_coe, id_eq])
   intro rx fx
-  simp
+  simp only [PiTensorProduct.tprodCoeff_eq_smul_tprod, LinearMapClass.map_smul, rep_tprod]
   apply congrArg
   change (PiTensorProduct.map _) ((PiTensorProduct.tprod R) _) =
     (𝓣.rep g) ((PiTensorProduct.map _) ((PiTensorProduct.tprod R) fx))
diff --git a/HepLean/SpaceTime/LorentzVector/Contraction.lean b/HepLean/SpaceTime/LorentzVector/Contraction.lean
index 21c6e3a..25c3585 100644
--- a/HepLean/SpaceTime/LorentzVector/Contraction.lean
+++ b/HepLean/SpaceTime/LorentzVector/Contraction.lean
@@ -175,18 +175,41 @@ open scoped minkowskiMatrix
 variable {d : ℕ}
 
 /-- The metric tensor as an element of `LorentzVector d ⊗[ℝ] LorentzVector d`. -/
-def asProdLorentzVector : LorentzVector d ⊗[ℝ] LorentzVector d :=
-  ∑ μ, η μ μ • (LorentzVector.stdBasis μ ⊗ₜ[ℝ] LorentzVector.stdBasis μ)
+def asTenProd : LorentzVector d ⊗[ℝ] LorentzVector d :=
+  ∑ μ, ∑ ν, η μ ν • (LorentzVector.stdBasis μ ⊗ₜ[ℝ] LorentzVector.stdBasis ν)
+
+lemma asTenProd_diag :
+    @asTenProd d = ∑ μ, η μ μ • (LorentzVector.stdBasis μ ⊗ₜ[ℝ] LorentzVector.stdBasis μ) := by
+  simp only [asTenProd]
+  refine Finset.sum_congr rfl (fun μ _ => ?_)
+  rw [Finset.sum_eq_single μ]
+  intro ν _ hμν
+  rw [minkowskiMatrix.off_diag_zero hμν.symm]
+  simp only [zero_smul]
+  intro a
+  simp_all only
 
 /-- The metric tensor as an element of `CovariantLorentzVector d ⊗[ℝ] CovariantLorentzVector d`. -/
-def asProdCovariantLorentzVector : CovariantLorentzVector d ⊗[ℝ] CovariantLorentzVector d :=
-  ∑ μ, η μ μ • (CovariantLorentzVector.stdBasis μ ⊗ₜ[ℝ] CovariantLorentzVector.stdBasis μ)
+def asCoTenProd : CovariantLorentzVector d ⊗[ℝ] CovariantLorentzVector d :=
+  ∑ μ, ∑ ν, η μ ν • (CovariantLorentzVector.stdBasis μ ⊗ₜ[ℝ] CovariantLorentzVector.stdBasis ν)
+
+lemma asCoTenProd_diag :
+    @asCoTenProd d = ∑ μ, η μ μ • (CovariantLorentzVector.stdBasis μ ⊗ₜ[ℝ]
+      CovariantLorentzVector.stdBasis μ) := by
+  simp only [asCoTenProd]
+  refine Finset.sum_congr rfl (fun μ _ => ?_)
+  rw [Finset.sum_eq_single μ]
+  intro ν _ hμν
+  rw [minkowskiMatrix.off_diag_zero hμν.symm]
+  simp only [zero_smul]
+  intro a
+  simp_all only
 
 @[simp]
-lemma contrLeft_asProdLorentzVector (x : CovariantLorentzVector d) :
-    contrLeftAux contrDownUp (x ⊗ₜ[ℝ] asProdLorentzVector) =
+lemma contrLeft_asTenProd (x : CovariantLorentzVector d) :
+    contrLeftAux contrDownUp (x ⊗ₜ[ℝ] asTenProd) =
     ∑ μ, ((η μ μ * x μ) • LorentzVector.stdBasis μ) := by
-  simp only [asProdLorentzVector]
+  simp only [asTenProd_diag]
   rw [tmul_sum]
   rw [map_sum]
   refine Finset.sum_congr rfl (fun μ _ => ?_)
@@ -196,10 +219,10 @@ lemma contrLeft_asProdLorentzVector (x : CovariantLorentzVector d) :
   exact smul_smul (η μ μ) (x μ) (e μ)
 
 @[simp]
-lemma contrLeft_asProdCovariantLorentzVector (x : LorentzVector d) :
-    contrLeftAux contrUpDown (x ⊗ₜ[ℝ] asProdCovariantLorentzVector) =
+lemma contrLeft_asCoTenProd (x : LorentzVector d) :
+    contrLeftAux contrUpDown (x ⊗ₜ[ℝ] asCoTenProd) =
     ∑ μ, ((η μ μ * x μ) • CovariantLorentzVector.stdBasis μ) := by
-  simp only [asProdCovariantLorentzVector]
+  simp only [asCoTenProd_diag]
   rw [tmul_sum]
   rw [map_sum]
   refine Finset.sum_congr rfl (fun μ _ => ?_)
@@ -209,17 +232,17 @@ lemma contrLeft_asProdCovariantLorentzVector (x : LorentzVector d) :
   exact smul_smul (η μ μ) (x μ) (CovariantLorentzVector.stdBasis μ)
 
 @[simp]
-lemma asProdLorentzVector_contr_asCovariantProdLorentzVector :
-    (contrMidAux (contrUpDown) (asProdLorentzVector ⊗ₜ[ℝ] asProdCovariantLorentzVector))
+lemma asTenProd_contr_asCoTenProd :
+    (contrMidAux (contrUpDown) (asTenProd ⊗ₜ[ℝ] asCoTenProd))
     = TensorProduct.comm ℝ _ _ (@unitUp d) := by
-  simp only [contrMidAux, LinearEquiv.refl_toLinearMap, asProdLorentzVector, LinearMap.coe_comp,
+  simp only [contrMidAux, LinearEquiv.refl_toLinearMap, asTenProd_diag, LinearMap.coe_comp,
     LinearEquiv.coe_coe, Function.comp_apply]
   rw [sum_tmul, map_sum, map_sum, unitUp]
   simp only [Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
     Finset.sum_singleton, map_add, comm_tmul, map_sum]
   refine Finset.sum_congr rfl (fun μ _ => ?_)
   rw [← tmul_smul, TensorProduct.assoc_tmul]
-  simp only [map_tmul, LinearMap.id_coe, id_eq, contrLeft_asProdCovariantLorentzVector]
+  simp only [map_tmul, LinearMap.id_coe, id_eq, contrLeft_asCoTenProd]
   rw [tmul_sum, Finset.sum_eq_single_of_mem μ, tmul_smul]
   change (η μ μ * (η μ μ * e μ μ)) • e μ ⊗ₜ[ℝ] CovariantLorentzVector.stdBasis μ = _
   rw [LorentzVector.stdBasis]
@@ -236,10 +259,10 @@ lemma asProdLorentzVector_contr_asCovariantProdLorentzVector :
   exact fun a => False.elim (hμν (id (Eq.symm a)))
 
 @[simp]
-lemma asProdCovariantLorentzVector_contr_asProdLorentzVector :
-    (contrMidAux (contrDownUp) (asProdCovariantLorentzVector ⊗ₜ[ℝ] asProdLorentzVector))
+lemma asCoTenProd_contr_asTenProd :
+    (contrMidAux (contrDownUp) (asCoTenProd ⊗ₜ[ℝ] asTenProd))
     = TensorProduct.comm ℝ _ _ (@unitDown d) := by
-  simp only [contrMidAux, LinearEquiv.refl_toLinearMap, asProdCovariantLorentzVector,
+  simp only [contrMidAux, LinearEquiv.refl_toLinearMap, asCoTenProd_diag,
     LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply]
   rw [sum_tmul, map_sum, map_sum, unitDown]
   simp only [Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
@@ -247,7 +270,7 @@ lemma asProdCovariantLorentzVector_contr_asProdLorentzVector :
   refine Finset.sum_congr rfl (fun μ _ => ?_)
   rw [smul_tmul, TensorProduct.assoc_tmul]
   simp only [tmul_smul, LinearMapClass.map_smul, map_tmul, LinearMap.id_coe, id_eq,
-    contrLeft_asProdLorentzVector]
+    contrLeft_asTenProd]
   rw [tmul_sum, Finset.sum_eq_single_of_mem μ, tmul_smul, smul_smul, LorentzVector.stdBasis]
   erw [Pi.basisFun_apply]
   simp only [LinearMap.stdBasis_same, mul_one, η_apply_mul_η_apply_diag, one_smul]
@@ -260,6 +283,86 @@ lemma asProdCovariantLorentzVector_contr_asProdLorentzVector :
     ite_eq_right_iff, smul_eq_zero, mul_eq_zero]
   exact fun a => False.elim (hμν (id (Eq.symm a)))
 
+lemma asTenProd_invariant (g : LorentzGroup d) :
+    TensorProduct.map (LorentzVector.rep g) (LorentzVector.rep g) asTenProd = asTenProd := by
+  simp only [asTenProd, map_sum, LinearMapClass.map_smul, map_tmul, rep_apply_stdBasis,
+    Matrix.transpose_apply]
+  trans ∑ μ : Fin 1 ⊕ Fin d, ∑ ν : Fin 1 ⊕ Fin d, ∑ φ : Fin 1 ⊕ Fin d,
+      η μ ν • (g.1 φ μ • e φ) ⊗ₜ[ℝ] ∑ ρ : Fin 1 ⊕ Fin d, g.1 ρ ν • e ρ
+  refine Finset.sum_congr rfl (fun μ _ => Finset.sum_congr rfl (fun ν _ => ?_))
+  rw [sum_tmul, Finset.smul_sum]
+  trans ∑ μ : Fin 1 ⊕ Fin d, ∑ ν : Fin 1 ⊕ Fin d, ∑ φ : Fin 1 ⊕ Fin d, ∑ ρ : Fin 1 ⊕ Fin d,
+      (η μ ν • (g.1 φ μ • e φ) ⊗ₜ[ℝ] (g.1 ρ ν • e ρ))
+  · refine Finset.sum_congr rfl (fun μ _ => Finset.sum_congr rfl (fun ν _ =>
+      Finset.sum_congr rfl (fun φ _ => ?_)))
+    rw [tmul_sum, Finset.smul_sum]
+  rw [Finset.sum_congr rfl (fun μ _ => Finset.sum_comm)]
+  rw [Finset.sum_congr rfl (fun μ _ => Finset.sum_congr rfl (fun ν _ => Finset.sum_comm))]
+  rw [Finset.sum_comm]
+  rw [Finset.sum_congr rfl (fun φ _ => Finset.sum_comm)]
+  trans ∑ φ : Fin 1 ⊕ Fin d, ∑ ρ : Fin 1 ⊕ Fin d, ∑ μ : Fin 1 ⊕ Fin d, ∑ ν : Fin 1 ⊕ Fin d,
+      ((g.1 φ μ * η μ ν * g.1 ρ ν) • (e φ) ⊗ₜ[ℝ] (e ρ))
+  · refine Finset.sum_congr rfl (fun φ _ => Finset.sum_congr rfl (fun ρ _ =>
+    Finset.sum_congr rfl (fun μ _ => Finset.sum_congr rfl (fun ν _ => ?_))))
+    rw [smul_tmul, tmul_smul, tmul_smul, smul_smul, smul_smul]
+    ring_nf
+  rw [Finset.sum_congr rfl (fun φ _ => Finset.sum_congr rfl (fun ρ _ =>
+    Finset.sum_congr rfl (fun μ _ => Finset.sum_smul.symm)))]
+  rw [Finset.sum_congr rfl (fun φ _ => Finset.sum_congr rfl (fun ρ _ => Finset.sum_smul.symm))]
+  trans ∑ φ : Fin 1 ⊕ Fin d, ∑ ρ : Fin 1 ⊕ Fin d,
+    (((g.1 * minkowskiMatrix * g.1.transpose : Matrix _ _ _) φ ρ) • (e φ) ⊗ₜ[ℝ] (e ρ))
+  · refine Finset.sum_congr rfl (fun φ _ => Finset.sum_congr rfl (fun ρ _ => ?_))
+    apply congrFun
+    apply congrArg
+    simp only [Matrix.mul_apply, Matrix.transpose_apply]
+    rw [Finset.sum_comm]
+    refine Finset.sum_congr rfl (fun μ _ => ?_)
+    rw [Finset.sum_mul]
+  simp
+
+open CovariantLorentzVector in
+lemma asCoTenProd_invariant (g : LorentzGroup d) :
+    TensorProduct.map (CovariantLorentzVector.rep g) (CovariantLorentzVector.rep g)
+      asCoTenProd = asCoTenProd := by
+  simp only [asCoTenProd, map_sum, LinearMapClass.map_smul, map_tmul,
+    CovariantLorentzVector.rep_apply_stdBasis, Matrix.transpose_apply]
+  trans ∑ μ : Fin 1 ⊕ Fin d, ∑ ν : Fin 1 ⊕ Fin d, ∑ φ : Fin 1 ⊕ Fin d,
+      η μ ν • (g⁻¹.1 μ φ • CovariantLorentzVector.stdBasis φ) ⊗ₜ[ℝ]
+        ∑ ρ : Fin 1 ⊕ Fin d, g⁻¹.1 ν ρ • CovariantLorentzVector.stdBasis ρ
+  · refine Finset.sum_congr rfl (fun μ _ => Finset.sum_congr rfl (fun ν _ => ?_))
+    rw [sum_tmul, Finset.smul_sum]
+  trans ∑ μ : Fin 1 ⊕ Fin d, ∑ ν : Fin 1 ⊕ Fin d, ∑ φ : Fin 1 ⊕ Fin d, ∑ ρ : Fin 1 ⊕ Fin d,
+      (η μ ν • (g⁻¹.1 μ φ • CovariantLorentzVector.stdBasis φ) ⊗ₜ[ℝ]
+      (g⁻¹.1 ν ρ • CovariantLorentzVector.stdBasis ρ))
+  · refine Finset.sum_congr rfl (fun μ _ => Finset.sum_congr rfl (fun ν _ =>
+      Finset.sum_congr rfl (fun φ _ => ?_)))
+    rw [tmul_sum, Finset.smul_sum]
+  rw [Finset.sum_congr rfl (fun μ _ => Finset.sum_comm)]
+  rw [Finset.sum_congr rfl (fun μ _ => Finset.sum_congr rfl (fun ν _ => Finset.sum_comm))]
+  rw [Finset.sum_comm]
+  rw [Finset.sum_congr rfl (fun φ _ => Finset.sum_comm)]
+  trans ∑ φ : Fin 1 ⊕ Fin d, ∑ ρ : Fin 1 ⊕ Fin d, ∑ μ : Fin 1 ⊕ Fin d, ∑ ν : Fin 1 ⊕ Fin d,
+      ((g⁻¹.1 μ φ * η μ ν * g⁻¹.1 ν ρ) • (CovariantLorentzVector.stdBasis φ) ⊗ₜ[ℝ]
+      (CovariantLorentzVector.stdBasis ρ))
+  · refine Finset.sum_congr rfl (fun φ _ => Finset.sum_congr rfl (fun ρ _ =>
+    Finset.sum_congr rfl (fun μ _ => Finset.sum_congr rfl (fun ν _ => ?_))))
+    rw [smul_tmul, tmul_smul, tmul_smul, smul_smul, smul_smul]
+    ring_nf
+  rw [Finset.sum_congr rfl (fun φ _ => Finset.sum_congr rfl (fun ρ _ =>
+    Finset.sum_congr rfl (fun μ _ => Finset.sum_smul.symm)))]
+  rw [Finset.sum_congr rfl (fun φ _ => Finset.sum_congr rfl (fun ρ _ => Finset.sum_smul.symm))]
+  trans ∑ φ : Fin 1 ⊕ Fin d, ∑ ρ : Fin 1 ⊕ Fin d,
+    (((g⁻¹.1.transpose * minkowskiMatrix * g⁻¹.1 : Matrix _ _ _) φ ρ) •
+    (CovariantLorentzVector.stdBasis φ) ⊗ₜ[ℝ] (CovariantLorentzVector.stdBasis ρ))
+  · refine Finset.sum_congr rfl (fun φ _ => Finset.sum_congr rfl (fun ρ _ => ?_))
+    apply congrFun
+    apply congrArg
+    simp only [Matrix.mul_apply, Matrix.transpose_apply]
+    rw [Finset.sum_comm]
+    refine Finset.sum_congr rfl (fun μ _ => ?_)
+    rw [Finset.sum_mul]
+  rw [LorentzGroup.transpose_mul_minkowskiMatrix_mul_self]
+
 end minkowskiMatrix
 
 end
diff --git a/HepLean/SpaceTime/LorentzVector/Covariant.lean b/HepLean/SpaceTime/LorentzVector/Covariant.lean
index b2e799b..0deadf7 100644
--- a/HepLean/SpaceTime/LorentzVector/Covariant.lean
+++ b/HepLean/SpaceTime/LorentzVector/Covariant.lean
@@ -94,6 +94,16 @@ lemma rep_apply (g : LorentzGroup d) : rep g v = (g.1⁻¹)ᵀ *ᵥ v := by
   rw [← LorentzGroup.coe_inv]
   rfl
 
+lemma rep_apply_stdBasis (g : LorentzGroup d) (μ : Fin 1 ⊕ Fin d) :
+    rep g (stdBasis μ) = ∑ ν, g⁻¹.1 μ ν • stdBasis ν := by
+  simp only [rep_apply, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+    Finset.sum_singleton, decomp_stdBasis']
+  funext ν
+  simp [LorentzVector.stdBasis, Pi.basisFun_apply]
+  erw [Pi.basisFun_apply, Matrix.mulVec_stdBasis]
+  rw [← LorentzGroup.coe_inv]
+  simp
+
 end CovariantLorentzVector
 
 end
diff --git a/HepLean/SpaceTime/LorentzVector/LorentzAction.lean b/HepLean/SpaceTime/LorentzVector/LorentzAction.lean
index 40ad4d1..4a58bfd 100644
--- a/HepLean/SpaceTime/LorentzVector/LorentzAction.lean
+++ b/HepLean/SpaceTime/LorentzVector/LorentzAction.lean
@@ -28,6 +28,14 @@ def rep : Representation ℝ (LorentzGroup d) (LorentzVector d) where
 open Matrix in
 lemma rep_apply (g : LorentzGroup d) : rep g v = g *ᵥ v := rfl
 
+lemma rep_apply_stdBasis (g : LorentzGroup d) (μ : Fin 1 ⊕ Fin d) :
+    rep g (stdBasis μ) = ∑ ν, g.1.transpose μ ν • stdBasis ν := by
+  simp only [rep_apply, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+    Finset.sum_singleton, decomp_stdBasis']
+  funext ν
+  simp [LorentzVector.stdBasis, Pi.basisFun_apply]
+  erw [Pi.basisFun_apply, Matrix.mulVec_stdBasis]
+
 end LorentzVector
 
 end
diff --git a/HepLean/SpaceTime/MinkowskiMetric.lean b/HepLean/SpaceTime/MinkowskiMetric.lean
index 82da1fd..972b85f 100644
--- a/HepLean/SpaceTime/MinkowskiMetric.lean
+++ b/HepLean/SpaceTime/MinkowskiMetric.lean
@@ -79,6 +79,12 @@ lemma as_block : @minkowskiMatrix d = (
   rw [← diagonal_neg]
   rfl
 
+@[simp]
+lemma off_diag_zero {μ ν : Fin 1 ⊕ Fin d} (h : μ ≠ ν) : η μ ν = 0 := by
+  simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
+  apply diagonal_apply_ne
+  exact h
+
 end minkowskiMatrix
 
 /-!