From cef7e574ca6aa91d827a5c38290b4468f0d6615f Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 6 Aug 2024 08:10:47 -0400
Subject: [PATCH 1/3] feat: More results regarding index notation.

---
 HepLean.lean                                  |   1 +
 HepLean/SpaceTime/LorentzTensor/Basic.lean    |  10 +-
 .../LorentzTensor/IndexNotation/Basic.lean    |  24 ++-
 .../IndexNotation/IndexListColor.lean         | 139 ++++++++++++++++--
 .../IndexNotation/IndexString.lean            |  32 +++-
 .../IndexNotation/TensorIndex.lean            |  95 +++++++++++-
 .../LorentzTensor/Real/IndexNotation.lean     | 117 +++++++++++++++
 .../LorentzTensor/RisingLowering.lean         |  18 +++
 README.md                                     |   2 +-
 lake-manifest.json                            |  14 +-
 lakefile.toml                                 |   2 +-
 lean-toolchain                                |   2 +-
 12 files changed, 424 insertions(+), 32 deletions(-)
 create mode 100644 HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean

diff --git a/HepLean.lean b/HepLean.lean
index a754390..3c66e66 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -79,6 +79,7 @@ import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexString
 import HepLean.SpaceTime.LorentzTensor.IndexNotation.TensorIndex
 import HepLean.SpaceTime.LorentzTensor.MulActionTensor
 import HepLean.SpaceTime.LorentzTensor.Real.Basic
+import HepLean.SpaceTime.LorentzTensor.Real.IndexNotation
 import HepLean.SpaceTime.LorentzTensor.RisingLowering
 import HepLean.SpaceTime.LorentzVector.AsSelfAdjointMatrix
 import HepLean.SpaceTime.LorentzVector.Basic
diff --git a/HepLean/SpaceTime/LorentzTensor/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Basic.lean
index 38c976f..526001d 100644
--- a/HepLean/SpaceTime/LorentzTensor/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Basic.lean
@@ -44,13 +44,16 @@ structure TensorColor where
 
 namespace TensorColor
 
