feat: Doing tensors generally

2024-07-25 16:57:57 -04:00 · 2024-07-25 16:57:57 -04:00 · 0f4092e0ec
commit 0f4092e0ec
parent 23e041295f
11 changed files with 1408 additions and 1479 deletions
--- a/HepLean/Mathematics/PiTensorProduct.lean
+++ b/HepLean/Mathematics/PiTensorProduct.lean
@ -0,0 +1,367 @@
 /-
 Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import Mathlib.LinearAlgebra.DirectSum.Finsupp
 import Mathlib.RingTheory.PiTensorProduct
 import Mathlib.Algebra.DirectSum.Module
 import Mathlib.LinearAlgebra.Multilinear.Basic
 import Mathlib.LinearAlgebra.FinsuppVectorSpace
 /-!
 # Pi Tensor Products
 This file contains some proofs regarding Pi tensor products authored by Sophie Morel
 in this Mathlib pull-request:
 https://github.com/leanprover-community/mathlib4/pull/11156
 Once this pull request has being merged, this file will be deleted.
 -/
 noncomputable section
 namespace MultilinearMap
 open DirectSum LinearMap BigOperators Function
 variable (R : Type*) [CommSemiring R]
 variable {ι : Type*} [Fintype ι] [DecidableEq ι]
 variable (κ : ι → Type*) [(i : ι) → DecidableEq (κ i)]
 variable {M : (i : ι) → κ i → Type*} {M' : Type*}
 variable [Π i (j : κ i), AddCommMonoid (M i j)] [AddCommMonoid M']
 variable [Π i (j : κ i), Module R (M i j)] [Module R M']
 variable [Π i (j : κ i) (x : M i j), Decidable (x ≠ 0)]
 theorem fromDirectSum_aux1 (f : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) M')
    (x : Π i, ⨁ (j : κ i), M i j) {p : Π i, κ i}
    (hp : p ∉ Fintype.piFinset (fun i ↦ (x i).support)) :
    (f p) (fun j ↦ (x j) (p j)) = 0 := by
  simp only [Fintype.mem_piFinset, DFinsupp.mem_support_toFun, ne_eq, not_forall, not_not] at hp
  obtain ⟨i, hi⟩ := hp
  exact (f p).map_coord_zero i hi
 theorem fromDirectSum_aux2 (x : Π i, ⨁ (j : κ i), M i j) (i : ι) (p : Π i, κ i)
    (a : ⨁ (j : κ i), M i j) :
    (fun j ↦ (update x i a j) (p j)) = update (fun j ↦ x j (p j)) i (a (p i)) := by
  ext j
  by_cases h : j =i
  · rw [h]; simp only [update_same]
  · simp only [ne_eq, h, not_false_eq_true, update_noteq]
 /-- Given a family indexed by `p : Π i : ι, κ i` of multilinear maps on the
 `fun i ↦ M i (p i)`, construct a multilinear map on `fun i ↦ ⨁ j : κ i, M i j`.-/
 def fromDirectSum (f : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) M') :
    MultilinearMap R (fun i ↦ ⨁ j : κ i, M i j) M' where
  toFun x := ∑ p in Fintype.piFinset (fun i ↦ (x i).support), f p (fun i ↦ x i (p i))
  map_add' x i a b := by
    simp only
    rename_i myinst _ _ _ _ _ _ _
    conv_lhs => rw [← Finset.sum_union_eq_right (s₁ := @Fintype.piFinset _ myinst _ _
        (fun j ↦ (update x i a j).support)
        ∪ @Fintype.piFinset _ myinst _ _ (fun j ↦ (update x i b j).support))
        (fun p _ hp ↦ by
          letI := myinst
          exact fromDirectSum_aux1 _ _ f _ hp)]
    rw [Finset.sum_congr rfl (fun p _ ↦ by rw [fromDirectSum_aux2 _ _ _ p (a + b)])]
    erw [Finset.sum_congr rfl (fun p _ ↦ (f p).map_add _ i (a (p i)) (b (p i)))]
    rw [Finset.sum_add_distrib]
    congr 1
    · conv_lhs => rw [← Finset.sum_congr rfl (fun p _ ↦ by rw [← fromDirectSum_aux2 _ _ _ p a]),
                    Finset.sum_congr (Finset.union_assoc _ _ _) (fun _ _ ↦ rfl)]
      rw [Finset.sum_union_eq_left (fun p _ hp ↦ by
        letI := myinst
        exact fromDirectSum_aux1 _ _ f _ hp)]
    · conv_lhs => rw [← Finset.sum_congr rfl (fun p _ ↦ by rw [← fromDirectSum_aux2 _ _ _ p b]),
        Finset.sum_congr (Finset.union_assoc _ _ _) (fun _ _ ↦ rfl),
        Finset.sum_congr (Finset.union_comm _ _) (fun _ _ ↦ rfl),
        Finset.sum_congr (Finset.union_assoc _ _ _) (fun _ _ ↦ rfl)]
      rw [Finset.sum_union_eq_left (fun p _ hp ↦ by
        letI := myinst
        exact fromDirectSum_aux1 _ _ f _ hp)]
  map_smul' x i c a := by
    simp only
    rename_i myinst _ _ _ _ _ _ _
    conv_lhs => rw [← Finset.sum_union_eq_right (s₁ := @Fintype.piFinset _ myinst _ _
      (fun j ↦ (update x i a j).support))
        (fun p _ hp ↦ by
          letI := myinst
          exact fromDirectSum_aux1 _ _ f _ hp),
      Finset.sum_congr rfl (fun p _ ↦ by rw [fromDirectSum_aux2 _ _ _ p _])]
    erw [Finset.sum_congr rfl (fun p _ ↦ (f p).map_smul _ i c (a (p i)))]
    rw [← Finset.smul_sum]
    conv_lhs => rw [← Finset.sum_congr rfl (fun p _ ↦ by rw [← fromDirectSum_aux2 _ _ _ p _]),
      Finset.sum_union_eq_left (fun p _ hp ↦ by
          letI := myinst
          exact fromDirectSum_aux1 _ _ f _ hp)]
@[simp]
 theorem fromDirectSum_apply (f : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) M')
    (x : Π i, ⨁ (j : κ i), M i j) : fromDirectSum R κ f x =
    ∑ p in Fintype.piFinset (fun i ↦ (x i).support), f p (fun i ↦ x i (p i)) := rfl
 /-- The construction `MultilinearMap.fromDirectSum`, as an `R`-linear map.-/
 def fromDirectSumₗ : ((p : Π i, κ i) → MultilinearMap R (fun i ↦ M i (p i)) M') →ₗ[R]
    MultilinearMap R (fun i ↦ ⨁ j : κ i, M i j) M' where
  toFun := fromDirectSum R κ
  map_add' f g := by
    ext x
    simp only [fromDirectSum_apply, Pi.add_apply, MultilinearMap.add_apply]
    rw [Finset.sum_add_distrib]
  map_smul' c f := by
    ext x
    simp only [fromDirectSum_apply, Pi.smul_apply, MultilinearMap.smul_apply, RingHom.id_apply]
    rw [Finset.smul_sum]
@[simp]
 theorem fromDirectSumₗ_apply (f : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) M')
    (x : Π i, ⨁ (j : κ i), M i j) : fromDirectSumₗ R κ f x =
    ∑ p in Fintype.piFinset (fun i ↦ (x i).support), f p (fun i ↦ x i (p i)) := rfl
 theorem _root_.piFinset_support_lof_sub (p : Π i, κ i) (a : Π i, M i (p i)) :
    Fintype.piFinset (fun i ↦ DFinsupp.support (lof R (κ i) (M i) (p i) (a i))) ⊆ {p} := by
  intro q
  simp only [Fintype.mem_piFinset, ne_eq, Finset.mem_singleton]
  simp_rw [DirectSum.lof_eq_of]
  exact fun hq ↦ funext fun i ↦ Finset.mem_singleton.mp (DirectSum.support_of_subset _ (hq i))
 /-- The linear equivalence between families indexed by `p : Π i : ι, κ i` of multilinear maps
 on the `fun i ↦ M i (p i)` and the space of multilinear map on `fun i ↦ ⨁ j : κ i, M i j`.-/
 def fromDirectSumEquiv : ((p : Π i, κ i) → MultilinearMap R (fun i ↦ M i (p i)) M') ≃ₗ[R]
    MultilinearMap R (fun i ↦ ⨁ j : κ i, M i j) M' := by
  refine LinearEquiv.ofLinear (fromDirectSumₗ R κ) (LinearMap.pi
    (fun p ↦ MultilinearMap.compLinearMapₗ (fun i ↦ DirectSum.lof R (κ i) _ (p i)))) ?_ ?_
  · ext f x
    simp only [coe_comp, Function.comp_apply, fromDirectSumₗ_apply, pi_apply,
      MultilinearMap.compLinearMapₗ_apply, MultilinearMap.compLinearMap_apply, id_coe, id_eq]
    change _ = f (fun i ↦ x i)
    rw [funext (fun i ↦ Eq.symm (DirectSum.sum_support_of (fun j ↦ M i j) (x i)))]
    rw [MultilinearMap.map_sum_finset]
    sorry
  · ext f p a
    simp only [coe_comp, Function.comp_apply, LinearMap.pi_apply, compLinearMapₗ_apply,
      compLinearMap_apply, fromDirectSumₗ_apply, id_coe, id_eq]
    rw [Finset.sum_subset (piFinset_support_lof_sub R κ p a)]
    · rw [Finset.sum_singleton]
      simp only [lof_apply]
    · simp only [Finset.mem_singleton, Fintype.mem_piFinset, DFinsupp.mem_support_toFun, ne_eq,
        not_forall, not_not, forall_exists_index, forall_eq, lof_apply]
      intro i hi
      exact (f p).map_coord_zero i hi
@[simp]
 theorem fromDirectSumEquiv_apply (f : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) M')
    (x : Π i, ⨁ (j : κ i), M i j) : fromDirectSumEquiv R κ f x =
    ∑ p in Fintype.piFinset (fun i ↦ (x i).support), f p (fun i ↦ x i (p i)) := rfl
@[simp]
 theorem fromDirectSumEquiv_symm_apply (f : MultilinearMap R (fun i ↦ ⨁ j : κ i, M i j) M')
    (p : Π i, κ i) : (fromDirectSumEquiv R κ).symm f p =
    f.compLinearMap (fun i ↦ DirectSum.lof R (κ i) _ (p i)) := rfl
 end MultilinearMap
 namespace PiTensorProduct
 open PiTensorProduct DirectSum LinearMap
 open scoped TensorProduct
 variable (R : Type*) [CommSemiring R]
 variable {ι : Type*} [Fintype ι] [DecidableEq ι]
 variable {κ : ι → Type*} [(i : ι) → DecidableEq (κ i)]
 variable (M : (i : ι) → κ i → Type*) (M' : Type*)
 variable [Π i (j : κ i), AddCommMonoid (M i j)] [AddCommMonoid M']
 variable [Π i (j : κ i), Module R (M i j)] [Module R M']
 variable [Π i (j : κ i) (x : M i j),  Decidable (x ≠ 0)]
 /-- The linear equivalence `⨂[R] i, (⨁ j : κ i, M i j) ≃ ⨁ p : (i : ι) → κ i, ⨂[R] i, M i (p i)`,
 i.e. "tensor product distributes over direct sum". -/
 protected def directSum :
    (⨂[R] i, (⨁ j : κ i, M i j)) ≃ₗ[R] ⨁ p : Π i, κ i, ⨂[R] i, M i (p i) := by
  refine LinearEquiv.ofLinear (R := R) (R₂ := R) ?toFun ?invFun ?left ?right
  · exact lift (MultilinearMap.fromDirectSumEquiv R (M := M)
      (fun p ↦ (DirectSum.lof R _ _ p).compMultilinearMap (PiTensorProduct.tprod R)))
  · exact DirectSum.toModule R _ _ (fun p ↦ lift (LinearMap.compMultilinearMap
      (PiTensorProduct.map (fun i ↦ DirectSum.lof R _ _ (p i))) (tprod R)))
  · ext p x
    simp only [compMultilinearMap_apply, coe_comp, Function.comp_apply, toModule_lof, lift.tprod,
      map_tprod, MultilinearMap.fromDirectSumEquiv_apply, id_comp]
    rw [Finset.sum_subset (piFinset_support_lof_sub R κ p x)]
    · rw [Finset.sum_singleton]
      simp only [lof_apply]
    · simp only [Finset.mem_singleton, Fintype.mem_piFinset, DFinsupp.mem_support_toFun, ne_eq,
        not_forall, not_not, forall_exists_index, forall_eq, lof_apply]
      intro i hi
      rw [(tprod R).map_coord_zero i hi, LinearMap.map_zero]
  · ext x
    simp only [compMultilinearMap_apply, coe_comp, Function.comp_apply, lift.tprod,
      MultilinearMap.fromDirectSumEquiv_apply, map_sum, toModule_lof, map_tprod, id_coe, id_eq]
    change _ = tprod R (fun i ↦ x i)
    rw [funext (fun i ↦ Eq.symm (DirectSum.sum_support_of (fun j ↦ M i j) (x i)))]
    rw [MultilinearMap.map_sum_finset]
    sorry
 end PiTensorProduct
 /-!
 The case of `PiTensorProduct`.
 -/
 open DirectSum Set LinearMap Submodule TensorProduct
 section PiTensorProduct
 open PiTensorProduct BigOperators
 attribute [local ext] TensorProduct.ext
 variable (R : Type*) [CommSemiring R]
 variable {ι : Type*}
 variable [Fintype ι]
 variable [DecidableEq ι]
 variable (κ : ι → Type*) [(i : ι) → DecidableEq (κ i)]
 variable (M : ι → Type*)
 variable [∀ i, AddCommMonoid (M i)]
 variable [∀ i, Module R (M i)]
 variable [(i : ι) → (x : M i) → Decidable (x ≠ 0)]
 /-- If `ι` is a `Fintype`, `κ i` is a family of types indexed by `ι` and `M i` is a family
 of modules indexed by `ι`, then the tensor product of the family `κ i →₀ M i` is linearly
 equivalent to `∏ i, κ i →₀ ⨂[R] i, M i`.
 -/
 def finsuppPiTensorProduct : (⨂[R] i, κ i →₀ M i) ≃ₗ[R] ((i : ι) → κ i) →₀ ⨂[R] i, M i :=
  PiTensorProduct.congr (fun i ↦ finsuppLEquivDirectSum R (M i) (κ i)) ≪≫ₗ
  (PiTensorProduct.directSum R (fun (i : ι) ↦ fun (_ : κ i) ↦ M i)) ≪≫ₗ
  (finsuppLEquivDirectSum R (⨂[R] i, M i) ((i : ι) → κ i)).symm
@[simp]
 theorem finsuppPiTensorProduct_single (p : (i : ι) → κ i) (m : (i : ι) → M i) :
    finsuppPiTensorProduct R κ M (⨂ₜ[R] i, Finsupp.single (p i) (m i)) =
    Finsupp.single p (⨂ₜ[R] i, m i) := by
  classical
  simp only [finsuppPiTensorProduct, PiTensorProduct.directSum, LinearEquiv.trans_apply,
    congr_tprod, finsuppLEquivDirectSum_single, LinearEquiv.ofLinear_apply, lift.tprod,
    MultilinearMap.fromDirectSumEquiv_apply, compMultilinearMap_apply, map_sum,
    finsuppLEquivDirectSum_symm_lof]
  rw [Finset.sum_subset (piFinset_support_lof_sub R κ p _)]
  · rw [Finset.sum_singleton]
    simp only [lof_apply]
  · intro q _ hq
    simp only [Fintype.mem_piFinset, DFinsupp.mem_support_toFun, ne_eq, not_forall, not_not] at hq
    obtain ⟨i, hi⟩ := hq
    simp only [Finsupp.single_eq_zero]
    exact (tprod R).map_coord_zero i hi
@[simp]
 theorem finsuppPiTensorProduct_apply (f : (i : ι) → (κ i →₀ M i)) (p : (i : ι) → κ i) :
    finsuppPiTensorProduct R κ M (⨂ₜ[R] i, f i) p = ⨂ₜ[R] i, f i (p i) := by
  rw [congrArg (tprod R) (funext (fun i ↦ (Eq.symm (Finsupp.sum_single (f i)))))]
  erw [MultilinearMap.map_sum_finset (tprod R)]
  simp only [map_sum, finsuppPiTensorProduct_single]
  rw [Finset.sum_apply']
  rw [← Finset.sum_union_eq_right (s₁ := {p}) (fun _ _ h ↦ by
       simp only [Fintype.mem_piFinset, Finsupp.mem_support_iff, ne_eq, not_forall, not_not] at h
       obtain ⟨i, hi⟩ := h
       rw [(tprod R).map_coord_zero i hi, Finsupp.single_zero, Finsupp.coe_zero, Pi.zero_apply]),
   Finset.sum_union_eq_left (fun _ _ h ↦ Finsupp.single_eq_of_ne (Finset.not_mem_singleton.mp h)),
   Finset.sum_singleton, Finsupp.single_eq_same]
@[simp]
 theorem finsuppPiTensorProduct_symm_single (p : (i : ι) → κ i) (m : (i : ι) → M i) :
    (finsuppPiTensorProduct R κ M).symm (Finsupp.single p (⨂ₜ[R] i, m i)) =
    ⨂ₜ[R] i, Finsupp.single (p i) (m i) :=
  (LinearEquiv.symm_apply_eq _).2 (finsuppPiTensorProduct_single _ _ _ _ _).symm
 variable [(x : R) → Decidable (x ≠ 0)]
 /-- A variant of `finsuppPiTensorProduct` where all modules `M i` are the ground ring.
 -/
 def finsuppPiTensorProduct' : (⨂[R] i, (κ i →₀ R)) ≃ₗ[R] ((i : ι) → κ i) →₀ R :=
  finsuppPiTensorProduct R κ (fun _ ↦ R) ≪≫ₗ
  Finsupp.lcongr (Equiv.refl ((i : ι) → κ i)) (constantBaseRingEquiv ι R).toLinearEquiv
@[simp]
 theorem finsuppPiTensorProduct'_apply_apply (f : (i : ι) → κ i →₀ R) (p : (i : ι) → κ i) :
    finsuppPiTensorProduct' R κ (⨂ₜ[R] i, f i) p = ∏ i, f i (p i) := by
  simp only [finsuppPiTensorProduct', LinearEquiv.trans_apply, Finsupp.lcongr_apply_apply,
    Equiv.refl_symm, Equiv.refl_apply, finsuppPiTensorProduct_apply, AlgEquiv.toLinearEquiv_apply,
    constantBaseRingEquiv_tprod]
@[simp]
 theorem finsuppPiTensorProduct'_tprod_single (p : (i : ι) → κ i) (r : ι → R) :
    finsuppPiTensorProduct' R κ (⨂ₜ[R] i, Finsupp.single (p i) (r i)) =
    Finsupp.single p (∏ i, r i) := by
  ext q
  simp only [finsuppPiTensorProduct'_apply_apply]
  by_cases h : q = p
  · rw [h]; simp only [Finsupp.single_eq_same]
  · obtain ⟨i, hi⟩ := Function.ne_iff.mp h
    rw [Finsupp.single_eq_of_ne (Ne.symm h), Finset.prod_eq_zero (Finset.mem_univ i)
      (by rw [(Finsupp.single_eq_of_ne (Ne.symm hi))])]
 end PiTensorProduct
 section PiTensorProduct
 open PiTensorProduct BigOperators
 attribute [local ext] PiTensorProduct.ext
 open LinearMap
 open scoped TensorProduct
 variable {ι R : Type*} [CommSemiring R]
 variable {M : ι → Type*} [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]
 variable {κ : ι → Type*}
 variable [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (κ i)] [(x : R) → Decidable (x ≠ 0)]
 /-- Let `ι` be a `Fintype` and `M` be a family of modules indexed by `ι`. If `b i : κ i → M i`
 is a basis for every `i` in `ι`, then `fun (p : Π i, κ i) ↦ ⨂ₜ[R] i, b i (p i)` is a basis
 of `⨂[R] i, M i`.
 -/
 def Basis.piTensorProduct (b : Π i, Basis (κ i) R (M i)) :
    Basis (Π i, κ i) R (⨂[R] i, M i) :=
  Finsupp.basisSingleOne.map
    ((PiTensorProduct.congr (fun i ↦ (b i).repr)).trans <|
        (finsuppPiTensorProduct R _ _).trans <|
          Finsupp.lcongr (Equiv.refl _) (constantBaseRingEquiv _ R).toLinearEquiv).symm
 theorem Basis.piTensorProduct_apply (b : Π i, Basis (κ i) R (M i)) (p : Π i, κ i) :
    Basis.piTensorProduct b p = ⨂ₜ[R] i, (b i) (p i) := by
  simp only [piTensorProduct, LinearEquiv.trans_symm, Finsupp.lcongr_symm, Equiv.refl_symm,
    AlgEquiv.toLinearEquiv_symm, map_apply, Finsupp.coe_basisSingleOne, LinearEquiv.trans_apply,
    Finsupp.lcongr_single, Equiv.refl_apply, AlgEquiv.toLinearEquiv_apply, _root_.map_one]
  apply LinearEquiv.injective (PiTensorProduct.congr (fun i ↦ (b i).repr))
  simp only [LinearEquiv.apply_symm_apply, congr_tprod, repr_self]
  apply LinearEquiv.injective (finsuppPiTensorProduct R κ fun _ ↦ R)
  simp only [LinearEquiv.apply_symm_apply, finsuppPiTensorProduct_single]
  rfl
 end PiTensorProduct
--- a/HepLean/SpaceTime/LorentzTensor/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Basic.lean
@ -0,0 +1,430 @@
 /-
 Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import Mathlib.Logic.Function.CompTypeclasses
 import Mathlib.Data.Real.Basic
 import Mathlib.Data.Fintype.BigOperators
 import Mathlib.Logic.Equiv.Fin
 import Mathlib.Tactic.FinCases
 import Mathlib.Logic.Equiv.Fintype
 import Mathlib.Algebra.Module.Pi
 import Mathlib.Algebra.Module.Equiv
 import Mathlib.Algebra.Module.LinearMap.Basic
 import Mathlib.LinearAlgebra.TensorProduct.Basic
 import Mathlib.LinearAlgebra.TensorProduct.Basis
 import Mathlib.LinearAlgebra.PiTensorProduct
 import Mathlib.RepresentationTheory.Basic
 /-!
 # Structure of Lorentz Tensors
 In this file we set up the basic structures we will use to define Lorentz tensors.
 ## References
 -- For modular operads see: [Raynor][raynor2021graphical]
 -/
 noncomputable section
 open TensorProduct
 variable {R : Type} [CommSemiring R]
 structure PreTensorStructure (R : Type) [CommSemiring R] where
  Color : Type
  ColorModule : Color → Type
  τ : Color → Color
  τ_involutive : Function.Involutive τ
  colorModule_addCommMonoid : ∀ μ, AddCommMonoid (ColorModule μ)
  colorModule_module : ∀ μ, Module R (ColorModule μ)
  contrDual : ∀ μ, ColorModule μ ⊗[R] ColorModule (τ μ) →ₗ[R] R
 namespace PreTensorStructure
 variable (𝓣 : PreTensorStructure R)
 variable {d : ℕ} {X Y Y' Z : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
  [Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z]
  {c c₂ : X → 𝓣.Color}  {d : Y → 𝓣.Color} {b : Z → 𝓣.Color}  {d' : Y' → 𝓣.Color}  {μ ν: 𝓣.Color}
 instance : AddCommMonoid (𝓣.ColorModule μ) := 𝓣.colorModule_addCommMonoid μ
 instance : Module R (𝓣.ColorModule μ) := 𝓣.colorModule_module μ
 def Tensor (c : X → 𝓣.Color): Type := ⨂[R] x, 𝓣.ColorModule (c x)
 instance : AddCommMonoid (𝓣.Tensor c) :=
  PiTensorProduct.instAddCommMonoid fun i => 𝓣.ColorModule (c i)
 instance : Module R (𝓣.Tensor c) := PiTensorProduct.instModule
 def colorModuleCast (h : μ = ν) : 𝓣.ColorModule μ ≃ₗ[R] 𝓣.ColorModule ν where
  toFun x := Equiv.cast (congrArg 𝓣.ColorModule h) x
  invFun x := (Equiv.cast (congrArg 𝓣.ColorModule h)).symm x
  map_add' x y := by
    subst h
    rfl
  map_smul' x y := by
    subst h
    rfl
  left_inv x := by
    subst h
    rfl
  right_inv x := by
    subst h
    rfl
 /-!
 ## Mapping isomorphisms
 -/
 def mapIso {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = d ∘ e) :
    𝓣.Tensor c ≃ₗ[R] 𝓣.Tensor d :=
  (PiTensorProduct.reindex R _ e) ≪≫ₗ
  (PiTensorProduct.congr (fun y => 𝓣.colorModuleCast (by rw [h]; simp)))
 lemma mapIso_trans_cond {e : X ≃ Y} {e' : Y ≃ Z} (h : c = d ∘ e) (h' : d = b ∘ e') :
    c = b ∘ (e.trans e') := by
  funext a
  subst h h'
  simp
@[simp]
 lemma mapIso_trans (e : X ≃ Y) (e' : Y ≃ Z) (h : c = d ∘ e) (h' : d = b ∘ e') :
    (𝓣.mapIso e h ≪≫ₗ 𝓣.mapIso e' h') = 𝓣.mapIso (e.trans e') (𝓣.mapIso_trans_cond h h') := by
  refine LinearEquiv.toLinearMap_inj.mp ?_
  apply PiTensorProduct.ext
  apply MultilinearMap.ext
  intro x
  simp only [mapIso, LinearMap.compMultilinearMap_apply, LinearEquiv.coe_coe,
    LinearEquiv.trans_apply, PiTensorProduct.reindex_tprod, Equiv.symm_trans_apply]
  change (PiTensorProduct.congr fun y => 𝓣.colorModuleCast (_))
    ((PiTensorProduct.reindex R (fun x => 𝓣.ColorModule (d x)) e')
    ((PiTensorProduct.congr fun y => 𝓣.colorModuleCast (_)) _)) =
    (PiTensorProduct.congr fun y => 𝓣.colorModuleCast _)
    ((PiTensorProduct.reindex R (fun x => 𝓣.ColorModule (c x)) (e.trans e')) _)
  rw [PiTensorProduct.congr_tprod, PiTensorProduct.reindex_tprod,
    PiTensorProduct.congr_tprod, PiTensorProduct.reindex_tprod, PiTensorProduct.congr]
  simp [colorModuleCast]
@[simp]
 lemma mapIso_mapIso (e : X ≃ Y) (e' : Y ≃ Z) (h : c = d ∘ e) (h' : d = b ∘ e')
    (T : 𝓣.Tensor c) :
    (𝓣.mapIso e' h') (𝓣.mapIso e h T) = 𝓣.mapIso (e.trans e') (𝓣.mapIso_trans_cond h h') T := by
  rw [← LinearEquiv.trans_apply, mapIso_trans]
@[simp]
 lemma mapIso_symm (e : X ≃ Y) (h : c = d ∘ e) :
    (𝓣.mapIso e h).symm = 𝓣.mapIso e.symm ((Equiv.eq_comp_symm e d c).mpr h.symm) := by
  refine LinearEquiv.toLinearMap_inj.mp ?_
  apply PiTensorProduct.ext
  apply MultilinearMap.ext
  intro x
  simp  [mapIso, LinearMap.compMultilinearMap_apply, LinearEquiv.coe_coe,
    LinearEquiv.symm_apply_apply, PiTensorProduct.reindex_tprod]
  change (PiTensorProduct.reindex R (fun x => 𝓣.ColorModule (c x)) e).symm
    ((PiTensorProduct.congr fun y => 𝓣.colorModuleCast _).symm ((PiTensorProduct.tprod R) x)) =
  (PiTensorProduct.congr fun y => 𝓣.colorModuleCast _)
    ((PiTensorProduct.reindex R (fun x => 𝓣.ColorModule (d x)) e.symm) ((PiTensorProduct.tprod R) x))
  rw [PiTensorProduct.reindex_tprod, PiTensorProduct.congr_tprod, PiTensorProduct.congr_symm_tprod,
    LinearEquiv.symm_apply_eq, PiTensorProduct.reindex_tprod]
  apply congrArg
  funext i
  simp only [colorModuleCast, Equiv.cast_symm, LinearEquiv.coe_symm_mk,
    Equiv.symm_symm_apply, LinearEquiv.coe_mk]
  rw [← Equiv.symm_apply_eq]
  simp only [Equiv.cast_symm, Equiv.cast_apply, cast_cast]
  apply cast_eq_iff_heq.mpr
  rw [Equiv.apply_symm_apply]
@[simp]
 lemma mapIso_refl : 𝓣.mapIso (Equiv.refl X) (rfl : c = c) = LinearEquiv.refl R _ := by
  refine LinearEquiv.toLinearMap_inj.mp ?_
  apply PiTensorProduct.ext
  apply MultilinearMap.ext
  intro x
  simp only [mapIso, Equiv.refl_symm, Equiv.refl_apply, PiTensorProduct.reindex_refl,
    LinearMap.compMultilinearMap_apply, LinearEquiv.coe_coe, LinearEquiv.trans_apply,
    LinearEquiv.refl_apply, LinearEquiv.refl_toLinearMap, LinearMap.id, LinearMap.coe_mk,
    AddHom.coe_mk, id_eq]
  change (PiTensorProduct.congr fun y => 𝓣.colorModuleCast _) ((PiTensorProduct.tprod R) x) = _
  rw [PiTensorProduct.congr_tprod]
  rfl
@[simp]
 lemma mapIso_tprod {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = d ∘ e) (f : (i : X) → 𝓣.ColorModule (c i)) :
    (𝓣.mapIso e h) (PiTensorProduct.tprod R f) =
    (PiTensorProduct.tprod R (fun i => 𝓣.colorModuleCast (by rw [h]; simp) (f (e.symm i)))) := by
  simp [mapIso]
  change (PiTensorProduct.congr fun y => 𝓣.colorModuleCast _)
    ((PiTensorProduct.reindex R (fun x => 𝓣.ColorModule (c x)) e) ((PiTensorProduct.tprod R) f)) = _
  rw [PiTensorProduct.reindex_tprod]
  simp only [PiTensorProduct.congr_tprod]
 /-!
 ## Contraction
 -/
 def pairProd : 𝓣.Tensor c ⊗[R] 𝓣.Tensor c₂ →ₗ[R]
    ⨂[R] x, 𝓣.ColorModule (c x) ⊗[R] 𝓣.ColorModule (c₂ x) :=
  TensorProduct.lift (
    PiTensorProduct.map₂ (fun x =>
      TensorProduct.mk R (𝓣.ColorModule (c x)) (𝓣.ColorModule (c₂ x)) ))
 lemma mkPiAlgebra_equiv (e : X ≃ Y) :
    (PiTensorProduct.lift (MultilinearMap.mkPiAlgebra R X R)) =
    (PiTensorProduct.lift (MultilinearMap.mkPiAlgebra R Y R)) ∘ₗ
    (PiTensorProduct.reindex R _ e).toLinearMap := by
  apply PiTensorProduct.ext
  apply MultilinearMap.ext
  intro x
  simp only [LinearMap.compMultilinearMap_apply, PiTensorProduct.lift.tprod,
    MultilinearMap.mkPiAlgebra_apply, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    PiTensorProduct.reindex_tprod, Equiv.prod_comp]
 def contrAll' : 𝓣.Tensor c ⊗[R] 𝓣.Tensor (𝓣.τ ∘ c) →ₗ[R] R :=
  (PiTensorProduct.lift (MultilinearMap.mkPiAlgebra R X R)) ∘ₗ
  (PiTensorProduct.map (fun x => 𝓣.contrDual (c x))) ∘ₗ
  (𝓣.pairProd)
 lemma contrAll'_mapIso_cond {e : X ≃ Y} (h : c = d ∘ e) :
   𝓣.τ ∘ d = (𝓣.τ ∘ c) ∘ ⇑e.symm := by
  subst h
  ext1 x
  simp
@[simp]
 lemma contrAll'_mapIso (e : X ≃ Y) (h : c = d ∘ e) :
  𝓣.contrAll' ∘ₗ
    (TensorProduct.congr (𝓣.mapIso e h) (LinearEquiv.refl R _)).toLinearMap =
  𝓣.contrAll' ∘ₗ  (TensorProduct.congr (LinearEquiv.refl R _)
    (𝓣.mapIso e.symm (𝓣.contrAll'_mapIso_cond h))).toLinearMap := by
  apply TensorProduct.ext'
  refine fun x ↦
    PiTensorProduct.induction_on' x ?_ (by
      intro a b hx hy y
      simp [map_add, add_tmul, hx, hy])
  intro rx fx
  refine fun y ↦
    PiTensorProduct.induction_on' y ?_ (by
      intro a b hx hy
      simp at hx hy
      simp [map_add, tmul_add, hx, hy])
  intro ry fy
  simp [contrAll']
  rw [mkPiAlgebra_equiv e]
  apply congrArg
  simp
  apply congrArg
  rw [← LinearEquiv.symm_apply_eq]
  rw [PiTensorProduct.reindex_symm]
  rw [← PiTensorProduct.map_reindex]
  subst h
  simp
  apply congrArg
  rw [pairProd, pairProd]
  simp
  apply congrArg
  change _ = ((PiTensorProduct.map₂ fun x => TensorProduct.mk R (𝓣.ColorModule (d (e x))) (𝓣.ColorModule (𝓣.τ (d (e x)))))
      ((PiTensorProduct.tprod R) fx))
    ((𝓣.mapIso e.symm _) ((PiTensorProduct.tprod R) fy))
  rw [mapIso_tprod]
  simp
  rw [PiTensorProduct.map₂_tprod_tprod]
  change (PiTensorProduct.reindex R (fun x => 𝓣.ColorModule (d x) ⊗[R] 𝓣.ColorModule (𝓣.τ (d x))) e.symm)
    (((PiTensorProduct.map₂ fun x => TensorProduct.mk R (𝓣.ColorModule (d x)) (𝓣.ColorModule (𝓣.τ (d x))))
        ((PiTensorProduct.tprod R) fun i => (𝓣.colorModuleCast _) (fx (e.symm i))))
      ((PiTensorProduct.tprod R) fy)) = _
  rw [PiTensorProduct.map₂_tprod_tprod]
  simp
  erw [PiTensorProduct.reindex_tprod]
  apply congrArg
  funext i
  simp
  congr
  simp [colorModuleCast]
  apply cast_eq_iff_heq.mpr
  rw [Equiv.symm_apply_apply]
@[simp]
 lemma contrAll'_mapIso_tmul (e : X ≃ Y) (h : c = d ∘ e) (x : 𝓣.Tensor c) (y : 𝓣.Tensor (𝓣.τ ∘ d)) :
  𝓣.contrAll' ((𝓣.mapIso e h) x ⊗ₜ[R] y) = 𝓣.contrAll' (x ⊗ₜ[R] (𝓣.mapIso e.symm (𝓣.contrAll'_mapIso_cond h) y)) := by
  change  (𝓣.contrAll' ∘ₗ
    (TensorProduct.congr (𝓣.mapIso e h) (LinearEquiv.refl R _)).toLinearMap) (x ⊗ₜ[R] y) = _
  rw [contrAll'_mapIso]
  rfl
 def contrAll {c : X → 𝓣.Color} {d : Y → 𝓣.Color}
    (e : X ≃ Y) (h : c = 𝓣.τ ∘ d ∘ e) : 𝓣.Tensor c ⊗[R] 𝓣.Tensor d →ₗ[R] R :=
  𝓣.contrAll' ∘ₗ (TensorProduct.congr (LinearEquiv.refl _ _)
    (𝓣.mapIso e.symm (by subst h; funext a; simp; rw [𝓣.τ_involutive]))).toLinearMap
 lemma contrAll_symm_cond {e : X ≃ Y} (h : c = 𝓣.τ ∘ d ∘ e) :
    d = 𝓣.τ ∘ c ∘ ⇑e.symm := by
  subst h
  ext1 x
  simp
  rw [𝓣.τ_involutive]
 lemma contrAll_mapIso_right_cond {e : X ≃ Y} {e' : Z ≃ Y}
    (h : c = 𝓣.τ ∘ d ∘ e) (h' : b = d ∘ e') : c = 𝓣.τ ∘ b ∘ ⇑(e.trans e'.symm) := by
  subst h h'
  ext1 x
  simp only [Function.comp_apply, Equiv.coe_trans, Equiv.apply_symm_apply]
@[simp]
 lemma contrAll_mapIso_right_tmul (e : X ≃ Y) (e' : Z ≃ Y)
    (h : c = 𝓣.τ ∘ d ∘ e) (h' : b = d ∘ e')  (x : 𝓣.Tensor c) (z : 𝓣.Tensor b) :
    𝓣.contrAll e h (x ⊗ₜ[R] (𝓣.mapIso e' h' z)) =
    𝓣.contrAll (e.trans e'.symm) (𝓣.contrAll_mapIso_right_cond h h') (x ⊗ₜ[R] z) := by
  rw [contrAll, contrAll]
  simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, congr_tmul,
    LinearEquiv.refl_apply, mapIso_mapIso]
  congr
@[simp]
 lemma contrAll_comp_mapIso_right (e : X ≃ Y) (e' : Z ≃ Y)
    (h : c = 𝓣.τ ∘ d ∘ e) (h' : b = d ∘ e')  : 𝓣.contrAll e h ∘ₗ
    (TensorProduct.congr (LinearEquiv.refl R (𝓣.Tensor c)) (𝓣.mapIso e' h')).toLinearMap
    = 𝓣.contrAll (e.trans e'.symm) (𝓣.contrAll_mapIso_right_cond h h') := by
  apply TensorProduct.ext'
  intro x y
  exact 𝓣.contrAll_mapIso_right_tmul e e' h h' x y
 lemma contrAll_mapIso_left_cond {e : X ≃ Y} {e' : Z ≃ X}
    (h : c = 𝓣.τ ∘ d ∘ e) (h' : b = c ∘ e') : b = 𝓣.τ ∘ d ∘ ⇑(e'.trans e) := by
  subst h h'
  ext1 x
  simp only [Function.comp_apply, Equiv.coe_trans, Equiv.apply_symm_apply]
@[simp]
 lemma contrAll_mapIso_left_tmul {e : X ≃ Y} {e' : Z ≃ X}
    (h : c = 𝓣.τ ∘ d ∘ e) (h' : b = c ∘ e') (x :  𝓣.Tensor b) (y : 𝓣.Tensor d) :
    𝓣.contrAll e h ((𝓣.mapIso e' h' x) ⊗ₜ[R] y) =
    𝓣.contrAll (e'.trans e) (𝓣.contrAll_mapIso_left_cond h h') (x ⊗ₜ[R] y) := by
  rw [contrAll, contrAll]
  simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, congr_tmul,
    LinearEquiv.refl_apply, contrAll'_mapIso_tmul, mapIso_mapIso]
  congr
@[simp]
 lemma contrAll_mapIso_left {e : X ≃ Y} {e' : Z ≃ X}
    (h : c = 𝓣.τ ∘ d ∘ e) (h' : b = c ∘ e') :
    𝓣.contrAll e h ∘ₗ
    (TensorProduct.congr (𝓣.mapIso e' h') (LinearEquiv.refl R (𝓣.Tensor d))).toLinearMap
    = 𝓣.contrAll (e'.trans e) (𝓣.contrAll_mapIso_left_cond h h') := by
  apply TensorProduct.ext'
  intro x y
  exact 𝓣.contrAll_mapIso_left_tmul h h' x y
 end PreTensorStructure
 structure TensorStructure (R : Type) [CommSemiring R] extends PreTensorStructure R where
  contrDual_symm : ∀ μ,
    (contrDual μ) ∘ₗ (TensorProduct.comm R (ColorModule (τ μ)) (ColorModule μ)).toLinearMap  =
    (contrDual (τ μ)) ∘ₗ (TensorProduct.congr (LinearEquiv.refl _ _)
    (toPreTensorStructure.colorModuleCast (by rw[toPreTensorStructure.τ_involutive]))).toLinearMap
 namespace TensorStructure
 open PreTensorStructure
 variable (𝓣 : TensorStructure R)
 variable {d : ℕ} {X Y Y' Z : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
  [Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z]
  {c c₂ : X → 𝓣.Color}  {d : Y → 𝓣.Color} {b : Z → 𝓣.Color}  {d' : Y' → 𝓣.Color}  {μ ν: 𝓣.Color}
 end TensorStructure
 structure GroupTensorStructure (R : Type) [CommSemiring R]
    (G : Type) [Group G] extends TensorStructure R where
  repColorModule : (μ : Color) → Representation R G (ColorModule μ)
  contrDual_inv : ∀ μ g, contrDual μ ∘ₗ
    TensorProduct.map (repColorModule μ g) (repColorModule (τ μ) g) = contrDual μ
 namespace GroupTensorStructure
 open TensorStructure
 open PreTensorStructure
 variable {G : Type} [Group G]
 variable (𝓣 : GroupTensorStructure R G)
 variable {d : ℕ} {X Y Y' Z : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
  [Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z]
  {c c₂ : X → 𝓣.Color}  {d : Y → 𝓣.Color} {b : Z → 𝓣.Color}  {d' : Y' → 𝓣.Color}  {μ ν: 𝓣.Color}
 def rep : Representation R G (𝓣.Tensor c) where
  toFun g := PiTensorProduct.map (fun x => 𝓣.repColorModule (c x) g)
  map_one' := by
    simp_all only [_root_.map_one, PiTensorProduct.map_one]
  map_mul' g g' := by
    simp_all only [_root_.map_mul]
    exact PiTensorProduct.map_mul _ _
 local infixl:78 " • " => 𝓣.rep
@[simp]
 lemma repColorModule_colorModuleCast_apply (h : μ = ν) (g : G) (x : 𝓣.ColorModule μ) :
    (𝓣.repColorModule ν g) ((𝓣.colorModuleCast h) x) = (𝓣.colorModuleCast h) ((𝓣.repColorModule μ g) x) := by
  subst h
  simp [colorModuleCast]
@[simp]
 lemma repColorModule_colorModuleCast (h : μ = ν) (g : G) :
    (𝓣.repColorModule ν g) ∘ₗ (𝓣.colorModuleCast h).toLinearMap =
    (𝓣.colorModuleCast h).toLinearMap  ∘ₗ (𝓣.repColorModule μ g) := by
  apply LinearMap.ext
  intro x
  simp
@[simp]
 lemma rep_mapIso (e : X ≃ Y) (h : c = d ∘ e) (g : G) :
    (𝓣.rep g) ∘ₗ (𝓣.mapIso e h).toLinearMap = (𝓣.mapIso e h).toLinearMap ∘ₗ 𝓣.rep g := by
  apply PiTensorProduct.ext
  apply MultilinearMap.ext
  intro x
  simp
  erw [mapIso_tprod]
  simp [rep]
  change (PiTensorProduct.map fun x => (𝓣.repColorModule (d x)) g)
    ((PiTensorProduct.tprod R) fun i => (𝓣.colorModuleCast _) (x (e.symm i))) =
    (𝓣.mapIso e h) ((PiTensorProduct.map fun x => (𝓣.repColorModule (c x)) g) ((PiTensorProduct.tprod R) x))
  rw [PiTensorProduct.map_tprod, PiTensorProduct.map_tprod]
  rw [mapIso_tprod]
  apply congrArg
  funext i
  subst h
  simp
@[simp]
 lemma rep_mapIso_apply (e : X ≃ Y) (h : c = d ∘ e) (g : G) (x : 𝓣.Tensor c) :
    (𝓣.rep g) ((𝓣.mapIso e h) x) = (𝓣.mapIso e h) ((𝓣.rep g) x) := by
  trans ((𝓣.rep g) ∘ₗ (𝓣.mapIso e h).toLinearMap) x
  rfl
  simp
 end GroupTensorStructure
 end
--- a/HepLean/SpaceTime/LorentzTensor/Complex/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Complex/Basic.lean
@ -0,0 +1,166 @@
 /-
 Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import Mathlib.Logic.Function.CompTypeclasses
 import Mathlib.Data.Real.Basic
 import Mathlib.Data.Fintype.BigOperators
 import Mathlib.Logic.Equiv.Fin
 import Mathlib.Tactic.FinCases
 import Mathlib.Logic.Equiv.Fintype
 import Mathlib.Algebra.Module.Pi
 import Mathlib.Algebra.Module.Equiv
 import Mathlib.Algebra.Module.LinearMap.Basic
 import Mathlib.LinearAlgebra.TensorProduct.Basic
 import Mathlib.LinearAlgebra.TensorProduct.Basis
 import Mathlib.Data.Complex.Basic
 /-!
 # Complex Lorentz Tensors
 In this file we define complex Lorentz tensors.
 We implicitly follow the definition of a modular operad.
 This will relation should be made explicit in the future.
 ## References
 -- For modular operads see: [Raynor][raynor2021graphical]
 -- For Van der Waerden notation see: [Dreiner et al.][Dreiner:2008tw]
 -/
 /-- The possible `color` of an index for a complex Lorentz tensor.
 There are four possiblities, specifying how the index transforms under `SL(2, C)`.
 This follows Van der Waerden notation. -/
 inductive ComplexLorentzTensor.Color where
  | up : ComplexLorentzTensor.Color
  | down : ComplexLorentzTensor.Color
  | weylUp : ComplexLorentzTensor.Color
  | weylDown : ComplexLorentzTensor.Color
  | weylUpDot : ComplexLorentzTensor.Color
  | weylDownDot : ComplexLorentzTensor.Color
 /-- To set of allowed index values associated to a color of index. -/
 def ComplexLorentzTensor.ColorIndex (μ : ComplexLorentzTensor.Color) : Type :=
  match μ with
  | ComplexLorentzTensor.Color.up => Fin 1 ⊕ Fin 3
  | ComplexLorentzTensor.Color.down => Fin 1 ⊕ Fin 3
  | ComplexLorentzTensor.Color.weylUp => Fin 2
  | ComplexLorentzTensor.Color.weylDown => Fin 2
  | ComplexLorentzTensor.Color.weylUpDot => Fin 2
  | ComplexLorentzTensor.Color.weylDownDot => Fin 2
 /-- The instance of a finite type on the set of allowed index values for a given color. -/
 instance (μ : ComplexLorentzTensor.Color) : Fintype (ComplexLorentzTensor.ColorIndex μ) :=
  match μ with
  | ComplexLorentzTensor.Color.up => instFintypeSum (Fin 1) (Fin 3)
  | ComplexLorentzTensor.Color.down => instFintypeSum (Fin 1) (Fin 3)
  | ComplexLorentzTensor.Color.weylUp => Fin.fintype 2
  | ComplexLorentzTensor.Color.weylDown => Fin.fintype 2
  | ComplexLorentzTensor.Color.weylUpDot => Fin.fintype 2
  | ComplexLorentzTensor.Color.weylDownDot => Fin.fintype 2
 /-- The color index set for each color has a decidable equality. -/
 instance (μ : ComplexLorentzTensor.Color) : DecidableEq (ComplexLorentzTensor.ColorIndex μ) :=
  match μ with
  | ComplexLorentzTensor.Color.up => instDecidableEqSum
  | ComplexLorentzTensor.Color.down => instDecidableEqSum
  | ComplexLorentzTensor.Color.weylUp => instDecidableEqFin 2
  | ComplexLorentzTensor.Color.weylDown => instDecidableEqFin 2
  | ComplexLorentzTensor.Color.weylUpDot => instDecidableEqFin 2
  | ComplexLorentzTensor.Color.weylDownDot => instDecidableEqFin 2
 /-- The set of all index values associated with a map from `X` to `ComplexLorentzTensor.Color`. -/
 def ComplexLorentzTensor.IndexValue {X : Type}  (c : X → ComplexLorentzTensor.Color) : Type :=
  (x : X) → ComplexLorentzTensor.ColorIndex (c x)
 /-- Complex lorentz tensors. -/
 def ComplexLorentzTensor {X : Type} (c : X → ComplexLorentzTensor.Color) : Type :=
  ComplexLorentzTensor.IndexValue c → ℂ
 /-- Complex Lorentz tensors form an additive commutative monoid. -/
 instance {X : Type} (c : X → ComplexLorentzTensor.Color) :
  AddCommMonoid (ComplexLorentzTensor c) := Pi.addCommMonoid
 /-- Complex Lorentz tensors form a module over the complex numbers. -/
 instance {X : Type} (c : X → ComplexLorentzTensor.Color) :
  Module ℂ (ComplexLorentzTensor c) := Pi.module _ _ _
 /-- Complex Lorentz tensors form an additive commutative group. -/
 instance {X : Type} (c : X → ComplexLorentzTensor.Color) :
  AddCommGroup (ComplexLorentzTensor c) := Pi.addCommGroup
 namespace ComplexLorentzTensor
 /-- A map taking every color to its dual color. -/
 def τ : Color → Color
  | Color.up => Color.down
  | Color.down => Color.up
  | Color.weylUp => Color.weylDown
  | Color.weylDown => Color.weylUp
  | Color.weylUpDot => Color.weylDownDot
  | Color.weylDownDot => Color.weylUpDot
 /-- The map τ is an involution. -/
@[simp]
 lemma τ_involutive : Function.Involutive τ := by
  intro x
  cases x <;> rfl
 /-!
 ## Color index value
 -/
 /-- An equivalence of `ColorIndex` types given an equality of color. -/
 def colorIndexCast {μ₁ μ₂ : Color} (h : μ₁ = μ₂) :
    ColorIndex μ₁ ≃ ColorIndex μ₂ := Equiv.cast (congrArg ColorIndex h)
@[simp]
 lemma colorIndexCast_symm {μ₁ μ₂ : Color} (h : μ₁ = μ₂) :
    (colorIndexCast h).symm = colorIndexCast h.symm := by
  rfl
 /-- The allowed index values of a color are equal to that of the dual color. -/
 lemma colorIndex_eq_on_dual {μ ν : Color} (h : μ = τ ν) :
    ColorIndex μ = ColorIndex ν := by
  match μ, ν, h with
  | .up, .down, _ => rfl
  | .down, .up, _ => rfl
  | .weylUp, .weylDown, _ => rfl
  | .weylDown, .weylUp, _ => rfl
  | .weylUpDot, .weylDownDot, _ => rfl
  | .weylDownDot, .weylUpDot, _ => rfl
 /-- An equivalence between the allowed index values of a color and a color dual to it. -/
 def colorIndexDualCast {μ ν : Color} (h : μ = τ ν) : ColorIndex μ ≃ ColorIndex ν :=
  Equiv.cast (colorIndex_eq_on_dual h)
@[simp]
 lemma colorIndexDualCast_symm {μ ν : Color} (h : μ = τ ν) : (colorIndexDualCast h).symm =
    colorIndexDualCast ((Function.Involutive.eq_iff τ_involutive).mp h.symm) := by
  rfl
@[simp]
 lemma colorIndexDualCast_trans {μ ν ξ : Color} (h : μ = τ ν) (h' : ν = τ ξ) :
    (colorIndexDualCast h).trans (colorIndexDualCast h') =
    colorIndexCast (by rw [h, h', τ_involutive]) := by
  simp [colorIndexDualCast, colorIndexCast]
@[simp]
 lemma colorIndexDualCast_trans_colorsIndexCast {μ ν ξ : Color} (h : μ = τ ν) (h' : ν = ξ) :
    (colorIndexDualCast h).trans (colorIndexCast h') =
    colorIndexDualCast (by rw [h, h']) := by
  simp [colorIndexDualCast, colorIndexCast]
@[simp]
 lemma colorIndexCast_trans_colorsIndexDualCast {μ ν ξ : Color} (h : μ = ν) (h' : ν = τ ξ) :
    (colorIndexCast h).trans (colorIndexDualCast h')  =
    colorIndexDualCast (by rw [h, h']) := by
  simp [colorIndexDualCast, colorIndexCast]
 end ComplexLorentzTensor
--- a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
@ -14,6 +14,8 @@ import Mathlib.Algebra.Module.Equiv
 import Mathlib.Algebra.Module.LinearMap.Basic
 import Mathlib.LinearAlgebra.TensorProduct.Basic
 import Mathlib.LinearAlgebra.TensorProduct.Basis
 import Mathlib.LinearAlgebra.PiTensorProduct
 import HepLean.Mathematics.PiTensorProduct
 /-!
 # Real Lorentz Tensors
@ -28,59 +30,106 @@ This will relation should be made explicit in the future.
 -- For modular operads see: [Raynor][raynor2021graphical]
 -/
-/-! TODO: Do complex tensors, with Van der Waerden notation for fermions. -/
+/-! TODO: Relate the constructions here to `PiTensorProduct`. -/
 /-! TODO: Generalize to maps into Lorentz tensors. -/
-/-- The possible `colors` of an index for a RealLorentzTensor.
+
 section PiTensorProductResults
 variable {ι ι₂ ι₃ : Type*}
 variable {R : Type*} [CommSemiring R]
 variable {R₁ R₂ : Type*}
 variable {s : ι → Type*} [∀ i, AddCommMonoid (s i)] [∀ i, Module R (s i)]
 variable {M : Type*} [AddCommMonoid M] [Module R M]
 variable {E : Type*} [AddCommMonoid E] [Module R E]
 variable {F : Type*} [AddCommMonoid F]
 end PiTensorProductResults
 open TensorProduct
 noncomputable section
 /-- The possible `color` of an index for a RealLorentzTensor.
 There are two possiblities, `up` and `down`. -/
-inductive RealLorentzTensor.Colors where
+inductive RealLorentzTensor.Color where
-  | up : RealLorentzTensor.Colors
+  | up : RealLorentzTensor.Color
-  | down : RealLorentzTensor.Colors
+  | down : RealLorentzTensor.Color
-/-- The association of colors with indices. For up and down this is `Fin 1 ⊕ Fin d`. -/
+/-- To set of allowed index values associated to a color of index. -/
-def RealLorentzTensor.ColorsIndex (d : ℕ) (μ : RealLorentzTensor.Colors) : Type :=
+def RealLorentzTensor.ColorIndex (d : ℕ) (μ : RealLorentzTensor.Color) : Type :=
  match μ with
-  | RealLorentzTensor.Colors.up => Fin 1 ⊕ Fin d
+  | RealLorentzTensor.Color.up => Fin 1 ⊕ Fin d
-  | RealLorentzTensor.Colors.down => Fin 1 ⊕ Fin d
+  | RealLorentzTensor.Color.down => Fin 1 ⊕ Fin d
-instance (d : ℕ) (μ : RealLorentzTensor.Colors) : Fintype (RealLorentzTensor.ColorsIndex d μ) :=
+/-- The instance of a finite type on the set of allowed index values for a given color. -/
 instance (d : ℕ) (μ : RealLorentzTensor.Color) : Fintype (RealLorentzTensor.ColorIndex d μ) :=
  match μ with
-  | RealLorentzTensor.Colors.up => instFintypeSum (Fin 1) (Fin d)
+  | RealLorentzTensor.Color.up => instFintypeSum (Fin 1) (Fin d)
-  | RealLorentzTensor.Colors.down => instFintypeSum (Fin 1) (Fin d)
+  | RealLorentzTensor.Color.down => instFintypeSum (Fin 1) (Fin d)
-instance (d : ℕ) (μ : RealLorentzTensor.Colors) : DecidableEq (RealLorentzTensor.ColorsIndex d μ) :=
+/-- The color index set for each color has a decidable equality. -/
 instance (d : ℕ) (μ : RealLorentzTensor.Color) : DecidableEq (RealLorentzTensor.ColorIndex d μ) :=
  match μ with
-  | RealLorentzTensor.Colors.up => instDecidableEqSum
+  | RealLorentzTensor.Color.up => instDecidableEqSum
-  | RealLorentzTensor.Colors.down => instDecidableEqSum
+  | RealLorentzTensor.Color.down => instDecidableEqSum
 def RealLorentzTensor.ColorModule (d : ℕ) (μ : RealLorentzTensor.Color) : Type :=
  RealLorentzTensor.ColorIndex d μ → ℝ
 instance (d : ℕ) (μ : RealLorentzTensor.Color) :
    AddCommMonoid (RealLorentzTensor.ColorModule d μ) :=
  Pi.addCommMonoid
 instance (d : ℕ) (μ : RealLorentzTensor.Color) : Module ℝ (RealLorentzTensor.ColorModule d μ) :=
  Pi.module _ _ _
 instance (d : ℕ) (μ : RealLorentzTensor.Color) : AddCommGroup (RealLorentzTensor.ColorModule d μ) :=
  Pi.addCommGroup
 /-- Real Lorentz tensors. -/
 def RealLorentzTensor {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Color) : Type :=
    ⨂[ℝ] i : X, RealLorentzTensor.ColorModule d (c i)
 instance {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Color) :
    AddCommMonoid (RealLorentzTensor d c) :=
  PiTensorProduct.instAddCommMonoid fun i => RealLorentzTensor.ColorModule d (c i)
 instance {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Color) :
  Module ℝ (RealLorentzTensor d c) := PiTensorProduct.instModule
 instance {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Color) :
  AddCommGroup (RealLorentzTensor d c) := PiTensorProduct.instAddCommGroup
 namespace RealLorentzTensor
 variable {d : ℕ} {X Y Z : Type} (c : X → Color)
    [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] [Fintype Z] [DecidableEq Z]
 /-- An `IndexValue` is a set of actual values an index can take. e.g. for a
  3-tensor (0, 1, 2). -/
-def RealLorentzTensor.IndexValue {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Colors) :
+def IndexValue {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Color) :
-    Type 0 := (x : X) → RealLorentzTensor.ColorsIndex d (c x)
+    Type 0 := (x : X) → ColorIndex d (c x)
-def RealLorentzTensor.ColorFiber {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Colors) : Type :=
+instance [Fintype X] [DecidableEq X] : Fintype (IndexValue d c) := Pi.fintype
    RealLorentzTensor.IndexValue d c → ℝ
-instance {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Colors) :
+instance [Fintype X] : DecidableEq (IndexValue d c) :=
-  AddCommMonoid (RealLorentzTensor.ColorFiber d c) := Pi.addCommMonoid
+  Fintype.decidablePiFintype
-instance {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Colors) :
+def basisColorModule {d : ℕ} (μ : Color) :
-  Module ℝ (RealLorentzTensor.ColorFiber d c) := Pi.module _ _ _
+    Basis (ColorIndex d μ) ℝ (ColorModule d μ) := Pi.basisFun _ _
-instance {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Colors) :
+def basis (d : ℕ) (c : X → RealLorentzTensor.Color) :
-  AddCommGroup (RealLorentzTensor.ColorFiber d c) := Pi.addCommGroup
+    Basis (IndexValue d c) ℝ (RealLorentzTensor d c) :=
  Basis.piTensorProduct (fun x => basisColorModule (c x))
-/-- A Lorentz Tensor defined by its coordinate map. -/
+abbrev PiModule (d : ℕ) (c : X → Color) := IndexValue d c → ℝ
-structure RealLorentzTensor (d : ℕ) (X : Type) where
+
-  /-- The color associated to each index of the tensor. -/
+def asPi {d : ℕ} {c : X → Color} :
-  color : X → RealLorentzTensor.Colors
+    RealLorentzTensor d c ≃ₗ[ℝ] PiModule d c  :=
-  /-- The coordinate map for the tensor. -/
+  (basis d c).repr  ≪≫ₗ
-  coord : RealLorentzTensor.ColorFiber d color
+  Finsupp.linearEquivFunOnFinite ℝ ℝ (IndexValue d c)
 namespace RealLorentzTensor
 open Matrix
 universe u1
 variable {d : ℕ} {X Y Z : Type} (c : X → Colors)
 /-!
@ -89,9 +138,9 @@ variable {d : ℕ} {X Y Z : Type} (c : X → Colors)
 -/
 /-- The involution acting on colors. -/
-def τ : Colors → Colors
+def τ : Color → Color
-  | Colors.up => Colors.down
+  | Color.up => Color.down
-  | Colors.down => Colors.up
+  | Color.down => Color.up
 /-- The map τ is an involution. -/
@[simp]
@ -99,75 +148,71 @@ lemma τ_involutive : Function.Involutive τ := by
  intro x
  cases x <;> rfl
-lemma color_eq_dual_symm {μ ν : Colors} (h : μ = τ ν) : ν = τ μ :=
+lemma color_eq_dual_symm {μ ν : Color} (h : μ = τ ν) : ν = τ μ :=
  (Function.Involutive.eq_iff τ_involutive).mp h.symm
-lemma color_comp_τ_symm {c1 c2 : X → Colors} (h : c1 = τ ∘ c2) : c2 = τ ∘ c1 :=
+lemma color_comp_τ_symm {c1 c2 : X → Color} (h : c1 = τ ∘ c2) : c2 = τ ∘ c1 :=
  funext (fun x => color_eq_dual_symm (congrFun h x))
-/-- The color associated with an element of `x ∈ X` for a tensor `T`. -/
+/-- An equivalence of `ColorIndex` types given an equality of colors. -/
-def ch {X : Type} (x : X) (T : RealLorentzTensor d X) : Colors := T.color x
+def colorIndexCast {d : ℕ} {μ₁ μ₂ : Color} (h : μ₁ = μ₂) :
-
+    ColorIndex d μ₁ ≃ ColorIndex d μ₂ :=
-/-- An equivalence of `ColorsIndex` types given an equality of colors. -/
+  Equiv.cast (congrArg (ColorIndex d) h)
 def colorsIndexCast {d : ℕ} {μ₁ μ₂ : RealLorentzTensor.Colors} (h : μ₁ = μ₂) :
    ColorsIndex d μ₁ ≃ ColorsIndex d μ₂ :=
  Equiv.cast (congrArg (ColorsIndex d) h)
@[simp]
-lemma colorsIndexCast_symm {d : ℕ} {μ₁ μ₂ : RealLorentzTensor.Colors} (h : μ₁ = μ₂) :
+lemma colorIndexCast_symm {d : ℕ} {μ₁ μ₂ : Color} (h : μ₁ = μ₂) :
-    (@colorsIndexCast d _ _ h).symm = colorsIndexCast h.symm := by
+    (@colorIndexCast d _ _ h).symm = colorIndexCast h.symm := by
  rfl
-/-- An equivalence of `ColorsIndex` between that of a color and that of its dual. -/
+/-- An equivalence of `ColorIndex` between that of a color and that of its dual.
-def colorsIndexDualCastSelf {d : ℕ} {μ : RealLorentzTensor.Colors}:
+   I.e. the allowed index values for a color and its dual are equivalent. -/
-    ColorsIndex d μ ≃ ColorsIndex d (τ μ) where
+def colorIndexDualCastSelf {d : ℕ} {μ : Color}:
    ColorIndex d μ ≃ ColorIndex d (τ μ) where
  toFun x :=
    match μ with
-    | RealLorentzTensor.Colors.up => x
+    | Color.up => x
-    | RealLorentzTensor.Colors.down => x
+    | Color.down => x
  invFun x :=
    match μ with
-    | RealLorentzTensor.Colors.up => x
+    | Color.up => x
-    | RealLorentzTensor.Colors.down => x
+    | Color.down => x
  left_inv x := by cases μ <;> rfl
  right_inv x := by cases μ <;> rfl
-/-- An equivalence of `ColorsIndex` types given an equality of a color and the dual of a color. -/
+/-- An equivalence between the allowed index values of a color and a color dual to it. -/
-def colorsIndexDualCast {μ ν : Colors} (h : μ = τ ν) :
+def colorIndexDualCast {μ ν : Color} (h : μ = τ ν) : ColorIndex d μ ≃ ColorIndex d ν :=
-    ColorsIndex d μ ≃ ColorsIndex d ν :=
+  (colorIndexCast h).trans colorIndexDualCastSelf.symm
  (colorsIndexCast h).trans colorsIndexDualCastSelf.symm
@[simp]
-lemma colorsIndexDualCast_symm {μ ν : Colors} (h : μ = τ ν) :
+lemma colorIndexDualCast_symm {μ ν : Color} (h : μ = τ ν) : (colorIndexDualCast h).symm =
-    (colorsIndexDualCast h).symm =
+    @colorIndexDualCast d _ _ ((Function.Involutive.eq_iff τ_involutive).mp h.symm) := by
    @colorsIndexDualCast d _ _ ((Function.Involutive.eq_iff τ_involutive).mp h.symm) := by
  match μ, ν with
-  | Colors.up, Colors.down => rfl
+  | Color.up, Color.down => rfl
-  | Colors.down, Colors.up => rfl
+  | Color.down, Color.up => rfl
@[simp]
-lemma colorsIndexDualCast_trans {μ ν ξ : Colors} (h : μ = τ ν) (h' : ν = τ ξ) :
+lemma colorIndexDualCast_trans {μ ν ξ : Color} (h : μ = τ ν) (h' : ν = τ ξ) :
-    (@colorsIndexDualCast d _ _ h).trans (colorsIndexDualCast h') =
+    (@colorIndexDualCast d _ _ h).trans (colorIndexDualCast h') =
-    colorsIndexCast (by rw [h, h', τ_involutive]) := by
+    colorIndexCast (by rw [h, h', τ_involutive]) := by
  match μ, ν, ξ with
-  | Colors.up, Colors.down, Colors.up => rfl
+  | Color.up, Color.down, Color.up => rfl
-  | Colors.down, Colors.up, Colors.down => rfl
+  | Color.down, Color.up, Color.down => rfl
@[simp]
-lemma colorsIndexDualCast_trans_colorsIndexCast {μ ν ξ : Colors} (h : μ = τ ν) (h' : ν = ξ) :
+lemma colorIndexDualCast_trans_colorsIndexCast {μ ν ξ : Color} (h : μ = τ ν) (h' : ν = ξ) :
-    (@colorsIndexDualCast d _ _ h).trans (colorsIndexCast h') =
+    (@colorIndexDualCast d _ _ h).trans (colorIndexCast h') =
-    colorsIndexDualCast (by rw [h, h']) := by
+    colorIndexDualCast (by rw [h, h']) := by
  match μ, ν, ξ with
-  | Colors.down, Colors.up, Colors.up => rfl
+  | Color.down, Color.up, Color.up => rfl
-  | Colors.up, Colors.down, Colors.down => rfl
+  | Color.up, Color.down, Color.down => rfl
@[simp]
-lemma colorsIndexCast_trans_colorsIndexDualCast {μ ν ξ : Colors} (h : μ = ν) (h' : ν = τ ξ) :
+lemma colorIndexCast_trans_colorsIndexDualCast {μ ν ξ : Color} (h : μ = ν) (h' : ν = τ ξ) :
-    (colorsIndexCast h).trans (@colorsIndexDualCast d _ _ h')  =
+    (colorIndexCast h).trans (@colorIndexDualCast d _ _ h')  =
-    colorsIndexDualCast (by rw [h, h']) := by
+    colorIndexDualCast (by rw [h, h']) := by
  match μ, ν, ξ with
-  | Colors.up, Colors.up, Colors.down => rfl
+  | Color.up, Color.up, Color.down => rfl
-  | Colors.down, Colors.down, Colors.up => rfl
+  | Color.down, Color.down, Color.up => rfl
 /-!
@ -176,10 +221,7 @@ lemma colorsIndexCast_trans_colorsIndexDualCast {μ ν ξ : Colors} (h : μ = ν
 -/
 instance [Fintype X] [DecidableEq X] : Fintype (IndexValue d c) := Pi.fintype
 instance [Fintype X] : DecidableEq (IndexValue d c) :=
  Fintype.decidablePiFintype
 /-!
@ -188,20 +230,20 @@ instance [Fintype X] : DecidableEq (IndexValue d c) :=
 -/
 /-- An isomorphism of the type of index values given an isomorphism of sets. -/
-def indexValueIso (d : ℕ) (f : X ≃ Y) {i : X → Colors} {j : Y → Colors} (h : i = j ∘ f) :
+def indexValueIso (d : ℕ) (f : X ≃ Y) {i : X → Color} {j : Y → Color} (h : i = j ∘ f) :
    IndexValue d i ≃ IndexValue d j :=
-  (Equiv.piCongrRight (fun μ => colorsIndexCast (congrFun h μ))).trans $
+  (Equiv.piCongrRight (fun μ => colorIndexCast (congrFun h μ))).trans $
-  Equiv.piCongrLeft (fun y => RealLorentzTensor.ColorsIndex d (j y)) f
+  Equiv.piCongrLeft (fun y => ColorIndex d (j y)) f
@[simp]
-lemma indexValueIso_symm_apply' (d : ℕ) (f : X ≃ Y) {i : X → Colors} {j : Y → Colors}
+lemma indexValueIso_symm_apply' (d : ℕ) (f : X ≃ Y) {i : X → Color} {j : Y → Color}
    (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
+    (indexValueIso d f h).symm y x = (colorIndexCast (congrFun h x)).symm (y (f x)) := by
  rfl
@[simp]
-lemma indexValueIso_trans (d : ℕ) (f : X ≃ Y) (g : Y ≃ Z) {i : X → Colors}
+lemma indexValueIso_trans (d : ℕ) (f : X ≃ Y) (g : Y ≃ Z) {i : X → Color}
-    {j : Y → Colors} {k : Z → Colors} (h : i = j ∘ f) (h' : j = k ∘ g) :
+    {j : Y → Color} {k : Z → Color} (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 =
@ -218,7 +260,7 @@ lemma indexValueIso_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) :
  rw [← Equiv.symm_apply_eq]
  funext y
  rw [indexValueIso_symm_apply', indexValueIso_symm_apply']
-  simp only [Function.comp_apply, colorsIndexCast, Equiv.cast_symm, Equiv.cast_apply, cast_cast]
+  simp only [Function.comp_apply, colorIndexCast, Equiv.cast_symm, Equiv.cast_apply, cast_cast]
  apply cast_eq_iff_heq.mpr
  rw [Equiv.apply_symm_apply]
@ -229,7 +271,7 @@ lemma indexValueIso_eq_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) :
  rfl
@[simp]
-lemma indexValueIso_refl (d : ℕ) (i : X → Colors) :
+lemma indexValueIso_refl (d : ℕ) (i : X → Color) :
    indexValueIso d (Equiv.refl X) (rfl : i = i) = Equiv.refl _ := by
  rfl
@ -242,17 +284,17 @@ lemma indexValueIso_refl (d : ℕ) (i : X → Colors) :
 -/
 /-- The isomorphism between the index values of a color map and its dual. -/
-def indexValueDualIso (d : ℕ) {i : X → Colors} {j : Y → Colors} (e : X ≃ Y)
+def indexValueDualIso (d : ℕ) {i : X → Color} {j : Y → Color} (e : X ≃ Y)
    (h : i = τ ∘ j ∘ e) : IndexValue d i ≃ IndexValue d j :=
-  (Equiv.piCongrRight (fun μ => colorsIndexDualCast (congrFun h μ))).trans $
+  (Equiv.piCongrRight (fun μ => colorIndexDualCast (congrFun h μ))).trans $
-  Equiv.piCongrLeft (fun y => ColorsIndex d (j y)) e
+  Equiv.piCongrLeft (fun y => ColorIndex d (j y)) e
-lemma indexValueDualIso_symm_apply' (d : ℕ) {i : X → Colors} {j : Y → Colors} (e : X ≃ Y)
+lemma indexValueDualIso_symm_apply' (d : ℕ) {i : X → Color} {j : Y → Color} (e : X ≃ Y)
    (h : i = τ ∘ j ∘ e) (y : IndexValue d j) (x : X) :
-    (indexValueDualIso d e h).symm y x = (colorsIndexDualCast (congrFun h x)).symm (y (e x)) := by
+    (indexValueDualIso d e h).symm y x = (colorIndexDualCast (congrFun h x)).symm (y (e x)) := by
  rfl
-lemma indexValueDualIso_cond_symm {i : X → Colors} {j : Y → Colors} {e : X ≃ Y}
+lemma indexValueDualIso_cond_symm {i : X → Color} {j : Y → Color} {e : X ≃ Y}
    (h : i = τ ∘ j ∘ e) : j = τ ∘ i ∘ e.symm := by
  subst h
  simp only [Function.comp.assoc, Equiv.self_comp_symm, CompTriple.comp_eq]
@ -261,26 +303,26 @@ lemma indexValueDualIso_cond_symm {i : X → Colors} {j : Y → Colors} {e : X
  simp only [τ_involutive, Function.Involutive.comp_self, Function.comp_apply, id_eq]
@[simp]
-lemma indexValueDualIso_symm {d : ℕ} {i : X → Colors} {j : Y → Colors} (e : X ≃ Y)
+lemma indexValueDualIso_symm {d : ℕ} {i : X → Color} {j : Y → Color} (e : X ≃ Y)
    (h : i = τ ∘ j ∘ e) : (indexValueDualIso d e h).symm =
    indexValueDualIso d e.symm (indexValueDualIso_cond_symm h) := by
  ext i : 1
  rw [← Equiv.symm_apply_eq]
  funext a
  rw [indexValueDualIso_symm_apply', indexValueDualIso_symm_apply']
-  erw [← Equiv.trans_apply, colorsIndexDualCast_symm, colorsIndexDualCast_symm,
+  erw [← Equiv.trans_apply, colorIndexDualCast_symm, colorIndexDualCast_symm,
-    colorsIndexDualCast_trans]
+    colorIndexDualCast_trans]
-  simp only [Function.comp_apply, colorsIndexCast, Equiv.cast_apply]
+  simp only [Function.comp_apply, colorIndexCast, Equiv.cast_apply]
  apply cast_eq_iff_heq.mpr
  rw [Equiv.apply_symm_apply]
-lemma indexValueDualIso_eq_symm {d : ℕ} {i : X → Colors} {j : Y → Colors} (e : X ≃ Y)
+lemma indexValueDualIso_eq_symm {d : ℕ} {i : X → Color} {j : Y → Color} (e : X ≃ Y)
    (h : i = τ ∘ j ∘ e) :
    indexValueDualIso d e h = (indexValueDualIso d e.symm (indexValueDualIso_cond_symm h)).symm := by
  rw [indexValueDualIso_symm]
  simp
-lemma indexValueDualIso_cond_trans {i : X → Colors} {j : Y → Colors} {k : Z → Colors}
+lemma indexValueDualIso_cond_trans {i : X → Color} {j : Y → Color} {k : Z → Color}
    {e : X ≃ Y} {f : Y ≃ Z} (h : i = τ ∘ j ∘ e) (h' : j = τ ∘ k ∘ f) :
    i = k ∘ (e.trans f) := by
  rw [h, h']
@ -289,7 +331,7 @@ lemma indexValueDualIso_cond_trans {i : X → Colors} {j : Y → Colors} {k : Z
  rw [τ_involutive]
@[simp]
-lemma indexValueDualIso_trans {d : ℕ} {i : X → Colors} {j : Y → Colors} {k : Z → Colors}
+lemma indexValueDualIso_trans {d : ℕ} {i : X → Color} {j : Y → Color} {k : Z → Color}
    (e : X ≃ Y) (f : Y ≃ Z) (h : i = τ ∘ j ∘ e) (h' : j = τ ∘ k ∘ f) :
    (indexValueDualIso d e h).trans (indexValueDualIso d f h') =
    indexValueIso d (e.trans f) (indexValueDualIso_cond_trans h h') := by
@ -300,14 +342,14 @@ lemma indexValueDualIso_trans {d : ℕ} {i : X → Colors} {j : Y → Colors} {k
  rw [indexValueDualIso_symm_apply', indexValueDualIso_symm_apply',
    indexValueIso_symm_apply']
  erw [← Equiv.trans_apply]
-  rw [colorsIndexDualCast_symm, colorsIndexDualCast_symm, colorsIndexDualCast_trans]
+  rw [colorIndexDualCast_symm, colorIndexDualCast_symm, colorIndexDualCast_trans]
-  simp only [Function.comp_apply, colorsIndexCast, Equiv.symm_trans_apply, Equiv.cast_symm,
+  simp only [Function.comp_apply, colorIndexCast, Equiv.symm_trans_apply, Equiv.cast_symm,
    Equiv.cast_apply, cast_cast]
  symm
  apply cast_eq_iff_heq.mpr
  rw [Equiv.symm_apply_apply, Equiv.symm_apply_apply]
-lemma indexValueDualIso_cond_trans_indexValueIso {i : X → Colors} {j : Y → Colors} {k : Z → Colors}
+lemma indexValueDualIso_cond_trans_indexValueIso {i : X → Color} {j : Y → Color} {k : Z → Color}
    {e : X ≃ Y} {f : Y ≃ Z} (h : i = τ ∘ j ∘ e) (h' : j = k ∘ f)  :
    i = τ ∘ k ∘ (e.trans f) := by
  rw [h, h']
@ -315,7 +357,7 @@ lemma indexValueDualIso_cond_trans_indexValueIso {i : X → Colors} {j : Y → C
  simp only [Function.comp_apply, Equiv.coe_trans]
@[simp]
-lemma indexValueDualIso_trans_indexValueIso {d : ℕ} {i : X → Colors} {j : Y → Colors} {k : Z → Colors}
+lemma indexValueDualIso_trans_indexValueIso {d : ℕ} {i : X → Color} {j : Y → Color} {k : Z → Color}
    (e : X ≃ Y) (f : Y ≃ Z) (h : i = τ ∘ j ∘ e) (h' : j = k ∘ f) :
    (indexValueDualIso d e h).trans (indexValueIso d f h') =
    indexValueDualIso d (e.trans f) (indexValueDualIso_cond_trans_indexValueIso h h') := by
@ -326,14 +368,14 @@ lemma indexValueDualIso_trans_indexValueIso {d : ℕ} {i : X → Colors} {j : Y
    indexValueIso_symm_apply',indexValueDualIso_eq_symm, indexValueDualIso_symm_apply']
  rw [Equiv.symm_apply_eq]
  erw [← Equiv.trans_apply, ← Equiv.trans_apply]
-  simp only [Function.comp_apply, Equiv.symm_trans_apply, colorsIndexDualCast_symm,
+  simp only [Function.comp_apply, Equiv.symm_trans_apply, colorIndexDualCast_symm,
-    colorsIndexCast_symm, colorsIndexCast_trans_colorsIndexDualCast, colorsIndexDualCast_trans]
+    colorIndexCast_symm, colorIndexCast_trans_colorsIndexDualCast, colorIndexDualCast_trans]
-  simp only [colorsIndexCast, Equiv.cast_apply]
+  simp only [colorIndexCast, Equiv.cast_apply]
  symm
  apply cast_eq_iff_heq.mpr
  rw [Equiv.symm_apply_apply]
-lemma indexValueIso_trans_indexValueDualIso_cond {i : X → Colors} {j : Y → Colors} {k : Z → Colors}
+lemma indexValueIso_trans_indexValueDualIso_cond {i : X → Color} {j : Y → Color} {k : Z → Color}
    {e : X ≃ Y} {f : Y ≃ Z} (h : i = j ∘ e) (h' : j = τ ∘ k ∘ f)   :
    i = τ ∘ k ∘ (e.trans f) := by
  rw [h, h']
@ -341,7 +383,7 @@ lemma indexValueIso_trans_indexValueDualIso_cond {i : X → Colors} {j : Y → C
  simp only [Function.comp_apply, Equiv.coe_trans]
@[simp]
-lemma indexValueIso_trans_indexValueDualIso {d : ℕ} {i : X → Colors} {j : Y → Colors} {k : Z → Colors}
+lemma indexValueIso_trans_indexValueDualIso {d : ℕ} {i : X → Color} {j : Y → Color} {k : Z → Color}
    (e : X ≃ Y) (f : Y ≃ Z) (h : i = j ∘ e) (h' : j = τ ∘ k ∘ f) :
    (indexValueIso d e h).trans (indexValueDualIso d f h') =
    indexValueDualIso d (e.trans f) (indexValueIso_trans_indexValueDualIso_cond h h') := by
@ -351,9 +393,9 @@ lemma indexValueIso_trans_indexValueDualIso {d : ℕ} {i : X → Colors} {j : Y
  rw [indexValueIso_symm_apply', indexValueDualIso_symm_apply',
    indexValueDualIso_eq_symm, indexValueDualIso_symm_apply']
  erw [← Equiv.trans_apply, ← Equiv.trans_apply]
-  simp only [Function.comp_apply, Equiv.symm_trans_apply, colorsIndexDualCast_symm,
+  simp only [Function.comp_apply, Equiv.symm_trans_apply, colorIndexDualCast_symm,
-    colorsIndexCast_symm, colorsIndexDualCast_trans_colorsIndexCast, colorsIndexDualCast_trans]
+    colorIndexCast_symm, colorIndexDualCast_trans_colorsIndexCast, colorIndexDualCast_trans]
-  simp only [colorsIndexCast, Equiv.cast_apply]
+  simp only [colorIndexCast, Equiv.cast_apply]
  symm
  apply cast_eq_iff_heq.mpr
  rw [Equiv.symm_apply_apply, Equiv.symm_apply_apply]
@ -367,8 +409,8 @@ lemma indexValueIso_trans_indexValueDualIso {d : ℕ} {i : X → Colors} {j : Y
 -/
@[simps!]
-def mapIsoFiber (d : ℕ) (f : X ≃ Y) {i : X → Colors} {j : Y → Colors} (h : i = j ∘ f) :
+def mapIso {d : ℕ} (f : X ≃ Y) {i : X → Color} {j : Y → Color} (h : i = j ∘ f) :
-    ColorFiber d i ≃ₗ[ℝ] ColorFiber d j where
+    RealLorentzTensor d i ≃ₗ[ℝ] RealLorentzTensor d j where
  toFun F := F ∘ (indexValueIso d f h).symm
  invFun F := F ∘ indexValueIso d f h
  map_add' F G := by rfl
@ -383,82 +425,21 @@ def mapIsoFiber (d : ℕ) (f : X ≃ Y) {i : X → Colors} {j : Y → Colors} (h
    exact congrArg _  $ Equiv.apply_symm_apply (indexValueIso d f h) x
@[simp]
-lemma mapIsoFiber_trans (d : ℕ) (f : X ≃ Y) (g : Y ≃ Z) {i : X → Colors}
+lemma mapIso_trans (d : ℕ) (f : X ≃ Y) (g : Y ≃ Z) {i : X → Color}
-    {j : Y → Colors} {k : Z → Colors} (h : i = j ∘ f) (h' : j = k ∘ g) :
+    {j : Y → Color} {k : Z → Color} (h : i = j ∘ f) (h' : j = k ∘ g) :
-    (mapIsoFiber d f h).trans (mapIsoFiber d g h') =
+    (@mapIso _ _ d f _ _ h).trans (mapIso g h') =
-    mapIsoFiber d (f.trans g) (by rw [h, h', Function.comp.assoc]; rfl)  := by
+    mapIso  (f.trans g) (by rw [h, h', Function.comp.assoc]; rfl)  := by
  refine LinearEquiv.toEquiv_inj.mp (Equiv.ext (fun x => (funext (fun a => ?_))))
-  simp only [LinearEquiv.coe_toEquiv, LinearEquiv.trans_apply, mapIsoFiber_apply,
+  simp only [LinearEquiv.coe_toEquiv, LinearEquiv.trans_apply, mapIso_apply,
    indexValueIso_symm, ← Equiv.trans_apply, indexValueIso_trans]
  rfl
-lemma mapIsoFiber_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) :
+lemma mapIso_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) :
-    (mapIsoFiber d f h).symm = mapIsoFiber d f.symm ((Equiv.eq_comp_symm f j i).mpr h.symm) := by
+    (@mapIso _ _ d f _ _ h).symm = mapIso f.symm ((Equiv.eq_comp_symm f j i).mpr h.symm) := by
  refine LinearEquiv.toEquiv_inj.mp (Equiv.ext (fun x => (funext (fun a => ?_))))
-  simp only [LinearEquiv.coe_toEquiv, mapIsoFiber_symm_apply, mapIsoFiber_apply, indexValueIso_symm,
+  simp only [LinearEquiv.coe_toEquiv, mapIso_symm_apply, mapIso_apply, indexValueIso_symm,
    Equiv.symm_symm]
 /-!
 ## Extensionality
 -/
 lemma ext {T₁ T₂ : RealLorentzTensor d X} (h : T₁.color = T₂.color)
    (h' : T₁.coord = mapIsoFiber d (Equiv.refl X) h.symm T₂.coord) : T₁ = T₂ := by
  cases T₁
  cases T₂
  simp_all only [IndexValue, mk.injEq]
  apply And.intro h
  simp only at h
  subst h
  rfl
 /-!
 ## Mapping isomorphisms
 -/
 /-- An equivalence of Tensors given an equivalence of underlying sets. -/
@[simps!]
 def mapIso (d : ℕ) (f : X ≃ Y) : RealLorentzTensor d X ≃ RealLorentzTensor d Y where
  toFun T := ⟨T.color ∘ f.symm, mapIsoFiber d f (by funext x; simp) T.coord⟩
  invFun T := ⟨T.color ∘ f, (mapIsoFiber d f (by funext x; simp)).symm T.coord⟩
  left_inv T := by
    refine ext ?_ ?_
    · simp [Function.comp.assoc]
    · simp only [Function.comp_apply, ← LinearEquiv.trans_apply, mapIsoFiber_symm,
        mapIsoFiber_trans]
      congr
      exact Equiv.self_trans_symm f
  right_inv T := by
    refine ext ?_ ?_
    · simp [Function.comp.assoc]
    · simp only [Function.comp_apply, ← LinearEquiv.trans_apply, mapIsoFiber_symm,
        mapIsoFiber_trans]
      congr
      exact Equiv.symm_trans_self f
@[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
  refine ext rfl ?_
  simp
  erw [← LinearEquiv.trans_apply, ← LinearEquiv.trans_apply, mapIsoFiber_trans, mapIsoFiber_trans]
  rfl
 lemma mapIso_symm (f : X ≃ Y) : (mapIso d f).symm = mapIso d f.symm := by
  refine Equiv.coe_inj.mp ?_
  funext T
  refine ext rfl ?_
  erw [← LinearEquiv.trans_apply]
  rw [mapIso_symm_apply_coord, mapIsoFiber_trans, mapIsoFiber_symm]
  rfl
 lemma mapIso_refl : mapIso d (Equiv.refl X) = Equiv.refl _ := rfl
 /-!
@ -467,7 +448,7 @@ lemma mapIso_refl : mapIso d (Equiv.refl X) = Equiv.refl _ := rfl
 -/
 /-- An equivalence that splits elements of `IndexValue d (Sum.elim TX TY)` into two components. -/
-def indexValueSumEquiv {X Y : Type} {TX : X → Colors} {TY : Y → Colors} :
+def indexValueTensorator {X Y : Type} {TX : X → Color} {TY : Y → Color} :
    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
@ -481,338 +462,37 @@ def indexValueSumEquiv {X Y : Type} {TX : X → Colors} {TY : Y → Colors} :
    | inr val_1 => rfl
  right_inv p := rfl
-/-- An equivalence between index values formed by commuting sums. -/
+/-! TODO : Move -/
-def indexValueSumComm {X Y : Type} (Tc : X → Colors) (Sc : Y → Colors) :
+lemma tensorator_mapIso_cond {cX : X → Color} {cY : Y → Color} {cX' : X' → Color}
-    IndexValue d (Sum.elim Tc Sc) ≃ IndexValue d (Sum.elim Sc Tc) :=
+    {cY' : Y' → Color} {eX : X ≃ X'} {eY : Y ≃ Y'} (hX : cX = cX' ∘ eX) (hY : cY = cY' ∘ eY) :
-  indexValueIso d (Equiv.sumComm X Y) (by aesop)
+    Sum.elim cX cY = Sum.elim cX' cY' ∘ ⇑(eX.sumCongr eY) := by
-
+  subst hX hY
 def indexValueFinOne {c : Fin 1 → Colors} :
    ColorsIndex d (c 0) ≃ IndexValue d c 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
 /-!
 ## Marked Lorentz tensors
 To define contraction and multiplication of Lorentz tensors we need to mark indices.
 -/
 /-- A `RealLorentzTensor` with `n` marked indices. -/
 def Marked (d : ℕ) (X : Type) (n : ℕ) : Type :=
  RealLorentzTensor d (X ⊕ Fin n)
 namespace Marked
 variable {n m : ℕ}
 /-- The marked point. -/
 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 → 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
 instance [Fintype 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 (T : Marked d X n) : Fintype T.MarkedIndexValue :=
  Pi.fintype
 instance (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
+  simp_all only [Function.comp_apply, Equiv.sumCongr_apply]
  cases x with
  | inl val => simp_all only [Sum.elim_inl, Function.comp_apply, Sum.map_inl]
  | inr val_1 => simp_all only [Sum.elim_inr, Function.comp_apply, Sum.map_inr]
-/-- An equivalence splitting elements of `IndexValue d T.color` into their two components. -/
+lemma indexValueTensorator_indexValueMapIso {cX : X → Color} {cY : Y → Color} {cX' : X' → Color}
-def splitIndexValue {T : Marked d X n} :
+    {cY' : Y' → Color} (eX : X ≃ X') (eY : Y ≃ Y') (hX : cX = cX' ∘ eX) (hY : cY = cY' ∘ eY) :
-    IndexValue d T.color ≃ T.UnmarkedIndexValue × T.MarkedIndexValue :=
+    (indexValueIso d (Equiv.sumCongr eX eY) (tensorator_mapIso_cond hX hY)).trans indexValueTensorator =
-  (indexValueIso d (Equiv.refl _) T.color_eq_elim).trans
+    indexValueTensorator.trans (Equiv.prodCongr (indexValueIso d eX hX) (indexValueIso d eY hY)) := by
-  indexValueSumEquiv
+  apply Equiv.ext
-
+  intro i
-@[simp]
+  simp
-lemma splitIndexValue_sum {T : Marked d X n} [Fintype X] [DecidableEq X]
+  simp [ indexValueTensorator]
-    (P : T.UnmarkedIndexValue × T.MarkedIndexValue → ℝ) :
+  apply And.intro
-    ∑ i, P (splitIndexValue i) = ∑ j, ∑ k, P (j, k) := by
+  all_goals
  rw [Equiv.sum_comp splitIndexValue, Fintype.sum_prod_type]
 /-- Construction of marked index values for the case of 1 marked index. -/
 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
+    rw [indexValueIso_eq_symm, indexValueIso_symm_apply']
-    rfl
+    rw [indexValueIso_eq_symm, indexValueIso_symm_apply']
-
+    simp
 /-- Construction 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 => 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 :=
  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 tensor. -/
 def unmarkFirst {X : Type} : Marked d X n.succ ≃ Marked d (X ⊕ Fin 1) n :=
  mapIso d (unmarkFirstSet X n)
 /-!
-## Marking elements.
+## A basis for Lorentz tensors
 -/
 section markingElements
 variable [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
 /-- Splits a type based on an embedding from `Fin n` into elements not in the image of the
  embedding, and elements in the image. -/
 def markEmbeddingSet {n : ℕ} (f : Fin n ↪ X) :
    X ≃ {x // x ∈ (Finset.image f Finset.univ)ᶜ} ⊕ Fin n :=
  (Equiv.Set.sumCompl (Set.range ⇑f)).symm.trans <|
  (Equiv.sumComm _ _).trans <|
  Equiv.sumCongr ((Equiv.subtypeEquivRight (by simp))) <|
  (Function.Embedding.toEquivRange f).symm
 lemma markEmbeddingSet_on_mem {n : ℕ} (f : Fin n ↪ X) (x : X)
    (hx : x ∈ Finset.image f Finset.univ) : markEmbeddingSet f x =
    Sum.inr (f.toEquivRange.symm ⟨x, by simpa using hx⟩) := by
  rw [markEmbeddingSet]
  simp only [Equiv.trans_apply, Equiv.sumComm_apply, Equiv.sumCongr_apply]
  rw [Equiv.Set.sumCompl_symm_apply_of_mem]
  rfl
 lemma markEmbeddingSet_on_not_mem {n : ℕ} (f : Fin n ↪ X) (x : X)
    (hx : ¬ x ∈ (Finset.image f Finset.univ)) : markEmbeddingSet f x =
    Sum.inl ⟨x, by simpa using hx⟩ := by
  rw [markEmbeddingSet]
  simp only [Equiv.trans_apply, Equiv.sumComm_apply, Equiv.sumCongr_apply]
  rw [Equiv.Set.sumCompl_symm_apply_of_not_mem]
  rfl
  simpa using hx
 /-- Marks the indices of tensor in the image of an embedding. -/
@[simps!]
 def markEmbedding {n : ℕ} (f : Fin n ↪ X) :
    RealLorentzTensor d X ≃ Marked d {x // x ∈ (Finset.image f Finset.univ)ᶜ} n :=
  mapIso d (markEmbeddingSet f)
 lemma markEmbeddingSet_on_mem_indexValue_apply {n : ℕ} (f : Fin n ↪ X) (T : RealLorentzTensor d X)
    (i : IndexValue d (markEmbedding f T).color) (x : X) (hx : x ∈ (Finset.image f Finset.univ)) :
    i (markEmbeddingSet f x) = colorsIndexCast (congrArg ((markEmbedding f) T).color
    (markEmbeddingSet_on_mem f x hx).symm)
    (i (Sum.inr (f.toEquivRange.symm ⟨x, by simpa using hx⟩))) := by
  simp [colorsIndexCast]
  symm
  apply cast_eq_iff_heq.mpr
  rw [markEmbeddingSet_on_mem f x hx]
 lemma markEmbeddingSet_on_not_mem_indexValue_apply {n : ℕ}
    (f : Fin n ↪ X) (T : RealLorentzTensor d X) (i : IndexValue d (markEmbedding f T).color)
    (x : X) (hx : ¬ x ∈ (Finset.image f Finset.univ)) :
    i (markEmbeddingSet f x) = colorsIndexCast (congrArg ((markEmbedding f) T).color
    (markEmbeddingSet_on_not_mem f x hx).symm) (i (Sum.inl ⟨x, by simpa using hx⟩)) := by
  simp [colorsIndexCast]
  symm
  apply cast_eq_iff_heq.mpr
  rw [markEmbeddingSet_on_not_mem f x hx]
 /-- An equivalence between the IndexValues for a tensor `T` and the corresponding
  tensor with indices maked by an embedding. -/
@[simps!]
 def markEmbeddingIndexValue {n : ℕ} (f : Fin n ↪ X) (T : RealLorentzTensor d X) :
    IndexValue d T.color ≃ IndexValue d (markEmbedding f T).color :=
  indexValueIso d (markEmbeddingSet f) (
    (Equiv.comp_symm_eq (markEmbeddingSet f) ((markEmbedding f) T).color T.color).mp rfl)
 lemma markEmbeddingIndexValue_apply_symm_on_mem {n : ℕ}
    (f : Fin n.succ ↪ X) (T : RealLorentzTensor d X) (i : IndexValue d (markEmbedding f T).color)
    (x : X) (hx : x ∈ (Finset.image f Finset.univ)) :
    (markEmbeddingIndexValue f T).symm i x = (colorsIndexCast ((congrFun ((Equiv.comp_symm_eq
    (markEmbeddingSet f) ((markEmbedding f) T).color T.color).mp rfl) x).trans
    (congrArg ((markEmbedding f) T).color (markEmbeddingSet_on_mem f x hx)))).symm
    (i (Sum.inr (f.toEquivRange.symm ⟨x, by simpa using hx⟩))) := by
  rw [markEmbeddingIndexValue, indexValueIso_symm_apply']
  rw [markEmbeddingSet_on_mem_indexValue_apply f T i x hx]
  simp [colorsIndexCast]
 lemma markEmbeddingIndexValue_apply_symm_on_not_mem {n : ℕ} (f : Fin n.succ ↪ X)
    (T : RealLorentzTensor d X) (i : IndexValue d (markEmbedding f T).color) (x : X)
    (hx : ¬ x ∈ (Finset.image f Finset.univ)) : (markEmbeddingIndexValue f T).symm i x =
    (colorsIndexCast ((congrFun ((Equiv.comp_symm_eq
      (markEmbeddingSet f) ((markEmbedding f) T).color T.color).mp rfl) x).trans
      ((congrArg ((markEmbedding f) T).color (markEmbeddingSet_on_not_mem f x hx))))).symm
     (i (Sum.inl ⟨x, by simpa using hx⟩)) := by
  rw [markEmbeddingIndexValue, indexValueIso_symm_apply']
  rw [markEmbeddingSet_on_not_mem_indexValue_apply f T i x hx]
  simp only [Nat.succ_eq_add_one, Function.comp_apply, markEmbedding_apply_color, colorsIndexCast,
    Equiv.cast_symm, id_eq, eq_mp_eq_cast, eq_mpr_eq_cast, Equiv.cast_apply, cast_cast, cast_eq,
    Equiv.cast_refl, Equiv.refl_symm]
  rfl
 /-- Given an equivalence of types, an embedding `f` to an embedding `g`, the equivalence
  taking the complement of the image of `f` to the complement of the image of `g`. -/
@[simps!]
 def equivEmbedCompl (e : X ≃ Y) {f : Fin n ↪ X} {g : Fin n ↪ Y} (he : f.trans e = g) :
    {x // x ∈ (Finset.image f Finset.univ)ᶜ} ≃ {y // y ∈ (Finset.image g Finset.univ)ᶜ} :=
  (Equiv.subtypeEquivOfSubtype' e).trans <|
  (Equiv.subtypeEquivRight (fun x => by simp [← he, Equiv.eq_symm_apply]))
 lemma markEmbedding_mapIso_right (e : X ≃ Y) (f : Fin n ↪ X) (g : Fin n ↪ Y) (he : f.trans e = g)
    (T : RealLorentzTensor d X) : markEmbedding g (mapIso d e T) =
    mapIso d (Equiv.sumCongr (equivEmbedCompl e he) (Equiv.refl (Fin n))) (markEmbedding f T) := by
  rw [markEmbedding, markEmbedding]
  erw [← Equiv.trans_apply, ← Equiv.trans_apply]
  rw [mapIso_trans, mapIso_trans]
  apply congrFun
  repeat apply congrArg
  refine Equiv.ext (fun x => ?_)
  simp only [Equiv.trans_apply, Equiv.sumCongr_apply, Equiv.coe_refl]
  by_cases hx : x ∈ Finset.image f Finset.univ
  · rw [markEmbeddingSet_on_mem f x hx, markEmbeddingSet_on_mem g (e x) (by simpa [← he] using hx)]
    subst he
    simp only [Sum.map_inr, id_eq, Sum.inr.injEq, Equiv.symm_apply_eq,
      Function.Embedding.toEquivRange_apply, Function.Embedding.trans_apply, Equiv.coe_toEmbedding,
      Subtype.mk.injEq, EmbeddingLike.apply_eq_iff_eq]
    change x = f.toEquivRange _
    rw [Equiv.apply_symm_apply]
  · rw [markEmbeddingSet_on_not_mem f x hx,
      markEmbeddingSet_on_not_mem g (e x) (by simpa [← he] using hx)]
    subst he
    rfl
 lemma markEmbedding_mapIso_left {n m : ℕ} (e : Fin n ≃ Fin m) (f : Fin n ↪ X) (g : Fin m ↪ X)
    (he : e.symm.toEmbedding.trans f = g) (T : RealLorentzTensor d X) :
    markEmbedding g T = mapIso d (Equiv.sumCongr (Equiv.subtypeEquivRight (fun x => by
     simpa [← he] using Equiv.forall_congr_left e)) e) (markEmbedding f T) := by
  rw [markEmbedding, markEmbedding]
  erw [← Equiv.trans_apply]
  rw [mapIso_trans]
  apply congrFun
  repeat apply congrArg
  refine Equiv.ext (fun x => ?_)
  simp only [Equiv.trans_apply, Equiv.sumCongr_apply]
  by_cases hx : x ∈ Finset.image f Finset.univ
  · rw [markEmbeddingSet_on_mem f x hx, markEmbeddingSet_on_mem g x (by
      simp [← he, hx]
      obtain ⟨y, _, hy2⟩ := Finset.mem_image.mp hx
      use e y
      simpa using hy2)]
    subst he
    simp [Equiv.symm_apply_eq]
    change x = f.toEquivRange _
    rw [Equiv.apply_symm_apply]
  · rw [markEmbeddingSet_on_not_mem f x hx, markEmbeddingSet_on_not_mem g x (by
      simpa [← he, hx] using fun x => not_exists.mp (Finset.mem_image.mpr.mt hx) (e.symm x))]
    subst he
    rfl
 /-!
 ## Marking a single element
 -/
 /-- An embedding from `Fin 1` into `X` given an element `x ∈ X`. -/
@[simps!]
 def embedSingleton (x : X) : Fin 1 ↪ X :=
  ⟨![x], fun x y => by fin_cases x; fin_cases y; simp⟩
 lemma embedSingleton_toEquivRange_symm (x : X) :
    (embedSingleton x).toEquivRange.symm ⟨x, by simp⟩ = 0 := by
  exact Fin.fin_one_eq_zero _
 /-- Equivalence, taking a tensor to a tensor with a single marked index. -/
@[simps!]
 def markSingle (x : X) : RealLorentzTensor d X ≃ Marked d {x' // x' ≠ x} 1 :=
  (markEmbedding (embedSingleton x)).trans
  (mapIso d (Equiv.sumCongr (Equiv.subtypeEquivRight (fun x => by simp)) (Equiv.refl _)))
 /-- Equivalence between index values of a tensor and the corresponding tensor with a single
  marked index. -/
@[simps!]
 def markSingleIndexValue (T : RealLorentzTensor d X) (x : X) :
    IndexValue d T.color ≃ IndexValue d (markSingle x T).color :=
  (markEmbeddingIndexValue (embedSingleton x) T).trans <|
  indexValueIso d (Equiv.sumCongr (Equiv.subtypeEquivRight (fun x => by simp)) (Equiv.refl _))
   (by funext x_1; simp)
 /-- Given an equivalence of types, taking `x` to `y` the corresponding equivalence of
  subtypes of elements not equal to `x` and not equal to `y` respectively. -/
@[simps!]
 def equivSingleCompl (e : X ≃ Y) {x : X} {y : Y} (he : e x = y) :
    {x' // x' ≠ x} ≃ {y' // y' ≠ y} :=
  (Equiv.subtypeEquivOfSubtype' e).trans <|
  Equiv.subtypeEquivRight (fun a => by simp [Equiv.symm_apply_eq, he])
 lemma markSingle_mapIso (e : X ≃ Y) (x : X) (y : Y) (he : e x = y)
    (T : RealLorentzTensor d X) : markSingle y (mapIso d e T) =
    mapIso d (Equiv.sumCongr (equivSingleCompl e he) (Equiv.refl _)) (markSingle x T) := by
  rw [markSingle, Equiv.trans_apply]
  rw [markEmbedding_mapIso_right e (embedSingleton x) (embedSingleton y)
    (Function.Embedding.ext_iff.mp (fun a => by simpa using he)), markSingle, markEmbedding]
  erw [← Equiv.trans_apply, ← Equiv.trans_apply, ← Equiv.trans_apply]
  rw [mapIso_trans, mapIso_trans, mapIso_trans, mapIso_trans]
  apply congrFun
  repeat apply congrArg
  refine Equiv.ext fun x => ?_
  simp only [ne_eq, Fintype.univ_ofSubsingleton, Fin.zero_eta, Fin.isValue, Equiv.sumCongr_trans,
    Equiv.trans_refl, Equiv.trans_apply, Equiv.sumCongr_apply, Equiv.coe_trans, Equiv.coe_refl,
    Sum.map_map, CompTriple.comp_eq]
  subst he
  rfl
 /-!
 ## Marking two elements
 -/
 /-- An embedding from `Fin 2` given two inequivalent elements. -/
@[simps!]
 def embedDoubleton (x y : X) (h : x ≠ y) : Fin 2 ↪ X :=
  ⟨![x, y], fun a b => by
    fin_cases a <;> fin_cases b <;> simp [h]
    exact h.symm⟩
 end markingElements
 end Marked
 noncomputable section basis
@ -821,28 +501,28 @@ open Set LinearMap Submodule
 variable {d : ℕ} {X Y Y' X'  : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
  [Fintype Y'] [DecidableEq Y'] [Fintype X'] [DecidableEq X']
-  (cX : X → Colors) (cY : Y → Colors)
+  (cX : X → Color) (cY : Y → Color)
-def basisColorFiber : Basis (IndexValue d cX) ℝ (ColorFiber d cX) := Pi.basisFun _ _
+def basis : Basis (IndexValue d cX) ℝ (RealLorentzTensor d cX) := Pi.basisFun _ _
@[simp]
 def basisProd :
-    Basis (IndexValue d cX × IndexValue d cY) ℝ (ColorFiber d cX ⊗[ℝ] ColorFiber d cY) :=
+    Basis (IndexValue d cX × IndexValue d cY) ℝ (RealLorentzTensor d cX ⊗[ℝ] RealLorentzTensor d cY) :=
-  (Basis.tensorProduct (basisColorFiber cX) (basisColorFiber cY))
+  (Basis.tensorProduct (basis cX) (basis cY))
-lemma mapIsoFiber_basis {cX : X → Colors} {cY : Y → Colors} (e : X ≃ Y) (h : cX = cY ∘ e)
+lemma mapIsoFiber_basis {cX : X → Color} {cY : Y → Color} (e : X ≃ Y) (h : cX = cY ∘ e)
-    (i : IndexValue d cX) : (mapIsoFiber d e h) (basisColorFiber cX i)
+    (i : IndexValue d cX) : (mapIso e h) (basis cX i)
-    = basisColorFiber cY (indexValueIso d e h i) := by
+    = basis cY (indexValueIso d e h i) := by
  funext a
-  rw [mapIsoFiber_apply]
+  rw [mapIso_apply]
  by_cases ha : a = ((indexValueIso d e h) i)
  · subst ha
    nth_rewrite 2 [indexValueIso_eq_symm]
    rw [Equiv.apply_symm_apply]
-    simp only [basisColorFiber]
+    simp only [basis]
    erw [Pi.basisFun_apply, Pi.basisFun_apply]
    simp only [stdBasis_same]
-  · simp only [basisColorFiber]
+  · simp only [basis]
    erw [Pi.basisFun_apply, Pi.basisFun_apply]
    simp
    rw [if_neg, if_neg]
@ -851,24 +531,7 @@ lemma mapIsoFiber_basis {cX : X → Colors} {cY : Y → Colors} (e : X ≃ Y) (h
    exact fun a_1 => ha (_root_.id (Eq.symm a_1))
 end basis
 /-!
 ## 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 $ colorsIndexDualCast h x))
 /-! TODO: Following the ethos of modular operads, prove properties of contraction. -/
--- a/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
@ -29,7 +29,7 @@ to the real numbers, i.e. which is invariant under transformations of mapIso.
 /-- An equivalence from Real tensors on an empty set to `ℝ`. -/
@[simps!]
-def toReal (d : ℕ) {X : Type} (h : IsEmpty X) : RealLorentzTensor d X ≃ ℝ where
+def toReal (d : ℕ) {X : Type} (h : IsEmpty X) (f : X → Color) : RealLorentzTensor d f ≃ ℝ where
  toFun := fun T => T.coord (IsEmpty.elim h)
  invFun := fun r => {
    color := fun x => IsEmpty.elim h x,
--- a/HepLean/SpaceTime/LorentzTensor/Real/Contraction.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Contraction.lean
@ -0,0 +1,119 @@
 /-
 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.TensorProducts
 /-!
 # 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: Set up a good notation for the multiplication. -/
 namespace RealLorentzTensor
 open TensorProduct
 open Set LinearMap Submodule
 variable {d : ℕ} {X Y Y' X'  : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
  [Fintype Y'] [DecidableEq Y'] [Fintype X'] [DecidableEq X']
  (cX : X → Color) (cY : Y → Color)
 /-- The contraction of all indices of two tensors with dual index-colors.
  This is a bilinear map to ℝ. -/
@[simps!]
 def contrAll {f1 : X → Color} {f2 : Y → Color} (e : X ≃ Y) (hc : f1 = τ ∘ f2 ∘ e) :
    RealLorentzTensor d f1 →ₗ[ℝ] RealLorentzTensor d f2 →ₗ[ℝ] ℝ where
  toFun T := {
    toFun := fun S => ∑ i, T i * S (indexValueDualIso d e hc i),
    map_add' := fun S F => by
      trans  ∑ i, (T i * S (indexValueDualIso d e hc i) + T i * F (indexValueDualIso d e hc i))
      exact Finset.sum_congr rfl (fun i _ => mul_add _ _ _ )
      exact Finset.sum_add_distrib,
    map_smul' := fun r S => by
      trans ∑ i , r * (T i * S (indexValueDualIso d e hc i))
      refine Finset.sum_congr rfl (fun x _ => ?_)
      ring_nf
      rw [mul_assoc]
      rfl
      rw [← Finset.mul_sum]
      rfl}
  map_add' := fun T S => by
    ext F
    trans ∑ i , (T i * F (indexValueDualIso d e hc i) + S i * F (indexValueDualIso d e hc i))
    exact Finset.sum_congr rfl (fun x _ => add_mul _ _ _)
    exact Finset.sum_add_distrib
  map_smul' := fun r T => by
    ext S
    trans ∑ i , r * (T i * S (indexValueDualIso d e hc i))
    refine Finset.sum_congr rfl (fun x _ => mul_assoc _ _ _)
    rw [← Finset.mul_sum]
    rfl
 lemma contrAll_symm {f1 : X → Color} {f2 : Y → Color} (e : X ≃ Y)
    (h : f1 = τ ∘ f2 ∘ e) (T : RealLorentzTensor d f1) (S : RealLorentzTensor d f2) :
    contrAll e h T S = contrAll e.symm (indexValueDualIso_cond_symm h) S T := by
  rw [contrAll_apply_apply, contrAll_apply_apply, ← Equiv.sum_comp (indexValueDualIso d e h)]
  refine Finset.sum_congr rfl (fun i _ => ?_)
  rw [mul_comm, ← Equiv.trans_apply]
  simp
 lemma contrAll_mapIsoFiber_right {f1 : X → Color} {f2 : Y → Color}
    {g2 : Y' → Color} (e : X ≃ Y) (eY : Y ≃ Y')
    (h : f1 = τ ∘ f2 ∘ e) (hY : f2 = g2 ∘ eY) (T : RealLorentzTensor d f1) (S : RealLorentzTensor d f2) :
    contrAll e h T S = contrAll (e.trans eY) (indexValueDualIso_cond_trans_indexValueIso h hY)
      T (mapIso eY hY S) := by
  rw [contrAll_apply_apply, contrAll_apply_apply]
  refine Finset.sum_congr rfl (fun i _ => Mathlib.Tactic.Ring.mul_congr rfl ?_ rfl)
  rw [mapIso_apply, ← Equiv.trans_apply]
  simp only [indexValueDualIso_trans_indexValueIso]
  congr
  ext1 x
  simp only [Equiv.trans_apply, Equiv.symm_apply_apply]
 lemma contrAll_mapIsoFiber_left {f1 : X → Color} {f2 : Y → Color}
    {g1 : X' → Color} (e : X ≃ Y) (eX : X ≃ X')
    (h : f1 = τ ∘ f2 ∘ e) (hX : f1 = g1 ∘ eX) (T : RealLorentzTensor d f1) (S : RealLorentzTensor d f2) :
    contrAll e h T S = contrAll (eX.symm.trans e)
    (indexValueIso_trans_indexValueDualIso_cond ((Equiv.eq_comp_symm eX g1 f1).mpr hX.symm) h)
    (mapIso eX hX T) S := by
  rw [contrAll_symm, contrAll_mapIsoFiber_right _ eX _ hX, contrAll_symm]
  rfl
 lemma contrAll_lorentzAction {f1 : X → Color} {f2 : Y → Color} (e : X ≃ Y)
    (hc : f1 = τ ∘ f2 ∘ e) (T : RealLorentzTensor d f1) (S : RealLorentzTensor d f2) (Λ : LorentzGroup d) :
    contrAll e hc (Λ • T) (Λ • S) = contrAll e hc T S := by
  change ∑ i, (∑ j, toTensorRepMat Λ i j * T j) *
    (∑ k, toTensorRepMat Λ (indexValueDualIso d e hc i) k * S k) = _
  trans ∑ i, ∑ j, ∑ k, (toTensorRepMat Λ (indexValueDualIso d e hc i) k * toTensorRepMat Λ i j)
      * T j * S 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, ∑ i, (toTensorRepMat Λ (indexValueDualIso d e hc i) k
    * toTensorRepMat Λ i j) * T j * S k
  · apply Finset.sum_congr rfl (fun j _ => ?_)
    rw [Finset.sum_comm]
  trans ∑ j, ∑ k, (toTensorRepMat 1 (indexValueDualIso d e.symm (indexValueDualIso_cond_symm hc) k) j) * T j * S k
  · apply Finset.sum_congr rfl (fun j _ => Finset.sum_congr rfl (fun k _ => ?_))
    rw [← Finset.sum_mul, ← Finset.sum_mul]
    erw [toTensorRepMat_indexValueDualIso_sum]
  rw [Finset.sum_comm]
  trans ∑ k, T (indexValueDualIso d e.symm (indexValueDualIso_cond_symm hc) k) * S k
  · apply Finset.sum_congr rfl (fun k _ => ?_)
    rw [← Finset.sum_mul, ← toTensorRepMat_one_coord_sum' T]
  rw [← Equiv.sum_comp (indexValueDualIso d e hc), ← indexValueDualIso_symm e hc]
  simp only [Equiv.symm_apply_apply, contrAll_apply_apply]
 end RealLorentzTensor
--- a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
@ -19,15 +19,15 @@ 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]
-  (T : RealLorentzTensor d X) (c : X → Colors) (Λ Λ' : LorentzGroup d) {μ : Colors}
+   (c : X → Color) (Λ Λ' : LorentzGroup d) {μ : Color}
-open LorentzGroup BigOperators Marked
+open LorentzGroup BigOperators
 /-- Monoid homomorphism from the Lorentz group to matrices indexed by `ColorsIndex d μ` for a
  color `μ`.
  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
+def colorMatrix (μ : Color) : LorentzGroup d →* Matrix (ColorIndex d μ) (ColorIndex d μ) ℝ where
  toFun Λ := match μ with
    | .up => fun i j => Λ.1 i j
    | .down => fun i j => (LorentzGroup.transpose Λ⁻¹).1 i j
@ -35,11 +35,11 @@ def colorMatrix (μ : Colors) : LorentzGroup d →* Matrix (ColorsIndex d μ) (C
    ext i j
    match μ with
    | .up =>
-        simp only [lorentzGroupIsGroup_one_coe, OfNat.ofNat, One.one, ColorsIndex]
+        simp only [lorentzGroupIsGroup_one_coe, OfNat.ofNat, One.one, ColorIndex]
        congr
    | .down =>
        simp only [transpose, inv_one, lorentzGroupIsGroup_one_coe, Matrix.transpose_one]
-        simp only [OfNat.ofNat, One.one, ColorsIndex]
+        simp only [OfNat.ofNat, One.one, ColorIndex]
        congr
  map_mul' Λ Λ' := by
    ext i j
@ -51,18 +51,18 @@ def colorMatrix (μ : Colors) : LorentzGroup d →* Matrix (ColorsIndex d μ) (C
          Matrix.transpose_mul, Matrix.transpose_apply]
        rfl
-lemma colorMatrix_ext  {μ : Colors} {a b c d : ColorsIndex d μ} (hab : a = b) (hcd : c = d) :
+lemma colorMatrix_ext  {μ : Color} {a b c d : ColorIndex d μ} (hab : a = b) (hcd : c = d) :
    (colorMatrix μ) Λ  a c = (colorMatrix  μ) Λ b d := by
    rw [hab, hcd]
-lemma colorMatrix_cast {μ ν : Colors} (h : μ = ν) (Λ : LorentzGroup d) :
+lemma colorMatrix_cast {μ ν : Color} (h : μ = ν) (Λ : LorentzGroup d) :
    colorMatrix ν Λ =
-    Matrix.reindex (colorsIndexCast h) (colorsIndexCast h) (colorMatrix μ Λ) := by
+    Matrix.reindex (colorIndexCast h) (colorIndexCast h) (colorMatrix μ Λ) := by
  subst h
  rfl
-lemma colorMatrix_dual_cast {μ ν : Colors} (Λ : LorentzGroup d) (h : μ = τ ν) :
+lemma colorMatrix_dual_cast {μ ν : Color} (Λ : LorentzGroup d) (h : μ = τ ν) :
-    colorMatrix ν Λ = Matrix.reindex (colorsIndexDualCast h) (colorsIndexDualCast h)
+    colorMatrix ν Λ = Matrix.reindex (colorIndexDualCast h) (colorIndexDualCast h)
    (colorMatrix μ (LorentzGroup.transpose Λ⁻¹)) := by
  subst h
  match ν with
@ -70,16 +70,16 @@ lemma colorMatrix_dual_cast {μ ν : Colors} (Λ : LorentzGroup d) (h : μ = τ
    ext i j
    simp only [colorMatrix, MonoidHom.coe_mk, OneHom.coe_mk, τ, transpose, lorentzGroupIsGroup_inv,
      Matrix.transpose_apply, minkowskiMetric.dual_transpose, minkowskiMetric.dual_dual,
-      Matrix.reindex_apply, colorsIndexDualCast_symm, Matrix.submatrix_apply]
+      Matrix.reindex_apply, colorIndexDualCast_symm, Matrix.submatrix_apply]
    rfl
  | .down =>
    ext i j
-    simp only [τ, colorMatrix, MonoidHom.coe_mk, OneHom.coe_mk, colorsIndexDualCastSelf, transpose,
+    simp only [τ, colorMatrix, MonoidHom.coe_mk, OneHom.coe_mk, colorIndexDualCastSelf, transpose,
      lorentzGroupIsGroup_inv, Matrix.transpose_apply, minkowskiMetric.dual_transpose,
      minkowskiMetric.dual_dual, Matrix.reindex_apply, Equiv.coe_fn_symm_mk, Matrix.submatrix_apply]
    rfl
-lemma colorMatrix_transpose {μ : Colors} (Λ : LorentzGroup d) :
+lemma colorMatrix_transpose {μ : Color} (Λ : LorentzGroup d) :
    colorMatrix μ (LorentzGroup.transpose Λ) = (colorMatrix μ Λ).transpose := by
  match μ with
  | .up => rfl
@ -96,7 +96,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} :
+def toTensorRepMat {c : X → Color} :
    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
@ -135,18 +135,18 @@ lemma toTensorRepMat_mul' (i j : IndexValue d c) :
  rw [Finset.prod_mul_distrib]
  rfl
-lemma toTensorRepMat_of_indexValueSumEquiv {cX : X → Colors} {cY : Y → Colors}
+lemma toTensorRepMat_of_indexValueSumEquiv {cX : X → Color} {cY : Y → Color}
    (i j : IndexValue d (Sum.elim cX cY)) :
-    toTensorRepMat Λ i j = toTensorRepMat Λ (indexValueSumEquiv i).1 (indexValueSumEquiv j).1 *
+    toTensorRepMat Λ i j = toTensorRepMat Λ (indexValueTensorator i).1 (indexValueTensorator j).1 *
-    toTensorRepMat Λ (indexValueSumEquiv i).2 (indexValueSumEquiv j).2 :=
+    toTensorRepMat Λ (indexValueTensorator i).2 (indexValueTensorator 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}
+lemma toTensorRepMat_of_indexValueSumEquiv' {cX : X → Color} {cY : Y → Color}
    (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)) :=
+    toTensorRepMat Λ (indexValueTensorator.symm (i, k)) (indexValueTensorator.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
+    (indexValueTensorator.symm (i, k) x) (indexValueTensorator.symm (j, l) x)).symm
 /-!
@ -154,7 +154,7 @@ lemma toTensorRepMat_of_indexValueSumEquiv' {cX : X → Colors} {cY : Y → Colo
 -/
-lemma toTensorRepMat_indexValueDualIso_left {f1 : X → Colors} {f2 : Y → Colors}
+lemma toTensorRepMat_indexValueDualIso_left {f1 : X → Color} {f2 : Y → Color}
    (e : X ≃ Y) (hc : f1 = τ ∘ f2 ∘ e) (i : IndexValue d f1) (j : IndexValue d f2) :
    toTensorRepMat Λ (indexValueDualIso d e hc i) j =
    toTensorRepMat Λ⁻¹ (indexValueDualIso d e.symm (indexValueDualIso_cond_symm hc) j) i := by
@ -162,18 +162,18 @@ lemma toTensorRepMat_indexValueDualIso_left {f1 : X → Colors} {f2 : Y → Colo
  apply Finset.prod_congr rfl (fun x _ => ?_)
  erw [colorMatrix_dual_cast Λ (congrFun hc x)]
  rw [Matrix.reindex_apply, colorMatrix_transpose]
-  simp only [Function.comp_apply, colorsIndexDualCast_symm,
+  simp only [Function.comp_apply, colorIndexDualCast_symm,
    Matrix.submatrix_apply, Matrix.transpose_apply]
  rw [indexValueDualIso_eq_symm, indexValueDualIso_symm_apply',
    indexValueDualIso_eq_symm, indexValueDualIso_symm_apply']
-  rw [← Equiv.trans_apply, colorsIndexDualCast_symm, colorsIndexDualCast_trans]
+  rw [← Equiv.trans_apply, colorIndexDualCast_symm, colorsIndexDualCast_trans]
  apply colorMatrix_ext
  simp
-  simp [colorsIndexCast]
+  simp [colorIndexCast]
  apply cast_eq_iff_heq.mpr
  rw [Equiv.symm_apply_apply]
-lemma toTensorRepMat_indexValueDualIso_sum {f1 : X → Colors} {f2 : Y → Colors}
+lemma toTensorRepMat_indexValueDualIso_sum {f1 : X → Color} {f2 : Y → Color}
    (e : X ≃ Y) (hc : f1 = τ ∘ f2 ∘ e) (j : IndexValue d f1) (k : IndexValue d f2) :
    (∑ i : IndexValue d f1, toTensorRepMat Λ ((indexValueDualIso d e hc) i) k * toTensorRepMat Λ i j) =
    toTensorRepMat 1 (indexValueDualIso d e.symm (indexValueDualIso_cond_symm hc) k) j := by
@ -183,8 +183,8 @@ lemma toTensorRepMat_indexValueDualIso_sum {f1 : X → Colors} {f2 : Y → Color
  rw [toTensorRepMat_indexValueDualIso_left]
  rw [← Matrix.mul_apply, ← toTensorRepMat.map_mul, inv_mul_self Λ]
-lemma toTensorRepMat_one_coord_sum' {f1 : X → Colors}
+lemma toTensorRepMat_one_coord_sum' {f1 : X → Color}
-      (T : ColorFiber d f1) (k : IndexValue d f1) :
+      (T : RealLorentzTensor d f1) (k : IndexValue d f1) :
        ∑ j, (toTensorRepMat 1 k j) * T j = T k := by
  erw [Finset.sum_eq_single_of_mem k]
  simp only [IndexValue, map_one, Matrix.one_apply_eq, one_mul]
@ -193,23 +193,6 @@ lemma toTensorRepMat_one_coord_sum' {f1 : X → Colors}
  simp only [IndexValue, map_one, mul_eq_zero]
  exact Or.inl (Matrix.one_apply_ne' hjk)
 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)) :=
  (Fintype.prod_sum_type fun x =>
  (colorMatrix (T.color x)) Λ (splitIndexValue.symm (i, k) x) (splitIndexValue.symm (j, l) x)).symm
 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, IndexValue]
  exact Or.inl (Matrix.one_apply_ne' hjk)
 /-!
@ -217,8 +200,8 @@ lemma toTensorRepMat_one_coord_sum (T : Marked d X n) (i : T.UnmarkedIndexValue)
 -/
@[simps!]
-def lorentzActionFiber {c : X → Colors} :
+def lorentzAction {c : X → Color} :
-    Representation ℝ (LorentzGroup d) (ColorFiber d c) where
+    Representation ℝ (LorentzGroup d) (RealLorentzTensor d c) where
  toFun Λ :=  {
    toFun := fun T i => ∑ j, toTensorRepMat Λ i j * T j,
    map_add' := fun T S => by
@ -260,13 +243,14 @@ def lorentzActionFiber {c : X → Colors} :
      rw [← mul_assoc, Finset.prod_mul_distrib]
      rfl
 scoped[RealLorentzTensor] infixl:78 " • " => lorentzAction
 /-- The Lorentz action commutes with `mapIso`. -/
-lemma lorentzActionFiber_mapIsoFiber (e : X ≃ Y) {f1 : X → Colors}
+lemma lorentzAction_mapIso (e : X ≃ Y) {f1 : X → Color}
-    {f2 : Y → Colors} (h : f1 = f2 ∘ e) (Λ : LorentzGroup d)
+    {f2 : Y → Color} (h : f1 = f2 ∘ e) (Λ : LorentzGroup d)
-    (T : ColorFiber d f1) : mapIsoFiber d e h (lorentzActionFiber Λ T) =
+    (T : RealLorentzTensor d f1) : mapIso e h (Λ • T) = Λ • (mapIso e h T) := by
    lorentzActionFiber Λ (mapIsoFiber d e h T) := by
  funext i
-  rw [mapIsoFiber_apply, lorentzActionFiber_apply_apply, lorentzActionFiber_apply_apply]
+  rw [mapIso_apply, lorentzAction_apply_apply, lorentzAction_apply_apply]
  rw [← Equiv.sum_comp (indexValueIso d e h)]
  refine Finset.sum_congr rfl (fun j _ => Mathlib.Tactic.Ring.mul_congr ?_ ?_ rfl)
  · rw [← Equiv.prod_comp e]
@ -277,236 +261,48 @@ lemma lorentzActionFiber_mapIsoFiber (e : X ≃ Y) {f1 : X → Colors}
    apply colorMatrix_ext
    rw [indexValueIso_eq_symm, indexValueIso_symm_apply']
    erw [← Equiv.eq_symm_apply]
-    simp only [Function.comp_apply, Equiv.symm_symm_apply, colorsIndexCast, Equiv.cast_symm,
+    simp only [Function.comp_apply, Equiv.symm_symm_apply, colorIndexCast, Equiv.cast_symm,
      Equiv.cast_apply, cast_cast, cast_eq]
    rw [indexValueIso_eq_symm, indexValueIso_symm_apply']
-    simp [colorsIndexCast]
+    simp [colorIndexCast]
    symm
    refine cast_eq_iff_heq.mpr ?_
    rw [Equiv.symm_apply_apply]
-  · rw [mapIsoFiber_apply]
+  · rw [mapIso_apply]
    apply congrArg
    rw [← Equiv.trans_apply]
    simp
 /-- Action of the Lorentz group on `X`-indexed Real Lorentz Tensors. -/
@[simps!]
 instance lorentzAction : MulAction (LorentzGroup d) (RealLorentzTensor d X) where
  smul Λ T := ⟨T.color, lorentzActionFiber Λ T.coord⟩
  one_smul T := by
    refine ext rfl ?_
    simp only [HSMul.hSMul, map_one, LinearMap.one_apply]
    rfl
  mul_smul Λ Λ' T := by
    refine ext rfl ?_
    simp  [HSMul.hSMul]
    rfl
 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
 /-!
 ## 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 ?_
  funext i
  erw [lorentzAction_smul_coord, mapIsoFiber_apply]
  simp only [lorentzActionFiber_apply_apply, Finset.univ_eq_empty, Finset.prod_empty, one_mul,
    indexValueIso_refl, Equiv.refl_symm]
  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) :
    mapIso d f (Λ • T) = Λ • (mapIso d f T) :=
  ext rfl (lorentzActionFiber_mapIsoFiber  f _ Λ T.coord)
 section
 variable {d : ℕ} {X Y Y' X'  : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
  [Fintype Y'] [DecidableEq Y'] [Fintype X'] [DecidableEq X']
-  (cX : X → Colors) (cY : Y → Colors)
+  (cX : X → Color) (cY : Y → Color)
-lemma lorentzActionFiber_basis (Λ : LorentzGroup d)  (i : IndexValue d cX) :
+lemma lorentzAction_basis (Λ : LorentzGroup d)  (i : IndexValue d cX) :
-    lorentzActionFiber Λ (basisColorFiber cX i) =
+    Λ • (basis cX i) = ∑ j, toTensorRepMat Λ j i • basis cX j := by
    ∑ j, toTensorRepMat Λ j i • basisColorFiber cX j := by
  funext k
-  simp only [lorentzActionFiber, MonoidHom.coe_mk, OneHom.coe_mk,
+  simp only [lorentzAction, MonoidHom.coe_mk, OneHom.coe_mk,
    LinearMap.coe_mk, AddHom.coe_mk]
  rw [Finset.sum_apply]
  rw [Finset.sum_eq_single_of_mem i, Finset.sum_eq_single_of_mem k]
  change _ = toTensorRepMat Λ k i * (Pi.basisFun ℝ (IndexValue d cX)) k k
-  rw [basisColorFiber]
+  rw [basis]
  erw [Pi.basisFun_apply, Pi.basisFun_apply]
  simp
  exact Finset.mem_univ k
  intro b _ hbk
-  change toTensorRepMat Λ b i • (basisColorFiber cX) b k = 0
+  change toTensorRepMat Λ b i • (basis cX) b k = 0
-  erw [basisColorFiber, Pi.basisFun_apply]
+  erw [basis, Pi.basisFun_apply]
  simp [hbk]
  exact Finset.mem_univ i
  intro b hb hbk
-  erw [basisColorFiber, Pi.basisFun_apply]
+  erw [basis, Pi.basisFun_apply]
  simp [hbk]
  intro a
  subst a
  simp_all only [Finset.mem_univ, ne_eq, not_true_eq_false]
 end
 /-!
 ## 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
 /-- 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. -/
 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
 /-- 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
  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
 /-- 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 contraction. -/
 /-! TODO: Show that the Lorentz action commutes with rising and lowering indices. -/
 end RealLorentzTensor
--- a/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
@ -1,534 +0,0 @@
 /-
 Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import 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: 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
 section mulMarkedFiber
 variable {cX : X → Colors} {cY : Y → Colors} {fX : Fin 1 → Colors} {fY : Fin 1 → Colors}
 /-- The index value appearing in the multiplication of Marked tensors on the left. -/
 def mulMarkedFiberFstArg  (i : IndexValue d (Sum.elim cX cY)) (x : ColorsIndex d (fX 0)) :
    IndexValue d (Sum.elim cX fX) :=
  indexValueSumEquiv.symm ((indexValueSumEquiv i).1, indexValueFinOne x)
 /-- The index value appearing in the multiplication of Marked tensors on the right. -/
 def mulMarkedFiberSndArg (i : IndexValue d (Sum.elim cX cY)) (x : ColorsIndex d (fX 0))
    (h : fX 0 = τ (fY 0)) : IndexValue d (Sum.elim cY fY) :=
  indexValueSumEquiv.symm ((indexValueSumEquiv i).2, indexValueFinOne $ colorsIndexDualCast h x)
 def mulMarkedFiber (h : fX 0 = τ (fY 0)) : ColorFiber d (Sum.elim cX fX) →ₗ[ℝ]
      ColorFiber d (Sum.elim cY fY) →ₗ[ℝ] ColorFiber d (Sum.elim cX cY) where
  toFun T := {
    toFun := fun S i => ∑ x, T (mulMarkedFiberFstArg i x) * S (mulMarkedFiberSndArg i x h),
    map_add' := fun F S => by
      funext i
      trans ∑ x , (T (mulMarkedFiberFstArg i x) * F (mulMarkedFiberSndArg i x h) +
        T (mulMarkedFiberFstArg i x) * S (mulMarkedFiberSndArg i x h))
      exact Finset.sum_congr rfl (fun x _ => mul_add _ _ _ )
      exact Finset.sum_add_distrib,
    map_smul' := fun r S => by
      funext i
      trans ∑ x , r * (T (mulMarkedFiberFstArg i x) * S (mulMarkedFiberSndArg i x h))
      refine Finset.sum_congr rfl (fun x _ => ?_)
      ring_nf
      rw [mul_assoc]
      rfl
      rw [← Finset.mul_sum]
      rfl}
  map_add' := fun T S => by
    ext F
    funext i
    trans ∑ x , (T (mulMarkedFiberFstArg i x) * F (mulMarkedFiberSndArg i x h) +
        S (mulMarkedFiberFstArg i x) * F (mulMarkedFiberSndArg i x h))
    exact Finset.sum_congr rfl (fun x _ => add_mul _ _ _)
    exact Finset.sum_add_distrib
  map_smul' := fun r T => by
    ext S
    funext i
    trans ∑ x , r * (T (mulMarkedFiberFstArg i x) * S (mulMarkedFiberSndArg i x h))
    refine Finset.sum_congr rfl (fun x _ => mul_assoc _ _ _)
    rw [← Finset.mul_sum]
    rfl
 end mulMarkedFiber
 /-- 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 mulMarked {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))
 /-- The index value appearing in the multiplication of Marked tensors on the left. -/
 def mulMarkedFstArg {X Y : Type} {T : Marked d X 1} {S : Marked d Y 1}
    (i : IndexValue d (Sum.elim T.unmarkedColor S.unmarkedColor))
    (x : ColorsIndex d (T.color (markedPoint X 0))) : IndexValue d T.color :=
  splitIndexValue.symm ((indexValueSumEquiv i).1, oneMarkedIndexValue x)
 lemma mulMarkedFstArg_inr {X Y : Type} {T : Marked d X 1} {S : Marked d Y 1}
    (i : IndexValue d (Sum.elim T.unmarkedColor S.unmarkedColor))
    (x : ColorsIndex d (T.color (markedPoint X 0))) :
    mulMarkedFstArg i x (Sum.inr 0) = x := by
  rfl
 lemma mulMarkedFstArg_inl {X Y : Type} {T : Marked d X 1} {S : Marked d Y 1}
    (i : IndexValue d (Sum.elim T.unmarkedColor S.unmarkedColor))
    (x : ColorsIndex d (T.color (markedPoint X 0))) (c : X):
    mulMarkedFstArg i x (Sum.inl c) = i (Sum.inl c) := by
  rfl
 /-- The index value appearing in the multiplication of Marked tensors on the right. -/
 def mulMarkedSndArg {X Y : Type} {T : Marked d X 1} {S : Marked d Y 1}
    (i : IndexValue d (Sum.elim T.unmarkedColor S.unmarkedColor))
    (x : ColorsIndex d (T.color (markedPoint X 0))) (h : T.markedColor 0 = τ (S.markedColor 0)) :
    IndexValue d S.color :=
  splitIndexValue.symm ((indexValueSumEquiv i).2, oneMarkedIndexValue $ colorsIndexDualCast h x)
 /-!
 ## Expressions for multiplication
 -/
 /-! TODO: Where appropriate write these expresions in terms of `indexValueDualIso`. -/
 lemma mulMarked_colorsIndex_right {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
    (h : T.markedColor 0 = τ (S.markedColor 0)) :
    (mulMarked T S h).coord = fun i => ∑ x,
    T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1,
    oneMarkedIndexValue $ colorsIndexDualCast (color_eq_dual_symm h) x)) *
    S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, oneMarkedIndexValue x)) := by
  funext i
  rw [← Equiv.sum_comp (colorsIndexDualCast h)]
  apply Finset.sum_congr rfl (fun x _ => ?_)
  congr
  rw [← colorsIndexDualCast_symm]
  exact (Equiv.apply_eq_iff_eq_symm_apply (colorsIndexDualCast h)).mp rfl
 lemma mulMarked_indexValue_left {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
    (h : T.markedColor 0 = τ (S.markedColor 0)) :
    (mulMarked T S h).coord = fun i => ∑ j,
    T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, j)) *
    S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2,
    (oneMarkedIndexValue $ (colorsIndexDualCast h) $ oneMarkedIndexValue.symm j))) := by
  funext i
  rw [← Equiv.sum_comp (oneMarkedIndexValue)]
  rfl
 lemma mulMarked_indexValue_right {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
    (h : T.markedColor 0 = τ (S.markedColor 0)) :
    (mulMarked T S h).coord = fun i => ∑ j,
    T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1,
    oneMarkedIndexValue $ (colorsIndexDualCast h).symm $ oneMarkedIndexValue.symm j)) *
    S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, j)) := by
  funext i
  rw [mulMarked_colorsIndex_right]
  rw [← Equiv.sum_comp (oneMarkedIndexValue)]
  apply Finset.sum_congr rfl (fun x _ => ?_)
  congr
  exact Eq.symm (colorsIndexDualCast_symm h)
 /-!
 ## Properties of multiplication
 -/
 /-- Multiplication is well behaved with regard to swapping tensors. -/
 lemma mulMarked_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) (mulMarked T S h) = mulMarked S T (color_eq_dual_symm h) := by
  refine ext ?_ ?_
  · funext a
    cases a with
    | inl _ => rfl
    | inr _ => rfl
  · funext i
    rw [mulMarked_colorsIndex_right]
    refine Fintype.sum_congr _ _ (fun x => ?_)
    rw [mul_comm]
    rfl
 /-- Multiplication commutes with `mapIso`. -/
 lemma mulMarked_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) (mulMarked T S h) = mulMarked (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, mapIsoFiber_apply, mapIsoFiber_apply, mulMarked_coord, mulMarked_coord]
    refine Fintype.sum_congr _ _ (fun x => ?_)
    rw [mapIso_apply_coord, mapIso_apply_coord]
    refine Mathlib.Tactic.Ring.mul_congr ?_ ?_ rfl
    · apply congrArg
      exact (Equiv.symm_apply_eq splitIndexValue).mpr rfl
    · apply congrArg
      exact (Equiv.symm_apply_eq splitIndexValue).mpr rfl
 /-!
 ## Lorentz action and multiplication.
 -/
 /-- The marked Lorentz Action leaves multiplication invariant. -/
 lemma mulMarked_markedLorentzAction (T : Marked d X 1) (S : Marked d Y 1)
    (h : T.markedColor 0 = τ (S.markedColor 1)) :
    mulMarked (Λ •ₘ T) (Λ •ₘ S) h = mulMarked 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 mulMarked_unmarkedLorentzAction (T : Marked d X 1) (S : Marked d Y 1)
    (h : T.markedColor 0 = τ (S.markedColor 1)) :
    mulMarked (Λ •ᵤₘ T) (Λ •ᵤₘ S) h = Λ • mulMarked 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))
  · exact Finset.sum_congr rfl (fun j _ => 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, mulMarked_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]
    exact Eq.symm Fintype.sum_prod_type
  rfl
 /-- The Lorentz action commutes with multiplication. -/
 lemma mulMarked_lorentzAction (T : Marked d X 1) (S : Marked d Y 1)
    (h : T.markedColor 0 = τ (S.markedColor 1)) :
    mulMarked (Λ • T) (Λ • S) h = Λ • mulMarked T S h := by
  simp only [← marked_unmarked_action_eq_action]
  rw [mulMarked_markedLorentzAction, mulMarked_unmarkedLorentzAction]
 /-!
 ## Multiplication on selected indices
 -/
 variable {n m : ℕ} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
  {X' Y' Z : Type} [Fintype X'] [DecidableEq X'] [Fintype Y'] [DecidableEq Y']
  [Fintype Z] [DecidableEq Z]
 /-- The multiplication of two real Lorentz Tensors along specified indices. -/
@[simps!]
 def mult (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) (x : X) (y : Y)
    (h : T.color x = τ (S.color y)) : RealLorentzTensor d ({x' // x' ≠ x} ⊕ {y' // y' ≠ y}) :=
  mulMarked (markSingle x T) (markSingle y S) h
 /-- The first index value appearing in the multiplication of two Lorentz tensors. -/
 def multFstArg {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
    (i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor))
    (a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0))) :
    IndexValue d T.color := (markSingleIndexValue T x).symm (mulMarkedFstArg i a)
 lemma multFstArg_ext {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
    {i j : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor)}
    {a b : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0))}
    (hij : i = j) (hab : a = b) : multFstArg i a = multFstArg j b := by
  subst hij; subst hab
  rfl
 lemma multFstArg_on_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
    (i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor))
    (a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0))) :
    multFstArg i a x = a := by
  rw [multFstArg, markSingleIndexValue]
  simp only [ne_eq, Fintype.univ_ofSubsingleton, Fin.zero_eta, Fin.isValue, Equiv.symm_trans_apply,
     Sum.map_inr, id_eq]
  erw [markEmbeddingIndexValue_apply_symm_on_mem]
  swap
  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Finset.univ_unique, Fin.default_eq_zero,
    Fin.isValue, Finset.image_singleton, embedSingleton_apply, Finset.mem_singleton]
  rw [indexValueIso_symm_apply']
  erw [Equiv.symm_apply_eq, Equiv.symm_apply_eq]
  simp only [Function.comp_apply, colorsIndexCast, Equiv.cast_symm, Equiv.cast_apply, cast_cast]
  symm
  apply cast_eq_iff_heq.mpr
  rw [embedSingleton_toEquivRange_symm]
  rfl
 lemma multFstArg_on_not_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
    (i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor))
    (a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0)))
    (c : X) (hc : c ≠ x) : multFstArg i a c = i (Sum.inl ⟨c, hc⟩) := by
  rw [multFstArg, markSingleIndexValue]
  simp only [ne_eq, Fintype.univ_ofSubsingleton, Fin.zero_eta, Fin.isValue, Equiv.symm_trans_apply,
     Sum.map_inr, id_eq]
  erw [markEmbeddingIndexValue_apply_symm_on_not_mem]
  swap
  simpa using hc
  rfl
 /-- The second index value appearing in the multiplication of two Lorentz tensors. -/
 def multSndArg {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
    (i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor))
    (a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0)))
    (h : T.color x = τ (S.color y)) : IndexValue d S.color :=
  (markSingleIndexValue S y).symm (mulMarkedSndArg i a h)
 lemma multSndArg_on_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
    (i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor))
    (a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0)))
    (h : T.color x = τ (S.color y)) : multSndArg i a h y = colorsIndexDualCast h a := by
  rw [multSndArg, markSingleIndexValue]
  simp only [ne_eq, Fintype.univ_ofSubsingleton, Fin.zero_eta, Fin.isValue, Equiv.symm_trans_apply,
     Sum.map_inr, id_eq]
  erw [markEmbeddingIndexValue_apply_symm_on_mem]
  swap
  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Finset.univ_unique, Fin.default_eq_zero,
    Fin.isValue, Finset.image_singleton, embedSingleton_apply, Finset.mem_singleton]
  rw [indexValueIso_symm_apply']
  erw [Equiv.symm_apply_eq, Equiv.symm_apply_eq]
  simp only [Function.comp_apply, colorsIndexCast, Equiv.cast_symm, Equiv.cast_apply, cast_cast]
  symm
  apply cast_eq_iff_heq.mpr
  rw [embedSingleton_toEquivRange_symm]
  rfl
 lemma multSndArg_on_not_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
    (i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor))
    (a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0)))
    (h : T.color x = τ (S.color y)) (c : Y) (hc : c ≠ y) :
    multSndArg i a h c = i (Sum.inr ⟨c, hc⟩) := by
  rw [multSndArg, markSingleIndexValue]
  simp only [ne_eq, Fintype.univ_ofSubsingleton, Fin.zero_eta, Fin.isValue, Equiv.symm_trans_apply,
     Sum.map_inr, id_eq]
  erw [markEmbeddingIndexValue_apply_symm_on_not_mem]
  swap
  simpa using hc
  rfl
 lemma multSndArg_ext {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
    {i j : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor)}
    {a b : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0))}
    (h : T.color x = τ (S.color y)) (hij : i = j) (hab : a = b) :
    multSndArg i a h = multSndArg j b h := by
  subst hij
  subst hab
  rfl
 lemma mult_coord_arg (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) (x : X) (y : Y)
    (h : T.color x = τ (S.color y))
    (i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor)) :
  (mult T S x y h).coord i = ∑ a, T.coord (multFstArg i a) * S.coord (multSndArg i a h) := by
  rfl
 lemma mult_mapIso (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y)
    (eX : X ≃ X') (eY : Y ≃ Y') (x : X) (y : Y) (x' : X') (y' : Y') (hx : eX x = x')
    (hy : eY y = y') (h : T.color x = τ (S.color y)) :
    mult (mapIso d eX T) (mapIso d eY S) x' y' (by subst hx hy; simpa using h) =
    mapIso d (Equiv.sumCongr (equivSingleCompl eX hx) (equivSingleCompl eY hy))
      (mult T S x y h) := by
  rw [mult, mult, mulMarked_mapIso]
  congr 1 <;> rw [markSingle_mapIso]
 lemma mult_lorentzAction (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y)
    (x : X) (y : Y) (h : T.color x = τ (S.color y)) (Λ : LorentzGroup d) :
    mult (Λ • T) (Λ • S) x y h = Λ • mult T S x y h := by
  rw [mult, mult, ← mulMarked_lorentzAction]
  congr 1
  all_goals
    rw [markSingle, markEmbedding, Equiv.trans_apply]
    erw [lorentzAction_mapIso, lorentzAction_mapIso]
    rfl
 lemma mult_symm (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y)
    (x : X) (y : Y) (h : T.color x = τ (S.color y)) :
    mapIso d (Equiv.sumComm _ _) (mult T S x y h) = mult S T y x (color_eq_dual_symm h) := by
  rw [mult, mult, mulMarked_symm]
 /-- An equivalence of types associated with multiplying two consecutive indices,
 with the second index appearing on the left. -/
 def multSplitLeft {y y' : Y} (hy : y ≠ y') (z : Z) :
    {yz // yz ≠ (Sum.inl ⟨y, hy⟩ : {y'' // y'' ≠ y'} ⊕ {z' // z' ≠ z})} ≃
    {y'' // y'' ≠ y' ∧ y'' ≠ y} ⊕ {z' // z' ≠ z} :=
  Equiv.subtypeSum.trans <|
  Equiv.sumCongr (
      (Equiv.subtypeEquivRight (fun a => by
        obtain ⟨a, p⟩ := a; simp only [ne_eq, Sum.inl.injEq, Subtype.mk.injEq])).trans
      (Equiv.subtypeSubtypeEquivSubtypeInter _ _)) <|
  Equiv.subtypeUnivEquiv (fun a => Sum.inr_ne_inl)
 /-- An equivalence of types associated with multiplying two consecutive indices with the
 second index appearing on the right. -/
 def multSplitRight {y y' : Y} (hy : y ≠ y') (z : Z) :
    {yz // yz ≠ (Sum.inr ⟨y', hy.symm⟩ : {z' // z' ≠ z} ⊕ {y'' // y'' ≠ y})} ≃
    {z' // z' ≠ z} ⊕ {y'' // y'' ≠ y' ∧ y'' ≠ y} :=
   Equiv.subtypeSum.trans <|
  Equiv.sumCongr (Equiv.subtypeUnivEquiv (fun a => Sum.inl_ne_inr)) <|
  (Equiv.subtypeEquivRight (fun a => by
    obtain ⟨a, p⟩ := a; simp only [ne_eq, Sum.inr.injEq, Subtype.mk.injEq])).trans <|
  ((Equiv.subtypeSubtypeEquivSubtypeInter _ _).trans
    (Equiv.subtypeEquivRight (fun y'' => And.comm)))
 /-- An equivalence of types associated with the associativity property of multiplication. -/
 def multAssocIso (x : X) {y y' : Y} (hy : y ≠ y') (z : Z) :
    {x' // x' ≠ x} ⊕ {yz // yz ≠ (Sum.inl ⟨y, hy⟩ : {y'' // y'' ≠ y'} ⊕ {z' // z' ≠ z})}
    ≃ {xy // xy ≠ (Sum.inr ⟨y', hy.symm⟩ : {x' // x' ≠ x} ⊕ {y'' // y'' ≠ y})} ⊕ {z' // z' ≠ z} :=
  (Equiv.sumCongr (Equiv.refl _) (multSplitLeft hy z)).trans <|
  (Equiv.sumAssoc _ _ _).symm.trans <|
  (Equiv.sumCongr (multSplitRight hy x).symm (Equiv.refl _))
 lemma mult_assoc_color {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y}
    {U : RealLorentzTensor d Z} {x : X} {y y' : Y} (hy : y ≠ y') {z : Z}
    (h : T.color x = τ (S.color y))
    (h' : S.color y' = τ (U.color z)) : (mult (mult T S x y h) U (Sum.inr ⟨y', hy.symm⟩) z h').color
    = (mapIso d (multAssocIso x hy z) (mult T (mult S U y' z h') x (Sum.inl ⟨y, hy⟩) h)).color := by
  funext a
  match a with
  | .inl ⟨.inl _, _⟩ => rfl
  | .inl ⟨.inr _, _⟩ => rfl
  | .inr _ => rfl
 /-- An equivalence of index values associated with the associativity property of multiplication. -/
 def multAssocIndexValue {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y}
    {U : RealLorentzTensor d Z} {x : X} {y y' : Y} (hy : y ≠ y') {z : Z}
    (h : T.color x = τ (S.color y)) (h' : S.color y' = τ (U.color z)) :
    IndexValue d ((T.mult S x y h).mult U (Sum.inr ⟨y', hy.symm⟩) z h').color ≃
    IndexValue d (T.mult (S.mult U y' z h') x (Sum.inl ⟨y, hy⟩) h).color :=
  indexValueIso d (multAssocIso x hy z).symm (mult_assoc_color hy h h')
 /-- Multiplication of indices is associative, up to a `mapIso` equivalence. -/
 lemma mult_assoc (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) (U : RealLorentzTensor d Z)
    (x : X) (y y' : Y) (hy : y ≠ y') (z : Z) (h : T.color x = τ (S.color y))
    (h' : S.color y' = τ (U.color z)) : mult (mult T S x y h) U (Sum.inr ⟨y', hy.symm⟩) z h' =
    mapIso d (multAssocIso x hy z) (mult T (mult S U y' z h') x (Sum.inl ⟨y, hy⟩) h) := by
  apply ext (mult_assoc_color _ _ _) ?_
  funext i
  trans ∑ a, (∑ b, T.coord (multFstArg (multFstArg i a) b) *
    S.coord (multSndArg (multFstArg i a) b h)) * U.coord (multSndArg i a h')
  rfl
  trans ∑ a, T.coord (multFstArg (multAssocIndexValue hy h h' i) a) *
    (∑ b, S.coord (multFstArg (multSndArg (multAssocIndexValue hy h h' i) a h) b) *
    U.coord (multSndArg (multSndArg (multAssocIndexValue hy h h' i) a h) b h'))
  swap
  rw [mapIso_apply_coord, mapIsoFiber_apply, mapIsoFiber_apply, mult_coord_arg, indexValueIso_symm]
  rfl
  rw [Finset.sum_congr rfl (fun x _ => Finset.sum_mul _ _ _)]
  rw [Finset.sum_congr rfl (fun x _ => Finset.mul_sum _ _ _)]
  rw [Finset.sum_comm]
  refine Finset.sum_congr rfl (fun a _ => Finset.sum_congr rfl (fun b _ => ?_))
  rw [mul_assoc]
  refine Mathlib.Tactic.Ring.mul_congr rfl (Mathlib.Tactic.Ring.mul_congr ?_ rfl rfl) rfl
  apply congrArg
  funext c
  by_cases hcy : c = y
  · subst hcy
    rw [multSndArg_on_mem, multFstArg_on_not_mem, multSndArg_on_mem]
    rfl
  · by_cases hcy' : c = y'
    · subst hcy'
      rw [multFstArg_on_mem, multSndArg_on_not_mem, multFstArg_on_mem]
    · rw [multFstArg_on_not_mem, multSndArg_on_not_mem, multSndArg_on_not_mem,
        multFstArg_on_not_mem]
      rw [multAssocIndexValue, indexValueIso_eq_symm, indexValueIso_symm_apply']
      simp only [ne_eq, Function.comp_apply, Equiv.symm_symm_apply, mult_color, Sum.elim_inr,
        colorsIndexCast, Equiv.cast_refl, Equiv.refl_symm]
      erw [Equiv.refl_apply]
      rfl
      exact hcy'
      simpa using hcy
 end RealLorentzTensor
--- a/HepLean/SpaceTime/LorentzTensor/Real/MultiplicationUnit.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/MultiplicationUnit.lean
@ -27,7 +27,7 @@ The main results of this file are:
 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}
+  (T : RealLorentzTensor d X) (c : X → Color) (Λ Λ' : LorentzGroup d) {μ : Color}
 open Marked
@ -38,7 +38,7 @@ open Marked
 -/
 /-- The unit for the multiplication of Lorentz tensors. -/
-def mulUnit (d : ℕ) (μ : Colors) : Marked d (Fin 1) 1 :=
+def mulUnit (d : ℕ) (μ : Color) : Marked d (Fin 1) 1 :=
  match μ with
  | .up => mapIso d ((Equiv.emptySum Empty (Fin (1 + 1))).trans finSumFinEquiv.symm)
    (ofMatUpDown 1)
@ -54,23 +54,23 @@ lemma mulUnit_down_coord : (mulUnit d Colors.down).coord = fun i =>
  rfl
@[simp]
-lemma mulUnit_markedColor (μ : Colors) : (mulUnit d μ).markedColor 0 = τ μ := by
+lemma mulUnit_markedColor (μ : Color) : (mulUnit d μ).markedColor 0 = τ μ := by
  cases μ
  case up => rfl
  case down => rfl
-lemma mulUnit_dual_markedColor (μ : Colors) : τ ((mulUnit d μ).markedColor 0) = μ := by
+lemma mulUnit_dual_markedColor (μ : Color) : τ ((mulUnit d μ).markedColor 0) = μ := by
  cases μ
  case up => rfl
  case down => rfl
@[simp]
-lemma mulUnit_unmarkedColor (μ : Colors) : (mulUnit d μ).unmarkedColor 0 = μ := by
+lemma mulUnit_unmarkedColor (μ : Color) : (mulUnit d μ).unmarkedColor 0 = μ := by
  cases μ
  case up => rfl
  case down => rfl
-lemma mulUnit_unmarkedColor_eq_dual_marked (μ : Colors) :
+lemma mulUnit_unmarkedColor_eq_dual_marked (μ : Color) :
    (mulUnit d μ).unmarkedColor = τ ∘ (mulUnit d μ).markedColor := by
  funext x
  fin_cases x
@ -78,7 +78,7 @@ lemma mulUnit_unmarkedColor_eq_dual_marked (μ : Colors) :
    mulUnit_markedColor]
  exact color_eq_dual_symm rfl
-lemma mulUnit_coord_diag (μ : Colors) (i : (mulUnit d μ).UnmarkedIndexValue) :
+lemma mulUnit_coord_diag (μ : Color) (i : (mulUnit d μ).UnmarkedIndexValue) :
    (mulUnit d μ).coord (splitIndexValue.symm (i,
    indexValueDualIso d (mulUnit_unmarkedColor_eq_dual_marked μ) i)) = 1 := by
  cases μ
@ -92,7 +92,7 @@ lemma mulUnit_coord_diag (μ : Colors) (i : (mulUnit d μ).UnmarkedIndexValue) :
    rfl
    next h => exact False.elim (h rfl)
-lemma mulUnit_coord_off_diag (μ : Colors) (i: (mulUnit d μ).UnmarkedIndexValue)
+lemma mulUnit_coord_off_diag (μ : Color) (i: (mulUnit d μ).UnmarkedIndexValue)
    (b : (mulUnit d μ).MarkedIndexValue)
    (hb : b ≠ indexValueDualIso d (mulUnit_unmarkedColor_eq_dual_marked μ) i) :
    (mulUnit d μ).coord (splitIndexValue.symm (i, b)) = 0 := by
@ -118,7 +118,7 @@ lemma mulUnit_coord_off_diag (μ : Colors) (i: (mulUnit d μ).UnmarkedIndexValue
      exact h
    exact hb (id (Eq.symm h1))
-lemma mulUnit_right (μ : Colors) (T : Marked d X 1) (h : T.markedColor 0 = μ) :
+lemma mulUnit_right (μ : Color) (T : Marked d X 1) (h : T.markedColor 0 = μ) :
    multMarked T (mulUnit d μ) (h.trans (mulUnit_dual_markedColor μ).symm) = T := by
  refine ext ?_ ?_
  · funext a
@ -130,9 +130,9 @@ lemma mulUnit_right (μ : Colors) (T : Marked d X 1) (h : T.markedColor 0 = μ)
  funext i
  rw [mulMarked_indexValue_right]
  change ∑ j,
-    T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, _)) *
+    T.coord (splitIndexValue.symm ((indexValueTensorator i).1, _)) *
-    (mulUnit d μ).coord (splitIndexValue.symm ((indexValueSumEquiv i).2, j)) = _
+    (mulUnit d μ).coord (splitIndexValue.symm ((indexValueTensorator i).2, j)) = _
-  let y := indexValueDualIso d (mulUnit_unmarkedColor_eq_dual_marked μ) (indexValueSumEquiv i).2
+  let y := indexValueDualIso d (mulUnit_unmarkedColor_eq_dual_marked μ) (indexValueTensorator i).2
  erw [Finset.sum_eq_single_of_mem y]
  rw [mulUnit_coord_diag]
  simp only [Fin.isValue, mul_one]
@ -140,14 +140,14 @@ lemma mulUnit_right (μ : Colors) (T : Marked d X 1) (h : T.markedColor 0 = μ)
  funext a
  match a with
  | .inl a =>
-    change (indexValueSumEquiv i).1 a = _
+    change (indexValueTensorator i).1 a = _
    rfl
  | .inr 0 =>
    change oneMarkedIndexValue
-      ((colorsIndexDualCast (Eq.trans h (Eq.symm (mulUnit_dual_markedColor μ)))).symm
+      ((colorIndexDualCast (Eq.trans h (Eq.symm (mulUnit_dual_markedColor μ)))).symm
      (oneMarkedIndexValue.symm y)) 0 = _
    rw [indexValueIso_eq_symm, indexValueIso_symm_apply']
-    simp only [Fin.isValue, oneMarkedIndexValue, colorsIndexDualCast, colorsIndexCast,
+    simp only [Fin.isValue, oneMarkedIndexValue, colorIndexDualCast, colorIndexCast,
      Equiv.coe_fn_symm_mk, indexValueDualIso_apply, Equiv.trans_apply, Equiv.cast_apply,
      Equiv.symm_trans_apply, Equiv.cast_symm, Equiv.symm_symm, Equiv.apply_symm_apply, cast_cast,
      Equiv.coe_fn_mk, Equiv.refl_symm, Equiv.coe_refl, Function.comp_apply, id_eq, mul_color,
@ -157,15 +157,15 @@ lemma mulUnit_right (μ : Colors) (T : Marked d X 1) (h : T.markedColor 0 = μ)
  intro b _ hab
  rw [mul_eq_zero]
  apply Or.inr
-  exact mulUnit_coord_off_diag μ (indexValueSumEquiv i).2 b hab
+  exact mulUnit_coord_off_diag μ (indexValueTensorator i).2 b hab
-lemma mulUnit_left (μ : Colors) (T : Marked d X 1) (h : T.markedColor 0 = μ) :
+lemma mulUnit_left (μ : Color) (T : Marked d X 1) (h : T.markedColor 0 = μ) :
    multMarked (mulUnit d μ) T ((mulUnit_markedColor μ).trans (congrArg τ h.symm)) =
    mapIso d (Equiv.sumComm X (Fin 1)) T := by
  rw [← mult_symmd_symm, mulUnit_right]
  exact h
-lemma mulUnit_lorentzAction (μ : Colors) (Λ : LorentzGroup d) :
+lemma mulUnit_lorentzAction (μ : Color) (Λ : LorentzGroup d) :
    Λ • mulUnit d μ = mulUnit d μ := by
  match μ with
  | Colors.up =>
--- a/HepLean/SpaceTime/LorentzTensor/Real/TensorProducts.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/TensorProducts.lean
@ -19,7 +19,7 @@ open Set LinearMap Submodule
 variable {d : ℕ} {X Y Y' X'  : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
  [Fintype Y'] [DecidableEq Y'] [Fintype X'] [DecidableEq X']
-  (cX : X → Colors) (cY : Y → Colors)
+  (cX : X → Color) (cY : Y → Color)
 /-!
@ -31,65 +31,60 @@ variable {d : ℕ} {X Y Y' X'  : Type} [Fintype X] [DecidableEq X] [Fintype Y] [
 /-- An equivalence between `ColorFiber d (Sum.elim cX cY)` and
  `ColorFiber d cX ⊗[ℝ] ColorFiber d cY`. This is related to the `tensorator` of
  the monoidal functor defined by `ColorFiber`, hence the terminology.  -/
-def tensorator {cX : X → Colors} {cY : Y → Colors} :
+def tensorator {cX : X → Color} {cY : Y → Color} :
-    ColorFiber d (Sum.elim cX cY) ≃ₗ[ℝ] ColorFiber d cX ⊗[ℝ] ColorFiber d cY :=
+    RealLorentzTensor d (Sum.elim cX cY) ≃ₗ[ℝ] RealLorentzTensor d cX ⊗[ℝ] RealLorentzTensor d cY :=
-  (basisColorFiber (Sum.elim cX cY)).equiv (basisProd cX cY) indexValueSumEquiv
+  (basis (Sum.elim cX cY)).equiv (basisProd cX cY) indexValueTensorator
-lemma tensorator_symm_apply {cX : X → Colors} {cY : Y → Colors}
+lemma tensorator_symm_apply {cX : X → Color} {cY : Y → Color}
-    (X : ColorFiber d cX ⊗[ℝ] ColorFiber d cY) (i : IndexValue d (Sum.elim cX cY)) :
+    (X : RealLorentzTensor d cX ⊗[ℝ] RealLorentzTensor d cY) (i : IndexValue d (Sum.elim cX cY)) :
-    (tensorator.symm X) i = (basisProd cX cY).repr X (indexValueSumEquiv i) := by
+    (tensorator.symm X) i = (basisProd cX cY).repr X (indexValueTensorator i) := by
  rfl
-/-! TODO : Move -/
+
 lemma tensorator_mapIso_cond {cX : X → Colors} {cY : Y → Colors} {cX' : X' → Colors}
    {cY' : Y' → Colors} {eX : X ≃ X'} {eY : Y ≃ Y'} (hX : cX = cX' ∘ eX) (hY : cY = cY' ∘ eY) :
    Sum.elim cX cY = Sum.elim cX' cY' ∘ ⇑(eX.sumCongr eY) := by
  subst hX hY
  ext1 x
  simp_all only [Function.comp_apply, Equiv.sumCongr_apply]
  cases x with
  | inl val => simp_all only [Sum.elim_inl, Function.comp_apply, Sum.map_inl]
  | inr val_1 => simp_all only [Sum.elim_inr, Function.comp_apply, Sum.map_inr]
 /-- The naturality condition for the `tensorator`. -/
-lemma tensorator_mapIso {cX : X → Colors} {cY : Y → Colors} {cX' : X' → Colors}
+lemma tensorator_mapIso {cX : X → Color} {cY : Y → Color} {cX' : X' → Color}
-    {cY' : Y' → Colors} (eX : X ≃ X') (eY : Y ≃ Y') (hX : cX = cX' ∘ eX) (hY : cY = cY' ∘ eY) :
+    {cY' : Y' → Color} (eX : X ≃ X') (eY : Y ≃ Y') (hX : cX = cX' ∘ eX) (hY : cY = cY' ∘ eY) :
-    (mapIsoFiber d (Equiv.sumCongr eX eY) (tensorator_mapIso_cond hX hY)).trans tensorator  =
+    (@mapIso _ _ d (Equiv.sumCongr eX eY) _ _ (tensorator_mapIso_cond hX hY)).trans tensorator  =
-    tensorator.trans (TensorProduct.congr (mapIsoFiber d eX hX) (mapIsoFiber d eY hY)) := by
+    tensorator.trans (TensorProduct.congr (mapIso eX hX) (mapIso eY hY)) := by
-  apply (basisColorFiber (Sum.elim cX cY)).ext'
+  apply (basis (Sum.elim cX cY)).ext'
  intro i
  simp
  nth_rewrite 2 [tensorator]
  simp
  rw [Basis.tensorProduct_apply, TensorProduct.congr_tmul, mapIsoFiber_basis]
  rw [tensorator]
-  simp
+  simp only [basisProd, Basis.equiv_apply]
  rw [Basis.tensorProduct_apply, mapIsoFiber_basis, mapIsoFiber_basis]
  congr
-  sorry
+  rw [← Equiv.trans_apply, indexValueTensorator_indexValueMapIso]
-  sorry
+  rfl
  exact hY
  rw [← Equiv.trans_apply, indexValueTensorator_indexValueMapIso]
  rfl
  exact hX
 lemma tensorator_lorentzAction  (Λ : LorentzGroup d)  :
-    (tensorator).toLinearMap ∘ₗ lorentzActionFiber Λ
+    (tensorator).toLinearMap ∘ₗ lorentzAction Λ
-    = (TensorProduct.map (lorentzActionFiber Λ) (lorentzActionFiber Λ) ) ∘ₗ
+    = (TensorProduct.map (lorentzAction Λ) (lorentzAction Λ) ) ∘ₗ
    ((@tensorator d X Y _ _ _ _ cX cY).toLinearMap) := by
-  apply (basisColorFiber (Sum.elim cX cY)).ext
+  apply (basis (Sum.elim cX cY)).ext
  intro i
  nth_rewrite 2 [tensorator]
  simp only [coe_comp, LinearEquiv.coe_coe, Function.comp_apply, Basis.equiv_apply]
-  rw [basisProd, Basis.tensorProduct_apply, TensorProduct.map_tmul, lorentzActionFiber_basis,
+  rw [basisProd, Basis.tensorProduct_apply, TensorProduct.map_tmul, lorentzAction_basis,
-    lorentzActionFiber_basis, lorentzActionFiber_basis, map_sum, tmul_sum]
+    lorentzAction_basis, lorentzAction_basis, map_sum, tmul_sum]
  simp only [sum_tmul]
-  rw [← Equiv.sum_comp (indexValueSumEquiv).symm, Fintype.sum_prod_type, Finset.sum_comm]
+  rw [← Equiv.sum_comp (indexValueTensorator).symm, Fintype.sum_prod_type, Finset.sum_comm]
  refine Finset.sum_congr rfl (fun j _ => (Finset.sum_congr rfl (fun k _ => ?_)))
  rw [tmul_smul, smul_tmul, tmul_smul, smul_smul, map_smul]
  congr 1
  · rw [toTensorRepMat_of_indexValueSumEquiv, Equiv.apply_symm_apply, mul_comm]
  · simp [tensorator]
-lemma tensorator_lorentzAction_apply  (Λ : LorentzGroup d) (T : ColorFiber d (Sum.elim cX cY)) :
+lemma tensorator_lorentzAction_apply  (Λ : LorentzGroup d) (T : RealLorentzTensor d (Sum.elim cX cY)) :
-    tensorator (lorentzActionFiber Λ T) =
+    tensorator (Λ • T) =
-    TensorProduct.map (lorentzActionFiber Λ) (lorentzActionFiber Λ) (tensorator T) := by
+    TensorProduct.map (lorentzAction Λ) (lorentzAction Λ) (tensorator T) := by
  erw [← LinearMap.comp_apply, tensorator_lorentzAction]
  rfl
@ -106,33 +101,33 @@ def decompEmbedSet (f : Y ↪ X) :
  Equiv.sumCongr ((Equiv.subtypeEquivRight (by simp))) <|
  (Function.Embedding.toEquivRange f).symm
-def decompEmbedColorLeft (f : Y ↪ X) : {x // x ∈ (Finset.image f Finset.univ)ᶜ} → Colors :=
+def decompEmbedColorLeft (f : Y ↪ X) : {x // x ∈ (Finset.image f Finset.univ)ᶜ} → Color :=
  (cX ∘ (decompEmbedSet f).symm) ∘ Sum.inl
-def decompEmbedColorRight (f : Y ↪ X) : Y → Colors :=
+def decompEmbedColorRight (f : Y ↪ X) : Y → Color :=
  (cX ∘ (decompEmbedSet f).symm) ∘ Sum.inr
 /-- Decomposes a tensor into a tensor product based on an embedding. -/
 def decompEmbed (f : Y ↪ X) :
-    ColorFiber d cX ≃ₗ[ℝ] ColorFiber d (decompEmbedColorLeft cX f) ⊗[ℝ] ColorFiber d (cX ∘ f) :=
+    RealLorentzTensor d cX ≃ₗ[ℝ] RealLorentzTensor d (decompEmbedColorLeft cX f) ⊗[ℝ] RealLorentzTensor d (cX ∘ f) :=
-  (@mapIsoFiber _ _ d (decompEmbedSet f) cX (Sum.elim (decompEmbedColorLeft cX f)
+  (@mapIso _ _ d (decompEmbedSet f) cX (Sum.elim (decompEmbedColorLeft cX f)
    (decompEmbedColorRight cX f)) (by
      simpa [decompEmbedColorLeft, decompEmbedColorRight] using (Equiv.comp_symm_eq _ _ _).mp rfl)).trans
  tensorator
-lemma decompEmbed_lorentzAction_apply {f : Y ↪ X} (Λ : LorentzGroup d) (T : ColorFiber d cX) :
+lemma decompEmbed_lorentzAction_apply {f : Y ↪ X} (Λ : LorentzGroup d) (T : RealLorentzTensor d cX) :
-    decompEmbed cX f (lorentzActionFiber Λ T) =
+    decompEmbed cX f (Λ • T) =
-    TensorProduct.map (lorentzActionFiber Λ) (lorentzActionFiber Λ) (decompEmbed cX f T) := by
+    TensorProduct.map (lorentzAction Λ) (lorentzAction Λ) (decompEmbed cX f T) := by
  rw [decompEmbed]
  simp
-  rw [lorentzActionFiber_mapIsoFiber]
+  rw [lorentzAction_mapIso]
  exact tensorator_lorentzAction_apply (decompEmbedColorLeft cX f) (decompEmbedColorRight cX f) Λ
-      ((mapIsoFiber d (decompEmbedSet f) (decompEmbed.proof_2 cX f)) T)
+      ((mapIso (decompEmbedSet f) (decompEmbed.proof_2 cX f)) T)
 def decompEmbedProd (f : X' ↪ X) (g : Y' ↪ Y) :
-    ColorFiber d cX ⊗[ℝ] ColorFiber d cY ≃ₗ[ℝ]
+    RealLorentzTensor d cX ⊗[ℝ] RealLorentzTensor d cY ≃ₗ[ℝ]
-    ColorFiber d (Sum.elim (decompEmbedColorLeft cX f) (decompEmbedColorLeft cY g))
+    RealLorentzTensor d (Sum.elim (decompEmbedColorLeft cX f) (decompEmbedColorLeft cY g))
-    ⊗[ℝ] (ColorFiber d (cX ∘ f) ⊗[ℝ] ColorFiber d (cY ∘ g)) :=
+    ⊗[ℝ] (RealLorentzTensor d (cX ∘ f) ⊗[ℝ] RealLorentzTensor d (cY ∘ g)) :=
  (TensorProduct.congr (decompEmbed cX f) (decompEmbed cY g)).trans <|
  (TensorProduct.assoc ℝ _ _ _).trans <|
  (TensorProduct.congr (LinearEquiv.refl ℝ _)
@ -144,95 +139,5 @@ def decompEmbedProd (f : X' ↪ X) (g : Y' ↪ Y) :
 /-- The contraction of all indices of two tensors with dual index-colors.
  This is a bilinear map to ℝ. -/
@[simps!]
 def contrAll {f1 : X → Colors} {f2 : Y → Colors} (e : X ≃ Y) (hc : f1 = τ ∘ f2 ∘ e) :
    ColorFiber d f1 →ₗ[ℝ] ColorFiber d f2 →ₗ[ℝ] ℝ where
  toFun T := {
    toFun := fun S => ∑ i, T i * S (indexValueDualIso d e hc i),
    map_add' := fun S F => by
      trans  ∑ i, (T i * S (indexValueDualIso d e hc i) + T i * F (indexValueDualIso d e hc i))
      exact Finset.sum_congr rfl (fun i _ => mul_add _ _ _ )
      exact Finset.sum_add_distrib,
    map_smul' := fun r S => by
      trans ∑ i , r * (T i * S (indexValueDualIso d e hc i))
      refine Finset.sum_congr rfl (fun x _ => ?_)
      ring_nf
      rw [mul_assoc]
      rfl
      rw [← Finset.mul_sum]
      rfl}
  map_add' := fun T S => by
    ext F
    trans ∑ i , (T i * F (indexValueDualIso d e hc i) + S i * F (indexValueDualIso d e hc i))
    exact Finset.sum_congr rfl (fun x _ => add_mul _ _ _)
    exact Finset.sum_add_distrib
  map_smul' := fun r T => by
    ext S
    trans ∑ i , r * (T i * S (indexValueDualIso d e hc i))
    refine Finset.sum_congr rfl (fun x _ => mul_assoc _ _ _)
    rw [← Finset.mul_sum]
    rfl
 lemma contrAll_symm {f1 : X → Colors} {f2 : Y → Colors} (e : X ≃ Y)
    (h : f1 = τ ∘ f2 ∘ e) (T : ColorFiber d f1) (S : ColorFiber d f2) :
    contrAll e h T S = contrAll e.symm (indexValueDualIso_cond_symm h) S T := by
  rw [contrAll_apply_apply, contrAll_apply_apply, ← Equiv.sum_comp (indexValueDualIso d e h)]
  refine Finset.sum_congr rfl (fun i _ => ?_)
  rw [mul_comm, ← Equiv.trans_apply]
  simp
 lemma contrAll_mapIsoFiber_right {f1 : X → Colors} {f2 : Y → Colors}
    {g2 : Y' → Colors} (e : X ≃ Y) (eY : Y ≃ Y')
    (h : f1 = τ ∘ f2 ∘ e) (hY : f2 = g2 ∘ eY) (T : ColorFiber d f1) (S : ColorFiber d f2) :
    contrAll e h T S = contrAll (e.trans eY) (indexValueDualIso_cond_trans_indexValueIso h hY)
      T (mapIsoFiber d eY hY S) := by
  rw [contrAll_apply_apply, contrAll_apply_apply]
  refine Finset.sum_congr rfl (fun i _ => Mathlib.Tactic.Ring.mul_congr rfl ?_ rfl)
  rw [mapIsoFiber_apply, ← Equiv.trans_apply]
  simp only [indexValueDualIso_trans_indexValueIso]
  congr
  ext1 x
  simp only [Equiv.trans_apply, Equiv.symm_apply_apply]
 lemma contrAll_mapIsoFiber_left {f1 : X → Colors} {f2 : Y → Colors}
    {g1 : X' → Colors} (e : X ≃ Y) (eX : X ≃ X')
    (h : f1 = τ ∘ f2 ∘ e) (hX : f1 = g1 ∘ eX) (T : ColorFiber d f1) (S : ColorFiber d f2) :
    contrAll e h T S = contrAll (eX.symm.trans e)
    (indexValueIso_trans_indexValueDualIso_cond ((Equiv.eq_comp_symm eX g1 f1).mpr hX.symm) h)
    (mapIsoFiber d eX hX T) S := by
  rw [contrAll_symm, contrAll_mapIsoFiber_right _ eX _ hX, contrAll_symm]
  rfl
 lemma contrAll_lorentzAction {f1 : X → Colors} {f2 : Y → Colors} (e : X ≃ Y)
    (hc : f1 = τ ∘ f2 ∘ e) (T : ColorFiber d f1) (S : ColorFiber d f2) (Λ : LorentzGroup d) :
    contrAll e hc (lorentzActionFiber Λ T) (lorentzActionFiber Λ S) = contrAll e hc T S := by
  change ∑ i, (∑ j, toTensorRepMat Λ i j * T j) *
    (∑ k, toTensorRepMat Λ (indexValueDualIso d e hc i) k * S k) = _
  trans ∑ i, ∑ j, ∑ k, (toTensorRepMat Λ (indexValueDualIso d e hc i) k * toTensorRepMat Λ i j)
      * T j * S 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, ∑ i, (toTensorRepMat Λ (indexValueDualIso d e hc i) k
    * toTensorRepMat Λ i j) * T j * S k
  · apply Finset.sum_congr rfl (fun j _ => ?_)
    rw [Finset.sum_comm]
  trans ∑ j, ∑ k, (toTensorRepMat 1 (indexValueDualIso d e.symm (indexValueDualIso_cond_symm hc) k) j) * T j * S k
  · apply Finset.sum_congr rfl (fun j _ => Finset.sum_congr rfl (fun k _ => ?_))
    rw [← Finset.sum_mul, ← Finset.sum_mul]
    erw [toTensorRepMat_indexValueDualIso_sum]
  rw [Finset.sum_comm]
  trans ∑ k, T (indexValueDualIso d e.symm (indexValueDualIso_cond_symm hc) k) * S k
  · apply Finset.sum_congr rfl (fun k _ => ?_)
    rw [← Finset.sum_mul, ← toTensorRepMat_one_coord_sum' T]
  rw [← Equiv.sum_comp (indexValueDualIso d e hc), ← indexValueDualIso_symm e hc]
  simp only [Equiv.symm_apply_apply, contrAll_apply_apply]
 end RealLorentzTensor
 end
--- a/docs/references.bib
+++ b/docs/references.bib
@ -20,6 +20,23 @@
  year          = "2022"
 }
@Article{         Dreiner:2008tw,
  author        = "Dreiner, Herbi K. and Haber, Howard E. and Martin, Stephen
                  P.",
  title         = "{Two-component spinor techniques and Feynman rules for
                  quantum field theory and supersymmetry}",
  eprint        = "0812.1594",
  archiveprefix = "arXiv",
  primaryclass  = "hep-ph",
  reportnumber  = "BN-TH-2008-12, SCIPP-08-08, FERMILAB-PUB-09-855-T,
                  BN-TH-2008-12 and SCIPP-08/08",
  doi           = "10.1016/j.physrep.2010.05.002",
  journal       = "Phys. Rept.",
  volume        = "494",
  pages         = "1--196",
  year          = "2010"
 }
@Article{         Lohitsiri:2019fuu,
  author        = "Lohitsiri, Nakarin and Tong, David",
  title         = "{Hypercharge Quantisation and Fermat's Last Theorem}",