From 7648f25d73d3cd871d15672bcda205bc84f31765 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 15 Jul 2024 16:57:06 -0400
Subject: [PATCH 1/9] refactor: Move LorentzTensor

---
 .../LorentzTensor/{ => Real}/Basic.lean       | 29 ++++---------------
 .../LorentzTensor/Real/LorentzAction.lean     | 18 ++++++++++++
 2 files changed, 24 insertions(+), 23 deletions(-)
 rename HepLean/SpaceTime/LorentzTensor/{ => Real}/Basic.lean (95%)
 create mode 100644 HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean

diff --git a/HepLean/SpaceTime/LorentzTensor/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
similarity index 95%
rename from HepLean/SpaceTime/LorentzTensor/Basic.lean
rename to HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
index fee2c0a..e67832e 100644
--- a/HepLean/SpaceTime/LorentzTensor/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
@@ -9,7 +9,7 @@ import Mathlib.Analysis.Normed.Field.Basic
 import Mathlib.LinearAlgebra.Matrix.Trace
 /-!
 
-# Lorentz Tensors
+# Real Lorentz Tensors
 
 In this file we define real Lorentz tensors.
 
@@ -23,11 +23,6 @@ This will relation should be made explicit in the future.
 -/
 /-! TODO: Do complex tensors, with Van der Waerden notation for fermions. -/
 /-! TODO: Generalize to maps into Lorentz tensors. -/
-/-!
-
-## Real Lorentz tensors
-
--/
 
 /-- The possible `colors` of an index for a RealLorentzTensor.
  There are two possiblities, `up` and `down`. -/