-variable (𝓒 : TensorColor)
+variable (𝓒 : TensorColor) [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
 variable {d : ℕ} {X Y Y' Z W : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
   [Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z] [Fintype W] [DecidableEq W]
 
 /-- A relation on colors which is true if the two colors are equal or are duals. -/
 def colorRel (μ ν : 𝓒.Color) : Prop := μ = ν ∨ μ = 𝓒.τ ν
 
+instance : Decidable (colorRel 𝓒 μ ν) :=
+  Or.decidable
+
 /-- An equivalence relation on colors which is true if the two colors are equal or are duals. -/
 lemma colorRel_equivalence : Equivalence 𝓒.colorRel where
   refl := by
@@ -87,6 +90,11 @@ instance colorSetoid : Setoid 𝓒.Color := ⟨𝓒.colorRel, 𝓒.colorRel_equi
 def colorQuot (μ : 𝓒.Color) : Quotient 𝓒.colorSetoid :=
   Quotient.mk 𝓒.colorSetoid μ
 
+instance (μ ν : 𝓒.Color) : Decidable (μ ≈ ν) :=
+  Or.decidable
+
+instance : DecidableEq (Quotient 𝓒.colorSetoid) :=
+  instDecidableEqQuotientOfDecidableEquiv
 end TensorColor
 
 noncomputable section
diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean
index 046bc5b..655355e 100644
--- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean
@@ -107,6 +107,8 @@ instance : Decidable (listCharIndex X l) :=
   e.g. `ᵘ¹²` or `ᵤ₄₃` etc. -/
 def Index : Type := {s : String // listCharIndex X s.toList ∧ s.toList ≠ []}
 
+instance : DecidableEq (Index X) := Subtype.instDecidableEq
+
 namespace Index
 
 variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
@@ -295,19 +297,19 @@ instance : DecidableEq l.contrSubtype :=
 
 /-- Given a `i : l.contrSubtype` the proposition on a `j` in `Fin s.length` for
   it to be an index of `s` contracting with `i`. -/
-def getDualProp (i : l.contrSubtype) (j : Fin l.length) : Prop :=
-    i.1 ≠ j ∧ l.idMap i.1 = l.idMap j
+def getDualProp (i j : Fin l.length) : Prop :=
+    i ≠ j ∧ l.idMap i = l.idMap j
 
-instance (i : l.contrSubtype) (j : Fin l.length) :
+instance (i j : Fin l.length) :
     Decidable (l.getDualProp i j) :=
   instDecidableAnd
 
 /-- Given a `i : l.contrSubtype` the index of `s` contracting with `i`. -/
 def getDualFin (i : l.contrSubtype) : Fin l.length :=
-  (Fin.find (l.getDualProp i)).get (by simpa [NoContr, Fin.isSome_find_iff] using i.prop)
+  (Fin.find (l.getDualProp i.1)).get (by simpa [NoContr, Fin.isSome_find_iff] using i.prop)
 
 lemma some_getDualFin_eq_find (i : l.contrSubtype) :
-    Fin.find (l.getDualProp i) = some (l.getDualFin i) := by
+    Fin.find (l.getDualProp i.1) = some (l.getDualFin i) := by
   simp [getDualFin]
 
 lemma getDualFin_not_NoContr (i : l.contrSubtype) : ¬ l.NoContr (l.getDualFin i) := by
@@ -333,6 +335,13 @@ lemma getDual_neq_self (i : l.contrSubtype) : i ≠ l.getDual i := by
   rw [Fin.find_eq_some_iff] at h1
   exact ne_of_apply_ne Subtype.val h1.1.1
 
+lemma getDual_getDualProp (i : l.contrSubtype) : l.getDualProp i.1 (l.getDual i).1 := by
+  simp [getDual]
+  have h1 := l.some_getDualFin_eq_find i
+  rw [Fin.find_eq_some_iff] at h1
+  simp only [getDualProp, ne_eq, and_imp] at h1
+  exact h1.1
+
 /-!
 
 ## Index lists with no contracting indices
@@ -444,6 +453,11 @@ lemma getDual_not_lt_self_mem_contrPairSet {i : l.contrSubtype}
   simp only
   exact l.getDual_id i
 
+/-- The list of elements of `l` which contract together. -/
+def contrPairList : List (Fin l.length × Fin l.length) :=
+  (List.product (Fin.list l.length) (Fin.list l.length)).filterMap fun (i, j) => if
+  l.getDualProp i j then some (i, j) else none
+
 end IndexList
 
 end IndexNotation
diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColor.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColor.lean
index d81b26c..c47b07e 100644
--- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColor.lean
+++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColor.lean
@@ -5,6 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.LorentzTensor.IndexNotation.Basic
 import HepLean.SpaceTime.LorentzTensor.Basic
+import Init.Data.List.Lemmas
 /-!
 
 # Index lists with color conditions
@@ -25,9 +26,11 @@ variable [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color
 /-- An index list is allowed if every contracting index has exactly one dual,
   and the color of the dual is dual to the color of the index. -/
 def IndexListColorProp (l : IndexList 𝓒.Color) : Prop :=
-  (∀ (i j : l.contrSubtype), l.getDualProp i j.1 → j = l.getDual i) ∧
+  (∀ (i j : l.contrSubtype), l.getDualProp i.1 j.1 → j = l.getDual i) ∧
   (∀ (i : l.contrSubtype), l.colorMap i.1 = 𝓒.τ (l.colorMap (l.getDual i).1))
 
+instance : DecidablePred (IndexListColorProp 𝓒) := fun _ => And.decidable
+
 /-- The type of index lists which satisfy `IndexListColorProp`. -/
 def IndexListColor : Type := {s : IndexList 𝓒.Color // IndexListColorProp 𝓒 s}
 
@@ -48,6 +51,64 @@ lemma indexListColorProp_of_hasNoContr {s : IndexList 𝓒.Color} (h : s.HasNoCo
 
 /-!
 
+## Conditions related to IndexListColorProp
+
+-/
+
+/-- The bool which is true if ever index appears at most once in the first element of entries of
+   `l.contrPairList`. I.e. If every element contracts with at most one other element. -/
+def colorPropFstBool (l : IndexList 𝓒.Color) : Bool :=
+  let l' := List.product l.contrPairList l.contrPairList
+  let l'' := l'.filterMap fun (i, j) => if i.1 = j.1 ∧ i.2 ≠ j.2 then some i else none
+  List.isEmpty l''
+
+lemma colorPropFstBool_indexListColorProp_fst (l : IndexList 𝓒.Color) (hl : colorPropFstBool l) :
+    ∀ (i j : l.contrSubtype), l.getDualProp i.1 j.1 → j = l.getDual i := by
+  simp [colorPropFstBool] at hl
+  rw [List.filterMap_eq_nil] at hl
+  simp at hl
+  intro i j hij
+  have hl' := hl i.1 j.1 i.1 (l.getDual i).1
+  simp [contrPairList] at hl'
+  have h1 {n : ℕ} (m : Fin n) : m ∈ Fin.list n := by
+    have h1' : (Fin.list n)[m] = m := by
+      erw [Fin.getElem_list]
+      rfl
+    rw [← h1']
+    apply List.getElem_mem
+  apply Subtype.ext (hl' (h1 _) (h1 _) hij (h1 _) (h1 _) (l.getDual_getDualProp i))
+
+/-- The bool which is true if the pairs in `l.contrPairList` have dual colors. -/
+def colorPropSndBool (l : IndexList 𝓒.Color) : Bool :=
+  List.all l.contrPairList (fun (i, j) => l.colorMap i = 𝓒.τ (l.colorMap j))
+
+lemma colorPropSndBool_indexListColorProp_snd (l : IndexList 𝓒.Color)
+    (hl2 : colorPropSndBool l) :
+    ∀ (i : l.contrSubtype), l.colorMap i.1 = 𝓒.τ (l.colorMap (l.getDual i).1) := by
+  simp [colorPropSndBool] at hl2
+  intro i
+  have h2 := hl2 i.1 (l.getDual i).1
+  simp [contrPairList] at h2
+  have h1 {n : ℕ} (m : Fin n) : m ∈ Fin.list n := by
+    have h1' : (Fin.list n)[m] = m := by
+      erw [Fin.getElem_list]
+      rfl
+    rw [← h1']
+    apply List.getElem_mem
+  exact h2 (h1 _) (h1 _) (l.getDual_getDualProp i)
+
+/-- The bool which is true if both `colorPropFstBool` and `colorPropSndBool` are true. -/
+def colorPropBool (l : IndexList 𝓒.Color) : Bool :=
+  colorPropFstBool l && colorPropSndBool l
+
+lemma colorPropBool_indexListColorProp {l : IndexList 𝓒.Color} (hl : colorPropBool l) :
+    IndexListColorProp 𝓒 l := by
+  simp [colorPropBool] at hl
+  exact And.intro (colorPropFstBool_indexListColorProp_fst l hl.1)
+    (colorPropSndBool_indexListColorProp_snd l hl.2)
+
+/-!
+
 ## Contraction pairs for IndexListColor
 
 -/
@@ -176,17 +237,19 @@ def PermContr (s1 s2 : IndexListColor 𝓒) : Prop :=
       s1.contr.1.idMap i = s2.contr.1.idMap j →
       s1.contr.1.colorMap i = s2.contr.1.colorMap j
 
-lemma PermContr.refl : Reflexive (@PermContr 𝓒 _) := by
+namespace PermContr
+
+lemma refl : Reflexive (@PermContr 𝓒 _) := by
   intro l
   simp only [PermContr, List.Perm.refl, true_and]
   have h1 : l.contr.1.HasNoContr := l.1.contrIndexList_hasNoContr
   exact fun i j a => hasNoContr_color_eq_of_id_eq (↑l.contr) h1 i j a
 
-lemma PermContr.symm : Symmetric (@PermContr 𝓒 _) :=
+lemma symm : Symmetric (@PermContr 𝓒 _) :=
   fun _ _ h => And.intro (List.Perm.symm h.1) fun i j hij => (h.2 j i hij.symm).symm
 
 /-- Given an index in `s1` the index in `s2` related by `PermContr` with the same id. -/
-def PermContr.get {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) (i : Fin s1.contr.1.length) :
+def get {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) (i : Fin s1.contr.1.length) :
     Fin s2.contr.1.length :=
   (Fin.find (fun j => s1.contr.1.idMap i = s2.contr.1.idMap j)).get (by
     rw [Fin.isSome_find_iff]
@@ -207,19 +270,19 @@ def PermContr.get {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) (i : Fin s
     change _ = (s2.contr.1.get j').id
     rw [hj'])
 
-lemma PermContr.some_get_eq_find {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
+lemma some_get_eq_find {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
     (i : Fin s1.contr.1.length) :
     Fin.find (fun j => s1.contr.1.idMap i = s2.contr.1.idMap j) = some (h.get i) := by
   simp [PermContr.get]
 
-lemma PermContr.get_id {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
+lemma get_id {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
     (i : Fin s1.contr.1.length) :
     s2.contr.1.idMap (h.get i) = s1.contr.1.idMap i := by
   have h1 := h.some_get_eq_find i
   rw [Fin.find_eq_some_iff] at h1
   exact h1.1.symm
 
-lemma PermContr.get_unique {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
+lemma get_unique {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
     {i : Fin s1.contr.1.length} {j : Fin s2.contr.1.length}
     (hij : s1.contr.1.idMap i = s2.contr.1.idMap j) :
     j = h.get i := by
@@ -230,17 +293,39 @@ lemma PermContr.get_unique {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
   apply And.intro hn
   rw [← hij, PermContr.get_id]
 
+lemma get_color {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
+    (i : Fin s1.contr.1.length) :
+    s1.contr.1.colorMap i = s2.contr.1.colorMap (h.get i) :=
+  h.2 i (h.get i) (h.get_id i).symm
+
 @[simp]
-lemma PermContr.get_symm_apply_get_apply {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
+lemma get_symm_apply_get_apply {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
     (i : Fin s1.contr.1.length) : h.symm.get (h.get i) = i :=
   (h.symm.get_unique (h.get_id i)).symm
 
-lemma PermContr.get_apply_get_symm_apply {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
+lemma get_apply_get_symm_apply {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
     (i : Fin s2.contr.1.length) : h.get (h.symm.get i) = i :=
   (h.get_unique (h.symm.get_id i)).symm
 
+lemma trans {s1 s2 s3 : IndexListColor 𝓒} (h1 : PermContr s1 s2) (h2 : PermContr s2 s3) :
+    PermContr s1 s3 := by
+  apply And.intro (h1.1.trans h2.1)
+  intro i j hij
+  rw [h1.get_color i]
+  have hj : j = h2.get (h1.get i) := by
+    apply h2.get_unique
+    rw [get_id]
+    exact hij
+  rw [hj, h2.get_color]
+
+lemma get_trans {s1 s2 s3 : IndexListColor 𝓒} (h1 : PermContr s1 s2) (h2 : PermContr s2 s3)
+    (i : Fin s1.contr.1.length) :
+    (h1.trans h2).get i = h2.get (h1.get i) := by
+  apply h2.get_unique
+  rw [get_id, get_id]
+
 /-- Equivalence of indexing types for two `IndexListColor` related by `PermContr`. -/
-def PermContr.toEquiv {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) :
+def toEquiv {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) :
     Fin s1.contr.1.length ≃ Fin s2.contr.1.length where
   toFun := h.get
   invFun := h.symm.get
@@ -249,16 +334,46 @@ def PermContr.toEquiv {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) :
   right_inv x := by
     simp
 
-lemma PermContr.toEquiv_symm {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) :
+lemma toEquiv_refl' {s : IndexListColor 𝓒} (h : PermContr s s) :
+    h.toEquiv = Equiv.refl _ := by
+  apply Equiv.ext
+  intro x
+  simp [toEquiv, get]
+  have h1 : Fin.find fun j => s.contr.1.idMap x = s.contr.1.idMap j = some x := by
+    rw [Fin.find_eq_some_iff]
+    have h2 := s.1.contrIndexList_hasNoContr x
+    simp only [true_and]
+    intro j hj
+    by_cases hjx : j = x
+    subst hjx
+    rfl
+    exact False.elim (h2 j (fun a => hjx a.symm) hj)
+  simp only [h1, Option.get_some]
+
+@[simp]
+lemma toEquiv_refl {s : IndexListColor 𝓒} :
+    PermContr.toEquiv (PermContr.refl s) = Equiv.refl _ := by
+  exact PermContr.toEquiv_refl' _
+
+lemma toEquiv_symm {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) :
     h.toEquiv.symm = h.symm.toEquiv := by
   rfl
 
-lemma PermContr.toEquiv_colorMap {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) :
+lemma toEquiv_colorMap {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) :
     s2.contr.1.colorMap = s1.contr.1.colorMap ∘ h.toEquiv.symm := by
   funext x
   refine (h.2 _ _ ?_).symm
   simp [← h.get_id, toEquiv]
 
+lemma toEquiv_trans {s1 s2 s3 : IndexListColor 𝓒} (h1 : PermContr s1 s2) (h2 : PermContr s2 s3) :
+    (h1.trans h2).toEquiv = h1.toEquiv.trans h2.toEquiv := by
+  apply Equiv.ext
+  intro x
+  simp [toEquiv]
+  rw [← get_trans]
+
+end PermContr
+
 /-! TODO: Show that `rel` is indeed an equivalence relation. -/
 
 /-!
diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexString.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexString.lean
index c62dbee..02ccf47 100644
--- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexString.lean
+++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexString.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.SpaceTime.LorentzTensor.IndexNotation.Basic
+import HepLean.SpaceTime.LorentzTensor.IndexNotation.TensorIndex
 /-!
 
 # Strings of indices
@@ -242,3 +242,33 @@ def toIndexList (s : IndexString X) : IndexList X :=
 end IndexString
 
 end IndexNotation
+namespace TensorStructure
+
+/-!
+
+## Making a tensor index from an index string
+
+-/
+
+namespace TensorIndex
+variable {R : Type} [CommSemiring R] (𝓣 : TensorStructure R)
+variable {𝓣 : TensorStructure R} [IndexNotation 𝓣.Color] [Fintype 𝓣.Color] [DecidableEq 𝓣.Color]
+variable {n m : ℕ} {cn : Fin n → 𝓣.Color} {cm : Fin m → 𝓣.Color}
+
+open IndexNotation IndexListColor
+
+/-- The construction of a tensor index from a tensor and a string satisfing conditions which are
+  easy to check automatically. -/
+noncomputable def fromIndexString (T : 𝓣.Tensor cn) (s : String)
+    (hs : listCharIndexStringBool 𝓣.toTensorColor.Color s.toList = true)
+    (hn : n = (IndexString.toIndexList (⟨s, hs⟩ : IndexString 𝓣.Color)).length)
+    (hc : IndexListColorProp 𝓣.toTensorColor (
+      IndexString.toIndexList (⟨s, hs⟩ : IndexString 𝓣.Color)))
+    (hd : TensorColor.DualMap (IndexString.toIndexList (⟨s, hs⟩ : IndexString 𝓣.Color)).colorMap
+    (cn ∘ Fin.cast hn.symm)) : 𝓣.TensorIndex :=
+  TensorStructure.TensorIndex.mkDualMap T
+    ⟨(IndexString.toIndexList (⟨s, hs⟩ : IndexString 𝓣.Color)), hc⟩ hn hd
+
+end TensorIndex
+
+end TensorStructure
diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean
index f640dc7..4ace483 100644
--- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean
+++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean
@@ -36,7 +36,7 @@ structure TensorIndex where
   tensor : 𝓣.Tensor index.1.colorMap
 
 namespace TensorIndex
-open TensorColor
+open TensorColor IndexListColor
 variable {𝓣 : TensorStructure R} [IndexNotation 𝓣.Color] [Fintype 𝓣.Color] [DecidableEq 𝓣.Color]
 variable {n m : ℕ} {cn : Fin n → 𝓣.Color} {cm : Fin m → 𝓣.Color}
 
@@ -69,6 +69,12 @@ def mkDualMap (T : 𝓣.Tensor cn) (l : IndexListColor 𝓣.toTensorColor) (hn :
       𝓣.dualize (DualMap.split l.1.colorMap (cn ∘ Fin.cast hn.symm)) <|
       (𝓣.mapIso (Fin.castOrderIso hn).toEquiv rfl T : 𝓣.Tensor (cn ∘ Fin.cast hn.symm))
 
+/-!
+
+## The contraction of indices
+
+-/
+
 /-- The contraction of indices in a `TensorIndex`. -/
 def contr (T : 𝓣.TensorIndex) : 𝓣.TensorIndex where
   index := T.index.contr
@@ -77,6 +83,14 @@ def contr (T : 𝓣.TensorIndex) : 𝓣.TensorIndex where
       T.index.contr_colorMap <|
       𝓣.contr (T.index.splitContr).symm T.index.splitContr_map T.tensor
 
+/-! TODO: Show that contracting twice is the same as contracting once. -/
+
+/-!
+
+## Product of `TensorIndex` allowed
+
+-/
+
 /-- The tensor product of two `TensorIndex`. -/
 def prod (T₁ T₂ : 𝓣.TensorIndex)
     (h : IndexListColorProp 𝓣.toTensorColor (T₁.index.1 ++ T₂.index.1)) : 𝓣.TensorIndex where
@@ -87,11 +101,28 @@ def prod (T₁ T₂ : 𝓣.TensorIndex)
       (IndexListColor.prod_colorMap h) <|
       𝓣.tensoratorEquiv _ _ (T₁.tensor ⊗ₜ[R] T₂.tensor)
 
+@[simp]
+lemma prod_index (T₁ T₂ : 𝓣.TensorIndex)
+    (h : IndexListColorProp 𝓣.toTensorColor (T₁.index.1 ++ T₂.index.1)) :
+    (prod T₁ T₂ h).index = T₁.index.prod T₂.index h := rfl
+
+/-!
+
+## Scalar multiplication of
+
+-/
+
 /-- The scalar multiplication of a `TensorIndex` by an element of `R`. -/
 def smul (r : R) (T : 𝓣.TensorIndex) : 𝓣.TensorIndex where
   index := T.index
   tensor := r • T.tensor
 
+/-!
+
+## Addition of allowed `TensorIndex`
+
+-/
+
 /-- The addition of two `TensorIndex` given the condition that, after contraction,
   their index lists are the same. -/
 def add (T₁ T₂ : 𝓣.TensorIndex) (h : IndexListColor.PermContr T₁.index T₂.index) :
@@ -103,12 +134,70 @@ def add (T₁ T₂ : 𝓣.TensorIndex) (h : IndexListColor.PermContr T₁.index
       𝓣.mapIso h.toEquiv.symm h.toEquiv_colorMap T₂.contr.tensor
     T1 + T2
 
-/-- An (equivalence) relation on two `TensorIndex` given that after contraction,
-  the two underlying tensors are the equal. -/
+/-!
+
+## Equivalence relation on `TensorIndex`
+
+-/
+
+/-- An (equivalence) relation on two `TensorIndex`.
+  The point in this equivalence relation is that certain things (like the
+  permutation of indices, the contraction of indices, or rising or lowering indices) can be placed
+  in the indices or moved to the tensor itself. These two descriptions are equivalent. -/
 def Rel (T₁ T₂ : 𝓣.TensorIndex) : Prop :=
   T₁.index.PermContr T₂.index ∧ ∀ (h : T₁.index.PermContr T₂.index),
   T₁.contr.tensor = 𝓣.mapIso h.toEquiv.symm h.toEquiv_colorMap T₂.contr.tensor
 
+namespace Rel
+
+/-- Rel is reflexive. -/
+lemma refl (T : 𝓣.TensorIndex) : Rel T T := by
+  apply And.intro
+  exact IndexListColor.PermContr.refl T.index
+  intro h
+  simp [PermContr.toEquiv_refl']
+
+/-- Rel is symmetric. -/
+lemma symm {T₁ T₂ : 𝓣.TensorIndex} (h : Rel T₁ T₂) : Rel T₂ T₁ := by
+  apply And.intro h.1.symm
+  intro h'
+  rw [← mapIso_symm]
+  symm
+  erw [LinearEquiv.symm_apply_eq]
+  rw [h.2]
+  apply congrFun
+  congr
+  exact h'.symm
+
+/-- Rel is transitive. -/
+lemma trans {T₁ T₂ T₃ : 𝓣.TensorIndex} (h1 : Rel T₁ T₂) (h2 : Rel T₂ T₃) : Rel T₁ T₃ := by
+  apply And.intro (h1.1.trans h2.1)
+  intro h
+  change _ = (𝓣.mapIso (h1.1.trans h2.1).toEquiv.symm _) T₃.contr.tensor
+  trans (𝓣.mapIso ((h1.1).toEquiv.trans (h2.1).toEquiv).symm (by
+    rw [← PermContr.toEquiv_trans]
+    exact proof_2 T₁ T₃ h)) T₃.contr.tensor
+  swap
+  congr
+  rw [← PermContr.toEquiv_trans]
+  erw [← mapIso_trans]
+  simp only [LinearEquiv.trans_apply]
+  apply (h1.2 h1.1).trans
+  apply congrArg
+  exact h2.2 h2.1
+
+/-- Rel forms an equivalence relation. -/
+lemma equivalence : Equivalence (@Rel _ _ 𝓣 _) where
+  refl := Rel.refl
+  symm := Rel.symm
+  trans := Rel.trans
+
+/-- The equality of tensors corresponding to related tensor indices. -/
+lemma to_eq {T₁ T₂ : 𝓣.TensorIndex} (h : Rel T₁ T₂) :
+    T₁.contr.tensor = 𝓣.mapIso h.1.toEquiv.symm h.1.toEquiv_colorMap T₂.contr.tensor := h.2 h.1
+
+end Rel
+
 end TensorIndex
 end
 end TensorStructure
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean b/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean
new file mode 100644
index 0000000..9090384
--- /dev/null
+++ b/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean
@@ -0,0 +1,117 @@
+/-
+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.IndexNotation.TensorIndex
+import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexString
+import HepLean.SpaceTime.LorentzTensor.Real.Basic
+/-!
+
+# Index notation for real Lorentz tensors
+
+This uses the general concepts of index notation in `HepLean.SpaceTime.LorentzTensor.IndexNotation`
+to define the index notation for real Lorentz tensors.
+
+-/
+
+
+instance : IndexNotation realTensorColor.Color where
+  charList := {'ᵘ', 'ᵤ'}
+  notaEquiv :=
+    ⟨fun c =>
+      match c with
+      | realTensorColor.ColorType.up => ⟨'ᵘ', Finset.mem_insert_self 'ᵘ' {'ᵤ'}⟩
+      | realTensorColor.ColorType.down => ⟨'ᵤ', Finset.insert_eq_self.mp (by rfl)⟩,
+    fun c =>
+      if c = 'ᵘ' then realTensorColor.ColorType.up
+      else realTensorColor.ColorType.down,
+    by
+      intro c
+      match c with
+      | realTensorColor.ColorType.up => rfl
+      | realTensorColor.ColorType.down => rfl,
+    by
+      intro c
+      by_cases hc : c = 'ᵘ'
+      simp [hc]
+      exact SetCoe.ext (id (Eq.symm hc))
+      have hc' : c = 'ᵤ' := by
+        have hc2 := c.2
+        simp at hc2
+        simp_all
+      simp [hc']
+      exact SetCoe.ext (id (Eq.symm hc'))⟩
+
+namespace realLorentzTensor
+
+open realTensorColor
+
+variable {d : ℕ}
+
+instance : IndexNotation (realLorentzTensor d).Color := instIndexNotationColorRealTensorColor
+instance : DecidableEq (realLorentzTensor d).Color := instDecidableEqColorRealTensorColor
+
+@[simp]
+lemma indexNotation_eq_color : @realLorentzTensor.instIndexNotationColor d = instIndexNotationColorRealTensorColor := by
+  rfl
+
+@[simp]
+lemma realLorentzTensor_color : (realLorentzTensor d).Color = realTensorColor.Color := by
+  rfl
+
+@[simp]
+lemma toTensorColor_eq : (realLorentzTensor d).toTensorColor = realTensorColor := by
+  rfl
+
+open IndexNotation IndexString
+
+open TensorStructure TensorIndex
+
+/-- The construction of a tensor index from a tensor and a string satisfying conditions
+  which can be automatically checked. This is a modified version of
+  `TensorStructure.TensorIndex.mkDualMap` specific to real Lorentz tensors. -/
+noncomputable def fromIndexStringColor {cn : Fin n → realTensorColor.Color}
+    (T : (realLorentzTensor d).Tensor cn) (s : String)
+    (hs : listCharIndexStringBool realTensorColor.Color s.toList = true)
+    (hn : n = (IndexString.toIndexList (⟨s, hs⟩ : IndexString realTensorColor.Color)).length)
+    (hc : IndexListColor.colorPropBool  (IndexString.toIndexList ⟨s, hs⟩))
+    (hd : TensorColor.DualMap.boolFin (IndexString.toIndexList ⟨s, hs⟩).colorMap (cn ∘ Fin.cast hn.symm)) :
+    (realLorentzTensor d).TensorIndex :=
+  TensorStructure.TensorIndex.mkDualMap T
+    ⟨(IndexString.toIndexList (⟨s, hs⟩ : IndexString realTensorColor.Color)),
+      IndexListColor.colorPropBool_indexListColorProp hc⟩ hn
+      (TensorColor.DualMap.boolFin_DualMap hd)
+
+/-- A tactics used to prove `colorPropBool` for real Lorentz tensors. -/
+macro "prodTactic" : tactic =>
+    `(tactic| {
+     change @IndexListColor.colorPropBool realTensorColor _ _ _
+     simp only [toTensorColor_eq, indexNotation_eq_color, fromIndexStringColor, mkDualMap,
+      String.toList, ↓Char.isValue, Equiv.coe_refl, Function.comp_apply, id_eq, ne_eq,
+      Function.comp_id, RelIso.coe_fn_toEquiv, prod_index, IndexListColor.prod]
+     rfl})
+
+/-- A tactic used to prove `boolFin` for real Lornetz tensors. -/
+macro "dualMapTactic" : tactic =>
+    `(tactic| {
+     simp only [String.toList, ↓Char.isValue, toTensorColor_eq]
+     rfl})
+
+/-- Notation for the construction of a tensor index from a tensor and a string.
+  Conditions are checked automatically. -/
+notation:20 T "|" S:21 => fromIndexStringColor T S (by rfl) (by rfl) (by rfl) (by dualMapTactic)
+
+/-- Notation for the product of two tensor indices. Conditions are checked automatically. -/
+notation:10 T "⊗ᵀ" S:11 => TensorIndex.prod T S (IndexListColor.colorPropBool_indexListColorProp
+  (by prodTactic))
+
+/-- An example showing the allowed constructions. -/
+example (T : (realLorentzTensor d).Tensor ![ColorType.up, ColorType.down]) : True := by
+  let _ :=  T|"ᵤ₁ᵤ₂"
+  let _ := T|"ᵘ³ᵤ₄"
+  let _ := T|"ᵤ₁ᵤ₂" ⊗ᵀ T|"ᵘ³ᵤ₄"
+  let _ :=  T|"ᵤ₁ᵤ₂" ⊗ᵀ T|"ᵘ³ᵤ₄" ⊗ᵀ T|"ᵘ¹ᵘ²" ⊗ᵀ T|"ᵘ⁴ᵤ₃"
+  exact trivial
+
+end realLorentzTensor
diff --git a/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean b/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean
index 180502a..d26748a 100644
--- a/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean
+++ b/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean
@@ -253,6 +253,24 @@ def DualMap (c₁ : X → 𝓒.Color) (c₂ : X → 𝓒.Color) : Prop :=
 namespace DualMap
 
 variable {c₁ c₂ c₃ : X → 𝓒.Color}
+variable {n : ℕ}
+
+/-- The bool which if `𝓒.colorQuot (c₁ i) = 𝓒.colorQuot (c₂ i)` is true for all `i`. -/
+def boolFin (c₁ c₂ : Fin n → 𝓒.Color) : Bool :=
+  (Fin.list n).all fun i => if 𝓒.colorQuot (c₁ i) = 𝓒.colorQuot (c₂ i) then true else false
+
+lemma boolFin_DualMap {c₁ c₂ : Fin n → 𝓒.Color} (h : boolFin c₁ c₂ = true) :
+    DualMap c₁ c₂ := by
+  simp [boolFin] at h
+  simp [DualMap]
+  funext x
+  have h2 {n : ℕ} (m : Fin n) : m ∈ Fin.list n := by
+    have h1' : (Fin.list n)[m] = m := by
+      erw [Fin.getElem_list]
+      rfl
+    rw [← h1']
+    apply List.getElem_mem
+  exact h x (h2 _)
 
 lemma refl : DualMap c₁ c₁ := by
   simp [DualMap]
diff --git a/README.md b/README.md
index f2de335..f35a25c 100644
--- a/README.md
+++ b/README.md
@@ -4,7 +4,7 @@
 [![](https://img.shields.io/badge/PRs-Welcome-green)](https://github.com/HEPLean/HepLean/pulls)
 [![](https://img.shields.io/badge/Lean-Zulip-green)](https://leanprover.zulipchat.com)
 [![](https://img.shields.io/badge/TODO-List-green)](https://heplean.github.io/HepLean/TODOList)
-[![](https://img.shields.io/badge/Lean-v4.10.0-blue)](https://github.com/leanprover/lean4/releases/tag/v4.10.0)
+[![](https://img.shields.io/badge/Lean-v4.11.0--rc1-blue)](https://github.com/leanprover/lean4/releases/tag/v4.11.0-rc1)
 
 A project to digitalize high energy physics.
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 115db29..9979f5b 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0f3e143dffdc3a591662f3401ce1d7a3405227c0",
+   "rev": "dc167d260ff7ee9849b436037add06bed15104be",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "209712c78b16c795453b6da7f7adbda4589a8f21",
+   "rev": "ae6ea60e9d8bc2d4b37ff02115854da2e1b710d0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,10 +35,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c87908619cccadda23f71262e6898b9893bffa36",
+   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.40",
+   "inputRev": "v0.0.41",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "543725b3bfed792097fc134adca628406f6145f5",
+   "rev": "68cd8ae0f5b996176d1243d94c56e17de570e3bf",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,10 +65,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a719ba5c3115d47b68bf0497a9dd1bcbb21ea663",
+   "rev": "5025874dc5f9f8dd1598190e60ef20dda7b42566",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.10.0",
+   "inputRev": "v4.11.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/acmepjz/md4lean",
diff --git a/lakefile.toml b/lakefile.toml
index d75251e..67e67b4 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -6,7 +6,7 @@ defaultTargets = ["HepLean"]
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.10.0"
+rev = "v4.11.0-rc1"
 
 [[require]]
 name = "«doc-gen4»"
diff --git a/lean-toolchain b/lean-toolchain
index 7f0ea50..64981ae 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.10.0
+leanprover/lean4:v4.11.0-rc1

From 73e67b8d3d4672d4b086f13e5b696c48a9f43c23 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 6 Aug 2024 08:12:20 -0400
Subject: [PATCH 2/3] chore: Update doc-gen

---
 lake-manifest.json | 4 ++--
 lakefile.toml      | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 9979f5b..ce3a4cd 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -105,10 +105,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "593ac5bd2ca98c5294675b5cccf3d89b300a76eb",
+   "rev": "6d8e3118ab526f8dfcabcbdf9f05dc34e5c423a8",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.10.0",
+   "inputRev": "v4.11.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "hep_lean",
diff --git a/lakefile.toml b/lakefile.toml
index 67e67b4..04b47d6 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -11,7 +11,7 @@ rev = "v4.11.0-rc1"
 [[require]]
 name = "«doc-gen4»"
 git = "https://github.com/leanprover/doc-gen4"
-rev = "v4.10.0"
+rev = "v4.11.0-rc1"
 
 [[lean_lib]]
 name = "HepLean"

From 91234314240925e4bc201750820009804f3411e7 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 6 Aug 2024 08:16:50 -0400
Subject: [PATCH 3/3] refactor: Lint

---
 HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean b/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean
index 9090384..7482ecd 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean
@@ -53,7 +53,8 @@ instance : IndexNotation (realLorentzTensor d).Color := instIndexNotationColorRe
 instance : DecidableEq (realLorentzTensor d).Color := instDecidableEqColorRealTensorColor
 
 @[simp]
-lemma indexNotation_eq_color : @realLorentzTensor.instIndexNotationColor d = instIndexNotationColorRealTensorColor := by
+lemma indexNotation_eq_color : @realLorentzTensor.instIndexNotationColor d =
+    instIndexNotationColorRealTensorColor := by
   rfl
 
 @[simp]
@@ -76,7 +77,8 @@ noncomputable def fromIndexStringColor {cn : Fin n → realTensorColor.Color}
     (hs : listCharIndexStringBool realTensorColor.Color s.toList = true)
     (hn : n = (IndexString.toIndexList (⟨s, hs⟩ : IndexString realTensorColor.Color)).length)
     (hc : IndexListColor.colorPropBool  (IndexString.toIndexList ⟨s, hs⟩))
-    (hd : TensorColor.DualMap.boolFin (IndexString.toIndexList ⟨s, hs⟩).colorMap (cn ∘ Fin.cast hn.symm)) :
+    (hd : TensorColor.DualMap.boolFin
+    (IndexString.toIndexList ⟨s, hs⟩).colorMap (cn ∘ Fin.cast hn.symm)) :
     (realLorentzTensor d).TensorIndex :=
   TensorStructure.TensorIndex.mkDualMap T
     ⟨(IndexString.toIndexList (⟨s, hs⟩ : IndexString realTensorColor.Color)),