Merge pull request #102 from HEPLean/Tensors-V2

feat: Add rising and lowering of Lorentz indices
2024-07-30 16:49:44 -04:00 · 2024-07-30 16:49:44 -04:00 · 78fba40a59
commit 78fba40a59
parent 12ca7afb49 a97cb62379
8 changed files with 496 additions and 99 deletions
--- a/HepLean.lean
+++ b/HepLean.lean
@ -76,6 +76,7 @@ import HepLean.SpaceTime.LorentzTensor.Fin
 import HepLean.SpaceTime.LorentzTensor.MulActionTensor
 import HepLean.SpaceTime.LorentzTensor.Notation
 import HepLean.SpaceTime.LorentzTensor.Real.Basic
+import HepLean.SpaceTime.LorentzTensor.RisingLowering
 import HepLean.SpaceTime.LorentzVector.AsSelfAdjointMatrix
 import HepLean.SpaceTime.LorentzVector.Basic
 import HepLean.SpaceTime.LorentzVector.Contraction
--- a/HepLean/SpaceTime/LorentzTensor/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Basic.lean
@ -34,22 +34,56 @@ open TensorProduct

 variable {R : Type} [CommSemiring R]

+namespace TensorStructure
+
 /-- An auxillary function to contract the vector space `V1` and `V2` in `V1 ⊗[R] V2 ⊗[R] V3`. -/
