Merge pull request #103 from HEPLean/Tensors-V2

feat: Equivariance of rising and lower operations
2024-07-31 09:01:26 -04:00 · 2024-07-31 09:01:26 -04:00 · 2439ec3d1d
commit 2439ec3d1d
parent 78fba40a59 7b0b979d51
9 changed files with 289 additions and 40 deletions
--- 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⟩
--- 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)
--- 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)) :
--- 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
--- 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 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))
+  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
--- 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
--- 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
--- 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
--- 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

 /-!