@@ -348,23 +343,11 @@ def twoMarkedIndexValue (T : Marked d X 2) (x : ColorsIndex d (T.color (markedPo
 
 /-- An equivalence of types used to turn the first marked index into an unmarked index. -/
 def unmarkFirstSet (X : Type) (n : ℕ) : (X ⊕ Σ _ : Fin n.succ, PUnit) ≃
-    ((X ⊕ PUnit) ⊕ Σ _ : Fin n, PUnit) where
-  toFun x := match x with
-    | Sum.inl x => Sum.inl (Sum.inl x)
-    | Sum.inr ⟨0, PUnit.unit⟩ => Sum.inl (Sum.inr PUnit.unit)
-    | Sum.inr ⟨⟨Nat.succ i, h⟩, PUnit.unit⟩ => Sum.inr ⟨⟨i, Nat.succ_lt_succ_iff.mp h⟩, PUnit.unit⟩
-  invFun x := match x with
-    | Sum.inl (Sum.inl x) => Sum.inl x
-    | Sum.inl (Sum.inr PUnit.unit) => Sum.inr ⟨0, PUnit.unit⟩
-    | Sum.inr ⟨⟨i, h⟩, PUnit.unit⟩ => Sum.inr ⟨⟨Nat.succ i, Nat.succ_lt_succ h⟩, PUnit.unit⟩
-  left_inv x := by match x with
-    | Sum.inl x => rfl
-    | Sum.inr ⟨0, PUnit.unit⟩ => rfl
-    | Sum.inr ⟨⟨Nat.succ i, h⟩, PUnit.unit⟩ => rfl
-  right_inv x := by match x with
-    | Sum.inl (Sum.inl x) => rfl
-    | Sum.inl (Sum.inr PUnit.unit) => rfl
-    | Sum.inr ⟨⟨i, h⟩, PUnit.unit⟩ => rfl
+    (X ⊕ PUnit) ⊕ Σ _ : Fin n, PUnit :=
+  trans (Equiv.sumCongr (Equiv.refl _) $ (Equiv.sigmaPUnit (Fin n.succ)).trans
+  (((Fin.castOrderIso (Nat.succ_eq_one_add n)).toEquiv.trans finSumFinEquiv.symm).trans
+  (Equiv.sumCongr finOneEquiv (Equiv.sigmaPUnit (Fin n)).symm)))
+  (Equiv.sumAssoc _ _ _).symm
 
 /-- Unmark the first marked index of a marked thensor. -/
 def unmarkFirst {X : Type} : Marked d X n.succ ≃ Marked d (X ⊕ PUnit) n :=
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
new file mode 100644
index 0000000..e320251
--- /dev/null
+++ b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
@@ -0,0 +1,18 @@
+/-
+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.Real.Basic
+/-!
+
+# Lorentz group action on Real Lorentz Tensors
+
+We define the action of the Lorentz group on Real Lorentz Tensors.
+
+This file is currently a stub.
+-/
+
+namespace RealLorentzTensor
+
+end RealLorentzTensor

From 05e1dda58c86406fefdce98a70eea0a371e5f4c6 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 16 Jul 2024 09:45:03 -0400
Subject: [PATCH 2/9] feat: add action on Lorentz group

---
 .../SpaceTime/LorentzTensor/Real/Basic.lean   |   5 +
 .../LorentzTensor/Real/LorentzAction.lean     | 136 +++++++++++++++++-
 2 files changed, 140 insertions(+), 1 deletion(-)

diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
index e67832e..b9f01e3 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
@@ -41,6 +41,11 @@ instance (d : ℕ) (μ : RealLorentzTensor.Colors) : Fintype (RealLorentzTensor.
   | RealLorentzTensor.Colors.up => instFintypeSum (Fin 1) (Fin d)
   | RealLorentzTensor.Colors.down => instFintypeSum (Fin 1) (Fin d)
 
+instance (d : ℕ) (μ : RealLorentzTensor.Colors) : DecidableEq (RealLorentzTensor.ColorsIndex d μ) :=
+  match μ with
+  | RealLorentzTensor.Colors.up => instDecidableEqSum
+  | RealLorentzTensor.Colors.down => instDecidableEqSum
+
 /-- An `IndexValue` is a set of actual values an index can take. e.g. for a
   3-tensor (0, 1, 2). -/
 @[simp]
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
index e320251..3e34ca0 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
@@ -4,15 +4,149 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.LorentzTensor.Real.Basic
+import HepLean.SpaceTime.LorentzGroup.Basic
 /-!
 
 # Lorentz group action on Real Lorentz Tensors
 
 We define the action of the Lorentz group on Real Lorentz Tensors.
 
-This file is currently a stub.
+The Lorentz action is currently only defined for finite and decidable types `X`.
+
 -/
 
 namespace RealLorentzTensor
 
+variable {d : ℕ} {X : Type} [Fintype X] [DecidableEq X] (T : RealLorentzTensor d X) (c : X → Colors)
+variable (Λ Λ' : LorentzGroup d)
+open LorentzGroup
+open BigOperators
+
+instance : Fintype (IndexValue d c) := Pi.fintype
+variable {μ : Colors}
+
+/-- Monoid homomorphism from the Lorentz group to matrices indexed by `ColorsIndex d μ` for a
+  color `μ`.
+
+  Thought of as the representation of the Lorentz group for that color index. -/
+def colorMatrix (μ : Colors) : LorentzGroup d →* Matrix (ColorsIndex d μ) (ColorsIndex d μ) ℝ where
+  toFun Λ := match μ with
+    | .up => fun i j => Λ.1 i j
+    | .down => fun i j => (LorentzGroup.transpose Λ⁻¹).1 i j
+  map_one' := by
+    match μ with
+    | .up =>
+        simp only [lorentzGroupIsGroup_one_coe]
+        ext i j
+        simp only [OfNat.ofNat, One.one, ColorsIndex]
+        congr
+    | .down =>
+        simp only [transpose, inv_one, lorentzGroupIsGroup_one_coe, Matrix.transpose_one]
+        ext i j
+        simp only [OfNat.ofNat, One.one, ColorsIndex]
+        congr
+  map_mul' Λ Λ' := by
+    match μ with
+    | .up =>
+        ext i j
+        simp only [lorentzGroupIsGroup_mul_coe]
+    | .down =>
+        ext i j
+        simp only [transpose, mul_inv_rev, lorentzGroupIsGroup_inv, lorentzGroupIsGroup_mul_coe,
+          Matrix.transpose_mul, Matrix.transpose_apply]
+        rfl
+
+/-- A real number which occurs in the definition of -/
+@[simp]
+def prodColorMatrixOnIndexValue (i j : IndexValue d c) : ℝ :=
+  ∏ x, colorMatrix (c x) Λ (i x) (j x)
+
+lemma one_prodColorMatrixOnIndexValue_on_diag (i : IndexValue d c) :
+  prodColorMatrixOnIndexValue c 1 i i = 1 := by
+  simp only [prodColorMatrixOnIndexValue]
+  rw [Finset.prod_eq_one]
+  intro x _
+  simp only [colorMatrix, MonoidHom.map_one, Matrix.one_apply]
+  rfl
+
+lemma one_prodColorMatrixOnIndexValue_off_diag {i j : IndexValue d c} (hij : j ≠ i) :
+  prodColorMatrixOnIndexValue c 1 i j = 0 := by
+  simp only [prodColorMatrixOnIndexValue]
+  obtain ⟨x, hijx⟩ := Function.ne_iff.mp hij
+  rw [@Finset.prod_eq_zero _ _ _ _ _ x]
+  exact Finset.mem_univ x
+  simp only [map_one]
+  exact Matrix.one_apply_ne' hijx
+
+lemma mul_prodColorMatrixOnIndexValue (i j : IndexValue d c) :
+    prodColorMatrixOnIndexValue c (Λ * Λ') i j =
+    ∑ (k : IndexValue d c),
+    ∏ x, (colorMatrix (c x) Λ (i x) (k x)) * (colorMatrix (c x) Λ' (k x) (j x)) := by
+  have h1 :  ∑ (k : IndexValue d c), ∏ x,
+      (colorMatrix (c x) Λ (i x) (k x)) * (colorMatrix (c x) Λ' (k x) (j x))  =
+      ∏ x, ∑ y, (colorMatrix (c x) Λ (i x) y) * (colorMatrix (c x) Λ' y (j x)) := by
+    rw [Finset.prod_sum]
+    simp only [Finset.prod_attach_univ, Finset.sum_univ_pi]
+    apply Finset.sum_congr
+    simp only [IndexValue, Fintype.piFinset_univ]
+    intro x _
+    rfl
+  rw [h1]
+  simp only [prodColorMatrixOnIndexValue, map_mul]
+  exact Finset.prod_congr rfl (fun x _ => rfl)
+
+/-- Action of the Lorentz group on the set of Real Lorentz Tensors indexed by `X`. -/
+def lorentzAction : MulAction (LorentzGroup d) (RealLorentzTensor d X) where
+  smul Λ T := {color := T.color,
+                coord := fun i => ∑ j, prodColorMatrixOnIndexValue T.color Λ i j * T.coord j}
+  one_smul T := by
+    refine ext' rfl ?_
+    funext i
+    simp only [HSMul.hSMul, map_one]
+    erw [Finset.sum_eq_single_of_mem i]
+    rw [one_prodColorMatrixOnIndexValue_on_diag]
+    simp only [one_mul, IndexValue]
+    rfl
+    exact Finset.mem_univ i
+    intro j _ hij
+    rw [one_prodColorMatrixOnIndexValue_off_diag]
+    simp only [zero_mul]
+    exact hij
+  mul_smul Λ Λ' T := by
+    refine ext' rfl ?_
+    simp only [HSMul.hSMul]
+    funext i
+    have h1 : ∑ j : IndexValue d T.color, prodColorMatrixOnIndexValue T.color (Λ * Λ') i j
+        * T.coord j = ∑ j : IndexValue d T.color, ∑ (k : IndexValue d T.color),
+        (∏ x, ((colorMatrix (T.color x) Λ (i x) (k x)) *
+        (colorMatrix (T.color x) Λ' (k x) (j x)))) * T.coord j := by
+      refine Finset.sum_congr rfl (fun j _ => ?_)
+      rw [mul_prodColorMatrixOnIndexValue, Finset.sum_mul]
+    rw [h1]
+    rw [Finset.sum_comm]
+    refine Finset.sum_congr rfl (fun j _ => ?_)
+    rw [Finset.mul_sum]
+    refine Finset.sum_congr rfl (fun k _ => ?_)
+    simp only [prodColorMatrixOnIndexValue, IndexValue]
+    rw [← mul_assoc]
+    congr
+    rw [Finset.prod_mul_distrib]
+    rfl
+
+/-!
+
+## The Lorentz action on constructors
+
+-/
+
+
+
+
+
+
+
+
+
+
+
 end RealLorentzTensor

From 9c77e18a701cdee9dba8067981a4cdd6b3561794 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 16 Jul 2024 11:40:00 -0400
Subject: [PATCH 3/9] refactor: Move constructors

---
 HepLean.lean                                  |   4 +-
 .../StandardParameterization/Basic.lean       |   2 +-
 .../SpaceTime/LorentzTensor/Real/Basic.lean   | 144 -------
 .../LorentzTensor/Real/Constructors.lean      | 403 ++++++++++++++++++
 .../LorentzTensor/Real/LorentzAction.lean     |  36 +-
 scripts/nolints.json                          |   1 +
 6 files changed, 421 insertions(+), 169 deletions(-)
 create mode 100644 HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
 create mode 100644 scripts/nolints.json

diff --git a/HepLean.lean b/HepLean.lean
index f0338a0..db49ab9 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -70,7 +70,9 @@ import HepLean.SpaceTime.LorentzGroup.Orthochronous
 import HepLean.SpaceTime.LorentzGroup.Proper
 import HepLean.SpaceTime.LorentzGroup.Restricted
 import HepLean.SpaceTime.LorentzGroup.Rotations
-import HepLean.SpaceTime.LorentzTensor.Basic
+import HepLean.SpaceTime.LorentzTensor.Real.Basic
+import HepLean.SpaceTime.LorentzTensor.Real.Constructors
+import HepLean.SpaceTime.LorentzTensor.Real.LorentzAction
 import HepLean.SpaceTime.LorentzVector.AsSelfAdjointMatrix
 import HepLean.SpaceTime.LorentzVector.Basic
 import HepLean.SpaceTime.LorentzVector.NormOne
diff --git a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
index 417371e..6166812 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
@@ -96,7 +96,7 @@ lemma standParamAsMatrix_unitary (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) :
     rw [sin_sq, sin_sq]
     ring
 
-/-- A CKM Matrix from four reals `θ₁₂`, `θ₁₃`, `θ₂₃`,  and `δ₁₃`. This is the standard
+/-- A CKM Matrix from four reals `θ₁₂`, `θ₁₃`, `θ₂₃`, and `δ₁₃`. This is the standard
   parameterization of CKM matrices. -/
 def standParam (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : CKMMatrix :=
   ⟨standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃, by
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
index b9f01e3..a65ef70 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
@@ -6,7 +6,6 @@ Authors: Joseph Tooby-Smith
 import Mathlib.Logic.Function.CompTypeclasses
 import Mathlib.Data.Real.Basic
 import Mathlib.Analysis.Normed.Field.Basic
-import Mathlib.LinearAlgebra.Matrix.Trace
 /-!
 
 # Real Lorentz Tensors
@@ -423,141 +422,6 @@ def contr {X : Type} (T : Marked d X 2)
 
 /-!
 
-# Tensors from reals, vectors and matrices
-
-Note that that these definitions are not equivariant with respect to an
-action of the Lorentz group. They are provided for constructive purposes.
-
--/
-
-/-- A 0-tensor from a real number. -/
-def ofReal (d : ℕ) (r : ℝ) : RealLorentzTensor d Empty where
-  color := fun _ => Colors.up
-  coord := fun _ => r
-
-/-- A marked 1-tensor with a single up index constructed from a vector.
-
-  Note: This is not the same as rising indices on `ofVecDown`. -/
-def ofVecUp {d : ℕ} (v : Fin 1 ⊕ Fin d → ℝ) :
-    Marked d Empty 1 where
-  color := fun _ => Colors.up
-  coord := fun i => v <| i <| Sum.inr <| ⟨0, PUnit.unit⟩
-
-/-- A marked 1-tensor with a single down index constructed from a vector.
-
-  Note: This is not the same as lowering indices on `ofVecUp`. -/
-def ofVecDown {d : ℕ} (v : Fin 1 ⊕ Fin d → ℝ) :
-    Marked d Empty 1 where
-  color := fun _ => Colors.down
-  coord := fun i => v <| i <| Sum.inr <| ⟨0, PUnit.unit⟩
-
-/-- A tensor with two up indices constructed from a matrix.
-
-Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
-def ofMatUpUp {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
-    Marked d Empty 2 where
-  color := fun _ => Colors.up
-  coord := fun i => m (i (Sum.inr ⟨0, PUnit.unit⟩)) (i (Sum.inr ⟨1, PUnit.unit⟩))
-
-/-- A tensor with two down indices constructed from a matrix.
-
-Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
-def ofMatDownDown {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
-    Marked d Empty 2 where
-  color := fun _ => Colors.down
-  coord := fun i => m (i (Sum.inr ⟨0, PUnit.unit⟩)) (i (Sum.inr ⟨1, PUnit.unit⟩))
-
-/-- A marked 2-tensor with the first index up and the second index down.
-
-Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
-@[simps!]
-def ofMatUpDown {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
-    Marked d Empty 2 where
-  color := fun i => match i with
-  | Sum.inr ⟨0, PUnit.unit⟩ => Colors.up
-  | Sum.inr ⟨1, PUnit.unit⟩ => Colors.down
-  coord := fun i => m (i (Sum.inr ⟨0, PUnit.unit⟩)) (i (Sum.inr ⟨1, PUnit.unit⟩))
-
-/-- A marked 2-tensor with the first index down and the second index up.
-
-Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
-def ofMatDownUp {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
-    Marked d Empty 2 where
-  color := fun i => match i with
-    | Sum.inr ⟨0, PUnit.unit⟩ => Colors.down
-    | Sum.inr ⟨1, PUnit.unit⟩ => Colors.up
-  coord := fun i => m (i (Sum.inr ⟨0, PUnit.unit⟩)) (i (Sum.inr ⟨1, PUnit.unit⟩))
-
-/-- Contracting the indices of `ofMatUpDown` returns the trace of the matrix. -/
-lemma contr_ofMatUpDown_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
-    contr (ofMatUpDown M) (by rfl) = ofReal d M.trace := by
-  refine ext' ?_ ?_
-  · funext i
-    exact Empty.elim i
-  · funext i
-    simp only [Fin.isValue, contr, IndexValue, Equiv.cast_apply, trace, diag_apply, ofReal,
-      Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
-    apply Finset.sum_congr rfl
-    intro x _
-    rfl
-
-/-- Contracting the indices of `ofMatDownUp` returns the trace of the matrix. -/
-lemma contr_ofMatDownUp_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
-    contr (ofMatDownUp M) (by rfl) = ofReal d M.trace := by
-  refine ext' ?_ ?_
-  · funext i
-    exact Empty.elim i
-  · funext i
-    rfl
-
-/-- Multiplying `ofVecUp` with `ofVecDown` gives the dot product. -/
-@[simp]
-lemma mul_ofVecUp_ofVecDown_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d → ℝ) :
-    congrSet (@Equiv.equivEmpty (Empty ⊕ Empty) instIsEmptySum)
-    (mul (ofVecUp v₁) (ofVecDown v₂) (by rfl)) = ofReal d (v₁ ⬝ᵥ v₂) := by
-  refine ext' ?_ ?_
-  · funext i
-    exact Empty.elim i
-  · funext i
-    rfl
-
-/-- Multiplying `ofVecDown` with `ofVecUp` gives the dot product. -/
-@[simp]
-lemma mul_ofVecDown_ofVecUp_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d → ℝ) :
-    congrSet (Equiv.equivEmpty (Empty ⊕ Empty))
-    (mul (ofVecDown v₁) (ofVecUp v₂) rfl) = ofReal d (v₁ ⬝ᵥ v₂) := by
-  refine ext' ?_ ?_
-  · funext i
-    exact Empty.elim i
-  · funext i
-    rfl
-
-lemma mul_ofMatUpDown_ofVecUp_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
-    (v : Fin 1 ⊕ Fin d → ℝ) :
-    congrSet ((Equiv.sumEmpty (Empty ⊕ PUnit.{1}) Empty).trans equivPUnitToSigma)
-    (mul (unmarkFirst $ ofMatUpDown M) (ofVecUp v) rfl) = ofVecUp (M *ᵥ v) := by
-  refine ext' ?_ ?_
-  · funext i
-    simp only [Nat.succ_eq_add_one, Nat.reduceAdd, congrSet_apply_color, mul_color, Equiv.symm_symm]
-    fin_cases i
-    rfl
-  · funext i
-    rfl
-
-lemma mul_ofMatDownUp_ofVecDown_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
-    (v : Fin 1 ⊕ Fin d → ℝ) :
-    congrSet ((Equiv.sumEmpty (Empty ⊕ PUnit.{1}) Empty).trans equivPUnitToSigma)
-    (mul (unmarkFirst $ ofMatDownUp M) (ofVecDown v) rfl) = ofVecDown (M *ᵥ v) := by
-  refine ext' ?_ ?_
-  · funext i
-    simp only [Nat.succ_eq_add_one, Nat.reduceAdd, congrSet_apply_color, mul_color, Equiv.symm_symm]
-    fin_cases i
-    rfl
-  · funext i
-    rfl
-
-/-!
-
 ## Rising and lowering indices
 
 Rising or lowering an index corresponds to changing the color of that index.
@@ -568,14 +432,6 @@ Rising or lowering an index corresponds to changing the color of that index.
 
 /-!
 
-## Action of the Lorentz group
-
--/
-
-/-! TODO: Define the action of the Lorentz group on the sets of Tensors. -/
-
-/-!
-
 ## Graphical species and Lorentz tensors
 
 -/
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean b/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
new file mode 100644
index 0000000..eb28427
--- /dev/null
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
@@ -0,0 +1,403 @@
+/-
+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.Real.Basic
+import HepLean.SpaceTime.LorentzTensor.Real.LorentzAction
+/-!
+
+# Constructors for real Lorentz tensors
+
+In this file we will constructors of real Lorentz tensors from real numbers,
+vectors and matrices.
+
+We will derive properties of these constructors.
+
+-/
+
+namespace RealLorentzTensor
+
+/-!
+
+# Tensors from reals, vectors and matrices
+
+Note that that these definitions are not equivariant with respect to an
+action of the Lorentz group. They are provided for constructive purposes.
+
+-/
+
+/-- A 0-tensor from a real number. -/
+def ofReal (d : ℕ) (r : ℝ) : RealLorentzTensor d Empty where
+  color := fun _ => Colors.up
+  coord := fun _ => r
+
+/-- A marked 1-tensor with a single up index constructed from a vector.
+
+  Note: This is not the same as rising indices on `ofVecDown`. -/
+def ofVecUp {d : ℕ} (v : Fin 1 ⊕ Fin d → ℝ) :
+    Marked d Empty 1 where
+  color := fun _ => Colors.up
+  coord := fun i => v <| i <| Sum.inr <| ⟨0, PUnit.unit⟩
+
+/-- A marked 1-tensor with a single down index constructed from a vector.
+
+  Note: This is not the same as lowering indices on `ofVecUp`. -/
+def ofVecDown {d : ℕ} (v : Fin 1 ⊕ Fin d → ℝ) :
+    Marked d Empty 1 where
+  color := fun _ => Colors.down
+  coord := fun i => v <| i <| Sum.inr <| ⟨0, PUnit.unit⟩
+
+/-- A tensor with two up indices constructed from a matrix.
+
+Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
+def ofMatUpUp {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
+    Marked d Empty 2 where
+  color := fun _ => Colors.up
+  coord := fun i => m (i (Sum.inr ⟨0, PUnit.unit⟩)) (i (Sum.inr ⟨1, PUnit.unit⟩))
+
+/-- A tensor with two down indices constructed from a matrix.
+
+Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
+def ofMatDownDown {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
+    Marked d Empty 2 where
+  color := fun _ => Colors.down
+  coord := fun i => m (i (Sum.inr ⟨0, PUnit.unit⟩)) (i (Sum.inr ⟨1, PUnit.unit⟩))
+
+/-- A marked 2-tensor with the first index up and the second index down.
+
+Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
+@[simps!]
+def ofMatUpDown {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
+    Marked d Empty 2 where
+  color := fun i => match i with
+  | Sum.inr ⟨0, PUnit.unit⟩ => Colors.up
+  | Sum.inr ⟨1, PUnit.unit⟩ => Colors.down
+  coord := fun i => m (i (Sum.inr ⟨0, PUnit.unit⟩)) (i (Sum.inr ⟨1, PUnit.unit⟩))
+
+/-- A marked 2-tensor with the first index down and the second index up.
+
+Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
+def ofMatDownUp {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
+    Marked d Empty 2 where
+  color := fun i => match i with
+    | Sum.inr ⟨0, PUnit.unit⟩ => Colors.down
+    | Sum.inr ⟨1, PUnit.unit⟩ => Colors.up
+  coord := fun i => m (i (Sum.inr ⟨0, PUnit.unit⟩)) (i (Sum.inr ⟨1, PUnit.unit⟩))
+
+/-!
+
+## Equivalence of `IndexValue` for constructors
+
+-/
+
+/-- Index values for `ofVecUp v` are equivalent to elements of `Fin 1 ⊕ Fin d`. -/
+def ofVecUpIndexValue (v : Fin 1 ⊕ Fin d → ℝ) :
+    IndexValue d (ofVecUp v).color ≃ (Fin 1 ⊕ Fin d) where
+  toFun i := i (Sum.inr ⟨0, PUnit.unit⟩)
+  invFun x := fun i => match i with
+    | Sum.inr ⟨0, PUnit.unit⟩ => x
+  left_inv i := by
+    funext y
+    match y with
+    | Sum.inr ⟨0, PUnit.unit⟩ => rfl
+  right_inv x := rfl
+
+/-- Index values for `ofVecDown v` are equivalent to elements of `Fin 1 ⊕ Fin d`. -/
+def ofVecDownIndexValue (v : Fin 1 ⊕ Fin d → ℝ) :
+    IndexValue d (ofVecDown v).color ≃ (Fin 1 ⊕ Fin d) where
+  toFun i := i (Sum.inr ⟨0, PUnit.unit⟩)
+  invFun x := fun i => match i with
+    | Sum.inr ⟨0, PUnit.unit⟩ => x
+  left_inv i := by
+    funext y
+    match y with
+    | Sum.inr ⟨0, PUnit.unit⟩ => rfl
+  right_inv x := rfl
+
+/-- Index values for `ofMatUpUp v` are equivalent to elements of
+  `(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)`. -/
+def ofMatUpUpIndexValue (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
+    IndexValue d (ofMatUpUp M).color ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) where
+  toFun i := (i (Sum.inr ⟨0, PUnit.unit⟩), i (Sum.inr ⟨1, PUnit.unit⟩))
+  invFun x := fun i => match i with
+    | Sum.inr ⟨0, PUnit.unit⟩ => x.1
+    | Sum.inr ⟨1, PUnit.unit⟩ => x.2
+  left_inv i := by
+    funext y
+    match y with
+    | Sum.inr ⟨0, PUnit.unit⟩ => rfl
+    | Sum.inr ⟨1, PUnit.unit⟩ => rfl
+  right_inv x := rfl
+
+/-- Index values for `ofMatDownDown v` are equivalent to elements of
+  `(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)`. -/
+def ofMatDownDownIndexValue (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
+    IndexValue d (ofMatDownDown M).color ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) where
+  toFun i := (i (Sum.inr ⟨0, PUnit.unit⟩), i (Sum.inr ⟨1, PUnit.unit⟩))
+  invFun x := fun i => match i with
+    | Sum.inr ⟨0, PUnit.unit⟩ => x.1
+    | Sum.inr ⟨1, PUnit.unit⟩ => x.2
+  left_inv i := by
+    funext y
+    match y with
+    | Sum.inr ⟨0, PUnit.unit⟩ => rfl
+    | Sum.inr ⟨1, PUnit.unit⟩ => rfl
+  right_inv x := rfl
+
+/-- Index values for `ofMatUpDown v` are equivalent to elements of
+  `(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)`. -/
+def ofMatUpDownIndexValue (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
+    IndexValue d (ofMatUpDown M).color ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) where
+  toFun i := (i (Sum.inr ⟨0, PUnit.unit⟩), i (Sum.inr ⟨1, PUnit.unit⟩))
+  invFun x := fun i => match i with
+    | Sum.inr ⟨0, PUnit.unit⟩ => x.1
+    | Sum.inr ⟨1, PUnit.unit⟩ => x.2
+  left_inv i := by
+    funext y
+    match y with
+    | Sum.inr ⟨0, PUnit.unit⟩ => rfl
+    | Sum.inr ⟨1, PUnit.unit⟩ => rfl
+  right_inv x := rfl
+
+/-- Index values for `ofMatDownUp v` are equivalent to elements of
+  `(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)`. -/
+def ofMatDownUpIndexValue (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
+    IndexValue d (ofMatDownUp M).color ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) where
+  toFun i := (i (Sum.inr ⟨0, PUnit.unit⟩), i (Sum.inr ⟨1, PUnit.unit⟩))
+  invFun x := fun i => match i with
+    | Sum.inr ⟨0, PUnit.unit⟩ => x.1
+    | Sum.inr ⟨1, PUnit.unit⟩ => x.2
+  left_inv i := by
+    funext y
+    match y with
+    | Sum.inr ⟨0, PUnit.unit⟩ => rfl
+    | Sum.inr ⟨1, PUnit.unit⟩ => rfl
+  right_inv x := rfl
+
+/-!
+
+## Contraction of indices of tensors from matrices
+
+-/
+open Matrix
+open Marked
+
+/-- Contracting the indices of `ofMatUpDown` returns the trace of the matrix. -/
+lemma contr_ofMatUpDown_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
+    contr (ofMatUpDown M) (by rfl) = ofReal d M.trace := by
+  refine ext' ?_ ?_
+  · funext i
+    exact Empty.elim i
+  · funext i
+    simp only [Fin.isValue, contr, IndexValue, Equiv.cast_apply, trace, diag_apply, ofReal,
+      Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
+    apply Finset.sum_congr rfl
+    intro x _
+    rfl
+
+/-- Contracting the indices of `ofMatDownUp` returns the trace of the matrix. -/
+lemma contr_ofMatDownUp_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
+    contr (ofMatDownUp M) (by rfl) = ofReal d M.trace := by
+  refine ext' ?_ ?_
+  · funext i
+    exact Empty.elim i
+  · funext i
+    rfl
+
+/-!
+
+## Multiplication of tensors from vectors and matrices
+
+-/
+
+/-- Multiplying `ofVecUp` with `ofVecDown` gives the dot product. -/
+@[simp]
+lemma mul_ofVecUp_ofVecDown_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d → ℝ) :
+    congrSet (@Equiv.equivEmpty (Empty ⊕ Empty) instIsEmptySum)
+    (mul (ofVecUp v₁) (ofVecDown v₂) (by rfl)) = ofReal d (v₁ ⬝ᵥ v₂) := by
+  refine ext' ?_ ?_
+  · funext i
+    exact Empty.elim i
+  · funext i
+    rfl
+
+/-- Multiplying `ofVecDown` with `ofVecUp` gives the dot product. -/
+@[simp]
+lemma mul_ofVecDown_ofVecUp_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d → ℝ) :
+    congrSet (Equiv.equivEmpty (Empty ⊕ Empty))
+    (mul (ofVecDown v₁) (ofVecUp v₂) rfl) = ofReal d (v₁ ⬝ᵥ v₂) := by
+  refine ext' ?_ ?_
+  · funext i
+    exact Empty.elim i
+  · funext i
+    rfl
+
+lemma mul_ofMatUpDown_ofVecUp_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
+    (v : Fin 1 ⊕ Fin d → ℝ) :
+    congrSet ((Equiv.sumEmpty (Empty ⊕ PUnit.{1}) Empty).trans equivPUnitToSigma)
+    (mul (unmarkFirst $ ofMatUpDown M) (ofVecUp v) rfl) = ofVecUp (M *ᵥ v) := by
+  refine ext' ?_ ?_
+  · funext i
+    simp only [Nat.succ_eq_add_one, Nat.reduceAdd, congrSet_apply_color, mul_color, Equiv.symm_symm]
+    fin_cases i
+    rfl
+  · funext i
+    rfl
+
+lemma mul_ofMatDownUp_ofVecDown_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
+    (v : Fin 1 ⊕ Fin d → ℝ) :
+    congrSet ((Equiv.sumEmpty (Empty ⊕ PUnit.{1}) Empty).trans equivPUnitToSigma)
+    (mul (unmarkFirst $ ofMatDownUp M) (ofVecDown v) rfl) = ofVecDown (M *ᵥ v) := by
+  refine ext' ?_ ?_
+  · funext i
+    simp only [Nat.succ_eq_add_one, Nat.reduceAdd, congrSet_apply_color, mul_color, Equiv.symm_symm]
+    fin_cases i
+    rfl
+  · funext i
+    rfl
+
+/-!
+
+## The Lorentz action on constructors
+
+-/
+section lorentzAction
+variable {d : ℕ} {X : Type} [Fintype X] [DecidableEq X] (T : RealLorentzTensor d X) (c : X → Colors)
+variable (Λ Λ' : LorentzGroup d)
+
+open Matrix
+
+/-- The action of the Lorentz group on `ofReal v` is trivial. -/
+@[simp]
+lemma lorentzAction_ofReal (r : ℝ) : Λ • ofReal d r = ofReal d r := by
+  refine ext' rfl ?_
+  funext i
+  erw [lorentzAction_smul_coord]
+  simp only [Finset.univ_unique, Finset.univ_eq_empty, Finset.prod_empty, one_mul,
+    Finset.sum_singleton, IndexValue]
+  rfl
+
+/-- The action of the Lorentz group on `ofVecUp v` is by vector multiplication. -/
+@[simp]
+lemma lorentzAction_ofVecUp (v : Fin 1 ⊕ Fin d → ℝ) :
+    Λ • ofVecUp v = ofVecUp (Λ *ᵥ v) := by
+  refine ext' rfl ?_
+  funext i
+  erw [lorentzAction_smul_coord]
+  simp only [ofVecUp, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty,
+    Finset.prod_empty, one_mul]
+  rw [mulVec]
+  simp only [Fin.isValue, dotProduct, Finset.univ_unique, Fin.default_eq_zero,
+    Finset.sum_singleton]
+  erw [Finset.sum_equiv (ofVecUpIndexValue v)]
+  intro i
+  simp_all only [Finset.mem_univ, Fin.isValue, Equiv.coe_fn_mk]
+  intro j _
+  erw [Finset.prod_singleton]
+  rfl
+
+/-- The action of the Lorentz group on `ofVecDown v` is
+  by vector multiplication of the transpose-inverse. -/
+@[simp]
+lemma lorentzAction_ofVecDown (v : Fin 1 ⊕ Fin d → ℝ) :
+    Λ • ofVecDown v = ofVecDown ((LorentzGroup.transpose Λ⁻¹) *ᵥ v) := by
+  refine ext' rfl ?_
+  funext i
+  erw [lorentzAction_smul_coord]
+  simp only [ofVecDown, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty,
+    Finset.prod_empty, one_mul, lorentzGroupIsGroup_inv]
+  rw [mulVec]
+  simp only [Fin.isValue, dotProduct, Finset.univ_unique, Fin.default_eq_zero,
+    Finset.sum_singleton]
+  erw [Finset.sum_equiv (ofVecUpIndexValue v)]
+  intro i
+  simp_all only [Finset.mem_univ, Fin.isValue, Equiv.coe_fn_mk]
+  intro j _
+  erw [Finset.prod_singleton]
+  rfl
+
+@[simp]
+lemma lorentzAction_ofMatUpUp (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
+    Λ • ofMatUpUp M = ofMatUpUp (Λ.1 * M * (LorentzGroup.transpose Λ).1) := by
+  refine ext' rfl ?_
+  funext i
+  erw [lorentzAction_smul_coord]
+  erw [← Equiv.sum_comp (ofMatUpUpIndexValue M).symm]
+  simp only [ofMatUpUp, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty,
+    Finset.prod_empty, one_mul, mul_apply]
+  erw [Finset.sum_product]
+  rw [Finset.sum_comm]
+  refine Finset.sum_congr rfl (fun x _ => ?_)
+  rw [Finset.sum_mul]
+  refine Finset.sum_congr rfl (fun y _ => ?_)
+  erw [← Equiv.prod_comp (Equiv.sigmaPUnit (Fin 2)).symm]
+  rw [Fin.prod_univ_two]
+  simp only [colorMatrix, Fin.isValue, MonoidHom.coe_mk, OneHom.coe_mk]
+  rw [mul_assoc, mul_comm _ (M _ _), ← mul_assoc]
+  congr
+
+@[simp]
+lemma lorentzAction_ofMatDownDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
+    Λ • ofMatDownDown M = ofMatDownDown ((LorentzGroup.transpose Λ⁻¹).1 * M * (Λ⁻¹).1) := by
+  refine ext' rfl ?_
+  funext i
+  erw [lorentzAction_smul_coord]
+  erw [← Equiv.sum_comp (ofMatDownDownIndexValue M).symm]
+  simp only [ofMatDownDown, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty,
+    Finset.prod_empty, one_mul, mul_apply]
+  erw [Finset.sum_product]
+  rw [Finset.sum_comm]
+  refine Finset.sum_congr rfl (fun x _ => ?_)
+  rw [Finset.sum_mul]
+  refine Finset.sum_congr rfl (fun y _ => ?_)
+  erw [← Equiv.prod_comp (Equiv.sigmaPUnit (Fin 2)).symm]
+  rw [Fin.prod_univ_two]
+  simp only [colorMatrix, Fin.isValue, MonoidHom.coe_mk, OneHom.coe_mk]
+  rw [mul_assoc, mul_comm _ (M _ _), ← mul_assoc]
+  congr
+
+@[simp]
+lemma lorentzAction_ofMatUpDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
+    Λ • ofMatUpDown M = ofMatUpDown (Λ.1 * M * (Λ⁻¹).1) := by
+  refine ext' rfl ?_
+  funext i
+  erw [lorentzAction_smul_coord]
+  erw [← Equiv.sum_comp (ofMatUpDownIndexValue M).symm]
+  simp only [ofMatUpDown, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty,
+    Finset.prod_empty, one_mul, mul_apply]
+  erw [Finset.sum_product]
+  rw [Finset.sum_comm]
+  refine Finset.sum_congr rfl (fun x _ => ?_)
+  rw [Finset.sum_mul]
+  refine Finset.sum_congr rfl (fun y _ => ?_)
+  erw [← Equiv.prod_comp (Equiv.sigmaPUnit (Fin 2)).symm]
+  rw [Fin.prod_univ_two]
+  simp only [colorMatrix, Fin.isValue, MonoidHom.coe_mk, OneHom.coe_mk]
+  rw [mul_assoc, mul_comm _ (M _ _), ← mul_assoc]
+  congr
+
+@[simp]
+lemma lorentzAction_ofMatDownUp (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
+    Λ • ofMatDownUp M =
+    ofMatDownUp ((LorentzGroup.transpose Λ⁻¹).1 * M * (LorentzGroup.transpose Λ).1) := by
+  refine ext' rfl ?_
+  funext i
+  erw [lorentzAction_smul_coord]
+  erw [← Equiv.sum_comp (ofMatDownUpIndexValue M).symm]
+  simp only [ofMatDownUp, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty,
+    Finset.prod_empty, one_mul, mul_apply]
+  erw [Finset.sum_product]
+  rw [Finset.sum_comm]
+  refine Finset.sum_congr rfl (fun x _ => ?_)
+  rw [Finset.sum_mul]
+  refine Finset.sum_congr rfl (fun y _ => ?_)
+  erw [← Equiv.prod_comp (Equiv.sigmaPUnit (Fin 2)).symm]
+  rw [Fin.prod_univ_two]
+  simp only [colorMatrix, Fin.isValue, MonoidHom.coe_mk, OneHom.coe_mk]
+  rw [mul_assoc, mul_comm _ (M _ _), ← mul_assoc]
+  congr
+
+end lorentzAction
+
+end RealLorentzTensor
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
index 3e34ca0..515f1c9 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
@@ -28,7 +28,7 @@ variable {μ : Colors}
 /-- Monoid homomorphism from the Lorentz group to matrices indexed by `ColorsIndex d μ` for a
   color `μ`.
 
-  Thought of as the representation of the Lorentz group for that color index. -/
+  This can be thought of as the representation of the Lorentz group for that color index. -/
 def colorMatrix (μ : Colors) : LorentzGroup d →* Matrix (ColorsIndex d μ) (ColorsIndex d μ) ℝ where
   toFun Λ := match μ with
     | .up => fun i j => Λ.1 i j
@@ -56,21 +56,23 @@ def colorMatrix (μ : Colors) : LorentzGroup d →* Matrix (ColorsIndex d μ) (C
           Matrix.transpose_mul, Matrix.transpose_apply]
         rfl
 
-/-- A real number which occurs in the definition of -/
+/-- A real number occuring in the action of the Lorentz group on Lorentz tensors. -/
 @[simp]
 def prodColorMatrixOnIndexValue (i j : IndexValue d c) : ℝ :=
   ∏ x, colorMatrix (c x) Λ (i x) (j x)
 
+/-- `prodColorMatrixOnIndexValue` evaluated at `1` on the diagonal returns `1`. -/
 lemma one_prodColorMatrixOnIndexValue_on_diag (i : IndexValue d c) :
-  prodColorMatrixOnIndexValue c 1 i i = 1 := by
+    prodColorMatrixOnIndexValue c 1 i i = 1 := by
   simp only [prodColorMatrixOnIndexValue]
   rw [Finset.prod_eq_one]
   intro x _
   simp only [colorMatrix, MonoidHom.map_one, Matrix.one_apply]
   rfl
 
+/-- `prodColorMatrixOnIndexValue` evaluated at `1` off the diagonal returns `0`. -/
 lemma one_prodColorMatrixOnIndexValue_off_diag {i j : IndexValue d c} (hij : j ≠ i) :
-  prodColorMatrixOnIndexValue c 1 i j = 0 := by
+    prodColorMatrixOnIndexValue c 1 i j = 0 := by
   simp only [prodColorMatrixOnIndexValue]
   obtain ⟨x, hijx⟩ := Function.ne_iff.mp hij
   rw [@Finset.prod_eq_zero _ _ _ _ _ x]
@@ -82,8 +84,8 @@ lemma mul_prodColorMatrixOnIndexValue (i j : IndexValue d c) :
     prodColorMatrixOnIndexValue c (Λ * Λ') i j =
     ∑ (k : IndexValue d c),
     ∏ x, (colorMatrix (c x) Λ (i x) (k x)) * (colorMatrix (c x) Λ' (k x) (j x)) := by
-  have h1 :  ∑ (k : IndexValue d c), ∏ x,
-      (colorMatrix (c x) Λ (i x) (k x)) * (colorMatrix (c x) Λ' (k x) (j x))  =
+  have h1 : ∑ (k : IndexValue d c), ∏ x,
+      (colorMatrix (c x) Λ (i x) (k x)) * (colorMatrix (c x) Λ' (k x) (j x)) =
       ∏ x, ∑ y, (colorMatrix (c x) Λ (i x) y) * (colorMatrix (c x) Λ' y (j x)) := by
     rw [Finset.prod_sum]
     simp only [Finset.prod_attach_univ, Finset.sum_univ_pi]
@@ -95,8 +97,9 @@ lemma mul_prodColorMatrixOnIndexValue (i j : IndexValue d c) :
   simp only [prodColorMatrixOnIndexValue, map_mul]
   exact Finset.prod_congr rfl (fun x _ => rfl)
 
-/-- Action of the Lorentz group on the set of Real Lorentz Tensors indexed by `X`. -/
-def lorentzAction : MulAction (LorentzGroup d) (RealLorentzTensor d X) where
+/-- Action of the Lorentz group on `X`-indexed Real Lorentz Tensors. -/
+@[simps!]
+instance lorentzAction : MulAction (LorentzGroup d) (RealLorentzTensor d X) where
   smul Λ T := {color := T.color,
                 coord := fun i => ∑ j, prodColorMatrixOnIndexValue T.color Λ i j * T.coord j}
   one_smul T := by
@@ -133,20 +136,7 @@ def lorentzAction : MulAction (LorentzGroup d) (RealLorentzTensor d X) where
     rw [Finset.prod_mul_distrib]
     rfl
 
-/-!
-
-## The Lorentz action on constructors
-
--/
-
-
-
-
-
-
-
-
-
-
+@[simps!]
+instance : MulAction (LorentzGroup d) (Marked d X n) := lorentzAction
 
 end RealLorentzTensor
diff --git a/scripts/nolints.json b/scripts/nolints.json
new file mode 100644
index 0000000..0637a08
--- /dev/null
+++ b/scripts/nolints.json
@@ -0,0 +1 @@
+[]
\ No newline at end of file

From 86e7ea6c0f8bcc49e4a8740a66cb802593ec8b37 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 16 Jul 2024 11:43:59 -0400
Subject: [PATCH 4/9] docs: Missing comma

---
 HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
index 141edc5..8bb3b3d 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
@@ -21,7 +21,7 @@ open SMνCharges
 open SMνACCs
 open BigOperators
 
-/-- A proposition which is true if for a given `n` a plane of charges of dimension `n` exists
+/-- A proposition which is true if for a given `n`, a plane of charges of dimension `n` exists
 in which each point is a solution. -/
 def ExistsPlane (n : ℕ) : Prop := ∃ (B : Fin n → (PlusU1 3).Charges),
    LinearIndependent ℚ B ∧ ∀ (f : Fin n → ℚ), (PlusU1 3).IsSolution (∑ i, f i • B i)

From d385f7208702dc0ba06fdb443194ee5fa0e01c2a Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 16 Jul 2024 11:59:29 -0400
Subject: [PATCH 5/9] feat: LorentzAction_on_isEmpty

---
 .../SpaceTime/LorentzTensor/Real/Constructors.lean  |  9 ++-------
 .../SpaceTime/LorentzTensor/Real/LorentzAction.lean | 13 +++++++++++++
 2 files changed, 15 insertions(+), 7 deletions(-)

diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean b/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
index eb28427..b72b913 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
@@ -270,13 +270,8 @@ open Matrix
 
 /-- The action of the Lorentz group on `ofReal v` is trivial. -/
 @[simp]
-lemma lorentzAction_ofReal (r : ℝ) : Λ • ofReal d r = ofReal d r := by
-  refine ext' rfl ?_
-  funext i
-  erw [lorentzAction_smul_coord]
-  simp only [Finset.univ_unique, Finset.univ_eq_empty, Finset.prod_empty, one_mul,
-    Finset.sum_singleton, IndexValue]
-  rfl
+lemma lorentzAction_ofReal (r : ℝ) : Λ • ofReal d r = ofReal d r :=
+  lorentzAction_on_isEmpty Λ (ofReal d r)
 
 /-- The action of the Lorentz group on `ofVecUp v` is by vector multiplication. -/
 @[simp]
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
index 515f1c9..14858ad 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
@@ -139,4 +139,17 @@ instance lorentzAction : MulAction (LorentzGroup d) (RealLorentzTensor d X) wher
 @[simps!]
 instance : MulAction (LorentzGroup d) (Marked d X n) := lorentzAction
 
+/-- The action on an empty Lorentz tensor is trivial. -/
+lemma lorentzAction_on_isEmpty [IsEmpty X] (Λ : LorentzGroup d) (T : RealLorentzTensor d X) :
+    Λ • T = T := by
+  refine ext' rfl ?_
+  funext i
+  erw [lorentzAction_smul_coord]
+  simp only [Finset.univ_unique, Finset.univ_eq_empty, Finset.prod_empty, one_mul,
+    Finset.sum_singleton]
+  simp only [IndexValue, Unique.eq_default]
+
+/-! TODO: Show that the Lorentz action commutes with multiplication. -/
+/-! TODO: Show that the Lorentz action commutes with contraction. -/
+/-! TODO: Show that the Lorentz action commutes with rising and lowering indices. -/
 end RealLorentzTensor

From 757afbc60f5fd5b853d32d23289f23979e9c3782 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 16 Jul 2024 16:58:42 -0400
Subject: [PATCH 6/9] refactor: Lorentz action on tensors

---
 .../SpaceTime/LorentzTensor/Real/Basic.lean   | 107 ++++++--
 .../LorentzTensor/Real/Constructors.lean      |  80 +++---
 .../LorentzTensor/Real/LorentzAction.lean     | 230 ++++++++++++++----
 3 files changed, 298 insertions(+), 119 deletions(-)

diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
index a65ef70..521aaa7 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
@@ -62,6 +62,10 @@ namespace RealLorentzTensor
 open Matrix
 universe u1
 variable {d : ℕ} {X Y Z : Type}
+variable (c : X → Colors)
+
+
+
 
 /-!
 
@@ -144,6 +148,11 @@ lemma color_eq_dual_symm {μ ν : Colors} (h : μ = τ ν) : ν = τ μ :=
 
 -/
 
+instance [Fintype X] [DecidableEq X] : Fintype (IndexValue d c) := Pi.fintype
+
+instance [Fintype X] [DecidableEq X] : DecidableEq (IndexValue d c) :=
+  Fintype.decidablePiFintype
+
 /-- An equivalence of Index values from an equality of color maps. -/
 def castIndexValue {X : Type} {T S : X → Colors} (h : T = S) :
     IndexValue d T ≃ IndexValue d S where
@@ -196,10 +205,19 @@ lemma ext' {T₁ T₂ : RealLorentzTensor d X} (h : T₁.color = T₂.color)
 
 /-- An equivalence between `X → Fin 1 ⊕ Fin d` and `Y → Fin 1 ⊕ Fin d` given an isomorphism
   between `X` and `Y`. -/
+@[simps!]
 def congrSetIndexValue (d : ℕ) (f : X ≃ Y) (i : X → Colors) :
     IndexValue d i ≃ IndexValue d (i ∘ f.symm) :=
   Equiv.piCongrLeft' _ f
 
+@[simp]
+lemma castColorsIndex_comp_congrSetIndexValue (c : X → Colors) (j : IndexValue d c) (f : X ≃ Y)
+    (h1 : (c <| f.symm <| f <| x) = c x) : (castColorsIndex h1 <| congrSetIndexValue d f c j <| f x)
+    = j x := by
+  rw [congrSetIndexValue_apply]
+  refine cast_eq_iff_heq.mpr ?_
+  rw [Equiv.symm_apply_apply]
+
 /-- Given an equivalence of indexing sets, a map on Lorentz tensors. -/
 @[simps!]
 def congrSetMap (f : X ≃ Y) (T : RealLorentzTensor d X) : RealLorentzTensor d Y where
@@ -301,60 +319,103 @@ To define contraction and multiplication of Lorentz tensors we need to mark indi
 
 /-- A `RealLorentzTensor` with `n` marked indices. -/
 def Marked (d : ℕ) (X : Type) (n : ℕ) : Type :=
-  RealLorentzTensor d (X ⊕ Σ _ : Fin n, PUnit)
+  RealLorentzTensor d (X ⊕ Fin n)
 
 namespace Marked
 
 variable {n m : ℕ}
 
+
 /-- The marked point. -/
-def markedPoint (X : Type) (i : Fin n) : (X ⊕ Σ _ : Fin n, PUnit) :=
-  Sum.inr ⟨i, PUnit.unit⟩
+def markedPoint (X : Type) (i : Fin n) : (X ⊕ Fin n) :=
+  Sum.inr i
 
 /-- The colors of unmarked indices. -/
 def unmarkedColor (T : Marked d X n) : X → Colors :=
   T.color ∘ Sum.inl
 
 /-- The colors of marked indices. -/
-def markedColor (T : Marked d X n) : (Σ _ : Fin n, PUnit) → Colors :=
+def markedColor (T : Marked d X n) : Fin n → Colors :=
   T.color ∘ Sum.inr
 
 /-- The index values restricted to unmarked indices. -/
 def UnmarkedIndexValue (T : Marked d X n) : Type :=
   IndexValue d T.unmarkedColor
 
+instance [Fintype X] [DecidableEq X]  (T : Marked d X n)  : Fintype T.UnmarkedIndexValue :=
+  Pi.fintype
+
 /-- The index values restricted to marked indices. -/
 def MarkedIndexValue (T : Marked d X n) : Type :=
   IndexValue d T.markedColor
 
+instance [Fintype X] [DecidableEq X]  (T : Marked d X n)  : Fintype T.MarkedIndexValue :=
+  Pi.fintype
+
 lemma sumElimIndexColor_of_marked (T : Marked d X n) :
     sumElimIndexColor T.unmarkedColor T.markedColor = T.color := by
   ext1 x
   cases' x <;> rfl
 
+def toUnmarkedIndexValue {T : Marked d X n} (i : IndexValue d T.color) : UnmarkedIndexValue T :=
+  inlIndexValue <| castIndexValue T.sumElimIndexColor_of_marked.symm <| i
+
+def toMarkedIndexValue {T : Marked d X n} (i : IndexValue d T.color) : MarkedIndexValue T :=
+  inrIndexValue <| castIndexValue T.sumElimIndexColor_of_marked.symm <| i
+
+def splitIndexValue {T : Marked d X n} :
+    IndexValue d T.color ≃ UnmarkedIndexValue T × MarkedIndexValue T where
+  toFun i := ⟨toUnmarkedIndexValue i, toMarkedIndexValue i⟩
+  invFun p := castIndexValue T.sumElimIndexColor_of_marked $
+      sumElimIndexValue  p.1 p.2
+  left_inv i := by
+    simp_all only [IndexValue]
+    ext1 x
+    cases x with
+    | inl _ => rfl
+    | inr _ => rfl
+  right_inv p := by
+    simp_all only [IndexValue]
+    obtain ⟨fst, snd⟩ := p
+    simp_all only [Prod.mk.injEq]
+    apply And.intro rfl rfl
+
+ @[simp]
+lemma splitIndexValue_sum {T : Marked d X n} [Fintype X] [DecidableEq X]
+    (P : T.UnmarkedIndexValue × T.MarkedIndexValue → ℝ) :
+    ∑ i, P (splitIndexValue i) = ∑ j, ∑ k, P (j, k) := by
+  rw [Equiv.sum_comp splitIndexValue, Fintype.sum_prod_type]
+
 /-- Contruction of marked index values for the case of 1 marked index. -/
-def oneMarkedIndexValue (T : Marked d X 1) (x : ColorsIndex d (T.color (markedPoint X 0))) :
-    T.MarkedIndexValue := fun i => match i with
-  | ⟨0, PUnit.unit⟩ => x
+def oneMarkedIndexValue {T : Marked d X 1} :
+    ColorsIndex d (T.color (markedPoint X 0)) ≃ T.MarkedIndexValue where
+  toFun x := fun i => match i with
+    | 0 => x
+  invFun i := i 0
+  left_inv x := rfl
+  right_inv i := by
+    funext x
+    fin_cases x
+    rfl
 
 /-- Contruction of marked index values for the case of 2 marked index. -/
 def twoMarkedIndexValue (T : Marked d X 2) (x : ColorsIndex d (T.color (markedPoint X 0)))
     (y : ColorsIndex d <| T.color <| markedPoint X 1) :
     T.MarkedIndexValue := fun i =>
   match i with
-  | ⟨0, PUnit.unit⟩ => x
-  | ⟨1, PUnit.unit⟩ => y
+  | 0 => x
+  | 1 => y
+
 
 /-- An equivalence of types used to turn the first marked index into an unmarked index. -/
-def unmarkFirstSet (X : Type) (n : ℕ) : (X ⊕ Σ _ : Fin n.succ, PUnit) ≃
-    (X ⊕ PUnit) ⊕ Σ _ : Fin n, PUnit :=
-  trans (Equiv.sumCongr (Equiv.refl _) $ (Equiv.sigmaPUnit (Fin n.succ)).trans
-  (((Fin.castOrderIso (Nat.succ_eq_one_add n)).toEquiv.trans finSumFinEquiv.symm).trans
-  (Equiv.sumCongr finOneEquiv (Equiv.sigmaPUnit (Fin n)).symm)))
+def unmarkFirstSet (X : Type) (n : ℕ) : (X ⊕ Fin n.succ) ≃
+    (X ⊕ Fin 1) ⊕ Fin n :=
+  trans (Equiv.sumCongr (Equiv.refl _) $
+    (((Fin.castOrderIso (Nat.succ_eq_one_add n)).toEquiv.trans finSumFinEquiv.symm)))
   (Equiv.sumAssoc _ _ _).symm
 
 /-- Unmark the first marked index of a marked thensor. -/
-def unmarkFirst {X : Type} : Marked d X n.succ ≃ Marked d (X ⊕ PUnit) n :=
+def unmarkFirst {X : Type} : Marked d X n.succ ≃ Marked d (X ⊕ Fin 1) n :=
   congrSet (unmarkFirstSet X n)
 
 end Marked
@@ -371,18 +432,16 @@ is dual to the others. The contraction is done via
 `φ^μ ψ_μ = φ^0 ψ_0 + φ^1 ψ_1 + ...`. -/
 @[simps!]
 def mul {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
-    (h : T.markedColor ⟨0, PUnit.unit⟩ = τ (S.markedColor ⟨0, PUnit.unit⟩)) :
+    (h : T.markedColor 0 = τ (S.markedColor 0)) :
     RealLorentzTensor d (X ⊕ Y) where
   color := sumElimIndexColor T.unmarkedColor S.unmarkedColor
   coord := fun i => ∑ x,
-    T.coord (castIndexValue T.sumElimIndexColor_of_marked $
-      sumElimIndexValue (inlIndexValue i) (T.oneMarkedIndexValue x)) *
-    S.coord (castIndexValue S.sumElimIndexColor_of_marked $
-      sumElimIndexValue (inrIndexValue i) (S.oneMarkedIndexValue $ congrColorsDual h x))
+    T.coord (splitIndexValue.symm (inlIndexValue i, oneMarkedIndexValue x)) *
+    S.coord (splitIndexValue.symm (inrIndexValue i, oneMarkedIndexValue $ congrColorsDual h x))
 
 /-- Multiplication is well behaved with regard to swapping tensors. -/
 lemma sumComm_mul {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
-    (h : T.markedColor ⟨0, PUnit.unit⟩ = τ (S.markedColor ⟨0, PUnit.unit⟩)) :
+    (h : T.markedColor 0 = τ (S.markedColor 0)) :
     sumComm (mul T S h) = mul S T (color_eq_dual_symm h) := by
   refine ext' (sumElimIndexColor_symm S.unmarkedColor T.unmarkedColor).symm ?_
   change (mul T S h).coord ∘
@@ -408,13 +467,11 @@ lemma sumComm_mul {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
 -/
 
 /-- The contraction of the marked indices in a tensor with two marked indices. -/
-def contr {X : Type} (T : Marked d X 2)
-    (h : T.markedColor ⟨0, PUnit.unit⟩ = τ (T.markedColor ⟨1, PUnit.unit⟩)) :
+def contr {X : Type} (T : Marked d X 2) (h : T.markedColor 0 = τ (T.markedColor 1)) :
     RealLorentzTensor d X where
   color := T.unmarkedColor
   coord := fun i =>
-    ∑ x, T.coord (castIndexValue T.sumElimIndexColor_of_marked $
-      sumElimIndexValue i $ T.twoMarkedIndexValue x $ congrColorsDual h x)
+    ∑ x, T.coord (splitIndexValue.symm (i, T.twoMarkedIndexValue x $ congrColorsDual h x))
 
 /-! TODO: Following the ethos of modular operads, prove properties of contraction. -/
 
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean b/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
index b72b913..4f60bc5 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
@@ -38,7 +38,7 @@ def ofReal (d : ℕ) (r : ℝ) : RealLorentzTensor d Empty where
 def ofVecUp {d : ℕ} (v : Fin 1 ⊕ Fin d → ℝ) :
     Marked d Empty 1 where
   color := fun _ => Colors.up
-  coord := fun i => v <| i <| Sum.inr <| ⟨0, PUnit.unit⟩
+  coord := fun i => v <| i <| Sum.inr <| 0
 
 /-- A marked 1-tensor with a single down index constructed from a vector.
 
@@ -46,7 +46,7 @@ def ofVecUp {d : ℕ} (v : Fin 1 ⊕ Fin d → ℝ) :
 def ofVecDown {d : ℕ} (v : Fin 1 ⊕ Fin d → ℝ) :
     Marked d Empty 1 where
   color := fun _ => Colors.down
-  coord := fun i => v <| i <| Sum.inr <| ⟨0, PUnit.unit⟩
+  coord := fun i => v <| i <| Sum.inr <| 0
 
 /-- A tensor with two up indices constructed from a matrix.
 
@@ -54,7 +54,7 @@ Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
 def ofMatUpUp {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
     Marked d Empty 2 where
   color := fun _ => Colors.up
-  coord := fun i => m (i (Sum.inr ⟨0, PUnit.unit⟩)) (i (Sum.inr ⟨1, PUnit.unit⟩))
+  coord := fun i => m (i (Sum.inr 0)) (i (Sum.inr 1))
 
 /-- A tensor with two down indices constructed from a matrix.
 
@@ -62,7 +62,7 @@ Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
 def ofMatDownDown {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
     Marked d Empty 2 where
   color := fun _ => Colors.down
-  coord := fun i => m (i (Sum.inr ⟨0, PUnit.unit⟩)) (i (Sum.inr ⟨1, PUnit.unit⟩))
+  coord := fun i => m (i (Sum.inr 0)) (i (Sum.inr 1))
 
 /-- A marked 2-tensor with the first index up and the second index down.
 
@@ -71,9 +71,9 @@ Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
 def ofMatUpDown {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
     Marked d Empty 2 where
   color := fun i => match i with
-  | Sum.inr ⟨0, PUnit.unit⟩ => Colors.up
-  | Sum.inr ⟨1, PUnit.unit⟩ => Colors.down
-  coord := fun i => m (i (Sum.inr ⟨0, PUnit.unit⟩)) (i (Sum.inr ⟨1, PUnit.unit⟩))
+  | Sum.inr 0 => Colors.up
+  | Sum.inr 1 => Colors.down
+  coord := fun i => m (i (Sum.inr 0)) (i (Sum.inr 1))
 
 /-- A marked 2-tensor with the first index down and the second index up.
 
@@ -81,9 +81,9 @@ Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
 def ofMatDownUp {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
     Marked d Empty 2 where
   color := fun i => match i with
-    | Sum.inr ⟨0, PUnit.unit⟩ => Colors.down
-    | Sum.inr ⟨1, PUnit.unit⟩ => Colors.up
-  coord := fun i => m (i (Sum.inr ⟨0, PUnit.unit⟩)) (i (Sum.inr ⟨1, PUnit.unit⟩))
+    | Sum.inr 0 => Colors.down
+    | Sum.inr 1 => Colors.up
+  coord := fun i => m (i (Sum.inr 0)) (i (Sum.inr 1))
 
 /-!
 
@@ -94,85 +94,85 @@ def ofMatDownUp {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
 /-- Index values for `ofVecUp v` are equivalent to elements of `Fin 1 ⊕ Fin d`. -/
 def ofVecUpIndexValue (v : Fin 1 ⊕ Fin d → ℝ) :
     IndexValue d (ofVecUp v).color ≃ (Fin 1 ⊕ Fin d) where
-  toFun i := i (Sum.inr ⟨0, PUnit.unit⟩)
+  toFun i := i (Sum.inr 0)
   invFun x := fun i => match i with
-    | Sum.inr ⟨0, PUnit.unit⟩ => x
+    | Sum.inr 0 => x
   left_inv i := by
     funext y
     match y with
-    | Sum.inr ⟨0, PUnit.unit⟩ => rfl
+    | Sum.inr 0 => rfl
   right_inv x := rfl
 
 /-- Index values for `ofVecDown v` are equivalent to elements of `Fin 1 ⊕ Fin d`. -/
 def ofVecDownIndexValue (v : Fin 1 ⊕ Fin d → ℝ) :
     IndexValue d (ofVecDown v).color ≃ (Fin 1 ⊕ Fin d) where
-  toFun i := i (Sum.inr ⟨0, PUnit.unit⟩)
+  toFun i := i (Sum.inr 0)
   invFun x := fun i => match i with
-    | Sum.inr ⟨0, PUnit.unit⟩ => x
+    | Sum.inr 0 => x
   left_inv i := by
     funext y
     match y with
-    | Sum.inr ⟨0, PUnit.unit⟩ => rfl
+    | Sum.inr 0 => rfl
   right_inv x := rfl
 
 /-- Index values for `ofMatUpUp v` are equivalent to elements of
   `(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)`. -/
 def ofMatUpUpIndexValue (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
     IndexValue d (ofMatUpUp M).color ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) where
-  toFun i := (i (Sum.inr ⟨0, PUnit.unit⟩), i (Sum.inr ⟨1, PUnit.unit⟩))
+  toFun i := (i (Sum.inr 0), i (Sum.inr 1))
   invFun x := fun i => match i with
-    | Sum.inr ⟨0, PUnit.unit⟩ => x.1
-    | Sum.inr ⟨1, PUnit.unit⟩ => x.2
+    | Sum.inr 0 => x.1
+    | Sum.inr 1 => x.2
   left_inv i := by
     funext y
     match y with
-    | Sum.inr ⟨0, PUnit.unit⟩ => rfl
-    | Sum.inr ⟨1, PUnit.unit⟩ => rfl
+    | Sum.inr 0 => rfl
+    | Sum.inr 1 => rfl
   right_inv x := rfl
 
 /-- Index values for `ofMatDownDown v` are equivalent to elements of
   `(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)`. -/
 def ofMatDownDownIndexValue (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
     IndexValue d (ofMatDownDown M).color ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) where
-  toFun i := (i (Sum.inr ⟨0, PUnit.unit⟩), i (Sum.inr ⟨1, PUnit.unit⟩))
+  toFun i := (i (Sum.inr 0), i (Sum.inr 1))
   invFun x := fun i => match i with
-    | Sum.inr ⟨0, PUnit.unit⟩ => x.1
-    | Sum.inr ⟨1, PUnit.unit⟩ => x.2
+    | Sum.inr 0 => x.1
+    | Sum.inr 1 => x.2
   left_inv i := by
     funext y
     match y with
-    | Sum.inr ⟨0, PUnit.unit⟩ => rfl
-    | Sum.inr ⟨1, PUnit.unit⟩ => rfl
+    | Sum.inr 0 => rfl
+    | Sum.inr 1 => rfl
   right_inv x := rfl
 
 /-- Index values for `ofMatUpDown v` are equivalent to elements of
   `(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)`. -/
 def ofMatUpDownIndexValue (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
     IndexValue d (ofMatUpDown M).color ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) where
-  toFun i := (i (Sum.inr ⟨0, PUnit.unit⟩), i (Sum.inr ⟨1, PUnit.unit⟩))
+  toFun i := (i (Sum.inr 0), i (Sum.inr 1))
   invFun x := fun i => match i with
-    | Sum.inr ⟨0, PUnit.unit⟩ => x.1
-    | Sum.inr ⟨1, PUnit.unit⟩ => x.2
+    | Sum.inr 0 => x.1
+    | Sum.inr 1 => x.2
   left_inv i := by
     funext y
     match y with
-    | Sum.inr ⟨0, PUnit.unit⟩ => rfl
-    | Sum.inr ⟨1, PUnit.unit⟩ => rfl
+    | Sum.inr 0 => rfl
+    | Sum.inr 1 => rfl
   right_inv x := rfl
 
 /-- Index values for `ofMatDownUp v` are equivalent to elements of
   `(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)`. -/
 def ofMatDownUpIndexValue (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
     IndexValue d (ofMatDownUp M).color ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) where
-  toFun i := (i (Sum.inr ⟨0, PUnit.unit⟩), i (Sum.inr ⟨1, PUnit.unit⟩))
+  toFun i := (i (Sum.inr 0), i (Sum.inr 1))
   invFun x := fun i => match i with
-    | Sum.inr ⟨0, PUnit.unit⟩ => x.1
-    | Sum.inr ⟨1, PUnit.unit⟩ => x.2
+    | Sum.inr 0 => x.1
+    | Sum.inr 1 => x.2
   left_inv i := by
     funext y
     match y with
-    | Sum.inr ⟨0, PUnit.unit⟩ => rfl
-    | Sum.inr ⟨1, PUnit.unit⟩ => rfl
+    | Sum.inr 0 => rfl
+    | Sum.inr 1 => rfl
   right_inv x := rfl
 
 /-!
@@ -235,7 +235,7 @@ lemma mul_ofVecDown_ofVecUp_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d 
 
 lemma mul_ofMatUpDown_ofVecUp_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
     (v : Fin 1 ⊕ Fin d → ℝ) :
-    congrSet ((Equiv.sumEmpty (Empty ⊕ PUnit.{1}) Empty).trans equivPUnitToSigma)
+    congrSet ((Equiv.sumEmpty (Empty ⊕ Fin 1) Empty))
     (mul (unmarkFirst $ ofMatUpDown M) (ofVecUp v) rfl) = ofVecUp (M *ᵥ v) := by
   refine ext' ?_ ?_
   · funext i
@@ -247,7 +247,7 @@ lemma mul_ofMatUpDown_ofVecUp_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d)
 
 lemma mul_ofMatDownUp_ofVecDown_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
     (v : Fin 1 ⊕ Fin d → ℝ) :
-    congrSet ((Equiv.sumEmpty (Empty ⊕ PUnit.{1}) Empty).trans equivPUnitToSigma)
+    congrSet (Equiv.sumEmpty (Empty ⊕ Fin 1) Empty)
     (mul (unmarkFirst $ ofMatDownUp M) (ofVecDown v) rfl) = ofVecDown (M *ᵥ v) := by
   refine ext' ?_ ?_
   · funext i
@@ -326,7 +326,6 @@ lemma lorentzAction_ofMatUpUp (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) 
   refine Finset.sum_congr rfl (fun x _ => ?_)
   rw [Finset.sum_mul]
   refine Finset.sum_congr rfl (fun y _ => ?_)
-  erw [← Equiv.prod_comp (Equiv.sigmaPUnit (Fin 2)).symm]
   rw [Fin.prod_univ_two]
   simp only [colorMatrix, Fin.isValue, MonoidHom.coe_mk, OneHom.coe_mk]
   rw [mul_assoc, mul_comm _ (M _ _), ← mul_assoc]
@@ -346,7 +345,6 @@ lemma lorentzAction_ofMatDownDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d
   refine Finset.sum_congr rfl (fun x _ => ?_)
   rw [Finset.sum_mul]
   refine Finset.sum_congr rfl (fun y _ => ?_)
-  erw [← Equiv.prod_comp (Equiv.sigmaPUnit (Fin 2)).symm]
   rw [Fin.prod_univ_two]
   simp only [colorMatrix, Fin.isValue, MonoidHom.coe_mk, OneHom.coe_mk]
   rw [mul_assoc, mul_comm _ (M _ _), ← mul_assoc]
@@ -366,7 +364,6 @@ lemma lorentzAction_ofMatUpDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)
   refine Finset.sum_congr rfl (fun x _ => ?_)
   rw [Finset.sum_mul]
   refine Finset.sum_congr rfl (fun y _ => ?_)
-  erw [← Equiv.prod_comp (Equiv.sigmaPUnit (Fin 2)).symm]
   rw [Fin.prod_univ_two]
   simp only [colorMatrix, Fin.isValue, MonoidHom.coe_mk, OneHom.coe_mk]
   rw [mul_assoc, mul_comm _ (M _ _), ← mul_assoc]
@@ -387,7 +384,6 @@ lemma lorentzAction_ofMatDownUp (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)
   refine Finset.sum_congr rfl (fun x _ => ?_)
   rw [Finset.sum_mul]
   refine Finset.sum_congr rfl (fun y _ => ?_)
-  erw [← Equiv.prod_comp (Equiv.sigmaPUnit (Fin 2)).symm]
   rw [Fin.prod_univ_two]
   simp only [colorMatrix, Fin.isValue, MonoidHom.coe_mk, OneHom.coe_mk]
   rw [mul_assoc, mul_comm _ (M _ _), ← mul_assoc]
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
index 14858ad..a4c3948 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
@@ -17,12 +17,13 @@ The Lorentz action is currently only defined for finite and decidable types `X`.
 
 namespace RealLorentzTensor
 
-variable {d : ℕ} {X : Type} [Fintype X] [DecidableEq X] (T : RealLorentzTensor d X) (c : X → Colors)
+variable {d : ℕ} {X Y : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
+variable (T : RealLorentzTensor d X) (c : X → Colors)
 variable (Λ Λ' : LorentzGroup d)
 open LorentzGroup
 open BigOperators
 
-instance : Fintype (IndexValue d c) := Pi.fintype
+
 variable {μ : Colors}
 
 /-- Monoid homomorphism from the Lorentz group to matrices indexed by `ColorsIndex d μ` for a
@@ -56,88 +57,159 @@ def colorMatrix (μ : Colors) : LorentzGroup d →* Matrix (ColorsIndex d μ) (C
           Matrix.transpose_mul, Matrix.transpose_apply]
         rfl
 
-/-- A real number occuring in the action of the Lorentz group on Lorentz tensors. -/
-@[simp]
-def prodColorMatrixOnIndexValue (i j : IndexValue d c) : ℝ :=
-  ∏ x, colorMatrix (c x) Λ (i x) (j x)
-
-/-- `prodColorMatrixOnIndexValue` evaluated at `1` on the diagonal returns `1`. -/
-lemma one_prodColorMatrixOnIndexValue_on_diag (i : IndexValue d c) :
-    prodColorMatrixOnIndexValue c 1 i i = 1 := by
-  simp only [prodColorMatrixOnIndexValue]
-  rw [Finset.prod_eq_one]
-  intro x _
-  simp only [colorMatrix, MonoidHom.map_one, Matrix.one_apply]
+lemma colorMatrix_cast {μ ν : Colors} (h : μ = ν) (Λ : LorentzGroup d) :
+    colorMatrix μ Λ =
+    Matrix.reindex (castColorsIndex h).symm (castColorsIndex h).symm (colorMatrix ν Λ) := by
+  subst h
   rfl
 
-/-- `prodColorMatrixOnIndexValue` evaluated at `1` off the diagonal returns `0`. -/
-lemma one_prodColorMatrixOnIndexValue_off_diag {i j : IndexValue d c} (hij : j ≠ i) :
-    prodColorMatrixOnIndexValue c 1 i j = 0 := by
-  simp only [prodColorMatrixOnIndexValue]
-  obtain ⟨x, hijx⟩ := Function.ne_iff.mp hij
-  rw [@Finset.prod_eq_zero _ _ _ _ _ x]
-  exact Finset.mem_univ x
-  simp only [map_one]
-  exact Matrix.one_apply_ne' hijx
+/-- A real number occuring in the action of the Lorentz group on Lorentz tensors. -/
+@[simps!]
+def toTensorRepMat {c : X → Colors} :
+    LorentzGroup d →* Matrix (IndexValue d c) (IndexValue d c) ℝ where
+  toFun Λ := fun i j => ∏ x, colorMatrix (c x) Λ (i x) (j x)
+  map_one' := by
+    ext i j
+    by_cases hij : i = j
+    · subst hij
+      simp only [map_one, Matrix.one_apply_eq, Finset.prod_const_one]
+    · obtain ⟨x, hijx⟩ := Function.ne_iff.mp hij
+      simp only [map_one]
+      rw [@Finset.prod_eq_zero _ _ _ _ _ x]
+      exact Eq.symm (Matrix.one_apply_ne' fun a => hij (id (Eq.symm a)))
+      exact Finset.mem_univ x
+      exact Matrix.one_apply_ne' (id (Ne.symm hijx))
+  map_mul' Λ Λ' := by
+    ext i j
+    rw [Matrix.mul_apply]
+    trans ∑ (k : IndexValue d c), ∏ x,
+        (colorMatrix (c x) Λ (i x) (k x)) * (colorMatrix (c x) Λ' (k x) (j x))
+    have h1 : ∑ (k : IndexValue d c), ∏ x,
+        (colorMatrix (c x) Λ (i x) (k x)) * (colorMatrix (c x) Λ' (k x) (j x)) =
+        ∏ x, ∑ y, (colorMatrix (c x) Λ (i x) y) * (colorMatrix (c x) Λ' y (j x)) := by
+      rw [Finset.prod_sum]
+      simp only [Finset.prod_attach_univ, Finset.sum_univ_pi]
+      apply Finset.sum_congr
+      simp only [IndexValue, Fintype.piFinset_univ]
+      intro x _
+      rfl
+    rw [h1]
+    simp only [map_mul]
+    exact Finset.prod_congr rfl (fun x _ => rfl)
+    refine Finset.sum_congr rfl (fun k _ => ?_)
+    rw [Finset.prod_mul_distrib]
 
-lemma mul_prodColorMatrixOnIndexValue (i j : IndexValue d c) :
-    prodColorMatrixOnIndexValue c (Λ * Λ') i j =
-    ∑ (k : IndexValue d c),
-    ∏ x, (colorMatrix (c x) Λ (i x) (k x)) * (colorMatrix (c x) Λ' (k x) (j x)) := by
-  have h1 : ∑ (k : IndexValue d c), ∏ x,
-      (colorMatrix (c x) Λ (i x) (k x)) * (colorMatrix (c x) Λ' (k x) (j x)) =
-      ∏ x, ∑ y, (colorMatrix (c x) Λ (i x) y) * (colorMatrix (c x) Λ' y (j x)) := by
-    rw [Finset.prod_sum]
-    simp only [Finset.prod_attach_univ, Finset.sum_univ_pi]
-    apply Finset.sum_congr
-    simp only [IndexValue, Fintype.piFinset_univ]
-    intro x _
-    rfl
-  rw [h1]
-  simp only [prodColorMatrixOnIndexValue, map_mul]
-  exact Finset.prod_congr rfl (fun x _ => rfl)
+lemma toTensorRepMat_mul' (i j : IndexValue d c) :
+    toTensorRepMat (Λ * Λ') i j = ∑ (k : IndexValue d c),
+    ∏ x, colorMatrix (c x) Λ (i x) (k x) * colorMatrix (c x) Λ' (k x) (j x) := by
+  simp [Matrix.mul_apply]
+  refine Finset.sum_congr rfl (fun k _ => ?_)
+  rw [Finset.prod_mul_distrib]
+  rfl
+
+@[simp]
+lemma toTensorRepMat_on_sum {cX : X → Colors} {cY : Y → Colors}
+    (i j : IndexValue d (sumElimIndexColor cX cY)) :
+    toTensorRepMat Λ i j = toTensorRepMat Λ (inlIndexValue i) (inlIndexValue j) *
+    toTensorRepMat Λ (inrIndexValue i) (inrIndexValue j)  := by
+  simp only [toTensorRepMat_apply]
+  rw [Fintype.prod_sum_type]
+  rfl
+
+open Marked
+
+lemma toTensorRepMap_on_splitIndexValue (T : Marked d X n)
+    (i : T.UnmarkedIndexValue) (k : T.MarkedIndexValue) (j : IndexValue d T.color) :
+    toTensorRepMat Λ (splitIndexValue.symm (i, k)) j =
+    toTensorRepMat Λ i (toUnmarkedIndexValue j) *
+    toTensorRepMat Λ k (toMarkedIndexValue j) := by
+  simp only [toTensorRepMat_apply]
+  rw [Fintype.prod_sum_type]
+  rfl
+
+/-!
+
+## Definition of the Lorentz group action on Real Lorentz Tensors.
+
+-/
 
 /-- Action of the Lorentz group on `X`-indexed Real Lorentz Tensors. -/
 @[simps!]
 instance lorentzAction : MulAction (LorentzGroup d) (RealLorentzTensor d X) where
   smul Λ T := {color := T.color,
-                coord := fun i => ∑ j, prodColorMatrixOnIndexValue T.color Λ i j * T.coord j}
+                coord := fun i => ∑ j, toTensorRepMat Λ i j * T.coord j}
   one_smul T := by
     refine ext' rfl ?_
     funext i
     simp only [HSMul.hSMul, map_one]
     erw [Finset.sum_eq_single_of_mem i]
-    rw [one_prodColorMatrixOnIndexValue_on_diag]
-    simp only [one_mul, IndexValue]
+    simp only [Matrix.one_apply_eq, one_mul, IndexValue]
     rfl
     exact Finset.mem_univ i
-    intro j _ hij
-    rw [one_prodColorMatrixOnIndexValue_off_diag]
-    simp only [zero_mul]
-    exact hij
+    exact fun j _ hij =>  mul_eq_zero.mpr (Or.inl (Matrix.one_apply_ne' hij))
   mul_smul Λ Λ' T := by
     refine ext' rfl ?_
     simp only [HSMul.hSMul]
     funext i
-    have h1 : ∑ j : IndexValue d T.color, prodColorMatrixOnIndexValue T.color (Λ * Λ') i j
+    have h1 : ∑ j : IndexValue d T.color, toTensorRepMat (Λ * Λ') i j
         * T.coord j = ∑ j : IndexValue d T.color, ∑ (k : IndexValue d T.color),
         (∏ x, ((colorMatrix (T.color x) Λ (i x) (k x)) *
         (colorMatrix (T.color x) Λ' (k x) (j x)))) * T.coord j := by
       refine Finset.sum_congr rfl (fun j _ => ?_)
-      rw [mul_prodColorMatrixOnIndexValue, Finset.sum_mul]
+      rw [toTensorRepMat_mul', Finset.sum_mul]
     rw [h1]
     rw [Finset.sum_comm]
     refine Finset.sum_congr rfl (fun j _ => ?_)
     rw [Finset.mul_sum]
     refine Finset.sum_congr rfl (fun k _ => ?_)
-    simp only [prodColorMatrixOnIndexValue, IndexValue]
+    simp only [toTensorRepMat, IndexValue]
     rw [← mul_assoc]
     congr
     rw [Finset.prod_mul_distrib]
     rfl
 
+/-!
+
+## The Lorentz action on marked tensors.
+
+-/
+
 @[simps!]
-instance : MulAction (LorentzGroup d) (Marked d X n) := lorentzAction
+instance  : MulAction (LorentzGroup d) (Marked d X n) := lorentzAction
+
+lemma lorentzAction_on_splitIndexValue' (T : Marked d X n)
+    (i : T.UnmarkedIndexValue) (k : T.MarkedIndexValue) :
+    (Λ • T).coord (splitIndexValue.symm (i, k)) =
+    ∑ (x : T.UnmarkedIndexValue), ∑ (y : T.MarkedIndexValue),
+    (toTensorRepMat Λ i x * toTensorRepMat Λ k y) * T.coord (splitIndexValue.symm (x, y)) := by
+  erw [lorentzAction_smul_coord]
+  erw [← Equiv.sum_comp splitIndexValue.symm]
+  rw [Fintype.sum_prod_type]
+  refine Finset.sum_congr rfl (fun x _ => ?_)
+  refine Finset.sum_congr rfl (fun y _ => ?_)
+  erw [toTensorRepMap_on_splitIndexValue]
+  rfl
+
+@[simp]
+lemma lorentzAction_on_splitIndexValue (T : Marked d X n)
+    (i : T.UnmarkedIndexValue) (k : T.MarkedIndexValue) :
+    (Λ • T).coord (splitIndexValue.symm (i, k)) =
+    ∑ (x : T.UnmarkedIndexValue), toTensorRepMat Λ i x *
+    ∑ (y : T.MarkedIndexValue), toTensorRepMat Λ k y *
+    T.coord (splitIndexValue.symm (x, y)) := by
+  rw [lorentzAction_on_splitIndexValue']
+  refine Finset.sum_congr rfl (fun x _ => ?_)
+  rw [Finset.mul_sum]
+  refine Finset.sum_congr rfl (fun y _ => ?_)
+  rw [NonUnitalRing.mul_assoc]
+
+
+/-!
+
+## Properties of the Lorentz action.
+
+-/
+
 
 /-- The action on an empty Lorentz tensor is trivial. -/
 lemma lorentzAction_on_isEmpty [IsEmpty X] (Λ : LorentzGroup d) (T : RealLorentzTensor d X) :
@@ -146,8 +218,62 @@ lemma lorentzAction_on_isEmpty [IsEmpty X] (Λ : LorentzGroup d) (T : RealLorent
   funext i
   erw [lorentzAction_smul_coord]
   simp only [Finset.univ_unique, Finset.univ_eq_empty, Finset.prod_empty, one_mul,
-    Finset.sum_singleton]
-  simp only [IndexValue, Unique.eq_default]
+    Finset.sum_singleton, toTensorRepMat_apply]
+  erw [toTensorRepMat_apply]
+  simp only [IndexValue, toTensorRepMat, Unique.eq_default]
+  rw [@mul_left_eq_self₀]
+  exact Or.inl rfl
+
+/-- The Lorentz action commutes with `congrSet`. -/
+lemma lorentzAction_comm_congrSet (f : X ≃ Y) (Λ : LorentzGroup d) (T : RealLorentzTensor d X) :
+    congrSet f (Λ • T) = Λ • (congrSet f T) := by
+  refine ext' rfl ?_
+  funext i
+  erw [lorentzAction_smul_coord, lorentzAction_smul_coord]
+  erw [← Equiv.sum_comp (congrSetIndexValue d f T.color)]
+  refine Finset.sum_congr rfl (fun j _ => ?_)
+  simp [toTensorRepMat]
+  erw [← Equiv.prod_comp f]
+  apply Or.inl
+  congr
+  funext x
+  have h1 : (T.color (f.symm (f x))) = T.color x := by
+    simp only [Equiv.symm_apply_apply]
+  rw [colorMatrix_cast h1]
+  simp only [Matrix.reindex_apply, Equiv.symm_symm, Matrix.submatrix_apply]
+  erw [castColorsIndex_comp_congrSetIndexValue]
+  apply congrFun
+  apply congrArg
+  symm
+  refine cast_eq_iff_heq.mpr ?_
+  simp only [congrSetIndexValue, Equiv.piCongrLeft'_symm_apply, heq_eqRec_iff_heq, heq_eq_eq]
+  rfl
+
+open Marked
+
+lemma lorentzAction_comm_mul  (T : Marked d X 1) (S : Marked d Y 1)
+    (h : T.markedColor 0 = τ (S.markedColor 1)) :
+    mul (Λ • T) (Λ • S) h = Λ • mul T S h  := by
+  refine ext' rfl ?_
+  funext i
+  trans ∑ j, toTensorRepMat Λ (inlIndexValue i) (inlIndexValue j) *
+    toTensorRepMat Λ (inrIndexValue i) (inrIndexValue j)
+    * (mul T S h).coord j
+  swap
+  refine Finset.sum_congr rfl (fun j _ => ?_)
+  erw [toTensorRepMat_on_sum]
+  rfl
+  change ∑ x, (∑ j, toTensorRepMat Λ (splitIndexValue.symm
+    (inlIndexValue i, T.oneMarkedIndexValue x)) j * T.coord j) *
+    (∑ k, toTensorRepMat Λ _ k * S.coord k) = _
+  trans ∑ x, (∑ j,
+    toTensorRepMat  Λ (inlIndexValue i) (toUnmarkedIndexValue j)
+    * toTensorRepMat  Λ (T.oneMarkedIndexValue x) (toMarkedIndexValue j)
+    * T.coord j) *
+
+  sorry
+
+
 
 /-! TODO: Show that the Lorentz action commutes with multiplication. -/
 /-! TODO: Show that the Lorentz action commutes with contraction. -/

From 5da7605301782d5377b1680c8c74968a5e47f508 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 17 Jul 2024 13:53:36 -0400
Subject: [PATCH 7/9] feat: Prove multiplication commute Lorentz action

---
 HepLean.lean                                  |   1 +
 .../SpaceTime/LorentzTensor/Real/Basic.lean   | 372 +++++++----------
 .../LorentzTensor/Real/Constructors.lean      |  57 +--
 .../LorentzTensor/Real/LorentzAction.lean     | 373 +++++++++++++-----
 .../LorentzTensor/Real/Multiplication.lean    | 194 +++++++++
 5 files changed, 649 insertions(+), 348 deletions(-)
 create mode 100644 HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean

diff --git a/HepLean.lean b/HepLean.lean
index db49ab9..b603d99 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -73,6 +73,7 @@ import HepLean.SpaceTime.LorentzGroup.Rotations
 import HepLean.SpaceTime.LorentzTensor.Real.Basic
 import HepLean.SpaceTime.LorentzTensor.Real.Constructors
 import HepLean.SpaceTime.LorentzTensor.Real.LorentzAction
+import HepLean.SpaceTime.LorentzTensor.Real.Multiplication
 import HepLean.SpaceTime.LorentzVector.AsSelfAdjointMatrix
 import HepLean.SpaceTime.LorentzVector.Basic
 import HepLean.SpaceTime.LorentzVector.NormOne
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
index 521aaa7..09cdaa4 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
@@ -6,6 +6,8 @@ Authors: Joseph Tooby-Smith
 import Mathlib.Logic.Function.CompTypeclasses
 import Mathlib.Data.Real.Basic
 import Mathlib.Analysis.Normed.Field.Basic
+import Mathlib.CategoryTheory.Core
+import Mathlib.CategoryTheory.Types
 /-!
 
 # Real Lorentz Tensors
@@ -59,35 +61,11 @@ structure RealLorentzTensor (d : ℕ) (X : Type) where
   coord : RealLorentzTensor.IndexValue d color → ℝ
 
 namespace RealLorentzTensor
-open Matrix
+open Matrix CategoryTheory
 universe u1
 variable {d : ℕ} {X Y Z : Type}
 variable (c : X → Colors)
 
-
-
-
-/-!
-
-## Some equivalences of types
-
-These come in use casting Lorentz tensors.
-There is likely a better way to deal with these castings.
-
--/
-
-/-- An equivalence from `Empty ⊕ PUnit.{1}` to `Empty ⊕ Σ _ : Fin 1, PUnit`. -/
-def equivPUnitToSigma :
-    (Empty ⊕ PUnit.{1}) ≃ (Empty ⊕ Σ _ : Fin 1, PUnit) where
-  toFun x := match x with
-    | Sum.inr x => Sum.inr ⟨0, x⟩
-  invFun x := match x with
-    | Sum.inr ⟨0, x⟩ => Sum.inr x
-  left_inv x := match x with
-    | Sum.inr _ => rfl
-  right_inv x := match x with
-    | Sum.inr ⟨0, _⟩ => rfl
-
 /-!
 
 ## Colors
@@ -105,11 +83,19 @@ lemma τ_involutive : Function.Involutive τ := by
   intro x
   cases x <;> rfl
 
+lemma color_eq_dual_symm {μ ν : Colors} (h : μ = τ ν) : ν = τ μ :=
+  (Function.Involutive.eq_iff τ_involutive).mp h.symm
+
 /-- The color associated with an element of `x ∈ X` for a tensor `T`. -/
 def ch {X : Type} (x : X) (T : RealLorentzTensor d X) : Colors := T.color x
 
+/-- An equivalence of `ColorsIndex` types given an equality of a colors. -/
+def colorsIndexCast {d : ℕ} {μ₁ μ₂ : RealLorentzTensor.Colors} (h : μ₁ = μ₂) :
+    ColorsIndex d μ₁ ≃ ColorsIndex d μ₂ :=
+  Equiv.cast (by rw [h])
+
 /-- An equivalence of `ColorsIndex` between that of a color and that of its dual. -/
-def dualColorsIndex {d : ℕ} {μ : RealLorentzTensor.Colors}:
+def colorsIndexDualCastSelf {d : ℕ} {μ : RealLorentzTensor.Colors}:
     ColorsIndex d μ ≃ ColorsIndex d (τ μ) where
   toFun x :=
     match μ with
@@ -122,26 +108,18 @@ def dualColorsIndex {d : ℕ} {μ : RealLorentzTensor.Colors}:
   left_inv x := by cases μ <;> rfl
   right_inv x := by cases μ <;> rfl
 
-/-- An equivalence of `ColorsIndex` types given an equality of a colors. -/
-def castColorsIndex {d : ℕ} {μ₁ μ₂ : RealLorentzTensor.Colors} (h : μ₁ = μ₂) :
-    ColorsIndex d μ₁ ≃ ColorsIndex d μ₂ :=
-  Equiv.cast (by rw [h])
-
 /-- An equivalence of `ColorsIndex` types given an equality of a color and the dual of a color. -/
-def congrColorsDual {μ ν : Colors} (h : μ = τ ν) :
+def colorsIndexDualCast {μ ν : Colors} (h : μ = τ ν) :
     ColorsIndex d μ ≃ ColorsIndex d ν :=
-  (castColorsIndex h).trans dualColorsIndex.symm
+  (colorsIndexCast h).trans colorsIndexDualCastSelf.symm
 
-lemma congrColorsDual_symm {μ ν : Colors} (h : μ = τ ν) :
-    (congrColorsDual h).symm =
-    @congrColorsDual d _ _ ((Function.Involutive.eq_iff τ_involutive).mp h.symm) := by
+lemma colorsIndexDualCast_symm {μ ν : Colors} (h : μ = τ ν) :
+    (colorsIndexDualCast h).symm =
+    @colorsIndexDualCast d _ _ ((Function.Involutive.eq_iff τ_involutive).mp h.symm) := by
   match μ, ν with
   | Colors.up, Colors.down => rfl
   | Colors.down, Colors.up => rfl
 
-lemma color_eq_dual_symm {μ ν : Colors} (h : μ = τ ν) : ν = τ μ :=
-  (Function.Involutive.eq_iff τ_involutive).mp h.symm
-
 /-!
 
 ## Index values
@@ -153,19 +131,54 @@ instance [Fintype X] [DecidableEq X] : Fintype (IndexValue d c) := Pi.fintype
 instance [Fintype X] [DecidableEq X] : DecidableEq (IndexValue d c) :=
   Fintype.decidablePiFintype
 
-/-- An equivalence of Index values from an equality of color maps. -/
-def castIndexValue {X : Type} {T S : X → Colors} (h : T = S) :
-    IndexValue d T ≃ IndexValue d S where
-  toFun i := (fun μ => castColorsIndex (congrFun h μ) (i μ))
-  invFun i := (fun μ => (castColorsIndex (congrFun h μ)).symm (i μ))
-  left_inv i := by
-    simp
-  right_inv i := by
-    simp
+/-!
 
-lemma indexValue_eq {T₁ T₂ : X → RealLorentzTensor.Colors} (d : ℕ) (h : T₁ = T₂) :
-    IndexValue d T₁ = IndexValue d T₂ :=
-  pi_congr fun a => congrArg (ColorsIndex d) (congrFun h a)
+## Induced isomorphisms between IndexValue sets
+
+-/
+
+@[simps!]
+def indexValueIso (d : ℕ) (f : X ≃ Y) {i : X → Colors} {j : Y → Colors} (h : i = j ∘ f) :
+    IndexValue d i ≃ IndexValue d j :=
+  (Equiv.piCongrRight (fun μ => colorsIndexCast (congrFun h μ))).trans $
+  Equiv.piCongrLeft (fun y => RealLorentzTensor.ColorsIndex d (j y)) f
+
+lemma indexValueIso_symm_apply' (d : ℕ) (f : X ≃ Y) {i : X → Colors} {j : Y → Colors}
+      (h : i = j ∘ f) (y : IndexValue d j) (x : X) :
+    (indexValueIso d f h).symm y x = (colorsIndexCast (congrFun h x)).symm (y (f x)) := by
+  rfl
+
+@[simp]
+lemma indexValueIso_trans (d : ℕ) (f : X ≃ Y) (g : Y ≃ Z) {i : X → Colors}
+    {j : Y → Colors} {k : Z → Colors} (h : i = j ∘ f) (h' : j = k ∘ g) :
+    (indexValueIso d f h).trans (indexValueIso d g h') =
+    indexValueIso d (f.trans g) (by rw [h, h', Function.comp.assoc]; rfl) := by
+  have h1 : ((indexValueIso d f h).trans (indexValueIso d g h')).symm =
+      (indexValueIso d (f.trans g) (by rw [h, h', Function.comp.assoc]; rfl)).symm := by
+    subst h' h
+    ext x : 2
+    rfl
+  simpa only [Equiv.symm_symm] using congrArg (fun e => e.symm) h1
+
+lemma indexValueIso_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) :
+    (indexValueIso d f h).symm = indexValueIso d f.symm (by rw [h, Function.comp.assoc]; simp) := by
+  ext i : 1
+  rw [← Equiv.symm_apply_eq]
+  funext y
+  rw [indexValueIso_symm_apply', indexValueIso_symm_apply']
+  simp [colorsIndexCast]
+  apply cast_eq_iff_heq.mpr
+  rw [Equiv.apply_symm_apply]
+
+lemma indexValueIso_eq_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) :
+    indexValueIso d f h = (indexValueIso d f.symm (by rw [h, Function.comp.assoc]; simp)).symm := by
+  rw [indexValueIso_symm]
+  congr
+
+@[simp]
+lemma indexValueIso_refl (d : ℕ) (i : X → Colors) :
+    indexValueIso d (Equiv.refl X) (rfl : i = i) = Equiv.refl _ := by
+  rfl
 
 /-!
 
@@ -174,19 +187,7 @@ lemma indexValue_eq {T₁ T₂ : X → RealLorentzTensor.Colors} (d : ℕ) (h :
 -/
 
 lemma ext {T₁ T₂ : RealLorentzTensor d X} (h : T₁.color = T₂.color)
-    (h' : T₁.coord = T₂.coord ∘ Equiv.cast (indexValue_eq d h)) : T₁ = T₂ := by
-  cases T₁
-  cases T₂
-  simp_all only [IndexValue, mk.injEq]
-  apply And.intro h
-  simp only at h
-  subst h
-  simp only [Equiv.cast_refl, Equiv.coe_refl, CompTriple.comp_eq] at h'
-  subst h'
-  rfl
-
-lemma ext' {T₁ T₂ : RealLorentzTensor d X} (h : T₁.color = T₂.color)
-    (h' : T₁.coord = fun i => T₂.coord (castIndexValue h i)) :
+    (h' : T₁.coord = fun i => T₂.coord (indexValueIso d (Equiv.refl X) h i)) :
       T₁ = T₂ := by
   cases T₁
   cases T₂
@@ -199,60 +200,69 @@ lemma ext' {T₁ T₂ : RealLorentzTensor d X} (h : T₁.color = T₂.color)
 
 /-!
 
-## Congruence
+## Mapping isomorphisms.
 
 -/
 
-/-- An equivalence between `X → Fin 1 ⊕ Fin d` and `Y → Fin 1 ⊕ Fin d` given an isomorphism
-  between `X` and `Y`. -/
-@[simps!]
-def congrSetIndexValue (d : ℕ) (f : X ≃ Y) (i : X → Colors) :
-    IndexValue d i ≃ IndexValue d (i ∘ f.symm) :=
-  Equiv.piCongrLeft' _ f
-
-@[simp]
-lemma castColorsIndex_comp_congrSetIndexValue (c : X → Colors) (j : IndexValue d c) (f : X ≃ Y)
-    (h1 : (c <| f.symm <| f <| x) = c x) : (castColorsIndex h1 <| congrSetIndexValue d f c j <| f x)
-    = j x := by
-  rw [congrSetIndexValue_apply]
-  refine cast_eq_iff_heq.mpr ?_
-  rw [Equiv.symm_apply_apply]
-
-/-- Given an equivalence of indexing sets, a map on Lorentz tensors. -/
-@[simps!]
-def congrSetMap (f : X ≃ Y) (T : RealLorentzTensor d X) : RealLorentzTensor d Y where
-  color := T.color ∘ f.symm
-  coord := T.coord ∘ (congrSetIndexValue d f T.color).symm
-
-lemma congrSetMap_trans (f : X ≃ Y) (g : Y ≃ Z) (T : RealLorentzTensor d X) :
-    congrSetMap g (congrSetMap f T) = congrSetMap (f.trans g) T := by
-  apply ext (by rfl)
-  have h1 : congrSetIndexValue d (f.trans g) T.color = (congrSetIndexValue d f T.color).trans
-    (congrSetIndexValue d g $ Equiv.piCongrLeft' (fun _ => Colors) f T.color) := by
-    exact Equiv.coe_inj.mp rfl
-  simp only [congrSetMap, Equiv.piCongrLeft'_apply, IndexValue, Equiv.symm_trans_apply, h1,
-    Equiv.cast_refl, Equiv.coe_refl, CompTriple.comp_eq]
-  rfl
-
 /-- An equivalence of Tensors given an equivalence of underlying sets. -/
 @[simps!]
-def congrSet (f : X ≃ Y) : RealLorentzTensor d X ≃ RealLorentzTensor d Y where
-  toFun := congrSetMap f
-  invFun := congrSetMap f.symm
+def mapIso (d : ℕ) (f : X ≃ Y) : RealLorentzTensor d X ≃ RealLorentzTensor d Y where
+  toFun T := {
+    color := T.color ∘ f.symm,
+    coord := T.coord ∘ (indexValueIso d f (by simp : T.color = T.color ∘ f.symm ∘ f)).symm}
+  invFun T := {
+    color := T.color ∘ f,
+    coord := T.coord ∘ (indexValueIso d f.symm (by simp : T.color = T.color ∘ f ∘ f.symm)).symm}
   left_inv T := by
-    rw [congrSetMap_trans, Equiv.self_trans_symm]
-    rfl
+    refine ext ?_ ?_
+    · simp [Function.comp.assoc]
+    · funext i
+      simp only [IndexValue, Function.comp_apply, Function.comp_id]
+      apply congrArg
+      funext x
+      erw [indexValueIso_symm_apply', indexValueIso_symm_apply', indexValueIso_eq_symm,
+        indexValueIso_symm_apply']
+      rw [← Equiv.apply_eq_iff_eq_symm_apply]
+      simp only [Equiv.refl_symm, Equiv.coe_refl, Function.comp_apply, id_eq, colorsIndexCast,
+        Equiv.cast_symm, Equiv.cast_apply, cast_cast, Equiv.refl_apply]
+      apply cast_eq_iff_heq.mpr
+      congr
+      exact Equiv.symm_apply_apply f x
   right_inv T := by
-    rw [congrSetMap_trans, Equiv.symm_trans_self]
-    rfl
+    refine ext ?_ ?_
+    · simp [Function.comp.assoc]
+    · funext i
+      simp only [IndexValue, Function.comp_apply, Function.comp_id]
+      apply congrArg
+      funext x
+      erw [indexValueIso_symm_apply', indexValueIso_symm_apply', indexValueIso_eq_symm,
+        indexValueIso_symm_apply']
+      rw [← Equiv.apply_eq_iff_eq_symm_apply]
+      simp only [Equiv.refl_symm, Equiv.coe_refl, Function.comp_apply, id_eq, colorsIndexCast,
+        Equiv.cast_symm, Equiv.cast_apply, cast_cast, Equiv.refl_apply]
+      apply cast_eq_iff_heq.mpr
+      congr
+      exact Equiv.apply_symm_apply f x
 
-lemma congrSet_trans (f : X ≃ Y) (g : Y ≃ Z) :
-    (@congrSet d _ _ f).trans (congrSet g) = congrSet (f.trans g) := by
+@[simp]
+lemma mapIso_trans (f : X ≃ Y) (g : Y ≃ Z) :
+    (mapIso d f).trans (mapIso d g) = mapIso d (f.trans g) := by
   refine Equiv.coe_inj.mp ?_
   funext T
-  exact congrSetMap_trans f g T
+  refine ext rfl ?_
+  simp only [Equiv.trans_apply, IndexValue, mapIso_apply_color, Equiv.symm_trans_apply,
+    indexValueIso_refl, Equiv.refl_apply, mapIso_apply_coord]
+  funext i
+  rw [mapIso_apply_coord, mapIso_apply_coord]
+  apply congrArg
+  rw [← indexValueIso_trans]
+  rfl
+  simp only [Function.comp.assoc, Equiv.symm_comp_self, CompTriple.comp_eq]
 
-lemma congrSet_refl : @congrSet d _ _ (Equiv.refl X) = Equiv.refl _ := rfl
+lemma mapIso_symm (f : X ≃ Y) : (mapIso d f).symm = mapIso d f.symm := by
+  rfl
+
+lemma mapIso_refl : mapIso d (Equiv.refl X) = Equiv.refl _ := rfl
 
 /-!
 
@@ -260,54 +270,24 @@ lemma congrSet_refl : @congrSet d _ _ (Equiv.refl X) = Equiv.refl _ := rfl
 
 -/
 
-/-- The sum of two color maps. -/
-def sumElimIndexColor (Tc : X → Colors) (Sc : Y → Colors) :
-    (X ⊕ Y) → Colors :=
-  Sum.elim Tc Sc
-
-/-- The symmetry property on `sumElimIndexColor`. -/
-lemma sumElimIndexColor_symm (Tc : X → Colors) (Sc : Y → Colors) : sumElimIndexColor Tc Sc =
-    Equiv.piCongrLeft' _ (Equiv.sumComm X Y).symm (sumElimIndexColor Sc Tc) := by
-  ext1 x
-  simp_all only [Equiv.piCongrLeft'_apply, Equiv.sumComm_symm, Equiv.sumComm_apply]
-  cases x <;> rfl
-
-/-- The sum of two index values for different color maps. -/
-@[simp]
-def sumElimIndexValue {X Y : Type} {TX : X → Colors} {TY : Y → Colors}
-    (i : IndexValue d TX) (j : IndexValue d TY) :
-    IndexValue d (sumElimIndexColor TX TY) :=
-  fun c => match c with
-  | Sum.inl x => i x
-  | Sum.inr x => j x
-
-/-- The projection of an index value on a sum of color maps to its left component. -/
-def inlIndexValue {Tc : X → Colors} {Sc : Y → Colors} (i : IndexValue d (sumElimIndexColor Tc Sc)) :
-    IndexValue d Tc := fun x => i (Sum.inl x)
-
-/-- The projection of an index value on a sum of color maps to its right component. -/
-def inrIndexValue {Tc : X → Colors} {Sc : Y → Colors}
-    (i : IndexValue d (sumElimIndexColor Tc Sc)) :
-  IndexValue d Sc := fun y => i (Sum.inr y)
+def indexValueSumEquiv {X Y : Type} {TX : X → Colors} {TY : Y → Colors} :
+    IndexValue d (Sum.elim TX TY) ≃ IndexValue d TX × IndexValue d TY where
+  toFun i := (fun x => i (Sum.inl x), fun x => i (Sum.inr x))
+  invFun p := fun c => match c with
+    | Sum.inl x => (p.1 x)
+    | Sum.inr x => (p.2 x)
+  left_inv i := by
+    simp only [IndexValue]
+    ext1 x
+    cases x with
+    | inl val => rfl
+    | inr val_1 => rfl
+  right_inv p := rfl
 
 /-- An equivalence between index values formed by commuting sums. -/
-def sumCommIndexValue {X Y : Type} (Tc : X → Colors) (Sc : Y → Colors) :
-    IndexValue d (sumElimIndexColor Tc Sc) ≃ IndexValue d (sumElimIndexColor Sc Tc) :=
-  (congrSetIndexValue d (Equiv.sumComm X Y) (sumElimIndexColor Tc Sc)).trans
-  (castIndexValue (sumElimIndexColor_symm Sc Tc).symm)
-
-lemma sumCommIndexValue_inlIndexValue {X Y : Type} {Tc : X → Colors} {Sc : Y → Colors}
-    (i : IndexValue d <| sumElimIndexColor Tc Sc) :
-    inlIndexValue (sumCommIndexValue Tc Sc i) = inrIndexValue i := rfl
-
-lemma sumCommIndexValue_inrIndexValue {X Y : Type} {Tc : X → Colors} {Sc : Y → Colors}
-    (i : IndexValue d <| sumElimIndexColor Tc Sc) :
-    inrIndexValue (sumCommIndexValue Tc Sc i) = inlIndexValue i := rfl
-
-/-- Equivalence between sets of `RealLorentzTensor` formed by commuting sums. -/
-@[simps!]
-def sumComm : RealLorentzTensor d (X ⊕ Y) ≃ RealLorentzTensor d (Y ⊕ X) :=
-  congrSet (Equiv.sumComm X Y)
+def indexValueSumComm {X Y : Type} (Tc : X → Colors) (Sc : Y → Colors) :
+    IndexValue d (Sum.elim Tc Sc) ≃ IndexValue d (Sum.elim Sc Tc) :=
+  indexValueIso d (Equiv.sumComm X Y) (by aesop)
 
 /-!
 
@@ -325,7 +305,6 @@ namespace Marked
 
 variable {n m : ℕ}
 
-
 /-- The marked point. -/
 def markedPoint (X : Type) (i : Fin n) : (X ⊕ Fin n) :=
   Sum.inr i
@@ -342,43 +321,31 @@ def markedColor (T : Marked d X n) : Fin n → Colors :=
 def UnmarkedIndexValue (T : Marked d X n) : Type :=
   IndexValue d T.unmarkedColor
 
-instance [Fintype X] [DecidableEq X]  (T : Marked d X n)  : Fintype T.UnmarkedIndexValue :=
+instance [Fintype X] [DecidableEq X] (T : Marked d X n) : Fintype T.UnmarkedIndexValue :=
   Pi.fintype
 
+instance [Fintype X] [DecidableEq X] (T : Marked d X n) : DecidableEq T.UnmarkedIndexValue :=
+  Fintype.decidablePiFintype
+
 /-- The index values restricted to marked indices. -/
 def MarkedIndexValue (T : Marked d X n) : Type :=
   IndexValue d T.markedColor
 
-instance [Fintype X] [DecidableEq X]  (T : Marked d X n)  : Fintype T.MarkedIndexValue :=
+instance [Fintype X] [DecidableEq X] (T : Marked d X n) : Fintype T.MarkedIndexValue :=
   Pi.fintype
 
-lemma sumElimIndexColor_of_marked (T : Marked d X n) :
-    sumElimIndexColor T.unmarkedColor T.markedColor = T.color := by
+instance [Fintype X] [DecidableEq X] (T : Marked d X n) : DecidableEq T.MarkedIndexValue :=
+  Fintype.decidablePiFintype
+
+lemma color_eq_elim (T : Marked d X n) :
+    T.color = Sum.elim T.unmarkedColor T.markedColor := by
   ext1 x
   cases' x <;> rfl
 
-def toUnmarkedIndexValue {T : Marked d X n} (i : IndexValue d T.color) : UnmarkedIndexValue T :=
-  inlIndexValue <| castIndexValue T.sumElimIndexColor_of_marked.symm <| i
-
-def toMarkedIndexValue {T : Marked d X n} (i : IndexValue d T.color) : MarkedIndexValue T :=
-  inrIndexValue <| castIndexValue T.sumElimIndexColor_of_marked.symm <| i
-
 def splitIndexValue {T : Marked d X n} :
-    IndexValue d T.color ≃ UnmarkedIndexValue T × MarkedIndexValue T where
-  toFun i := ⟨toUnmarkedIndexValue i, toMarkedIndexValue i⟩
-  invFun p := castIndexValue T.sumElimIndexColor_of_marked $
-      sumElimIndexValue  p.1 p.2
-  left_inv i := by
-    simp_all only [IndexValue]
-    ext1 x
-    cases x with
-    | inl _ => rfl
-    | inr _ => rfl
-  right_inv p := by
-    simp_all only [IndexValue]
-    obtain ⟨fst, snd⟩ := p
-    simp_all only [Prod.mk.injEq]
-    apply And.intro rfl rfl
+    IndexValue d T.color ≃ T.UnmarkedIndexValue × T.MarkedIndexValue :=
+  (indexValueIso d (Equiv.refl _) T.color_eq_elim).trans
+  indexValueSumEquiv
 
  @[simp]
 lemma splitIndexValue_sum {T : Marked d X n} [Fintype X] [DecidableEq X]
@@ -406,7 +373,6 @@ def twoMarkedIndexValue (T : Marked d X 2) (x : ColorsIndex d (T.color (markedPo
   | 0 => x
   | 1 => y
 
-
 /-- An equivalence of types used to turn the first marked index into an unmarked index. -/
 def unmarkFirstSet (X : Type) (n : ℕ) : (X ⊕ Fin n.succ) ≃
     (X ⊕ Fin 1) ⊕ Fin n :=
@@ -416,62 +382,24 @@ def unmarkFirstSet (X : Type) (n : ℕ) : (X ⊕ Fin n.succ) ≃
 
 /-- Unmark the first marked index of a marked thensor. -/
 def unmarkFirst {X : Type} : Marked d X n.succ ≃ Marked d (X ⊕ Fin 1) n :=
-  congrSet (unmarkFirstSet X n)
+  mapIso d (unmarkFirstSet X n)
 
 end Marked
 
 /-!
 
-## Multiplication
-
--/
-open Marked
-
-/-- The contraction of the marked indices of two tensors each with one marked index, which
-is dual to the others. The contraction is done via
-`φ^μ ψ_μ = φ^0 ψ_0 + φ^1 ψ_1 + ...`. -/
-@[simps!]
-def mul {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
-    (h : T.markedColor 0 = τ (S.markedColor 0)) :
-    RealLorentzTensor d (X ⊕ Y) where
-  color := sumElimIndexColor T.unmarkedColor S.unmarkedColor
-  coord := fun i => ∑ x,
-    T.coord (splitIndexValue.symm (inlIndexValue i, oneMarkedIndexValue x)) *
-    S.coord (splitIndexValue.symm (inrIndexValue i, oneMarkedIndexValue $ congrColorsDual h x))
-
-/-- Multiplication is well behaved with regard to swapping tensors. -/
-lemma sumComm_mul {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
-    (h : T.markedColor 0 = τ (S.markedColor 0)) :
-    sumComm (mul T S h) = mul S T (color_eq_dual_symm h) := by
-  refine ext' (sumElimIndexColor_symm S.unmarkedColor T.unmarkedColor).symm ?_
-  change (mul T S h).coord ∘
-    (congrSetIndexValue d (Equiv.sumComm X Y) (mul T S h).color).symm = _
-  rw [Equiv.comp_symm_eq]
-  funext i
-  simp only [mul_coord, IndexValue, mul_color, Function.comp_apply, sumComm_apply_color]
-  erw [sumCommIndexValue_inlIndexValue, sumCommIndexValue_inrIndexValue,
-    ← Equiv.sum_comp (congrColorsDual h)]
-  refine Fintype.sum_congr _ _ (fun a => ?_)
-  rw [mul_comm]
-  repeat apply congrArg
-  rw [← congrColorsDual_symm h]
-  exact (Equiv.apply_eq_iff_eq_symm_apply <| congrColorsDual h).mp rfl
-
-/-! TODO: Following the ethos of modular operads, prove properties of multiplication. -/
-
-/-! TODO: Use `mul` to generalize to any pair of marked index. -/
-/-!
-
 ## Contraction of indices
 
 -/
 
+open Marked
+
 /-- The contraction of the marked indices in a tensor with two marked indices. -/
 def contr {X : Type} (T : Marked d X 2) (h : T.markedColor 0 = τ (T.markedColor 1)) :
     RealLorentzTensor d X where
   color := T.unmarkedColor
   coord := fun i =>
-    ∑ x, T.coord (splitIndexValue.symm (i, T.twoMarkedIndexValue x $ congrColorsDual h x))
+    ∑ x, T.coord (splitIndexValue.symm (i, T.twoMarkedIndexValue x $ colorsIndexDualCast h x))
 
 /-! TODO: Following the ethos of modular operads, prove properties of contraction. -/
 
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean b/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
index 4f60bc5..e661a9f 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
@@ -5,6 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.LorentzTensor.Real.Basic
 import HepLean.SpaceTime.LorentzTensor.Real.LorentzAction
+import HepLean.SpaceTime.LorentzTensor.Real.Multiplication
 /-!
 
 # Constructors for real Lorentz tensors
@@ -186,7 +187,7 @@ open Marked
 /-- Contracting the indices of `ofMatUpDown` returns the trace of the matrix. -/
 lemma contr_ofMatUpDown_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
     contr (ofMatUpDown M) (by rfl) = ofReal d M.trace := by
-  refine ext' ?_ ?_
+  refine ext ?_ ?_
   · funext i
     exact Empty.elim i
   · funext i
@@ -199,7 +200,7 @@ lemma contr_ofMatUpDown_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1
 /-- Contracting the indices of `ofMatDownUp` returns the trace of the matrix. -/
 lemma contr_ofMatDownUp_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
     contr (ofMatDownUp M) (by rfl) = ofReal d M.trace := by
-  refine ext' ?_ ?_
+  refine ext ?_ ?_
   · funext i
     exact Empty.elim i
   · funext i
@@ -214,9 +215,9 @@ lemma contr_ofMatDownUp_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1
 /-- Multiplying `ofVecUp` with `ofVecDown` gives the dot product. -/
 @[simp]
 lemma mul_ofVecUp_ofVecDown_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d → ℝ) :
-    congrSet (@Equiv.equivEmpty (Empty ⊕ Empty) instIsEmptySum)
+    mapIso d (@Equiv.equivEmpty (Empty ⊕ Empty) instIsEmptySum)
     (mul (ofVecUp v₁) (ofVecDown v₂) (by rfl)) = ofReal d (v₁ ⬝ᵥ v₂) := by
-  refine ext' ?_ ?_
+  refine ext ?_ ?_
   · funext i
     exact Empty.elim i
   · funext i
@@ -225,9 +226,9 @@ lemma mul_ofVecUp_ofVecDown_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d 
 /-- Multiplying `ofVecDown` with `ofVecUp` gives the dot product. -/
 @[simp]
 lemma mul_ofVecDown_ofVecUp_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d → ℝ) :
-    congrSet (Equiv.equivEmpty (Empty ⊕ Empty))
+    mapIso d (Equiv.equivEmpty (Empty ⊕ Empty))
     (mul (ofVecDown v₁) (ofVecUp v₂) rfl) = ofReal d (v₁ ⬝ᵥ v₂) := by
-  refine ext' ?_ ?_
+  refine ext ?_ ?_
   · funext i
     exact Empty.elim i
   · funext i
@@ -235,11 +236,11 @@ lemma mul_ofVecDown_ofVecUp_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d 
 
 lemma mul_ofMatUpDown_ofVecUp_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
     (v : Fin 1 ⊕ Fin d → ℝ) :
-    congrSet ((Equiv.sumEmpty (Empty ⊕ Fin 1) Empty))
+    mapIso d ((Equiv.sumEmpty (Empty ⊕ Fin 1) Empty))
     (mul (unmarkFirst $ ofMatUpDown M) (ofVecUp v) rfl) = ofVecUp (M *ᵥ v) := by
-  refine ext' ?_ ?_
+  refine ext ?_ ?_
   · funext i
-    simp only [Nat.succ_eq_add_one, Nat.reduceAdd, congrSet_apply_color, mul_color, Equiv.symm_symm]
+    simp only [Nat.succ_eq_add_one, Nat.reduceAdd, mapIso_apply_color, mul_color, Equiv.symm_symm]
     fin_cases i
     rfl
   · funext i
@@ -247,11 +248,11 @@ lemma mul_ofMatUpDown_ofVecUp_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d)
 
 lemma mul_ofMatDownUp_ofVecDown_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
     (v : Fin 1 ⊕ Fin d → ℝ) :
-    congrSet (Equiv.sumEmpty (Empty ⊕ Fin 1) Empty)
+    mapIso d (Equiv.sumEmpty (Empty ⊕ Fin 1) Empty)
     (mul (unmarkFirst $ ofMatDownUp M) (ofVecDown v) rfl) = ofVecDown (M *ᵥ v) := by
-  refine ext' ?_ ?_
+  refine ext ?_ ?_
   · funext i
-    simp only [Nat.succ_eq_add_one, Nat.reduceAdd, congrSet_apply_color, mul_color, Equiv.symm_symm]
+    simp only [Nat.succ_eq_add_one, Nat.reduceAdd, mapIso_apply_color, mul_color, Equiv.symm_symm]
     fin_cases i
     rfl
   · funext i
@@ -277,7 +278,7 @@ lemma lorentzAction_ofReal (r : ℝ) : Λ • ofReal d r = ofReal d r :=
 @[simp]
 lemma lorentzAction_ofVecUp (v : Fin 1 ⊕ Fin d → ℝ) :
     Λ • ofVecUp v = ofVecUp (Λ *ᵥ v) := by
-  refine ext' rfl ?_
+  refine ext rfl ?_
   funext i
   erw [lorentzAction_smul_coord]
   simp only [ofVecUp, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty,
@@ -289,7 +290,7 @@ lemma lorentzAction_ofVecUp (v : Fin 1 ⊕ Fin d → ℝ) :
   intro i
   simp_all only [Finset.mem_univ, Fin.isValue, Equiv.coe_fn_mk]
   intro j _
-  erw [Finset.prod_singleton]
+  erw [toTensorRepMat_apply, Finset.prod_singleton]
   rfl
 
 /-- The action of the Lorentz group on `ofVecDown v` is
@@ -297,7 +298,7 @@ lemma lorentzAction_ofVecUp (v : Fin 1 ⊕ Fin d → ℝ) :
 @[simp]
 lemma lorentzAction_ofVecDown (v : Fin 1 ⊕ Fin d → ℝ) :
     Λ • ofVecDown v = ofVecDown ((LorentzGroup.transpose Λ⁻¹) *ᵥ v) := by
-  refine ext' rfl ?_
+  refine ext rfl ?_
   funext i
   erw [lorentzAction_smul_coord]
   simp only [ofVecDown, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty,
@@ -309,13 +310,13 @@ lemma lorentzAction_ofVecDown (v : Fin 1 ⊕ Fin d → ℝ) :
   intro i
   simp_all only [Finset.mem_univ, Fin.isValue, Equiv.coe_fn_mk]
   intro j _
-  erw [Finset.prod_singleton]
+  erw [toTensorRepMat_apply, Finset.prod_singleton]
   rfl
 
 @[simp]
 lemma lorentzAction_ofMatUpUp (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
     Λ • ofMatUpUp M = ofMatUpUp (Λ.1 * M * (LorentzGroup.transpose Λ).1) := by
-  refine ext' rfl ?_
+  refine ext rfl ?_
   funext i
   erw [lorentzAction_smul_coord]
   erw [← Equiv.sum_comp (ofMatUpUpIndexValue M).symm]
@@ -326,7 +327,9 @@ lemma lorentzAction_ofMatUpUp (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) 
   refine Finset.sum_congr rfl (fun x _ => ?_)
   rw [Finset.sum_mul]
   refine Finset.sum_congr rfl (fun y _ => ?_)
-  rw [Fin.prod_univ_two]
+  erw [toTensorRepMat_apply]
+  simp only [Fintype.prod_sum_type, Finset.univ_eq_empty, Finset.prod_empty, Fin.prod_univ_two,
+    Fin.isValue, one_mul, indexValueIso_refl, IndexValue]
   simp only [colorMatrix, Fin.isValue, MonoidHom.coe_mk, OneHom.coe_mk]
   rw [mul_assoc, mul_comm _ (M _ _), ← mul_assoc]
   congr
@@ -334,7 +337,7 @@ lemma lorentzAction_ofMatUpUp (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) 
 @[simp]
 lemma lorentzAction_ofMatDownDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
     Λ • ofMatDownDown M = ofMatDownDown ((LorentzGroup.transpose Λ⁻¹).1 * M * (Λ⁻¹).1) := by
-  refine ext' rfl ?_
+  refine ext rfl ?_
   funext i
   erw [lorentzAction_smul_coord]
   erw [← Equiv.sum_comp (ofMatDownDownIndexValue M).symm]
@@ -345,7 +348,9 @@ lemma lorentzAction_ofMatDownDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d
   refine Finset.sum_congr rfl (fun x _ => ?_)
   rw [Finset.sum_mul]
   refine Finset.sum_congr rfl (fun y _ => ?_)
-  rw [Fin.prod_univ_two]
+  erw [toTensorRepMat_apply]
+  simp only [Fintype.prod_sum_type, Finset.univ_eq_empty, Finset.prod_empty, Fin.prod_univ_two,
+    Fin.isValue, one_mul, lorentzGroupIsGroup_inv, indexValueIso_refl, IndexValue]
   simp only [colorMatrix, Fin.isValue, MonoidHom.coe_mk, OneHom.coe_mk]
   rw [mul_assoc, mul_comm _ (M _ _), ← mul_assoc]
   congr
@@ -353,7 +358,7 @@ lemma lorentzAction_ofMatDownDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d
 @[simp]
 lemma lorentzAction_ofMatUpDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
     Λ • ofMatUpDown M = ofMatUpDown (Λ.1 * M * (Λ⁻¹).1) := by
-  refine ext' rfl ?_
+  refine ext rfl ?_
   funext i
   erw [lorentzAction_smul_coord]
   erw [← Equiv.sum_comp (ofMatUpDownIndexValue M).symm]
@@ -364,7 +369,9 @@ lemma lorentzAction_ofMatUpDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)
   refine Finset.sum_congr rfl (fun x _ => ?_)
   rw [Finset.sum_mul]
   refine Finset.sum_congr rfl (fun y _ => ?_)
-  rw [Fin.prod_univ_two]
+  erw [toTensorRepMat_apply]
+  simp only [Fintype.prod_sum_type, Finset.univ_eq_empty, Finset.prod_empty, Fin.prod_univ_two,
+    Fin.isValue, one_mul, indexValueIso_refl, IndexValue, lorentzGroupIsGroup_inv]
   simp only [colorMatrix, Fin.isValue, MonoidHom.coe_mk, OneHom.coe_mk]
   rw [mul_assoc, mul_comm _ (M _ _), ← mul_assoc]
   congr
@@ -373,7 +380,7 @@ lemma lorentzAction_ofMatUpDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)
 lemma lorentzAction_ofMatDownUp (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
     Λ • ofMatDownUp M =
     ofMatDownUp ((LorentzGroup.transpose Λ⁻¹).1 * M * (LorentzGroup.transpose Λ).1) := by
-  refine ext' rfl ?_
+  refine ext rfl ?_
   funext i
   erw [lorentzAction_smul_coord]
   erw [← Equiv.sum_comp (ofMatDownUpIndexValue M).symm]
@@ -384,7 +391,9 @@ lemma lorentzAction_ofMatDownUp (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)
   refine Finset.sum_congr rfl (fun x _ => ?_)
   rw [Finset.sum_mul]
   refine Finset.sum_congr rfl (fun y _ => ?_)
-  rw [Fin.prod_univ_two]
+  erw [toTensorRepMat_apply]
+  simp only [Fintype.prod_sum_type, Finset.univ_eq_empty, Finset.prod_empty, Fin.prod_univ_two,
+    Fin.isValue, one_mul, lorentzGroupIsGroup_inv, indexValueIso_refl, IndexValue]
   simp only [colorMatrix, Fin.isValue, MonoidHom.coe_mk, OneHom.coe_mk]
   rw [mul_assoc, mul_comm _ (M _ _), ← mul_assoc]
   congr
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
index a4c3948..05554da 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
@@ -18,13 +18,9 @@ The Lorentz action is currently only defined for finite and decidable types `X`.
 namespace RealLorentzTensor
 
 variable {d : ℕ} {X Y : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
-variable (T : RealLorentzTensor d X) (c : X → Colors)
-variable (Λ Λ' : LorentzGroup d)
-open LorentzGroup
-open BigOperators
+  (T : RealLorentzTensor d X) (c : X → Colors) (Λ Λ' : LorentzGroup d) {μ : Colors}
 
-
-variable {μ : Colors}
+open LorentzGroup BigOperators Marked
 
 /-- Monoid homomorphism from the Lorentz group to matrices indexed by `ColorsIndex d μ` for a
   color `μ`.
@@ -59,11 +55,35 @@ def colorMatrix (μ : Colors) : LorentzGroup d →* Matrix (ColorsIndex d μ) (C
 
 lemma colorMatrix_cast {μ ν : Colors} (h : μ = ν) (Λ : LorentzGroup d) :
     colorMatrix μ Λ =
-    Matrix.reindex (castColorsIndex h).symm (castColorsIndex h).symm (colorMatrix ν Λ) := by
+    Matrix.reindex (colorsIndexCast h).symm (colorsIndexCast h).symm (colorMatrix ν Λ) := by
   subst h
   rfl
 
-/-- A real number occuring in the action of the Lorentz group on Lorentz tensors. -/
+lemma colorMatrix_dual_cast {μ : Colors} (Λ : LorentzGroup d) :
+    colorMatrix (τ μ) Λ = Matrix.reindex (colorsIndexDualCastSelf) (colorsIndexDualCastSelf)
+    (colorMatrix μ (LorentzGroup.transpose Λ⁻¹)) := by
+  match μ with
+  | .up => rfl
+  | .down =>
+    ext i j
+    simp only [τ, colorMatrix, MonoidHom.coe_mk, OneHom.coe_mk, colorsIndexDualCastSelf, transpose,
+      lorentzGroupIsGroup_inv, Matrix.transpose_apply, minkowskiMetric.dual_transpose,
+      minkowskiMetric.dual_dual, Matrix.reindex_apply, Equiv.coe_fn_symm_mk, Matrix.submatrix_apply]
+lemma colorMatrix_transpose {μ : Colors} (Λ : LorentzGroup d) :
+    colorMatrix μ (LorentzGroup.transpose Λ) = (colorMatrix μ Λ).transpose := by
+  match μ with
+  | .up => rfl
+  | .down =>
+    ext i j
+    simp only [colorMatrix, transpose, lorentzGroupIsGroup_inv, Matrix.transpose_apply,
+      MonoidHom.coe_mk, OneHom.coe_mk, minkowskiMetric.dual_transpose]
+
+/-!
+
+## Lorentz group to tensor representation matrices.
+
+-/
+
 @[simps!]
 def toTensorRepMat {c : X → Colors} :
     LorentzGroup d →* Matrix (IndexValue d c) (IndexValue d c) ℝ where
@@ -108,27 +128,83 @@ lemma toTensorRepMat_mul' (i j : IndexValue d c) :
   rfl
 
 @[simp]
-lemma toTensorRepMat_on_sum {cX : X → Colors} {cY : Y → Colors}
-    (i j : IndexValue d (sumElimIndexColor cX cY)) :
-    toTensorRepMat Λ i j = toTensorRepMat Λ (inlIndexValue i) (inlIndexValue j) *
-    toTensorRepMat Λ (inrIndexValue i) (inrIndexValue j)  := by
+lemma toTensorRepMat_of_indexValueSumEquiv {cX : X → Colors} {cY : Y → Colors}
+    (i j : IndexValue d (Sum.elim cX cY)) :
+    toTensorRepMat Λ i j = toTensorRepMat Λ (indexValueSumEquiv i).1 (indexValueSumEquiv j).1 *
+    toTensorRepMat Λ (indexValueSumEquiv i).2 (indexValueSumEquiv j).2 := by
   simp only [toTensorRepMat_apply]
   rw [Fintype.prod_sum_type]
   rfl
 
-open Marked
-
-lemma toTensorRepMap_on_splitIndexValue (T : Marked d X n)
-    (i : T.UnmarkedIndexValue) (k : T.MarkedIndexValue) (j : IndexValue d T.color) :
-    toTensorRepMat Λ (splitIndexValue.symm (i, k)) j =
-    toTensorRepMat Λ i (toUnmarkedIndexValue j) *
-    toTensorRepMat Λ k (toMarkedIndexValue j) := by
+lemma toTensorRepMat_of_indexValueSumEquiv' {cX : X → Colors} {cY : Y → Colors}
+    (i j : IndexValue d cX) (k l : IndexValue d cY) :
+    toTensorRepMat Λ i j * toTensorRepMat Λ k l =
+    toTensorRepMat Λ (indexValueSumEquiv.symm (i, k)) (indexValueSumEquiv.symm (j, l)) := by
   simp only [toTensorRepMat_apply]
   rw [Fintype.prod_sum_type]
   rfl
 
 /-!
 
+## Tensor representation matrices and marked tensors.
+
+-/
+
+lemma toTensorRepMat_of_splitIndexValue' (T : Marked d X n)
+    (i j : T.UnmarkedIndexValue) (k l : T.MarkedIndexValue) :
+    toTensorRepMat Λ i j * toTensorRepMat Λ k l =
+    toTensorRepMat Λ (splitIndexValue.symm (i, k)) (splitIndexValue.symm (j, l)) := by
+  simp only [toTensorRepMat_apply]
+  rw [Fintype.prod_sum_type]
+  rfl
+
+lemma toTensorRepMat_oneMarkedIndexValue_dual (T : Marked d X 1) (S : Marked d Y 1)
+    (h : T.markedColor 0 = τ (S.markedColor 0)) (x : ColorsIndex d (T.markedColor 0))
+    (k : S.MarkedIndexValue) :
+    toTensorRepMat Λ (oneMarkedIndexValue $ colorsIndexDualCast h x) k =
+    toTensorRepMat Λ⁻¹ (oneMarkedIndexValue
+      $ (colorsIndexDualCast h).symm $ oneMarkedIndexValue.symm k)
+      (oneMarkedIndexValue x) := by
+  rw [toTensorRepMat_apply, toTensorRepMat_apply]
+  erw [Finset.prod_singleton, Finset.prod_singleton]
+  simp
+  rw [colorMatrix_cast h, colorMatrix_dual_cast]
+  rw [Matrix.reindex_apply, Matrix.reindex_apply]
+  simp
+  rw [colorMatrix_transpose]
+  simp
+  apply congrArg
+  simp only [Fin.isValue, oneMarkedIndexValue, colorsIndexDualCast, Equiv.coe_fn_symm_mk,
+    Equiv.symm_trans_apply, Equiv.symm_symm, Equiv.coe_fn_mk, Equiv.apply_symm_apply,
+    Equiv.symm_apply_apply]
+
+lemma toTensorRepMap_sum_dual (T : Marked d X 1) (S : Marked d Y 1)
+    (h : T.markedColor 0 = τ (S.markedColor 0)) (j : T.MarkedIndexValue) (k : S.MarkedIndexValue) :
+    ∑ x, toTensorRepMat Λ (oneMarkedIndexValue $ colorsIndexDualCast h x) k
+    * toTensorRepMat Λ (oneMarkedIndexValue x) j =
+    toTensorRepMat 1
+    (oneMarkedIndexValue $ (colorsIndexDualCast h).symm $ oneMarkedIndexValue.symm k) j := by
+  trans ∑ x, toTensorRepMat Λ⁻¹ (oneMarkedIndexValue$ (colorsIndexDualCast h).symm $
+    oneMarkedIndexValue.symm k) (oneMarkedIndexValue x) * toTensorRepMat Λ (oneMarkedIndexValue x) j
+  apply Finset.sum_congr rfl (fun x _ => ?_)
+  rw [toTensorRepMat_oneMarkedIndexValue_dual]
+  rw [← Equiv.sum_comp oneMarkedIndexValue.symm]
+  change ∑ i, toTensorRepMat Λ⁻¹ (oneMarkedIndexValue $ (colorsIndexDualCast h).symm $
+    oneMarkedIndexValue.symm k) i * toTensorRepMat Λ i j = _
+  rw [← Matrix.mul_apply, ← toTensorRepMat.map_mul, inv_mul_self Λ]
+
+lemma toTensorRepMat_one_coord_sum (T : Marked d X n) (i : T.UnmarkedIndexValue)
+    (k : T.MarkedIndexValue) : T.coord (splitIndexValue.symm (i, k)) = ∑ j, toTensorRepMat 1 k j *
+    T.coord (splitIndexValue.symm (i, j)) := by
+  erw [Finset.sum_eq_single_of_mem k]
+  simp only [IndexValue, map_one, Matrix.one_apply_eq, one_mul]
+  exact Finset.mem_univ k
+  intro j _ hjk
+  simp [hjk]
+  exact Or.inl (Matrix.one_apply_ne' hjk)
+
+/-!
+
 ## Definition of the Lorentz group action on Real Lorentz Tensors.
 
 -/
@@ -139,16 +215,16 @@ instance lorentzAction : MulAction (LorentzGroup d) (RealLorentzTensor d X) wher
   smul Λ T := {color := T.color,
                 coord := fun i => ∑ j, toTensorRepMat Λ i j * T.coord j}
   one_smul T := by
-    refine ext' rfl ?_
+    refine ext rfl ?_
     funext i
     simp only [HSMul.hSMul, map_one]
     erw [Finset.sum_eq_single_of_mem i]
     simp only [Matrix.one_apply_eq, one_mul, IndexValue]
     rfl
     exact Finset.mem_univ i
-    exact fun j _ hij =>  mul_eq_zero.mpr (Or.inl (Matrix.one_apply_ne' hij))
+    exact fun j _ hij => mul_eq_zero.mpr (Or.inl (Matrix.one_apply_ne' hij))
   mul_smul Λ Λ' T := by
-    refine ext' rfl ?_
+    refine ext rfl ?_
     simp only [HSMul.hSMul]
     funext i
     have h1 : ∑ j : IndexValue d T.color, toTensorRepMat (Λ * Λ') i j
@@ -168,53 +244,21 @@ instance lorentzAction : MulAction (LorentzGroup d) (RealLorentzTensor d X) wher
     rw [Finset.prod_mul_distrib]
     rfl
 
-/-!
-
-## The Lorentz action on marked tensors.
-
--/
-
-@[simps!]
-instance  : MulAction (LorentzGroup d) (Marked d X n) := lorentzAction
-
-lemma lorentzAction_on_splitIndexValue' (T : Marked d X n)
-    (i : T.UnmarkedIndexValue) (k : T.MarkedIndexValue) :
-    (Λ • T).coord (splitIndexValue.symm (i, k)) =
-    ∑ (x : T.UnmarkedIndexValue), ∑ (y : T.MarkedIndexValue),
-    (toTensorRepMat Λ i x * toTensorRepMat Λ k y) * T.coord (splitIndexValue.symm (x, y)) := by
-  erw [lorentzAction_smul_coord]
-  erw [← Equiv.sum_comp splitIndexValue.symm]
-  rw [Fintype.sum_prod_type]
-  refine Finset.sum_congr rfl (fun x _ => ?_)
-  refine Finset.sum_congr rfl (fun y _ => ?_)
-  erw [toTensorRepMap_on_splitIndexValue]
+lemma lorentzAction_smul_coord' {d : ℕ} {X : Type} [Fintype X] [DecidableEq X] (Λ : ↑(𝓛 d))
+    (T : RealLorentzTensor d X) (i : IndexValue d T.color) :
+    (Λ • T).coord i = ∑ j : IndexValue d T.color, toTensorRepMat Λ i j * T.coord j := by
   rfl
 
-@[simp]
-lemma lorentzAction_on_splitIndexValue (T : Marked d X n)
-    (i : T.UnmarkedIndexValue) (k : T.MarkedIndexValue) :
-    (Λ • T).coord (splitIndexValue.symm (i, k)) =
-    ∑ (x : T.UnmarkedIndexValue), toTensorRepMat Λ i x *
-    ∑ (y : T.MarkedIndexValue), toTensorRepMat Λ k y *
-    T.coord (splitIndexValue.symm (x, y)) := by
-  rw [lorentzAction_on_splitIndexValue']
-  refine Finset.sum_congr rfl (fun x _ => ?_)
-  rw [Finset.mul_sum]
-  refine Finset.sum_congr rfl (fun y _ => ?_)
-  rw [NonUnitalRing.mul_assoc]
-
-
 /-!
 
 ## Properties of the Lorentz action.
 
 -/
 
-
 /-- The action on an empty Lorentz tensor is trivial. -/
 lemma lorentzAction_on_isEmpty [IsEmpty X] (Λ : LorentzGroup d) (T : RealLorentzTensor d X) :
     Λ • T = T := by
-  refine ext' rfl ?_
+  refine ext rfl ?_
   funext i
   erw [lorentzAction_smul_coord]
   simp only [Finset.univ_unique, Finset.univ_eq_empty, Finset.prod_empty, one_mul,
@@ -224,58 +268,183 @@ lemma lorentzAction_on_isEmpty [IsEmpty X] (Λ : LorentzGroup d) (T : RealLorent
   rw [@mul_left_eq_self₀]
   exact Or.inl rfl
 
-/-- The Lorentz action commutes with `congrSet`. -/
-lemma lorentzAction_comm_congrSet (f : X ≃ Y) (Λ : LorentzGroup d) (T : RealLorentzTensor d X) :
-    congrSet f (Λ • T) = Λ • (congrSet f T) := by
-  refine ext' rfl ?_
+/-- The Lorentz action commutes with `mapIso`. -/
+lemma lorentzAction_mapIso (f : X ≃ Y) (Λ : LorentzGroup d) (T : RealLorentzTensor d X) :
+    mapIso d f (Λ • T) = Λ • (mapIso d f T) := by
+  refine ext rfl ?_
   funext i
-  erw [lorentzAction_smul_coord, lorentzAction_smul_coord]
-  erw [← Equiv.sum_comp (congrSetIndexValue d f T.color)]
+  rw [mapIso_apply_coord]
+  rw [lorentzAction_smul_coord', lorentzAction_smul_coord']
+  let is : IndexValue d T.color ≃ IndexValue d ((mapIso d f) T).color :=
+    indexValueIso d f (by funext x ; simp)
+  rw [← Equiv.sum_comp is]
   refine Finset.sum_congr rfl (fun j _ => ?_)
-  simp [toTensorRepMat]
-  erw [← Equiv.prod_comp f]
-  apply Or.inl
-  congr
-  funext x
-  have h1 : (T.color (f.symm (f x))) = T.color x := by
-    simp only [Equiv.symm_apply_apply]
-  rw [colorMatrix_cast h1]
-  simp only [Matrix.reindex_apply, Equiv.symm_symm, Matrix.submatrix_apply]
-  erw [castColorsIndex_comp_congrSetIndexValue]
-  apply congrFun
-  apply congrArg
-  symm
-  refine cast_eq_iff_heq.mpr ?_
-  simp only [congrSetIndexValue, Equiv.piCongrLeft'_symm_apply, heq_eqRec_iff_heq, heq_eq_eq]
+  rw [mapIso_apply_coord]
+  refine Mathlib.Tactic.Ring.mul_congr ?_ ?_ rfl
+  · simp only [IndexValue, toTensorRepMat, MonoidHom.coe_mk, OneHom.coe_mk, mapIso_apply_color,
+    indexValueIso_refl]
+    rw [← Equiv.prod_comp f]
+    apply Finset.prod_congr rfl (fun x _ => ?_)
+    have h1 : (T.color (f.symm (f x))) = T.color x := by
+      simp only [Equiv.symm_apply_apply]
+    rw [colorMatrix_cast h1]
+    apply congrArg
+    simp only [is]
+    erw [indexValueIso_eq_symm, indexValueIso_symm_apply']
+    simp only [colorsIndexCast, Function.comp_apply, mapIso_apply_color, Equiv.cast_refl,
+      Equiv.refl_symm, Equiv.refl_apply, Equiv.cast_apply]
+    symm
+    refine cast_eq_iff_heq.mpr ?_
+    congr
+    exact Equiv.symm_apply_apply f x
+  · apply congrArg
+    funext a
+    simp only [IndexValue, mapIso_apply_color, Equiv.symm_apply_apply, is]
+
+/-!
+
+## The Lorentz action on marked tensors.
+
+-/
+
+@[simps!]
+instance : MulAction (LorentzGroup d) (Marked d X n) := lorentzAction
+
+/-- Action of the Lorentz group on just marked indices. -/
+@[simps!]
+def markedLorentzAction : MulAction (LorentzGroup d) (Marked d X n) where
+  smul Λ T := {
+    color := T.color,
+    coord := fun i => ∑ j, toTensorRepMat Λ (splitIndexValue i).2 j *
+      T.coord (splitIndexValue.symm ((splitIndexValue i).1, j))}
+  one_smul T := by
+    refine ext rfl ?_
+    funext i
+    simp only [HSMul.hSMul, map_one]
+    erw [Finset.sum_eq_single_of_mem (splitIndexValue i).2]
+    erw [Matrix.one_apply_eq (splitIndexValue i).2]
+    simp only [IndexValue, one_mul, indexValueIso_refl, Equiv.refl_apply]
+    apply congrArg
+    exact Equiv.symm_apply_apply splitIndexValue i
+    exact Finset.mem_univ (splitIndexValue i).2
+    exact fun j _ hij => mul_eq_zero.mpr (Or.inl (Matrix.one_apply_ne' hij))
+  mul_smul Λ Λ' T := by
+    refine ext rfl ?_
+    simp only [HSMul.hSMul]
+    funext i
+    have h1 : ∑ (j : T.MarkedIndexValue), toTensorRepMat (Λ * Λ') (splitIndexValue i).2 j
+        * T.coord (splitIndexValue.symm ((splitIndexValue i).1, j)) =
+        ∑ (j : T.MarkedIndexValue), ∑ (k : T.MarkedIndexValue),
+        (∏ x, ((colorMatrix (T.markedColor x) Λ ((splitIndexValue i).2 x) (k x)) *
+        (colorMatrix (T.markedColor x) Λ' (k x) (j x)))) *
+        T.coord (splitIndexValue.symm ((splitIndexValue i).1, j)) := by
+      refine Finset.sum_congr rfl (fun j _ => ?_)
+      rw [toTensorRepMat_mul', Finset.sum_mul]
+      rfl
+    erw [h1]
+    rw [Finset.sum_comm]
+    refine Finset.sum_congr rfl (fun j _ => ?_)
+    rw [Finset.mul_sum]
+    refine Finset.sum_congr rfl (fun k _ => ?_)
+    simp only [toTensorRepMat, IndexValue]
+    rw [← mul_assoc]
+    congr
+    rw [Finset.prod_mul_distrib]
+    rfl
+
+/-- Action of the Lorentz group on just unmarked indices. -/
+@[simps!]
+def unmarkedLorentzAction : MulAction (LorentzGroup d) (Marked d X n) where
+  smul Λ T := {
+    color := T.color,
+    coord := fun i => ∑ j, toTensorRepMat Λ (splitIndexValue i).1 j *
+      T.coord (splitIndexValue.symm (j, (splitIndexValue i).2))}
+  one_smul T := by
+    refine ext rfl ?_
+    funext i
+    simp only [HSMul.hSMul, map_one]
+    erw [Finset.sum_eq_single_of_mem (splitIndexValue i).1]
+    erw [Matrix.one_apply_eq (splitIndexValue i).1]
+    simp only [IndexValue, one_mul, indexValueIso_refl, Equiv.refl_apply]
+    apply congrArg
+    exact Equiv.symm_apply_apply splitIndexValue i
+    exact Finset.mem_univ (splitIndexValue i).1
+    exact fun j _ hij => mul_eq_zero.mpr (Or.inl (Matrix.one_apply_ne' hij))
+  mul_smul Λ Λ' T := by
+    refine ext rfl ?_
+    simp only [HSMul.hSMul]
+    funext i
+    have h1 : ∑ (j : T.UnmarkedIndexValue), toTensorRepMat (Λ * Λ') (splitIndexValue i).1 j
+        * T.coord (splitIndexValue.symm (j, (splitIndexValue i).2)) =
+        ∑ (j : T.UnmarkedIndexValue), ∑ (k : T.UnmarkedIndexValue),
+        (∏ x, ((colorMatrix (T.unmarkedColor x) Λ ((splitIndexValue i).1 x) (k x)) *
+        (colorMatrix (T.unmarkedColor x) Λ' (k x) (j x)))) *
+        T.coord (splitIndexValue.symm (j, (splitIndexValue i).2)) := by
+      refine Finset.sum_congr rfl (fun j _ => ?_)
+      rw [toTensorRepMat_mul', Finset.sum_mul]
+      rfl
+    erw [h1]
+    rw [Finset.sum_comm]
+    refine Finset.sum_congr rfl (fun j _ => ?_)
+    rw [Finset.mul_sum]
+    refine Finset.sum_congr rfl (fun k _ => ?_)
+    simp only [toTensorRepMat, IndexValue]
+    rw [← mul_assoc]
+    congr
+    rw [Finset.prod_mul_distrib]
+    rfl
+
+scoped[RealLorentzTensor] infixr:73 " •ₘ " => markedLorentzAction.smul
+scoped[RealLorentzTensor] infixr:73 " •ᵤₘ " => unmarkedLorentzAction.smul
+
+/-- Acting on unmarked and then marked indices is equivalent to acting on all indices. -/
+lemma marked_unmarked_action_eq_action (T : Marked d X n) : Λ •ₘ (Λ •ᵤₘ T) = Λ • T := by
+  refine ext rfl ?_
+  funext i
+  change ∑ j, toTensorRepMat Λ (splitIndexValue i).2 j *
+    (∑ k, toTensorRepMat Λ (splitIndexValue i).1 k * T.coord (splitIndexValue.symm (k, j))) = _
+  trans ∑ j, ∑ k, (toTensorRepMat Λ (splitIndexValue i).2 j *
+      toTensorRepMat Λ (splitIndexValue i).1 k) * T.coord (splitIndexValue.symm (k, j))
+  apply Finset.sum_congr rfl (fun j _ => ?_)
+  rw [Finset.mul_sum]
+  apply Finset.sum_congr rfl (fun k _ => ?_)
+  exact Eq.symm (mul_assoc _ _ _)
+  trans ∑ j, ∑ k, (toTensorRepMat Λ i (splitIndexValue.symm (k, j))
+    * T.coord (splitIndexValue.symm (k, j)))
+  apply Finset.sum_congr rfl (fun j _ => (Finset.sum_congr rfl (fun k _ => ?_)))
+  rw [mul_comm (toTensorRepMat _ _ _), toTensorRepMat_of_splitIndexValue']
+  simp only [IndexValue, Finset.mem_univ, Prod.mk.eta, Equiv.symm_apply_apply]
+  trans ∑ p, (toTensorRepMat Λ i p * T.coord p)
+  rw [← Equiv.sum_comp splitIndexValue.symm, Fintype.sum_prod_type, Finset.sum_comm]
+  rfl
   rfl
 
-open Marked
-
-lemma lorentzAction_comm_mul  (T : Marked d X 1) (S : Marked d Y 1)
-    (h : T.markedColor 0 = τ (S.markedColor 1)) :
-    mul (Λ • T) (Λ • S) h = Λ • mul T S h  := by
-  refine ext' rfl ?_
+/-- Acting on marked and then unmarked indices is equivalent to acting on all indices. -/
+lemma unmarked_marked_action_eq_action (T : Marked d X n) : Λ •ᵤₘ (Λ •ₘ T) = Λ • T := by
+  refine ext rfl ?_
   funext i
-  trans ∑ j, toTensorRepMat Λ (inlIndexValue i) (inlIndexValue j) *
-    toTensorRepMat Λ (inrIndexValue i) (inrIndexValue j)
-    * (mul T S h).coord j
-  swap
-  refine Finset.sum_congr rfl (fun j _ => ?_)
-  erw [toTensorRepMat_on_sum]
+  change ∑ j, toTensorRepMat Λ (splitIndexValue i).1 j *
+      (∑ k, toTensorRepMat Λ (splitIndexValue i).2 k * T.coord (splitIndexValue.symm (j, k))) = _
+  trans ∑ j, ∑ k, (toTensorRepMat Λ (splitIndexValue i).1 j *
+      toTensorRepMat Λ (splitIndexValue i).2 k) * T.coord (splitIndexValue.symm (j, k))
+  apply Finset.sum_congr rfl (fun j _ => ?_)
+  rw [Finset.mul_sum]
+  apply Finset.sum_congr rfl (fun k _ => ?_)
+  exact Eq.symm (mul_assoc _ _ _)
+  trans ∑ j, ∑ k, (toTensorRepMat Λ i (splitIndexValue.symm (j, k))
+    * T.coord (splitIndexValue.symm (j, k)))
+  apply Finset.sum_congr rfl (fun j _ => (Finset.sum_congr rfl (fun k _ => ?_)))
+  rw [toTensorRepMat_of_splitIndexValue']
+  simp only [IndexValue, Finset.mem_univ, Prod.mk.eta, Equiv.symm_apply_apply]
+  trans ∑ p, (toTensorRepMat Λ i p * T.coord p)
+  rw [← Equiv.sum_comp splitIndexValue.symm, Fintype.sum_prod_type]
+  rfl
   rfl
-  change ∑ x, (∑ j, toTensorRepMat Λ (splitIndexValue.symm
-    (inlIndexValue i, T.oneMarkedIndexValue x)) j * T.coord j) *
-    (∑ k, toTensorRepMat Λ _ k * S.coord k) = _
-  trans ∑ x, (∑ j,
-    toTensorRepMat  Λ (inlIndexValue i) (toUnmarkedIndexValue j)
-    * toTensorRepMat  Λ (T.oneMarkedIndexValue x) (toMarkedIndexValue j)
-    * T.coord j) *
 
-  sorry
+/-- The marked and unmarked actions commute. -/
+lemma marked_unmarked_action_comm (T : Marked d X n) : Λ •ᵤₘ (Λ •ₘ T) = Λ •ₘ (Λ •ᵤₘ T) := by
+  rw [unmarked_marked_action_eq_action, marked_unmarked_action_eq_action]
 
-
-
-/-! TODO: Show that the Lorentz action commutes with multiplication. -/
 /-! TODO: Show that the Lorentz action commutes with contraction. -/
 /-! TODO: Show that the Lorentz action commutes with rising and lowering indices. -/
 end RealLorentzTensor
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean b/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
new file mode 100644
index 0000000..fdd9fcb
--- /dev/null
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
@@ -0,0 +1,194 @@
+/-
+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.Real.Basic
+import HepLean.SpaceTime.LorentzTensor.Real.LorentzAction
+/-!
+
+# Multiplication of Real Lorentz Tensors along an index
+
+We define the multiplication of two singularly marked Lorentz tensors along the
+marked index. This is equivalent to contracting two Lorentz tensors.
+
+We prove various results about this multiplication.
+
+-/
+/-! TODO: Add unit to the multiplication. -/
+/-! TODO: Generalize to contracting any marked index of a marked tensor. -/
+/-! TODO: Set up a good notation for the multiplication. -/
+
+namespace RealLorentzTensor
+
+variable {d : ℕ} {X Y : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
+  (T : RealLorentzTensor d X) (c : X → Colors) (Λ Λ' : LorentzGroup d) {μ : Colors}
+
+open Marked
+
+/-- The contraction of the marked indices of two tensors each with one marked index, which
+is dual to the others. The contraction is done via
+`φ^μ ψ_μ = φ^0 ψ_0 + φ^1 ψ_1 + ...`. -/
+@[simps!]
+def mul {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
+    (h : T.markedColor 0 = τ (S.markedColor 0)) :
+    RealLorentzTensor d (X ⊕ Y) where
+  color := Sum.elim T.unmarkedColor S.unmarkedColor
+  coord := fun i => ∑ x,
+    T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, oneMarkedIndexValue x)) *
+    S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2,
+      oneMarkedIndexValue $ colorsIndexDualCast h x))
+
+/-- Multiplication is well behaved with regard to swapping tensors. -/
+lemma mul_symm {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
+    (h : T.markedColor 0 = τ (S.markedColor 0)) :
+    mapIso d (Equiv.sumComm X Y) (mul T S h) = mul S T (color_eq_dual_symm h) := by
+  refine ext ?_ ?_
+  · funext a
+    cases a with
+    | inl _ => rfl
+    | inr _ => rfl
+  · funext i
+    rw [mapIso_apply_coord, mul_coord, mul_coord]
+    erw [← Equiv.sum_comp (colorsIndexDualCast h).symm]
+    refine Fintype.sum_congr _ _ (fun x => ?_)
+    rw [mul_comm]
+    congr
+    · exact Equiv.apply_symm_apply (colorsIndexDualCast h) x
+    · exact colorsIndexDualCast_symm h
+
+lemma mul_mapIso {X Y Z : Type} (T : Marked d X 1) (S : Marked d Y 1) (f : X ≃ W)
+    (g : Y ≃ Z) (h : T.markedColor 0 = τ (S.markedColor 0)) :
+    mapIso d (Equiv.sumCongr f g) (mul T S h) = mul (mapIso d (Equiv.sumCongr f (Equiv.refl _)) T)
+    (mapIso d (Equiv.sumCongr g (Equiv.refl _)) S) h := by
+  refine ext ?_ ?_
+  · funext a
+    cases a with
+    | inl _ => rfl
+    | inr _ => rfl
+  · funext i
+    rw [mapIso_apply_coord, mul_coord, mul_coord]
+    refine Fintype.sum_congr _ _ (fun x => ?_)
+    rw [mapIso_apply_coord, mapIso_apply_coord]
+    refine Mathlib.Tactic.Ring.mul_congr ?_ ?_ rfl
+    · apply congrArg
+      ext1 r
+      cases r with
+      | inl val => rfl
+      | inr val_1 => rfl
+    · apply congrArg
+      ext1 r
+      cases r with
+      | inl val => rfl
+      | inr val_1 => rfl
+
+/-!
+
+## Lorentz action and multiplication.
+
+-/
+
+/-- The marked Lorentz Action leaves multiplication invariant. -/
+lemma mul_markedLorentzAction (T : Marked d X 1) (S : Marked d Y 1)
+    (h : T.markedColor 0 = τ (S.markedColor 1)) :
+    mul (Λ •ₘ T) (Λ •ₘ S) h = mul T S h := by
+  refine ext rfl ?_
+  funext i
+  change ∑ x, (∑ j, toTensorRepMat Λ (oneMarkedIndexValue x) j *
+      T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, j))) *
+      (∑ k, toTensorRepMat Λ (oneMarkedIndexValue $ colorsIndexDualCast h x) k *
+      S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, k))) = _
+  trans ∑ x, ∑ j, ∑ k, (toTensorRepMat Λ (oneMarkedIndexValue $ colorsIndexDualCast h x) k
+    * toTensorRepMat Λ (oneMarkedIndexValue x) j) *
+    T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, j))
+    * S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, k))
+  apply Finset.sum_congr rfl (fun x _ => ?_)
+  rw [Finset.sum_mul_sum ]
+  apply Finset.sum_congr rfl (fun j _ => ?_)
+  apply Finset.sum_congr rfl (fun k _ => ?_)
+  ring
+  rw [Finset.sum_comm]
+  trans ∑ j, ∑ k, ∑ x, (toTensorRepMat Λ (oneMarkedIndexValue $ colorsIndexDualCast h x) k
+    * toTensorRepMat Λ (oneMarkedIndexValue x) j) *
+    T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, j))
+    * S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, k))
+  apply Finset.sum_congr rfl (fun j _ => ?_)
+  rw [Finset.sum_comm]
+  trans ∑ j, ∑ k, (toTensorRepMat 1
+    (oneMarkedIndexValue $ (colorsIndexDualCast h).symm $ oneMarkedIndexValue.symm k) j) *
+    T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, j))
+    * S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, k))
+  apply Finset.sum_congr rfl (fun j _ => Finset.sum_congr rfl (fun k _ => ?_))
+  rw [← Finset.sum_mul, ← Finset.sum_mul]
+  erw [toTensorRepMap_sum_dual]
+  rfl
+  rw [Finset.sum_comm]
+  trans ∑ k,
+    T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1,
+    (oneMarkedIndexValue $ (colorsIndexDualCast h).symm $ oneMarkedIndexValue.symm k)))*
+    S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, k))
+  apply Finset.sum_congr rfl (fun k _ => ?_)
+  rw [← Finset.sum_mul, ← toTensorRepMat_one_coord_sum T]
+  rw [← Equiv.sum_comp (oneMarkedIndexValue)]
+  erw [← Equiv.sum_comp (colorsIndexDualCast h)]
+  simp
+  rfl
+
+/-- The unmarked Lorentz Action commutes with multiplication. -/
+lemma mul_unmarkedLorentzAction (T : Marked d X 1) (S : Marked d Y 1)
+    (h : T.markedColor 0 = τ (S.markedColor 1)) :
+    mul (Λ •ᵤₘ T) (Λ •ᵤₘ S) h = Λ • mul T S h := by
+  refine ext rfl ?_
+  funext i
+  change ∑ x, (∑ j, toTensorRepMat Λ (indexValueSumEquiv i).1 j *
+      T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x)))*
+      ∑ k, toTensorRepMat Λ (indexValueSumEquiv i).2 k *
+      S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x)) = _
+  trans ∑ x, ∑ j, ∑ k, (toTensorRepMat Λ (indexValueSumEquiv i).1 j *
+      T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x)))*
+       toTensorRepMat Λ (indexValueSumEquiv i).2 k *
+      S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x))
+  apply Finset.sum_congr rfl (fun x _ => ?_)
+  rw [Finset.sum_mul_sum ]
+  apply Finset.sum_congr rfl (fun j _ => ?_)
+  apply Finset.sum_congr rfl (fun k _ => ?_)
+  ring
+  rw [Finset.sum_comm]
+  trans ∑ j, ∑ k, ∑ x, (toTensorRepMat Λ (indexValueSumEquiv i).1 j *
+      T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x)))*
+       toTensorRepMat Λ (indexValueSumEquiv i).2 k *
+      S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x))
+  apply Finset.sum_congr rfl (fun j _ => ?_)
+  rw [Finset.sum_comm]
+  trans ∑ j, ∑ k,
+    ((toTensorRepMat Λ (indexValueSumEquiv i).1 j) * toTensorRepMat Λ (indexValueSumEquiv i).2 k)
+    * ∑ x, (T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x)))
+    * S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x))
+  apply Finset.sum_congr rfl (fun j _ => Finset.sum_congr rfl (fun k _ => ?_))
+  rw [Finset.mul_sum]
+  apply Finset.sum_congr rfl (fun x _ => ?_)
+  ring
+  trans ∑ j, ∑ k, toTensorRepMat Λ i (indexValueSumEquiv.symm (j, k)) *
+    ∑ x, (T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x)))
+      * S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x))
+  apply Finset.sum_congr rfl (fun j _ => Finset.sum_congr rfl (fun k _ => ?_))
+  rw [toTensorRepMat_of_indexValueSumEquiv']
+  congr
+  simp only [IndexValue, Finset.mem_univ, Prod.mk.eta, Equiv.symm_apply_apply, mul_color]
+  trans ∑ p, toTensorRepMat Λ i p *
+    ∑ x, (T.coord (splitIndexValue.symm ((indexValueSumEquiv p).1, oneMarkedIndexValue x)))
+    * S.coord (splitIndexValue.symm ((indexValueSumEquiv p).2,
+      oneMarkedIndexValue $ colorsIndexDualCast h x))
+  erw [← Equiv.sum_comp indexValueSumEquiv.symm]
+  rw [Fintype.sum_prod_type]
+  rfl
+  rfl
+
+/-- The Lorentz action commutes with multiplication. -/
+lemma mul_lorentzAction (T : Marked d X 1) (S : Marked d Y 1)
+    (h : T.markedColor 0 = τ (S.markedColor 1)) :
+    mul (Λ • T) (Λ • S) h = Λ • mul T S h := by
+  simp only [← marked_unmarked_action_eq_action]
+  rw [mul_markedLorentzAction, mul_unmarkedLorentzAction]
+
+end RealLorentzTensor

From 36752fa5c4096385289b8cf049a933ede14f37ac Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 17 Jul 2024 15:15:44 -0400
Subject: [PATCH 8/9] refactor: Lint

---
 HepLean/SpaceTime/LorentzTensor/Real/Basic.lean | 17 ++++++++---------
 .../LorentzTensor/Real/LorentzAction.lean       |  9 +++++----
 2 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
index 09cdaa4..f1249fb 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
@@ -5,9 +5,9 @@ Authors: Joseph Tooby-Smith
 -/
 import Mathlib.Logic.Function.CompTypeclasses
 import Mathlib.Data.Real.Basic
-import Mathlib.Analysis.Normed.Field.Basic
-import Mathlib.CategoryTheory.Core
-import Mathlib.CategoryTheory.Types
+import Mathlib.Data.Fintype.BigOperators
+import Mathlib.Logic.Equiv.Fin
+import Mathlib.Tactic.FinCases
 /-!
 
 # Real Lorentz Tensors
@@ -61,10 +61,9 @@ structure RealLorentzTensor (d : ℕ) (X : Type) where
   coord : RealLorentzTensor.IndexValue d color → ℝ
 
 namespace RealLorentzTensor
-open Matrix CategoryTheory
+open Matrix
 universe u1
-variable {d : ℕ} {X Y Z : Type}
-variable (c : X → Colors)
+variable {d : ℕ} {X Y Z : Type} (c : X → Colors)
 
 /-!
 
@@ -144,7 +143,7 @@ def indexValueIso (d : ℕ) (f : X ≃ Y) {i : X → Colors} {j : Y → Colors}
   Equiv.piCongrLeft (fun y => RealLorentzTensor.ColorsIndex d (j y)) f
 
 lemma indexValueIso_symm_apply' (d : ℕ) (f : X ≃ Y) {i : X → Colors} {j : Y → Colors}
-      (h : i = j ∘ f) (y : IndexValue d j) (x : X) :
+    (h : i = j ∘ f) (y : IndexValue d j) (x : X) :
     (indexValueIso d f h).symm y x = (colorsIndexCast (congrFun h x)).symm (y (f x)) := by
   rfl
 
@@ -324,7 +323,7 @@ def UnmarkedIndexValue (T : Marked d X n) : Type :=
 instance [Fintype X] [DecidableEq X] (T : Marked d X n) : Fintype T.UnmarkedIndexValue :=
   Pi.fintype
 
-instance [Fintype X] [DecidableEq X] (T : Marked d X n) : DecidableEq T.UnmarkedIndexValue :=
+instance [Fintype X] (T : Marked d X n) : DecidableEq T.UnmarkedIndexValue :=
   Fintype.decidablePiFintype
 
 /-- The index values restricted to marked indices. -/
@@ -334,7 +333,7 @@ def MarkedIndexValue (T : Marked d X n) : Type :=
 instance [Fintype X] [DecidableEq X] (T : Marked d X n) : Fintype T.MarkedIndexValue :=
   Pi.fintype
 
-instance [Fintype X] [DecidableEq X] (T : Marked d X n) : DecidableEq T.MarkedIndexValue :=
+instance [Fintype X] (T : Marked d X n) : DecidableEq T.MarkedIndexValue :=
   Fintype.decidablePiFintype
 
 lemma color_eq_elim (T : Marked d X n) :
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
index 05554da..a565058 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
@@ -167,12 +167,13 @@ lemma toTensorRepMat_oneMarkedIndexValue_dual (T : Marked d X 1) (S : Marked d Y
       (oneMarkedIndexValue x) := by
   rw [toTensorRepMat_apply, toTensorRepMat_apply]
   erw [Finset.prod_singleton, Finset.prod_singleton]
-  simp
+  simp only [Fin.zero_eta, Fin.isValue, lorentzGroupIsGroup_inv]
   rw [colorMatrix_cast h, colorMatrix_dual_cast]
   rw [Matrix.reindex_apply, Matrix.reindex_apply]
-  simp
+  simp only [Fin.isValue, lorentzGroupIsGroup_inv, minkowskiMetric.dual_dual, Subtype.coe_eta,
+    Equiv.symm_symm, Matrix.submatrix_apply]
   rw [colorMatrix_transpose]
-  simp
+  simp only [Fin.isValue, Matrix.transpose_apply]
   apply congrArg
   simp only [Fin.isValue, oneMarkedIndexValue, colorsIndexDualCast, Equiv.coe_fn_symm_mk,
     Equiv.symm_trans_apply, Equiv.symm_symm, Equiv.coe_fn_mk, Equiv.apply_symm_apply,
@@ -276,7 +277,7 @@ lemma lorentzAction_mapIso (f : X ≃ Y) (Λ : LorentzGroup d) (T : RealLorentzT
   rw [mapIso_apply_coord]
   rw [lorentzAction_smul_coord', lorentzAction_smul_coord']
   let is : IndexValue d T.color ≃ IndexValue d ((mapIso d f) T).color :=
-    indexValueIso d f (by funext x ; simp)
+    indexValueIso d f (by funext x; simp)
   rw [← Equiv.sum_comp is]
   refine Finset.sum_congr rfl (fun j _ => ?_)
   rw [mapIso_apply_coord]

From 73df7d24a7ec50399be54a47fbfc0e10a0a50967 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 17 Jul 2024 16:12:30 -0400
Subject: [PATCH 9/9] refactor: Lint

---
 .../SpaceTime/LorentzTensor/Real/Basic.lean   | 29 +++++----
 .../LorentzTensor/Real/Constructors.lean      | 64 +++++--------------
 .../LorentzTensor/Real/LorentzAction.lean     | 45 ++++++-------
 .../LorentzTensor/Real/Multiplication.lean    | 11 +---
 4 files changed, 53 insertions(+), 96 deletions(-)

diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
index f1249fb..00f48ff 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
@@ -49,7 +49,6 @@ instance (d : ℕ) (μ : RealLorentzTensor.Colors) : DecidableEq (RealLorentzTen
 
 /-- An `IndexValue` is a set of actual values an index can take. e.g. for a
   3-tensor (0, 1, 2). -/
-@[simp]
 def RealLorentzTensor.IndexValue {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Colors) :
     Type 0 := (x : X) → RealLorentzTensor.ColorsIndex d (c x)
 
@@ -91,7 +90,7 @@ def ch {X : Type} (x : X) (T : RealLorentzTensor d X) : Colors := T.color x
 /-- An equivalence of `ColorsIndex` types given an equality of a colors. -/
 def colorsIndexCast {d : ℕ} {μ₁ μ₂ : RealLorentzTensor.Colors} (h : μ₁ = μ₂) :
     ColorsIndex d μ₁ ≃ ColorsIndex d μ₂ :=
-  Equiv.cast (by rw [h])
+  Equiv.cast (congrArg (ColorsIndex d) h)
 
 /-- An equivalence of `ColorsIndex` between that of a color and that of its dual. -/
 def colorsIndexDualCastSelf {d : ℕ} {μ : RealLorentzTensor.Colors}:
@@ -127,7 +126,7 @@ lemma colorsIndexDualCast_symm {μ ν : Colors} (h : μ = τ ν) :
 
 instance [Fintype X] [DecidableEq X] : Fintype (IndexValue d c) := Pi.fintype
 
-instance [Fintype X] [DecidableEq X] : DecidableEq (IndexValue d c) :=
+instance [Fintype X] : DecidableEq (IndexValue d c) :=
   Fintype.decidablePiFintype
 
 /-!
@@ -136,6 +135,7 @@ instance [Fintype X] [DecidableEq X] : DecidableEq (IndexValue d c) :=
 
 -/
 
+/-- An isomorphism of the type of index values given an isomorphism of sets. -/
 @[simps!]
 def indexValueIso (d : ℕ) (f : X ≃ Y) {i : X → Colors} {j : Y → Colors} (h : i = j ∘ f) :
     IndexValue d i ≃ IndexValue d j :=
@@ -155,12 +155,12 @@ lemma indexValueIso_trans (d : ℕ) (f : X ≃ Y) (g : Y ≃ Z) {i : X → Color
   have h1 : ((indexValueIso d f h).trans (indexValueIso d g h')).symm =
       (indexValueIso d (f.trans g) (by rw [h, h', Function.comp.assoc]; rfl)).symm := by
     subst h' h
-    ext x : 2
-    rfl
+    exact Equiv.coe_inj.mp rfl
   simpa only [Equiv.symm_symm] using congrArg (fun e => e.symm) h1
 
 lemma indexValueIso_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) :
-    (indexValueIso d f h).symm = indexValueIso d f.symm (by rw [h, Function.comp.assoc]; simp) := by
+    (indexValueIso d f h).symm =
+    indexValueIso d f.symm ((Equiv.eq_comp_symm f j i).mpr (id (Eq.symm h))) := by
   ext i : 1
   rw [← Equiv.symm_apply_eq]
   funext y
@@ -170,9 +170,10 @@ lemma indexValueIso_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) :
   rw [Equiv.apply_symm_apply]
 
 lemma indexValueIso_eq_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) :
-    indexValueIso d f h = (indexValueIso d f.symm (by rw [h, Function.comp.assoc]; simp)).symm := by
+    indexValueIso d f h =
+    (indexValueIso d f.symm ((Equiv.eq_comp_symm f j i).mpr (id (Eq.symm h)))).symm := by
   rw [indexValueIso_symm]
-  congr
+  rfl
 
 @[simp]
 lemma indexValueIso_refl (d : ℕ) (i : X → Colors) :
@@ -256,10 +257,9 @@ lemma mapIso_trans (f : X ≃ Y) (g : Y ≃ Z) :
   apply congrArg
   rw [← indexValueIso_trans]
   rfl
-  simp only [Function.comp.assoc, Equiv.symm_comp_self, CompTriple.comp_eq]
+  exact (Equiv.comp_symm_eq f (T.color ∘ ⇑f.symm) T.color).mp rfl
 
-lemma mapIso_symm (f : X ≃ Y) : (mapIso d f).symm = mapIso d f.symm := by
-  rfl
+lemma mapIso_symm (f : X ≃ Y) : (mapIso d f).symm = mapIso d f.symm := rfl
 
 lemma mapIso_refl : mapIso d (Equiv.refl X) = Equiv.refl _ := rfl
 
@@ -268,7 +268,7 @@ lemma mapIso_refl : mapIso d (Equiv.refl X) = Equiv.refl _ := rfl
 ## Sums
 
 -/
-
+/-- An equivalence splitting elements of `IndexValue d (Sum.elim TX TY)` into two components. -/
 def indexValueSumEquiv {X Y : Type} {TX : X → Colors} {TY : Y → Colors} :
     IndexValue d (Sum.elim TX TY) ≃ IndexValue d TX × IndexValue d TY where
   toFun i := (fun x => i (Sum.inl x), fun x => i (Sum.inr x))
@@ -330,10 +330,10 @@ instance [Fintype X] (T : Marked d X n) : DecidableEq T.UnmarkedIndexValue :=
 def MarkedIndexValue (T : Marked d X n) : Type :=
   IndexValue d T.markedColor
 
-instance [Fintype X] [DecidableEq X] (T : Marked d X n) : Fintype T.MarkedIndexValue :=
+instance (T : Marked d X n) : Fintype T.MarkedIndexValue :=
   Pi.fintype
 
-instance [Fintype X] (T : Marked d X n) : DecidableEq T.MarkedIndexValue :=
+instance (T : Marked d X n) : DecidableEq T.MarkedIndexValue :=
   Fintype.decidablePiFintype
 
 lemma color_eq_elim (T : Marked d X n) :
@@ -341,6 +341,7 @@ lemma color_eq_elim (T : Marked d X n) :
   ext1 x
   cases' x <;> rfl
 
+/-- An equivalence splitting elements of `IndexValue d T.color` into their two components. -/
 def splitIndexValue {T : Marked d X n} :
     IndexValue d T.color ≃ T.UnmarkedIndexValue × T.MarkedIndexValue :=
   (indexValueIso d (Equiv.refl _) T.color_eq_elim).trans
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean b/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
index e661a9f..a349177 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
@@ -187,24 +187,16 @@ open Marked
 /-- Contracting the indices of `ofMatUpDown` returns the trace of the matrix. -/
 lemma contr_ofMatUpDown_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
     contr (ofMatUpDown M) (by rfl) = ofReal d M.trace := by
-  refine ext ?_ ?_
+  refine ext ?_ rfl
   · funext i
     exact Empty.elim i
-  · funext i
-    simp only [Fin.isValue, contr, IndexValue, Equiv.cast_apply, trace, diag_apply, ofReal,
-      Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
-    apply Finset.sum_congr rfl
-    intro x _
-    rfl
 
 /-- Contracting the indices of `ofMatDownUp` returns the trace of the matrix. -/
 lemma contr_ofMatDownUp_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
     contr (ofMatDownUp M) (by rfl) = ofReal d M.trace := by
-  refine ext ?_ ?_
+  refine ext ?_ rfl
   · funext i
     exact Empty.elim i
-  · funext i
-    rfl
 
 /-!
 
@@ -217,46 +209,38 @@ lemma contr_ofMatDownUp_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1
 lemma mul_ofVecUp_ofVecDown_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d → ℝ) :
     mapIso d (@Equiv.equivEmpty (Empty ⊕ Empty) instIsEmptySum)
     (mul (ofVecUp v₁) (ofVecDown v₂) (by rfl)) = ofReal d (v₁ ⬝ᵥ v₂) := by
-  refine ext ?_ ?_
+  refine ext ?_ rfl
   · funext i
     exact Empty.elim i
-  · funext i
-    rfl
 
 /-- Multiplying `ofVecDown` with `ofVecUp` gives the dot product. -/
 @[simp]
 lemma mul_ofVecDown_ofVecUp_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d → ℝ) :
     mapIso d (Equiv.equivEmpty (Empty ⊕ Empty))
     (mul (ofVecDown v₁) (ofVecUp v₂) rfl) = ofReal d (v₁ ⬝ᵥ v₂) := by
-  refine ext ?_ ?_
+  refine ext ?_ rfl
   · funext i
     exact Empty.elim i
-  · funext i
-    rfl
 
 lemma mul_ofMatUpDown_ofVecUp_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
     (v : Fin 1 ⊕ Fin d → ℝ) :
     mapIso d ((Equiv.sumEmpty (Empty ⊕ Fin 1) Empty))
     (mul (unmarkFirst $ ofMatUpDown M) (ofVecUp v) rfl) = ofVecUp (M *ᵥ v) := by
-  refine ext ?_ ?_
+  refine ext ?_ rfl
   · funext i
     simp only [Nat.succ_eq_add_one, Nat.reduceAdd, mapIso_apply_color, mul_color, Equiv.symm_symm]
     fin_cases i
     rfl
-  · funext i
-    rfl
 
 lemma mul_ofMatDownUp_ofVecDown_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
     (v : Fin 1 ⊕ Fin d → ℝ) :
     mapIso d (Equiv.sumEmpty (Empty ⊕ Fin 1) Empty)
     (mul (unmarkFirst $ ofMatDownUp M) (ofVecDown v) rfl) = ofVecDown (M *ᵥ v) := by
-  refine ext ?_ ?_
+  refine ext ?_ rfl
   · funext i
     simp only [Nat.succ_eq_add_one, Nat.reduceAdd, mapIso_apply_color, mul_color, Equiv.symm_symm]
     fin_cases i
     rfl
-  · funext i
-    rfl
 
 /-!
 
@@ -290,7 +274,7 @@ lemma lorentzAction_ofVecUp (v : Fin 1 ⊕ Fin d → ℝ) :
   intro i
   simp_all only [Finset.mem_univ, Fin.isValue, Equiv.coe_fn_mk]
   intro j _
-  erw [toTensorRepMat_apply, Finset.prod_singleton]
+  simp_all only [Finset.mem_univ, Fin.isValue, Finset.prod_singleton, indexValueIso_refl]
   rfl
 
 /-- The action of the Lorentz group on `ofVecDown v` is
@@ -310,7 +294,7 @@ lemma lorentzAction_ofVecDown (v : Fin 1 ⊕ Fin d → ℝ) :
   intro i
   simp_all only [Finset.mem_univ, Fin.isValue, Equiv.coe_fn_mk]
   intro j _
-  erw [toTensorRepMat_apply, Finset.prod_singleton]
+  simp_all only [Finset.mem_univ, Fin.isValue, Finset.prod_singleton, indexValueIso_refl]
   rfl
 
 @[simp]
@@ -327,12 +311,8 @@ lemma lorentzAction_ofMatUpUp (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) 
   refine Finset.sum_congr rfl (fun x _ => ?_)
   rw [Finset.sum_mul]
   refine Finset.sum_congr rfl (fun y _ => ?_)
-  erw [toTensorRepMat_apply]
-  simp only [Fintype.prod_sum_type, Finset.univ_eq_empty, Finset.prod_empty, Fin.prod_univ_two,
-    Fin.isValue, one_mul, indexValueIso_refl, IndexValue]
-  simp only [colorMatrix, Fin.isValue, MonoidHom.coe_mk, OneHom.coe_mk]
-  rw [mul_assoc, mul_comm _ (M _ _), ← mul_assoc]
-  congr
+  simp only [Fin.prod_univ_two, Fin.isValue, indexValueIso_refl, IndexValue]
+  exact mul_right_comm _ _ _
 
 @[simp]
 lemma lorentzAction_ofMatDownDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
@@ -348,12 +328,8 @@ lemma lorentzAction_ofMatDownDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d
   refine Finset.sum_congr rfl (fun x _ => ?_)
   rw [Finset.sum_mul]
   refine Finset.sum_congr rfl (fun y _ => ?_)
-  erw [toTensorRepMat_apply]
-  simp only [Fintype.prod_sum_type, Finset.univ_eq_empty, Finset.prod_empty, Fin.prod_univ_two,
-    Fin.isValue, one_mul, lorentzGroupIsGroup_inv, indexValueIso_refl, IndexValue]
-  simp only [colorMatrix, Fin.isValue, MonoidHom.coe_mk, OneHom.coe_mk]
-  rw [mul_assoc, mul_comm _ (M _ _), ← mul_assoc]
-  congr
+  simp only [Fin.prod_univ_two, Fin.isValue, indexValueIso_refl, IndexValue]
+  exact mul_right_comm _ _ _
 
 @[simp]
 lemma lorentzAction_ofMatUpDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
@@ -369,12 +345,8 @@ lemma lorentzAction_ofMatUpDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)
   refine Finset.sum_congr rfl (fun x _ => ?_)
   rw [Finset.sum_mul]
   refine Finset.sum_congr rfl (fun y _ => ?_)
-  erw [toTensorRepMat_apply]
-  simp only [Fintype.prod_sum_type, Finset.univ_eq_empty, Finset.prod_empty, Fin.prod_univ_two,
-    Fin.isValue, one_mul, indexValueIso_refl, IndexValue, lorentzGroupIsGroup_inv]
-  simp only [colorMatrix, Fin.isValue, MonoidHom.coe_mk, OneHom.coe_mk]
-  rw [mul_assoc, mul_comm _ (M _ _), ← mul_assoc]
-  congr
+  simp only [Fin.prod_univ_two, Fin.isValue, indexValueIso_refl, IndexValue]
+  exact mul_right_comm _ _ _
 
 @[simp]
 lemma lorentzAction_ofMatDownUp (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
@@ -391,12 +363,8 @@ lemma lorentzAction_ofMatDownUp (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)
   refine Finset.sum_congr rfl (fun x _ => ?_)
   rw [Finset.sum_mul]
   refine Finset.sum_congr rfl (fun y _ => ?_)
-  erw [toTensorRepMat_apply]
-  simp only [Fintype.prod_sum_type, Finset.univ_eq_empty, Finset.prod_empty, Fin.prod_univ_two,
-    Fin.isValue, one_mul, lorentzGroupIsGroup_inv, indexValueIso_refl, IndexValue]
-  simp only [colorMatrix, Fin.isValue, MonoidHom.coe_mk, OneHom.coe_mk]
-  rw [mul_assoc, mul_comm _ (M _ _), ← mul_assoc]
-  congr
+  simp only [Fin.prod_univ_two, Fin.isValue, indexValueIso_refl, IndexValue]
+  exact mul_right_comm _ _ _
 
 end lorentzAction
 
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
index a565058..eee0dff 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
@@ -84,6 +84,7 @@ lemma colorMatrix_transpose {μ : Colors} (Λ : LorentzGroup d) :
 
 -/
 
+/-- The matrix representation of the Lorentz group given a color of index. -/
 @[simps!]
 def toTensorRepMat {c : X → Colors} :
     LorentzGroup d →* Matrix (IndexValue d c) (IndexValue d c) ℝ where
@@ -109,40 +110,33 @@ def toTensorRepMat {c : X → Colors} :
         ∏ x, ∑ y, (colorMatrix (c x) Λ (i x) y) * (colorMatrix (c x) Λ' y (j x)) := by
       rw [Finset.prod_sum]
       simp only [Finset.prod_attach_univ, Finset.sum_univ_pi]
-      apply Finset.sum_congr
-      simp only [IndexValue, Fintype.piFinset_univ]
-      intro x _
       rfl
     rw [h1]
     simp only [map_mul]
-    exact Finset.prod_congr rfl (fun x _ => rfl)
+    rfl
     refine Finset.sum_congr rfl (fun k _ => ?_)
     rw [Finset.prod_mul_distrib]
 
 lemma toTensorRepMat_mul' (i j : IndexValue d c) :
     toTensorRepMat (Λ * Λ') i j = ∑ (k : IndexValue d c),
     ∏ x, colorMatrix (c x) Λ (i x) (k x) * colorMatrix (c x) Λ' (k x) (j x) := by
-  simp [Matrix.mul_apply]
+  simp [Matrix.mul_apply, IndexValue]
   refine Finset.sum_congr rfl (fun k _ => ?_)
   rw [Finset.prod_mul_distrib]
   rfl
 
-@[simp]
 lemma toTensorRepMat_of_indexValueSumEquiv {cX : X → Colors} {cY : Y → Colors}
     (i j : IndexValue d (Sum.elim cX cY)) :
     toTensorRepMat Λ i j = toTensorRepMat Λ (indexValueSumEquiv i).1 (indexValueSumEquiv j).1 *
-    toTensorRepMat Λ (indexValueSumEquiv i).2 (indexValueSumEquiv j).2 := by
-  simp only [toTensorRepMat_apply]
-  rw [Fintype.prod_sum_type]
-  rfl
+    toTensorRepMat Λ (indexValueSumEquiv i).2 (indexValueSumEquiv j).2 :=
+  Fintype.prod_sum_type fun x => (colorMatrix (Sum.elim cX cY x)) Λ (i x) (j x)
 
 lemma toTensorRepMat_of_indexValueSumEquiv' {cX : X → Colors} {cY : Y → Colors}
     (i j : IndexValue d cX) (k l : IndexValue d cY) :
     toTensorRepMat Λ i j * toTensorRepMat Λ k l =
-    toTensorRepMat Λ (indexValueSumEquiv.symm (i, k)) (indexValueSumEquiv.symm (j, l)) := by
-  simp only [toTensorRepMat_apply]
-  rw [Fintype.prod_sum_type]
-  rfl
+    toTensorRepMat Λ (indexValueSumEquiv.symm (i, k)) (indexValueSumEquiv.symm (j, l)) :=
+  (Fintype.prod_sum_type fun x => (colorMatrix (Sum.elim cX cY x)) Λ
+    (indexValueSumEquiv.symm (i, k) x) (indexValueSumEquiv.symm (j, l) x)).symm
 
 /-!
 
@@ -153,10 +147,9 @@ lemma toTensorRepMat_of_indexValueSumEquiv' {cX : X → Colors} {cY : Y → Colo
 lemma toTensorRepMat_of_splitIndexValue' (T : Marked d X n)
     (i j : T.UnmarkedIndexValue) (k l : T.MarkedIndexValue) :
     toTensorRepMat Λ i j * toTensorRepMat Λ k l =
-    toTensorRepMat Λ (splitIndexValue.symm (i, k)) (splitIndexValue.symm (j, l)) := by
-  simp only [toTensorRepMat_apply]
-  rw [Fintype.prod_sum_type]
-  rfl
+    toTensorRepMat Λ (splitIndexValue.symm (i, k)) (splitIndexValue.symm (j, l)) :=
+  (Fintype.prod_sum_type fun x =>
+  (colorMatrix (T.color x)) Λ (splitIndexValue.symm (i, k) x) (splitIndexValue.symm (j, l) x)).symm
 
 lemma toTensorRepMat_oneMarkedIndexValue_dual (T : Marked d X 1) (S : Marked d Y 1)
     (h : T.markedColor 0 = τ (S.markedColor 0)) (x : ColorsIndex d (T.markedColor 0))
@@ -201,7 +194,7 @@ lemma toTensorRepMat_one_coord_sum (T : Marked d X n) (i : T.UnmarkedIndexValue)
   simp only [IndexValue, map_one, Matrix.one_apply_eq, one_mul]
   exact Finset.mem_univ k
   intro j _ hjk
-  simp [hjk]
+  simp [hjk, IndexValue]
   exact Or.inl (Matrix.one_apply_ne' hjk)
 
 /-!
@@ -264,10 +257,8 @@ lemma lorentzAction_on_isEmpty [IsEmpty X] (Λ : LorentzGroup d) (T : RealLorent
   erw [lorentzAction_smul_coord]
   simp only [Finset.univ_unique, Finset.univ_eq_empty, Finset.prod_empty, one_mul,
     Finset.sum_singleton, toTensorRepMat_apply]
-  erw [toTensorRepMat_apply]
-  simp only [IndexValue, toTensorRepMat, Unique.eq_default]
-  rw [@mul_left_eq_self₀]
-  exact Or.inl rfl
+  simp only [IndexValue, Unique.eq_default, Finset.univ_unique, Finset.sum_const,
+    Finset.card_singleton, one_smul]
 
 /-- The Lorentz action commutes with `mapIso`. -/
 lemma lorentzAction_mapIso (f : X ≃ Y) (Λ : LorentzGroup d) (T : RealLorentzTensor d X) :
@@ -277,7 +268,7 @@ lemma lorentzAction_mapIso (f : X ≃ Y) (Λ : LorentzGroup d) (T : RealLorentzT
   rw [mapIso_apply_coord]
   rw [lorentzAction_smul_coord', lorentzAction_smul_coord']
   let is : IndexValue d T.color ≃ IndexValue d ((mapIso d f) T).color :=
-    indexValueIso d f (by funext x; simp)
+    indexValueIso d f ((Equiv.comp_symm_eq f ((mapIso d f) T).color T.color).mp rfl)
   rw [← Equiv.sum_comp is]
   refine Finset.sum_congr rfl (fun j _ => ?_)
   rw [mapIso_apply_coord]
@@ -299,8 +290,7 @@ lemma lorentzAction_mapIso (f : X ≃ Y) (Λ : LorentzGroup d) (T : RealLorentzT
     congr
     exact Equiv.symm_apply_apply f x
   · apply congrArg
-    funext a
-    simp only [IndexValue, mapIso_apply_color, Equiv.symm_apply_apply, is]
+    exact (Equiv.apply_eq_iff_eq_symm_apply (indexValueIso d f (mapIso.proof_1 d f T))).mp rfl
 
 /-!
 
@@ -395,7 +385,10 @@ def unmarkedLorentzAction : MulAction (LorentzGroup d) (Marked d X n) where
     rw [Finset.prod_mul_distrib]
     rfl
 
+/-- Notation for `markedLorentzAction.smul`. -/
 scoped[RealLorentzTensor] infixr:73 " •ₘ " => markedLorentzAction.smul
+
+/-- Notation for `unmarkedLorentzAction.smul`. -/
 scoped[RealLorentzTensor] infixr:73 " •ᵤₘ " => unmarkedLorentzAction.smul
 
 /-- Acting on unmarked and then marked indices is equivalent to acting on all indices. -/
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean b/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
index fdd9fcb..0c1b5bb 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
@@ -72,15 +72,10 @@ lemma mul_mapIso {X Y Z : Type} (T : Marked d X 1) (S : Marked d Y 1) (f : X ≃
     rw [mapIso_apply_coord, mapIso_apply_coord]
     refine Mathlib.Tactic.Ring.mul_congr ?_ ?_ rfl
     · apply congrArg
-      ext1 r
-      cases r with
-      | inl val => rfl
-      | inr val_1 => rfl
+      simp only [IndexValue]
+      exact (Equiv.symm_apply_eq splitIndexValue).mpr rfl
     · apply congrArg
-      ext1 r
-      cases r with
-      | inl val => rfl
-      | inr val_1 => rfl
+      exact (Equiv.symm_apply_eq splitIndexValue).mpr rfl
 
 /-!