-def contrDualLeftAux {V1 V2 V3 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [AddCommMonoid V3]
+def contrLeftAux {V1 V2 V3 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [AddCommMonoid V3]
    [Module R V1] [Module R V2] [Module R V3] (f : V1 ⊗[R] V2 →ₗ[R] R) :
    V1 ⊗[R] V2 ⊗[R] V3 →ₗ[R] V3 :=
  (TensorProduct.lid R _).toLinearMap ∘ₗ
  TensorProduct.map (f) (LinearEquiv.refl R V3).toLinearMap
  ∘ₗ (TensorProduct.assoc R _ _ _).symm.toLinearMap

+/-- An auxillary function to contract the vector space `V1` and `V2` in `(V3 ⊗[R] V1) ⊗[R] V2`. -/
+def contrRightAux {V1 V2 V3 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [AddCommMonoid V3]
+    [Module R V1] [Module R V2] [Module R V3] (f : V1 ⊗[R] V2 →ₗ[R] R) :
+    (V3 ⊗[R] V1) ⊗[R] V2 →ₗ[R] V3 :=
+  (TensorProduct.rid R _).toLinearMap ∘ₗ
+  TensorProduct.map (LinearEquiv.refl R V3).toLinearMap f ∘ₗ
+  (TensorProduct.assoc R _ _ _).toLinearMap
+
 /-- An auxillary function to contract the vector space `V1` and `V2` in
  `V4 ⊗[R] V1 ⊗[R] V2 ⊗[R] V3`. -/
-def contrDualMidAux {V1 V2 V3 V4 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [AddCommMonoid V3]
+def contrMidAux {V1 V2 V3 V4 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [AddCommMonoid V3]
    [AddCommMonoid V4] [Module R V1] [Module R V2] [Module R V3] [Module R V4]
    (f : V1 ⊗[R] V2 →ₗ[R] R) : (V4 ⊗[R] V1) ⊗[R] (V2 ⊗[R] V3) →ₗ[R] V4 ⊗[R] V3 :=
-  (TensorProduct.map (LinearEquiv.refl R V4).toLinearMap (contrDualLeftAux f)) ∘ₗ
+  (TensorProduct.map (LinearEquiv.refl R V4).toLinearMap (contrLeftAux f)) ∘ₗ
  (TensorProduct.assoc R _ _ _).toLinearMap

+lemma contrRightAux_comp {V1 V2 V3 V4 V5 : Type} [AddCommMonoid V1] [AddCommMonoid V2]
+    [AddCommMonoid V3] [AddCommMonoid V4] [AddCommMonoid V5] [Module R V1] [Module R V3]
+    [Module R V2] [Module R V4] [Module R V5] (f : V2 ⊗[R] V3 →ₗ[R] R) (g : V4 ⊗[R] V5 →ₗ[R] R) :
+    (contrRightAux f ∘ₗ TensorProduct.map (LinearMap.id : V1 ⊗[R] V2 →ₗ[R] V1 ⊗[R] V2)
+      (contrRightAux g)) =
+    (contrRightAux g) ∘ₗ TensorProduct.map (contrMidAux f) LinearMap.id
+    ∘ₗ (TensorProduct.assoc R _ _ _).symm.toLinearMap := by
+  apply TensorProduct.ext'
+  intro x y
+  refine TensorProduct.induction_on x (by simp) ?_ (fun x z h1 h2 =>
+    by simp [add_tmul, LinearMap.map_add, h1, h2])
+  intro x1 x2
+  refine TensorProduct.induction_on y (by simp) ?_ (fun x z h1 h2 =>
+    by simp [add_tmul, tmul_add, LinearMap.map_add, h1, h2])
+  intro y x5
+  refine TensorProduct.induction_on y (by simp) ?_ (fun x z h1 h2 =>
+    by simp [add_tmul, tmul_add, LinearMap.map_add, h1, h2])
+  intro x3 x4
+  simp [contrRightAux, contrMidAux, contrLeftAux]
+  erw [TensorProduct.map_tmul]
+  simp only [LinearMapClass.map_smul, LinearMap.id_coe, id_eq, mk_apply, rid_tmul]
+
+end TensorStructure
+
 /-- An initial structure specifying a tensor system (e.g. a system in which you can
  define real Lorentz tensors or Einstein notation convention). -/
 structure TensorStructure (R : Type) [CommSemiring R] where
@ -72,18 +106,15 @@ structure TensorStructure (R : Type) [CommSemiring R] where
  contrDual_symm : ∀ μ x y, (contrDual μ) (x ⊗ₜ[R] y) =
    (contrDual (τ μ)) (y ⊗ₜ[R] (Equiv.cast (congrArg ColorModule (τ_involutive μ).symm) x))
  /-- The unit of the contraction. -/
-  unit : (μ : Color) → ColorModule μ ⊗[R] ColorModule (τ μ)
+  unit : (μ : Color) → ColorModule (τ μ) ⊗[R] ColorModule μ
  /-- The unit is a right identity. -/
-  unit_lid : ∀ μ (x : ColorModule μ),
-    TensorProduct.rid R _
-    (TensorProduct.map (LinearEquiv.refl R (ColorModule μ)).toLinearMap
-    (contrDual μ ∘ₗ (TensorProduct.comm R _ _).toLinearMap)
-    ((TensorProduct.assoc R _ _ _) (unit μ ⊗ₜ[R] x))) = x
+  unit_rid : ∀ μ (x : ColorModule μ),
+    TensorStructure.contrLeftAux (contrDual μ) (x ⊗ₜ[R] unit μ) = x
  /-- The metric for a given color. -/
  metric : (μ : Color) → ColorModule μ ⊗[R] ColorModule μ
  /-- The metric contracted with its dual is the unit. -/
-  metric_dual : ∀ (μ : Color), (contrDualMidAux (contrDual μ)
-    (metric μ ⊗ₜ[R] metric (τ μ))) = unit μ
+  metric_dual : ∀ (μ : Color), (TensorStructure.contrMidAux (contrDual μ)
+    (metric μ ⊗ₜ[R] metric (τ μ))) = TensorProduct.comm _ _ _ (unit μ)

 namespace TensorStructure

@ -92,7 +123,7 @@ variable (𝓣 : TensorStructure R)
 variable {d : ℕ} {X Y Y' Z W : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
  [Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z] [Fintype W] [DecidableEq W]
  {cX cX2 : X → 𝓣.Color} {cY : Y → 𝓣.Color} {cZ : Z → 𝓣.Color}
-  {cW : W → 𝓣.Color} {cY' : Y' → 𝓣.Color} {μ ν: 𝓣.Color}
+  {cW : W → 𝓣.Color} {cY' : Y' → 𝓣.Color} {μ ν η : 𝓣.Color}

 instance : AddCommMonoid (𝓣.ColorModule μ) := 𝓣.colorModule_addCommMonoid μ

@ -107,6 +138,16 @@ instance : AddCommMonoid (𝓣.Tensor cX) :=

 instance : Module R (𝓣.Tensor cX) := PiTensorProduct.instModule

+/-!
+
+## Color
+
+Recall the `color` of an index describes the type of the index.
+
+For example, in a real Lorentz tensor the colors are `{up, down}`.
+
+-/
+
 /-- Equivalence of `ColorModule` given an equality of colors. -/
 def colorModuleCast (h : μ = ν) : 𝓣.ColorModule μ ≃ₗ[R] 𝓣.ColorModule ν where
  toFun := Equiv.cast (congrArg 𝓣.ColorModule h)
@ -120,6 +161,45 @@ def colorModuleCast (h : μ = ν) : 𝓣.ColorModule μ ≃ₗ[R] 𝓣.ColorModu
  left_inv x := Equiv.symm_apply_apply (Equiv.cast (congrArg 𝓣.ColorModule h)) x
  right_inv x := Equiv.apply_symm_apply (Equiv.cast (congrArg 𝓣.ColorModule h)) x

+/-- A relation on colors which is true if the two colors are equal or are duals. -/
+def colorRel (μ ν : 𝓣.Color) : Prop := μ = ν ∨ μ = 𝓣.τ ν
+
+/-- An equivalence relation on colors which is true if the two colors are equal or are duals. -/
+lemma colorRel_equivalence : Equivalence 𝓣.colorRel where
+  refl := by
+    intro x
+    left
+    rfl
+  symm := by
+    intro x y h
+    rcases h with h | h
+    · left
+      exact h.symm
+    · right
+      subst h
+      exact (𝓣.τ_involutive y).symm
+  trans := by
+    intro x y z hxy hyz
+    rcases hxy with hxy | hxy <;>
+      rcases hyz with hyz | hyz <;>
+      subst hxy hyz
+    · left
+      rfl
+    · right
+      rfl
+    · right
+      rfl
+    · left
+      exact 𝓣.τ_involutive z
+
+/-- The structure of a setoid on colors, two colors are related if they are equal,
+  or dual. -/
+instance colorSetoid : Setoid 𝓣.Color := ⟨𝓣.colorRel, 𝓣.colorRel_equivalence⟩
+
+/-- A map taking a color to its equivalence class in `colorSetoid`. -/
+def colorQuot (μ : 𝓣.Color) : Quotient 𝓣.colorSetoid :=
+  Quotient.mk 𝓣.colorSetoid μ
+
 lemma tensorProd_piTensorProd_ext {M : Type} [AddCommMonoid M] [Module R M]
    {f g : 𝓣.Tensor cX ⊗[R] 𝓣.Tensor cY →ₗ[R] M}
    (h : ∀ p q, f (PiTensorProduct.tprod R p ⊗ₜ[R] PiTensorProduct.tprod R q)
@ -479,6 +559,55 @@ lemma tensoratorEquiv_mapIso_tmul (e : X ≃ Y) (e' : Z ≃ Y) (e'' : W ≃ X)

 /-!

+## contrDual properties
+
+-/
+
+lemma contrDual_cast (h : μ = ν) (x : 𝓣.ColorModule μ) (y : 𝓣.ColorModule (𝓣.τ μ)) :
+    𝓣.contrDual μ (x ⊗ₜ[R] y) = 𝓣.contrDual ν (𝓣.colorModuleCast h x ⊗ₜ[R]
+      𝓣.colorModuleCast (congrArg 𝓣.τ h) y) := by
+  subst h
+  rfl
+
+/-- `𝓣.contrDual (𝓣.τ μ)` in terms of `𝓣.contrDual μ`. -/
+@[simp]
+lemma contrDual_symm' (μ : 𝓣.Color) (x : 𝓣.ColorModule (𝓣.τ μ))
+    (y : 𝓣.ColorModule (𝓣.τ (𝓣.τ μ))) : 𝓣.contrDual (𝓣.τ μ) (x ⊗ₜ[R] y) =
+    (𝓣.contrDual μ) ((𝓣.colorModuleCast (𝓣.τ_involutive μ) y) ⊗ₜ[R] x) := by
+  rw [𝓣.contrDual_symm, 𝓣.contrDual_cast (𝓣.τ_involutive μ)]
+  congr
+  simp [colorModuleCast]
+
+lemma contrDual_symm_contrRightAux (h : ν = η) :
+    (𝓣.colorModuleCast h) ∘ₗ contrRightAux (𝓣.contrDual μ) =
+    contrRightAux (𝓣.contrDual (𝓣.τ (𝓣.τ μ))) ∘ₗ
+    (TensorProduct.congr (
+      TensorProduct.congr (𝓣.colorModuleCast h) (𝓣.colorModuleCast (𝓣.τ_involutive μ).symm))
+    (𝓣.colorModuleCast ((𝓣.τ_involutive (𝓣.τ μ)).symm))).toLinearMap := by
+  apply TensorProduct.ext'
+  intro x y
+  refine TensorProduct.induction_on x (by simp) ?_ ?_
+  · intro x z
+    simp [contrRightAux]
+    congr
+    simp [colorModuleCast]
+    simp [colorModuleCast]
+  · intro x z h1 h2
+    simp [add_tmul, LinearMap.map_add, h1, h2]
+
+lemma contrDual_symm_contrRightAux_apply_tmul (h : ν = η)
+    (m : 𝓣.ColorModule ν ⊗[R] 𝓣.ColorModule μ) (x : 𝓣.ColorModule (𝓣.τ μ)) :
+    𝓣.colorModuleCast h (contrRightAux (𝓣.contrDual μ) (m ⊗ₜ[R] x)) =
+    contrRightAux (𝓣.contrDual (𝓣.τ (𝓣.τ μ))) ((TensorProduct.congr
+    (𝓣.colorModuleCast h) (𝓣.colorModuleCast (𝓣.τ_involutive μ).symm) (m)) ⊗ₜ
+    (𝓣.colorModuleCast (𝓣.τ_involutive (𝓣.τ μ)).symm x)) := by
+  trans ((𝓣.colorModuleCast h) ∘ₗ contrRightAux (𝓣.contrDual μ)) (m ⊗ₜ[R] x)
+  rfl
+  rw [contrDual_symm_contrRightAux]
+  rfl
+
+/-!
+
 ## Splitting tensors into tensor products

 -/
--- a/HepLean/SpaceTime/LorentzTensor/Contraction.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Contraction.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
 /-!

 # Contraction of indices
@ -30,9 +30,13 @@ We define a number of ways to contract indices of tensors:
  `𝓣.Tensor (Sum.elim cW cX) ⊗[R] 𝓣.Tensor (Sum.elim cY cZ) →ₗ[R] 𝓣.Tensor (Sum.elim cW cZ)`

 -/
+
+/-! TODO: Define contraction based on an equivalence `(C ⊗ C) ⊗ P ≃ X` satisfying ... . -/
+
 noncomputable section

 open TensorProduct
+open MulActionTensor

 variable {R : Type} [CommSemiring R]

@ -40,11 +44,14 @@ namespace TensorStructure

 variable (𝓣 : TensorStructure R)

-variable {d : ℕ} {X Y Y' Z W : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
+variable {d : ℕ} {X Y Y' Z W C P : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
  [Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z] [Fintype W] [DecidableEq W]
+  [Fintype C] [DecidableEq C] [Fintype P] [DecidableEq P]
  {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
 /-!

 # Contractions of vectors
@ -55,7 +62,7 @@ variable {d : ℕ} {X Y Y' Z W : Type} [Fintype X] [DecidableEq X] [Fintype Y] [
  `𝓣.ColorModule (𝓣.τ ν) ⊗[R] 𝓣.ColorModule η` to form a vector in `𝓣.ColorModule η`. -/
 def contrDualLeft {ν η : 𝓣.Color} :
    𝓣.ColorModule ν ⊗[R] 𝓣.ColorModule (𝓣.τ ν) ⊗[R] 𝓣.ColorModule η →ₗ[R] 𝓣.ColorModule η :=
-  contrDualLeftAux (𝓣.contrDual ν)
+  contrLeftAux (𝓣.contrDual ν)

 /-- The contraction of a vector in `𝓣.ColorModule μ ⊗[R] 𝓣.ColorModule ν` with a vector in
  `𝓣.ColorModule (𝓣.τ ν) ⊗[R] 𝓣.ColorModule η` to form a vector in
@ -63,7 +70,7 @@ def contrDualLeft {ν η : 𝓣.Color} :
 def contrDualMid {μ ν η : 𝓣.Color} :
    (𝓣.ColorModule μ ⊗[R] 𝓣.ColorModule ν) ⊗[R] (𝓣.ColorModule (𝓣.τ ν) ⊗[R] 𝓣.ColorModule η) →ₗ[R]
      𝓣.ColorModule μ ⊗[R] 𝓣.ColorModule η :=
-  contrDualMidAux (𝓣.contrDual ν)
+  contrMidAux (𝓣.contrDual ν)

 /-- A linear map taking tensors mapped with the same index set to the product of paired tensors. -/
 def pairProd : 𝓣.Tensor cX ⊗[R] 𝓣.Tensor cX2 →ₗ[R]
@ -248,4 +255,104 @@ def contrElim (e : X ≃ Y) (h : cX = 𝓣.τ ∘ cY ∘ e) :
    (TensorProduct.congr (𝓣.tensoratorEquiv cW cX).symm
      (𝓣.tensoratorEquiv cY cZ).symm).toLinearMap

+/-!
+
+## Group acting on contraction
+
+-/
+
+@[simp]
+lemma contrAll_rep {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = 𝓣.τ ∘ d ∘ e) (g : G) :
+    𝓣.contrAll e h ∘ₗ (TensorProduct.map (𝓣.rep g) (𝓣.rep g)) = 𝓣.contrAll e h := by
+  apply TensorProduct.ext'
+  refine fun x ↦ PiTensorProduct.induction_on' x ?_ (by
+      intro a b hx hy y
+      simp [map_add, add_tmul, hx, hy])
+  intro rx fx
+  refine fun y ↦ PiTensorProduct.induction_on' y ?_ (by
+      intro a b hx hy
+      simp at hx hy
+      simp [map_add, tmul_add, hx, hy])
+  intro ry fy
+  simp [contrAll, TensorProduct.smul_tmul]
+  apply congrArg
+  apply congrArg
+  simp [contrAll']
+  apply congrArg
+  simp [pairProd]
+  change (PiTensorProduct.map _) ((PiTensorProduct.map₂ _ _) _) =
+    (PiTensorProduct.map _) ((PiTensorProduct.map₂ _ _) _)
+  rw [PiTensorProduct.map₂_tprod_tprod, PiTensorProduct.map₂_tprod_tprod, PiTensorProduct.map_tprod,
+  PiTensorProduct.map_tprod]
+  simp only [mk_apply]
+  apply congrArg
+  funext x
+  rw [← repColorModule_colorModuleCast_apply]
+  nth_rewrite 2 [← contrDual_inv (c x) g]
+  rfl
+
+@[simp]
+lemma contrAll_rep_apply {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = 𝓣.τ ∘ d ∘ e)
+    (g : G) (x : 𝓣.Tensor c ⊗ 𝓣.Tensor d) :
+    𝓣.contrAll e h (TensorProduct.map (𝓣.rep g) (𝓣.rep g) x) = 𝓣.contrAll e h x := by
+  change (𝓣.contrAll e h ∘ₗ (TensorProduct.map (𝓣.rep g) (𝓣.rep g))) x = _
+  rw [contrAll_rep]
+
+@[simp]
+lemma contrAll_rep_tmul {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = 𝓣.τ ∘ d ∘ e)
+    (g : G) (x : 𝓣.Tensor c) (y : 𝓣.Tensor d) :
+    𝓣.contrAll e h ((g • x) ⊗ₜ[R] (g • y)) = 𝓣.contrAll e h (x ⊗ₜ[R] y) := by
+  nth_rewrite 2 [← @contrAll_rep_apply R _ 𝓣 _ _ _ G]
+  rfl
+
+/-!
+
+## Contraction based on specification
+
+-/
+
+lemma contr_cond (e : (C ⊕ C) ⊕ P ≃ X) :
+    cX = Sum.elim (Sum.elim (cX ∘ ⇑e ∘ Sum.inl ∘ Sum.inl) (cX ∘ ⇑e ∘ Sum.inl ∘ Sum.inr)) (
+      cX ∘ ⇑e ∘ Sum.inr) ∘ ⇑e.symm := by
+  rw [Equiv.eq_comp_symm]
+  funext x
+  match x with
+  | Sum.inl (Sum.inl x) => rfl
+  | Sum.inl (Sum.inr x) => rfl
+  | Sum.inr x => rfl
+
+/-- Contraction of indices based on an equivalence `(C ⊕ C) ⊕ P ≃ X`. The indices
+  in `C` are contracted pair-wise, whilst the indices in `P` are preserved. -/
+def contr (e : (C ⊕ C) ⊕ P ≃ X)
+    (h : cX ∘ e ∘ Sum.inl ∘ Sum.inl = 𝓣.τ ∘ cX ∘ e ∘ Sum.inl ∘ Sum.inr) :
+    𝓣.Tensor cX →ₗ[R] 𝓣.Tensor (cX ∘ e ∘ Sum.inr) :=
+  (TensorProduct.lid R _).toLinearMap ∘ₗ
+  (TensorProduct.map (𝓣.contrAll (Equiv.refl C) (by simpa using h)) LinearMap.id) ∘ₗ
+  (TensorProduct.congr (𝓣.tensoratorEquiv _ _).symm (LinearEquiv.refl R _)).toLinearMap ∘ₗ
+  (𝓣.tensoratorEquiv _ _).symm.toLinearMap ∘ₗ
+  (𝓣.mapIso e.symm (𝓣.contr_cond e)).toLinearMap
+
+/-- The contraction of indices via `contr` is equivariant. -/
+@[simp]
+lemma contr_equivariant (e : (C ⊕ C) ⊕ P ≃ X)
+    (h : cX ∘ e ∘ Sum.inl ∘ Sum.inl = 𝓣.τ ∘ cX ∘ e ∘ Sum.inl ∘ Sum.inr)
+    (g : G) (x : 𝓣.Tensor cX) : 𝓣.contr e h (g • x) = g • 𝓣.contr e h x := by
+  simp only [contr, TensorProduct.congr, LinearEquiv.refl_toLinearMap, LinearEquiv.symm_symm,
+    LinearEquiv.refl_symm, LinearEquiv.ofLinear_toLinearMap, LinearEquiv.comp_coe,
+    LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, LinearEquiv.trans_apply,
+    rep_mapIso_apply, rep_tensoratorEquiv_symm_apply]
+  rw [← LinearMap.comp_apply (TensorProduct.map _ _), ← TensorProduct.map_comp]
+  rw [← LinearMap.comp_apply (TensorProduct.map _ _), ← TensorProduct.map_comp]
+  rw [LinearMap.comp_assoc, rep_tensoratorEquiv_symm, ← LinearMap.comp_assoc]
+  simp only [contrAll_rep, LinearMap.comp_id, LinearMap.id_comp]
+  have h1 {M N A B : Type} [AddCommMonoid M] [AddCommMonoid N]
+      [AddCommMonoid A] [AddCommMonoid B] [Module R M] [Module R N] [Module R A] [Module R B]
+      (f : M →ₗ[R] N) (g : A →ₗ[R] B) : TensorProduct.map f g
+      = TensorProduct.map (LinearMap.id) g ∘ₗ TensorProduct.map f (LinearMap.id) :=
+    ext rfl
+  rw [h1]
+  simp only [LinearMap.coe_comp, Function.comp_apply, rep_lid_apply]
+  rw [← LinearMap.comp_apply (TensorProduct.map _ _), ← TensorProduct.map_comp]
+  rfl
+
 end TensorStructure
--- a/HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean
+++ b/HepLean/SpaceTime/LorentzTensor/MulActionTensor.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.Contraction
+import HepLean.SpaceTime.LorentzTensor.Basic
 import Mathlib.RepresentationTheory.Basic
 /-!

@ -124,10 +124,10 @@ lemma rep_mapIso (e : X ≃ Y) (h : cX = cY ∘ e) (g : G) :

@[simp]
 lemma rep_mapIso_apply (e : X ≃ Y) (h : cX = cY ∘ e) (g : G) (x : 𝓣.Tensor cX) :
-    g • (𝓣.mapIso e h x) = (𝓣.mapIso e h) (g • x) := by
+    (𝓣.mapIso e h) (g • x) = g • (𝓣.mapIso e h x) := by
  trans ((𝓣.rep g) ∘ₗ (𝓣.mapIso e h).toLinearMap) x
-  rfl
  simp
+  rfl

@[simp]
 lemma rep_tprod (g : G) (f : (i : X) → 𝓣.ColorModule (cX i)) :
@ -170,54 +170,37 @@ lemma rep_tensoratorEquiv_tmul (g : G) (x : 𝓣.Tensor cX) (y : 𝓣.Tensor cY)
  nth_rewrite 1 [← rep_tensoratorEquiv_apply]
  rfl

-/-!
-
-## Group acting on contraction
-
-/
+lemma rep_tensoratorEquiv_symm (g : G) :
+    (𝓣.tensoratorEquiv cX cY).symm ∘ₗ 𝓣.rep g = (TensorProduct.map (𝓣.rep g) (𝓣.rep 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)

@[simp]
-lemma contrAll_rep {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = 𝓣.τ ∘ d ∘ e) (g : G) :
-    𝓣.contrAll e h ∘ₗ (TensorProduct.map (𝓣.rep g) (𝓣.rep g)) = 𝓣.contrAll e h := by
-  apply TensorProduct.ext'
-  refine fun x ↦ PiTensorProduct.induction_on' x ?_ (by
-      intro a b hx hy y
-      simp [map_add, add_tmul, hx, hy])
-  intro rx fx
-  refine fun y ↦ PiTensorProduct.induction_on' y ?_ (by
-      intro a b hx hy
-      simp at hx hy
-      simp [map_add, tmul_add, hx, hy])
-  intro ry fy
-  simp [contrAll, TensorProduct.smul_tmul]
-  apply congrArg
-  apply congrArg
-  simp [contrAll']
-  apply congrArg
-  simp [pairProd]
-  change (PiTensorProduct.map _) ((PiTensorProduct.map₂ _ _) _) =
-    (PiTensorProduct.map _) ((PiTensorProduct.map₂ _ _) _)
-  rw [PiTensorProduct.map₂_tprod_tprod, PiTensorProduct.map₂_tprod_tprod, PiTensorProduct.map_tprod,
-  PiTensorProduct.map_tprod]
-  simp only [mk_apply]
-  apply congrArg
-  funext x
-  rw [← repColorModule_colorModuleCast_apply]
-  nth_rewrite 2 [← contrDual_inv (c x) g]
+lemma rep_tensoratorEquiv_symm_apply (g : G) (x : 𝓣.Tensor (Sum.elim cX cY)) :
+    (𝓣.tensoratorEquiv cX cY).symm ((𝓣.rep g) x) =
+    (TensorProduct.map (𝓣.rep g) (𝓣.rep g)) ((𝓣.tensoratorEquiv cX cY).symm x) := by
+  trans ((𝓣.tensoratorEquiv cX cY).symm ∘ₗ 𝓣.rep g) x
+  rfl
+  rw [rep_tensoratorEquiv_symm]
  rfl

@[simp]
-lemma contrAll_rep_apply {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = 𝓣.τ ∘ d ∘ e)
-    (g : G) (x : 𝓣.Tensor c ⊗ 𝓣.Tensor d) :
-    𝓣.contrAll e h (TensorProduct.map (𝓣.rep g) (𝓣.rep g) x) = 𝓣.contrAll e h x := by
-  change (𝓣.contrAll e h ∘ₗ (TensorProduct.map (𝓣.rep g) (𝓣.rep g))) x = _
-  rw [contrAll_rep]
+lemma rep_lid (g : G) : TensorProduct.lid R (𝓣.Tensor cX) ∘ₗ
+    (TensorProduct.map (LinearMap.id) (𝓣.rep g)) = (𝓣.rep g) ∘ₗ
+    (TensorProduct.lid R (𝓣.Tensor cX)).toLinearMap := by
+  apply TensorProduct.ext'
+  intro r y
+  simp

@[simp]
-lemma contrAll_rep_tmul {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = 𝓣.τ ∘ d ∘ e)
-    (g : G) (x : 𝓣.Tensor c) (y : 𝓣.Tensor d) :
-    𝓣.contrAll e h ((g • x) ⊗ₜ[R] (g • y)) = 𝓣.contrAll e h (x ⊗ₜ[R] y) := by
-  nth_rewrite 2 [← @contrAll_rep_apply R _ G]
+lemma rep_lid_apply (g : G) (x : R ⊗[R] 𝓣.Tensor cX) :
+    (TensorProduct.lid R (𝓣.Tensor cX)) ((TensorProduct.map (LinearMap.id) (𝓣.rep g)) x) =
+    (𝓣.rep g) ((TensorProduct.lid R (𝓣.Tensor cX)).toLinearMap x) := by
+  trans ((TensorProduct.lid R (𝓣.Tensor cX)) ∘ₗ (TensorProduct.map (LinearMap.id) (𝓣.rep g))) x
+  rfl
+  rw [rep_lid]
  rfl

 end TensorStructure
--- a/HepLean/SpaceTime/LorentzTensor/Notation.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Notation.lean
@ -27,4 +27,7 @@ Further we plan to make easy to define tensors with indices. E.g. `(ψ : Tenᵘ
  For `(ψ : Tenᵘ¹ᵘ²ᵤ₃)`, if one writes e.g. `ψᵤ₁ᵘ²ᵤ₃`, this should correspond to a
  lowering of the first index of `ψ`.

+Further, it will be nice if we can have implicit contractions of indices
+  e.g. in Weyl fermions.
+
 -/
--- a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
@ -75,10 +75,10 @@ def realLorentzTensor (d : ℕ) : TensorStructure ℝ where
    match μ with
    | .up => LorentzVector.unitUp
    | .down => LorentzVector.unitDown
-  unit_lid μ :=
+  unit_rid μ :=
    match μ with
-    | .up => LorentzVector.unitUp_lid
-    | .down => LorentzVector.unitDown_lid
+    | .up => LorentzVector.unitUp_rid
+    | .down => LorentzVector.unitDown_rid
  metric μ :=
    match μ with
    | realTensor.ColorType.up => asProdLorentzVector
--- a/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean
+++ b/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean
@ -0,0 +1,174 @@
+/-
+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
+/-!
+
+# Rising and Lowering of indices
+
+We use the term `dualize` to describe the more general version of rising and lowering of indices.
+
+In particular, rising and lowering indices corresponds taking the color of that index
+to its dual.
+
+-/
+
+noncomputable section
+
+open TensorProduct
+
+variable {R : Type} [CommSemiring R]
+
+namespace TensorStructure
+
+variable (𝓣 : TensorStructure R)
+
+variable {d : ℕ} {X Y Y' Z W C P : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
+  [Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z] [Fintype W] [DecidableEq W]
+  [Fintype C] [DecidableEq C] [Fintype P] [DecidableEq P]
+  {cX cX2 : X → 𝓣.Color} {cY : Y → 𝓣.Color} {cZ : Z → 𝓣.Color}
+  {cW : W → 𝓣.Color} {cY' : Y' → 𝓣.Color} {μ ν: 𝓣.Color}
+
+/-!
+
+## Properties of the unit
+
+-/
+
+/-! TODO: Move -/
+
+lemma unit_lhs_eq (x : 𝓣.ColorModule μ) (y : 𝓣.ColorModule (𝓣.τ μ) ⊗[R] 𝓣.ColorModule μ) :
+    contrLeftAux (𝓣.contrDual μ) (x ⊗ₜ[R] y) =
+    (contrRightAux (𝓣.contrDual (𝓣.τ μ))) ((TensorProduct.comm R _ _) y
+    ⊗ₜ[R] (𝓣.colorModuleCast (𝓣.τ_involutive μ).symm) x) := by
+  refine TensorProduct.induction_on y (by simp) ?_ (fun z1 z2 h1 h2 => ?_)
+  intro x1 x2
+  simp only [contrRightAux, LinearEquiv.refl_toLinearMap, comm_tmul, colorModuleCast,
+    Equiv.cast_symm, LinearEquiv.coe_mk, Equiv.cast_apply, LinearMap.coe_comp, LinearEquiv.coe_coe,
+    Function.comp_apply, assoc_tmul, map_tmul, LinearMap.id_coe, id_eq, contrDual_symm', cast_cast,
+    cast_eq, rid_tmul]
+  rfl
+  simp [LinearMap.map_add, add_tmul]
+  rw [← h1, ← h2, tmul_add, LinearMap.map_add]
+
+@[simp]
+lemma unit_lid : (contrRightAux (𝓣.contrDual (𝓣.τ μ))) ((TensorProduct.comm R _ _) (𝓣.unit μ)
+    ⊗ₜ[R] (𝓣.colorModuleCast (𝓣.τ_involutive μ).symm) x) = x := by
+  have h1 := 𝓣.unit_rid μ x
+  rw [← unit_lhs_eq]
+  exact h1
+
+/-!
+
+## Properties of the metric
+
+-/
+
+@[simp]
+lemma metric_cast (h : μ = ν) :
+    (TensorProduct.congr (𝓣.colorModuleCast h) (𝓣.colorModuleCast h)) (𝓣.metric μ) =
+    𝓣.metric ν := by
+  subst h
+  erw [congr_refl_refl]
+  simp only [LinearEquiv.refl_apply]
+
+@[simp]
+lemma metric_contrRight_unit (μ : 𝓣.Color) (x : 𝓣.ColorModule μ) :
+    (contrRightAux (𝓣.contrDual μ)) (𝓣.metric μ ⊗ₜ[R]
+    ((contrRightAux (𝓣.contrDual (𝓣.τ μ)))
+      (𝓣.metric (𝓣.τ μ) ⊗ₜ[R] (𝓣.colorModuleCast (𝓣.τ_involutive μ).symm x)))) = x := by
+  change (contrRightAux (𝓣.contrDual μ) ∘ₗ TensorProduct.map (LinearMap.id)
+      (contrRightAux (𝓣.contrDual (𝓣.τ μ)))) (𝓣.metric μ
+      ⊗ₜ[R] 𝓣.metric (𝓣.τ μ) ⊗ₜ[R] (𝓣.colorModuleCast (𝓣.τ_involutive μ).symm x)) = _
+  rw [contrRightAux_comp]
+  simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, assoc_symm_tmul,
+    map_tmul, LinearMap.id_coe, id_eq]
+  rw [𝓣.metric_dual]
+  simp only [unit_lid]
+
+/-!
+
+## Dualizing
+
+-/
+
+/-- Takes a vector with index with dual color to a vector with index the underlying color.
+  Obtained by contraction with the metric. -/
+def dualizeSymm (μ : 𝓣.Color) : 𝓣.ColorModule (𝓣.τ μ) →ₗ[R] 𝓣.ColorModule μ :=
+  contrRightAux (𝓣.contrDual μ) ∘ₗ
+    TensorProduct.lTensorHomToHomLTensor R _ _ _ (𝓣.metric μ ⊗ₜ[R] LinearMap.id)
+
+/-- Takes a vector to a vector with the dual color index.
+  Obtained by contraction with the metric. -/
+def dualizeFun (μ : 𝓣.Color) : 𝓣.ColorModule μ →ₗ[R] 𝓣.ColorModule (𝓣.τ μ) :=
+  𝓣.dualizeSymm (𝓣.τ μ) ∘ₗ (𝓣.colorModuleCast (𝓣.τ_involutive μ).symm).toLinearMap
+
+/-- Equivalence between the module with a color `μ` and the module with color
+  `𝓣.τ μ` obtained by contraction with the metric. -/
+def dualizeModule (μ : 𝓣.Color) : 𝓣.ColorModule μ ≃ₗ[R] 𝓣.ColorModule (𝓣.τ μ) := by
+  refine LinearEquiv.ofLinear (𝓣.dualizeFun μ) (𝓣.dualizeSymm μ) ?_ ?_
+  · apply LinearMap.ext
+    intro x
+    simp [dualizeFun, dualizeSymm, LinearMap.coe_comp, LinearEquiv.coe_coe,
+      Function.comp_apply, lTensorHomToHomLTensor_apply, LinearMap.id_coe, id_eq,
+      contrDual_symm_contrRightAux_apply_tmul, metric_cast]
+  · apply LinearMap.ext
+    intro x
+    simp only [dualizeSymm, dualizeFun, LinearMap.coe_comp, LinearEquiv.coe_coe,
+      Function.comp_apply, lTensorHomToHomLTensor_apply, LinearMap.id_coe, id_eq,
+      metric_contrRight_unit]
+
+/-- 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
+    (PiTensorProduct.map (fun x => (𝓣.dualizeModule (cX x)).toLinearMap))
+    (PiTensorProduct.map (fun x => (𝓣.dualizeModule (cX x)).symm.toLinearMap)) ?_ ?_
+  all_goals
+    apply LinearMap.ext
+    refine fun x ↦ 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 [Function.comp_apply, PiTensorProduct.tprodCoeff_eq_smul_tprod,
+      LinearMapClass.map_smul, LinearMap.coe_comp, LinearMap.id_coe, id_eq]
+    apply congrArg
+    change (PiTensorProduct.map _)
+      ((PiTensorProduct.map _) ((PiTensorProduct.tprod R) fx)) = _
+    rw [PiTensorProduct.map_tprod, PiTensorProduct.map_tprod]
+    apply congrArg
+    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]
+  funext x
+  match x with
+  | Sum.inl x => rfl
+  | Sum.inr x => rfl
+
+lemma dualize_cond' (e : C ⊕ P ≃ X) :
+    Sum.elim (𝓣.τ ∘ cX ∘ ⇑e ∘ Sum.inl) (cX ∘ ⇑e ∘ Sum.inr) =
+    (Sum.elim (𝓣.τ ∘ cX ∘ ⇑e ∘ Sum.inl) (cX ∘ ⇑e ∘ Sum.inr) ∘ ⇑e.symm) ∘ ⇑e := by
+  funext x
+  match x with
+  | Sum.inl x => simp
+  | Sum.inr x => simp
+
+/-! TODO: Show that `dualize` is equivariant with respect to the group action. -/
+
+/-- Given an equivalence `C ⊕ P ≃ X` dualizes those indices of a tensor which correspond to
+  `C` whilst leaving the indices `P` invariant. -/
+def dualize (e : C ⊕ P ≃ X) : 𝓣.Tensor cX ≃ₗ[R]
+    𝓣.Tensor (Sum.elim (𝓣.τ ∘ cX ∘ e ∘ Sum.inl) (cX ∘ e ∘ Sum.inr) ∘ e.symm) :=
+  𝓣.mapIso e.symm (𝓣.dualize_cond e) ≪≫ₗ
+  (𝓣.tensoratorEquiv _ _).symm ≪≫ₗ
+  TensorProduct.congr 𝓣.dualizeAll (LinearEquiv.refl _ _) ≪≫ₗ
+  (𝓣.tensoratorEquiv _ _) ≪≫ₗ
+  𝓣.mapIso e (𝓣.dualize_cond' e)
+
+end TensorStructure
+
+end
--- a/HepLean/SpaceTime/LorentzVector/Contraction.lean
+++ b/HepLean/SpaceTime/LorentzVector/Contraction.lean
@ -115,37 +115,32 @@ lemma contrDownUp_tmul_eq_dotProduct {x : CovariantLorentzVector d} {y : Lorentz

 /-- The unit of the contraction of contravariant Lorentz vector and a
  covariant Lorentz vector. -/
-def unitUp : LorentzVector d ⊗[ℝ] CovariantLorentzVector d :=
-  ∑ i, LorentzVector.stdBasis i ⊗ₜ[ℝ] CovariantLorentzVector.stdBasis i
+def unitUp : CovariantLorentzVector d ⊗[ℝ] LorentzVector d :=
+  ∑ i, CovariantLorentzVector.stdBasis i ⊗ₜ[ℝ] LorentzVector.stdBasis i

-lemma unitUp_lid (x : LorentzVector d) :
-    TensorProduct.rid ℝ _
-    (TensorProduct.map (LinearEquiv.refl ℝ _).toLinearMap
-    (contrUpDown ∘ₗ (TensorProduct.comm ℝ _ _).toLinearMap)
-    ((TensorProduct.assoc ℝ _ _ _) (unitUp ⊗ₜ[ℝ] x))) = x := by
-  simp only [LinearEquiv.refl_toLinearMap, unitUp]
-  rw [sum_tmul]
-  simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
-    Finset.sum_singleton, map_add, assoc_tmul, map_sum, map_tmul, LinearMap.id_coe, id_eq,
-    LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, comm_tmul,
-    contrUpDown_stdBasis_left, rid_tmul, decomp_stdBasis']
+lemma unitUp_rid (x : LorentzVector d) :
+    TensorStructure.contrLeftAux contrUpDown (x ⊗ₜ[ℝ] unitUp) = x := by
+  simp only [unitUp, LinearEquiv.refl_toLinearMap]
+  rw [tmul_sum]
+  simp only [TensorStructure.contrLeftAux, LinearEquiv.refl_toLinearMap, Fintype.sum_sum_type,
+    Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, Finset.sum_singleton, map_add,
+    LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, assoc_symm_tmul, map_tmul,
+    contrUpDown_stdBasis_left, LinearMap.id_coe, id_eq, lid_tmul, map_sum, decomp_stdBasis']

 /-- The unit of the contraction of covariant Lorentz vector and a
  contravariant Lorentz vector. -/
-def unitDown : CovariantLorentzVector d ⊗[ℝ] LorentzVector d :=
-  ∑ i, CovariantLorentzVector.stdBasis i ⊗ₜ[ℝ] LorentzVector.stdBasis i
+def unitDown : LorentzVector d ⊗[ℝ] CovariantLorentzVector d :=
+  ∑ i, LorentzVector.stdBasis i ⊗ₜ[ℝ] CovariantLorentzVector.stdBasis i

-lemma unitDown_lid (x : CovariantLorentzVector d) :
-    TensorProduct.rid ℝ _
-    (TensorProduct.map (LinearEquiv.refl ℝ _).toLinearMap
-    (contrDownUp ∘ₗ (TensorProduct.comm ℝ _ _).toLinearMap)
-    ((TensorProduct.assoc ℝ _ _ _) (unitDown ⊗ₜ[ℝ] x))) = x := by
-  simp only [LinearEquiv.refl_toLinearMap, unitDown]
-  rw [sum_tmul]
-  simp only [contrDownUp, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero,
-    Fin.isValue, Finset.sum_singleton, map_add, assoc_tmul, map_sum, map_tmul, LinearMap.id_coe,
-    id_eq, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, comm_tmul,
-    contrUpDown_stdBasis_right, rid_tmul, CovariantLorentzVector.decomp_stdBasis']
+lemma unitDown_rid (x : CovariantLorentzVector d) :
+    TensorStructure.contrLeftAux contrDownUp (x ⊗ₜ[ℝ] unitDown) = x := by
+  simp only [unitDown, LinearEquiv.refl_toLinearMap]
+  rw [tmul_sum]
+  simp only [TensorStructure.contrLeftAux, contrDownUp, LinearEquiv.refl_toLinearMap,
+    Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+    Finset.sum_singleton, map_add, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
+    assoc_symm_tmul, map_tmul, comm_tmul, contrUpDown_stdBasis_right, LinearMap.id_coe, id_eq,
+    lid_tmul, map_sum, CovariantLorentzVector.decomp_stdBasis']

 /-!

@ -175,6 +170,7 @@ end LorentzVector

 namespace minkowskiMatrix
 open LorentzVector
+open TensorStructure
 open scoped minkowskiMatrix
 variable {d : ℕ}

@ -188,37 +184,39 @@ def asProdCovariantLorentzVector : CovariantLorentzVector d ⊗[ℝ] CovariantLo

@[simp]
 lemma contrLeft_asProdLorentzVector (x : CovariantLorentzVector d) :
-    contrDualLeftAux contrDownUp (x ⊗ₜ[ℝ] asProdLorentzVector) =
+    contrLeftAux contrDownUp (x ⊗ₜ[ℝ] asProdLorentzVector) =
    ∑ μ, ((η μ μ * x μ) • LorentzVector.stdBasis μ) := by
  simp only [asProdLorentzVector]
  rw [tmul_sum]
  rw [map_sum]
  refine Finset.sum_congr rfl (fun μ _ => ?_)
-  simp only [contrDualLeftAux, contrDownUp, LinearEquiv.refl_toLinearMap, tmul_smul, map_smul,
+  simp only [contrLeftAux, contrDownUp, LinearEquiv.refl_toLinearMap, tmul_smul, map_smul,
    LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, assoc_symm_tmul, map_tmul,
    comm_tmul, contrUpDown_stdBasis_right, LinearMap.id_coe, id_eq, lid_tmul]
  exact smul_smul (η μ μ) (x μ) (e μ)

@[simp]
 lemma contrLeft_asProdCovariantLorentzVector (x : LorentzVector d) :
-    contrDualLeftAux contrUpDown (x ⊗ₜ[ℝ] asProdCovariantLorentzVector) =
+    contrLeftAux contrUpDown (x ⊗ₜ[ℝ] asProdCovariantLorentzVector) =
    ∑ μ, ((η μ μ * x μ) • CovariantLorentzVector.stdBasis μ) := by
  simp only [asProdCovariantLorentzVector]
  rw [tmul_sum]
  rw [map_sum]
  refine Finset.sum_congr rfl (fun μ _ => ?_)
-  simp only [contrDualLeftAux, LinearEquiv.refl_toLinearMap, tmul_smul, LinearMapClass.map_smul,
+  simp only [contrLeftAux, LinearEquiv.refl_toLinearMap, tmul_smul, LinearMapClass.map_smul,
    LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, assoc_symm_tmul, map_tmul,
    contrUpDown_stdBasis_left, LinearMap.id_coe, id_eq, lid_tmul]
  exact smul_smul (η μ μ) (x μ) (CovariantLorentzVector.stdBasis μ)

@[simp]
 lemma asProdLorentzVector_contr_asCovariantProdLorentzVector :
-    (contrDualMidAux (contrUpDown) (asProdLorentzVector ⊗ₜ[ℝ] asProdCovariantLorentzVector))
-    = @unitUp d := by
-  simp only [contrDualMidAux, LinearEquiv.refl_toLinearMap, asProdLorentzVector, LinearMap.coe_comp,
+    (contrMidAux (contrUpDown) (asProdLorentzVector ⊗ₜ[ℝ] asProdCovariantLorentzVector))
+    = TensorProduct.comm ℝ _ _ (@unitUp d) := by
+  simp only [contrMidAux, LinearEquiv.refl_toLinearMap, asProdLorentzVector, 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]
@ -239,11 +237,13 @@ lemma asProdLorentzVector_contr_asCovariantProdLorentzVector :

@[simp]
 lemma asProdCovariantLorentzVector_contr_asProdLorentzVector :
-    (contrDualMidAux (contrDownUp) (asProdCovariantLorentzVector ⊗ₜ[ℝ] asProdLorentzVector))
-    = @unitDown d := by
-  simp only [contrDualMidAux, LinearEquiv.refl_toLinearMap, asProdCovariantLorentzVector,
+    (contrMidAux (contrDownUp) (asProdCovariantLorentzVector ⊗ₜ[ℝ] asProdLorentzVector))
+    = TensorProduct.comm ℝ _ _ (@unitDown d) := by
+  simp only [contrMidAux, LinearEquiv.refl_toLinearMap, asProdCovariantLorentzVector,
    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,
+    Finset.sum_singleton, map_add, comm_tmul, map_sum]
  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,