feat: List properties of contrIndexList

HepLean/SpaceTime/LorentzTensor/Contraction.lean

@@ -31,8 +31,6 @@ We define a number of ways to contract indices of tensors:
 
 -/
 
-/-! TODO: Define contraction based on an equivalence `(C ⊗ C) ⊗ P ≃ X` satisfying ... . -/
-
 noncomputable section
 
 open TensorProduct

HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean

@@ -286,6 +286,10 @@ variable (l l2 l3 : IndexList X)
 instance : HAppend (IndexList X) (IndexList X) (IndexList X) where
   hAppend := fun l l2 => {val := l.val ++ l2.val}
 
+@[simp]
+lemma cons_append (i : Index X) : (l.cons i) ++ l2 = (l ++ l2).cons i := by
+  rfl
+
 @[simp]
 lemma append_length : (l ++ l2).length = l.length + l2.length := by
   simp [IndexList.length]

HepLean/SpaceTime/LorentzTensor/IndexNotation/Color.lean

@@ -481,7 +481,10 @@ lemma contrEquiv_on_withDual_empty (i : Fin l.contr.length) (h : l.withDual =
 -/
 
 /-- The condition on the `ColorIndexList`s `l` and `l2` so that on appending they form
-  a `ColorIndexList`. -/
+  a `ColorIndexList`.
+
+  Note: `AppendCond` does not form an equivalence relation as it is not reflexive or
+  transitive. -/
 def AppendCond : Prop :=
   (l.toIndexList ++ l2.toIndexList).withUniqueDual = (l.toIndexList ++ l2.toIndexList).withDual
   ∧ ColorCond (l.toIndexList ++ l2.toIndexList)
@@ -506,6 +509,7 @@ namespace AppendCond
 
 variable {l l2 l3 : ColorIndexList 𝓒}
 
+@[symm]
 lemma symm (h : AppendCond l l2) : AppendCond l2 l := by
   apply And.intro _ (h.2.symm h.1)
   rw [append_withDual_eq_withUniqueDual_symm]
@@ -543,7 +547,9 @@ lemma swap (h : AppendCond l l2) (h' : AppendCond (l ++[h] l2) l3) :
     simpa using h'.1
   · exact ColorCond.swap h'.1 h'.2
 
-lemma appendCond_of_eq (h1 : l.withUniqueDual = l.withDual)
+/-! TODO: Show that `AppendCond l l2` implies `AppendCond l.contr l2.contr`. -/
+
+lemma of_eq (h1 : l.withUniqueDual = l.withDual)
     (h2 : l2.withUniqueDual = l2.withDual)
     (h3 : l.withUniqueDualInOther l2 = l.withDualInOther l2)
     (h4 : l2.withUniqueDualInOther l = l2.withDualInOther l)

HepLean/SpaceTime/LorentzTensor/IndexNotation/Contraction.lean

@@ -255,6 +255,15 @@ def dualEquiv : l.withDual ⊕ Fin l.withoutDual.card ≃ Fin l.length :=
 def contrIndexList : IndexList X where
   val := l.val.filter (fun i => l.val.countP (fun j => i.id = j.id) = 1)
 
+@[simp]
+lemma contrIndexList_empty : (⟨[]⟩ : IndexList X).contrIndexList = { val := [] } := by
+  apply ext
+  simp [contrIndexList]
+
+lemma contrIndexList_val : l.contrIndexList.val =
+    l.val.filter (fun i => l.val.countP (fun j => i.id = j.id) = 1) := by
+  rfl
+
 /-- An alternative form of the contracted index list. -/
 @[simp]
 def contrIndexList' : IndexList X where
@@ -370,6 +379,98 @@ lemma contrIndexList_getDualInOther?_self (i : Fin l.contrIndexList.length) :
     exact (contrIndexList_areDualInSelf_false l i j).mp h
   exact Fin.ge_of_eq (id (Eq.symm h1))
 
+lemma mem_contrIndexList_count {I : Index X} (h : I ∈ l.contrIndexList.val) :
+    l.val.countP (fun J => I.id = J.id) = 1 := by
+  simp only [contrIndexList, List.mem_filter, decide_eq_true_eq] at h
+  exact h.2
+
+lemma mem_contrIndexList_filter {I : Index X} (h : I ∈ l.contrIndexList.val) :
+    l.val.filter (fun J => I.id = J.id) = [I] := by
+  have h1 : (l.val.filter (fun J => I.id = J.id)).length = 1 := by
+    rw [← List.countP_eq_length_filter]
+    exact l.mem_contrIndexList_count h
+  have h2 : I ∈ l.val.filter (fun J => I.id = J.id) := by
+    simp
+    simp [contrIndexList] at h
+    exact h.1
+  rw [List.length_eq_one] at h1
+  obtain ⟨J, hJ⟩ := h1
+  rw [hJ] at h2
+  simp at h2
+  subst h2
+  exact hJ
+
+lemma cons_contrIndexList_of_countP_eq_zero {I : Index X}
+    (h : l.val.countP (fun J => I.id = J.id) = 0) :
+    (l.cons I).contrIndexList = l.contrIndexList.cons I := by
+  apply ext
+  simp [contrIndexList]
+  rw [List.filter_cons_of_pos]
+  · apply congrArg
+    apply List.filter_congr
+    intro J hJ
+    simp only [decide_eq_decide]
+    rw [List.countP_eq_zero] at h
+    simp only [decide_eq_true_eq] at h
+    rw [List.countP_cons_of_neg]
+    simp only [decide_eq_true_eq]
+    exact fun a => h J hJ (id (Eq.symm a))
+  · simp only [decide_True, List.countP_cons_of_pos, add_left_eq_self, decide_eq_true_eq]
+    exact h
+
+lemma cons_contrIndexList_of_countP_neq_zero {I : Index X}
+    (h : l.val.countP (fun J => I.id = J.id) ≠ 0) :
+    (l.cons I).contrIndexList.val = l.contrIndexList.val.filter (fun J => ¬ I.id = J.id) := by
+  simp only [contrIndexList, cons_val, decide_not, List.filter_filter, Bool.not_eq_true',
+    decide_eq_false_iff_not, decide_eq_true_eq, Bool.decide_and]
+  rw [List.filter_cons_of_neg]
+  · apply List.filter_congr
+    intro J hJ
+    by_cases hI : I.id = J.id
+    · simp only [hI, decide_True, List.countP_cons_of_pos, add_left_eq_self, Bool.not_true,
+      Bool.false_and, decide_eq_false_iff_not]
+      rw [hI] at h
+      simp only [h, not_false_eq_true]
+    · simp only [hI, decide_False, Bool.not_false, Bool.true_and, decide_eq_decide]
+      rw [List.countP_cons_of_neg]
+      simp
+      exact fun a => hI (id (Eq.symm a))
+  · simp only [decide_True, List.countP_cons_of_pos, add_left_eq_self, decide_eq_true_eq]
+    exact h
+
+lemma mem_contrIndexList_count_contrIndexList {I : Index X} (h : I ∈ l.contrIndexList.val) :
+    l.contrIndexList.val.countP (fun J => I.id = J.id) = 1 := by
+  trans (l.val.filter (fun J => I.id = J.id)).countP
+    (fun i => l.val.countP (fun j => i.id = j.id) = 1)
+  · rw [contrIndexList]
+    simp only
+    rw [List.countP_filter, List.countP_filter]
+    simp only [decide_eq_true_eq, Bool.decide_and]
+    congr
+    funext a
+    rw [Bool.and_comm]
+  · rw [l.mem_contrIndexList_filter h, List.countP_cons_of_pos]
+    rfl
+    simp only [decide_eq_true_eq]
+    exact mem_contrIndexList_count l h
+
+lemma countP_contrIndexList_zero_of_countP (I : Index X)
+    (h : List.countP (fun J => I.id = J.id) l.val = 0) :
+    l.contrIndexList.val.countP (fun J => I.id = J.id) = 0 := by
+  trans (l.val.filter (fun J => I.id = J.id)).countP
+    (fun i => l.val.countP (fun j => i.id = j.id) = 1)
+  · rw [contrIndexList]
+    simp
+    rw [List.countP_filter, List.countP_filter]
+    simp only [decide_eq_true_eq, Bool.decide_and]
+    congr
+    funext a
+    rw [Bool.and_comm]
+  · rw [List.countP_eq_length_filter] at h
+    rw [List.length_eq_zero] at h
+    rw [h]
+    simp only [List.countP_nil]
+
 /-!
 
 ## Splitting withUniqueDual

HepLean/SpaceTime/LorentzTensor/IndexNotation/Relations.lean

@@ -30,14 +30,77 @@ open IndexList TensorColor
 
 -/
 
-/-- Two `ColorIndexList` are said to be reindexes of one another if they:
-  (1) have the same length and (2) every corresponding index has the same color,
-    and duals which correspond.
+/--
+  Two `ColorIndexList` are said to be reindexes of one another if they:
+    1. have the same length.
+    2. every corresponding index has the same color, and duals which correspond.
 
-  Note: This does not allow for reordrings of indices. -/
+  Note: This does not allow for reordrings of indices.
+-/
 def Reindexing : Prop := l.length = l'.length ∧
   ∀ (h : l.length = l'.length), l.colorMap = l'.colorMap ∘ Fin.cast h ∧
-    Option.map (Fin.cast h) ∘ l.getDual? = l'.getDual? ∘ Fin.cast h
+    l.getDual? = Option.map (Fin.cast h.symm) ∘  l'.getDual? ∘ Fin.cast h
+
+namespace Reindexing
+
+variable {l l' l2 l3 : ColorIndexList 𝓒}
+
+/-- The relation `Reindexing` is symmetric. -/
+@[symm]
+lemma symm (h : Reindexing l l') : Reindexing l' l := by
+  apply And.intro h.1.symm
+  intro h'
+  have h2 := h.2 h.1
+  apply And.intro
+  · rw [h2.1]
+    funext a
+    simp only [Function.comp_apply, Fin.cast_trans, Fin.cast_eq_self]
+  · rw [h2.2]
+    funext a
+    simp only [Function.comp_apply, Fin.cast_trans, Fin.cast_eq_self, Option.map_map]
+    have h1 (h : l.length = l'.length) : Fin.cast h ∘  Fin.cast h.symm = id := by
+      funext a
+      simp only [Function.comp_apply, Fin.cast_trans, Fin.cast_eq_self, id_eq]
+    rw [h1]
+    simp only [Option.map_id', id_eq]
+
+/-- The relation `Reindexing` is reflexive. -/
+@[simp]
+lemma refl (l : ColorIndexList 𝓒) : Reindexing l l := by
+  apply And.intro rfl
+  intro h
+  apply And.intro
+  · funext a
+    rfl
+  · funext a
+    simp only [Fin.cast_refl, Option.map_id', CompTriple.comp_eq, Function.comp_apply, id_eq]
+
+/-- The relation `Reindexing` is transitive. -/
+@[trans]
+lemma trans (h1 : Reindexing l l2) (h2 : Reindexing l2 l3) : Reindexing l l3 := by
+  apply And.intro (h1.1.trans h2.1)
+  intro h'
+  have h1' := h1.2 h1.1
+  have h2' := h2.2 h2.1
+  apply And.intro
+  · simp only [h1'.1, h2'.1]
+    funext a
+    rfl
+  · simp only [h1'.2, h2'.2]
+    funext a
+    simp only [Function.comp_apply, Fin.cast_trans, Option.map_map]
+    apply congrFun
+    apply congrArg
+    funext a
+    rfl
+
+/-- `Reindexing` forms an equivalence relation. -/
+lemma equivalence : Equivalence (@Reindexing 𝓒 _) where
+  refl := refl
+  symm := symm
+  trans := trans
+
+end Reindexing
 
 /-!
 
@@ -48,10 +111,14 @@ To prevent choice problems, this has to be done after contraction.
 
 -/
 
-/-- Two `ColorIndexList` are said to be related by contracted permutations, `ContrPerm`,
-  if and only if: 1) Their contractions are the same length.
+/--
+  Two `ColorIndexList`s are said to be related by contracted permutations, `ContrPerm`,
+  if and only if:
+
+    1) Their contractions are the same length.
     2) Every index in the contracted list of one has a unqiue dual in the contracted
-      list of the other and that dual has a the same color. -/
+      list of the other and that dual has a the same color.
+-/
 def ContrPerm : Prop :=
   l.contr.length = l'.contr.length ∧
   l.contr.withUniqueDualInOther l'.contr = Finset.univ ∧
@@ -62,6 +129,7 @@ namespace ContrPerm
 
 variable {l l' l2 l3 : ColorIndexList 𝓒}
 
+/-- The relation `ContrPerm` is symmetric. -/
 @[symm]
 lemma symm (h : ContrPerm l l') : ContrPerm l' l := by
   rw [ContrPerm] at h ⊢
@@ -72,12 +140,14 @@ lemma symm (h : ContrPerm l l') : ContrPerm l' l := by
     (l'.contr.getDualInOtherEquiv l.contr).symm from rfl]
   simp only [Equiv.symm_comp_self, CompTriple.comp_eq]
 
+/-- The relation `ContrPerm` is reflexive. -/
 @[simp]
-lemma refl : ContrPerm l l := by
+lemma refl (l : ColorIndexList 𝓒) : ContrPerm l l := by
   apply And.intro rfl
   apply And.intro l.withUniqueDualInOther_eq_univ_contr_refl
   simp only [getDualInOtherEquiv_self_refl, Equiv.coe_refl, CompTriple.comp_eq]
 
+/-- The relation `ContrPerm` is transitive. -/
 @[trans]
 lemma trans (h1 : ContrPerm l l2) (h2 : ContrPerm l2 l3) : ContrPerm l l3 := by
   apply And.intro (h1.1.trans h2.1)
@@ -98,6 +168,12 @@ lemma trans (h1 : ContrPerm l l2) (h2 : ContrPerm l2 l3) : ContrPerm l l3 := by
   rw [h2.2.1]
   simp
 
+/-- `ContrPerm` forms an equivalence relation. -/
+lemma equivalence : Equivalence (@ContrPerm 𝓒 _) where
+  refl := refl
+  symm := symm
+  trans := trans
+
 lemma symm_trans (h1 : ContrPerm l l2) (h2 : ContrPerm l2 l3) :
     (h1.trans h2).symm = h2.symm.trans h1.symm := by
   simp only
@@ -130,6 +206,12 @@ lemma mem_withUniqueDualInOther_of_no_contr (h : l.ContrPerm l') (h1 : l.withDua
 
 end ContrPerm
 
+/-!
+
+## Equivalences from `ContrPerm`
+
+-/
+
 open ContrPerm
 
 /-- Given two `ColorIndexList` related by contracted permutations, the equivalence between

HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean

@@ -181,31 +181,7 @@ lemma contr_toColorIndexList (T : 𝓣.TensorIndex) :
     T.contr.toColorIndexList = T.toColorIndexList.contr := rfl
 
 lemma contr_toIndexList (T : 𝓣.TensorIndex) :
-    T.contr.toIndexList = T.toIndexList.contrIndexList := by
-  rfl
-/-!
-
-## Scalar multiplication of
-
--/
-
-/-- The scalar multiplication of a `TensorIndex` by an element of `R`. -/
-instance : SMul R 𝓣.TensorIndex where
-  smul := fun r T => {
-    toColorIndexList := T.toColorIndexList
-    tensor := r • T.tensor}
-
-@[simp]
-lemma smul_index (r : R) (T : 𝓣.TensorIndex) : (r • T).toColorIndexList = T.toColorIndexList := rfl
-
-@[simp]
-lemma smul_tensor (r : R) (T : 𝓣.TensorIndex) : (r • T).tensor = r • T.tensor := rfl
-
-@[simp]
-lemma smul_contr (r : R) (T : 𝓣.TensorIndex) : (r • T).contr = r • T.contr := by
-  refine ext rfl ?_
-  simp only [contr, smul_index, smul_tensor, LinearMapClass.map_smul, Fin.castOrderIso_refl,
-    OrderIso.refl_toEquiv, mapIso_refl, LinearEquiv.refl_apply]
+    T.contr.toIndexList = T.toIndexList.contrIndexList := rfl
 
 /-!
 
@@ -310,7 +286,32 @@ lemma rel_contr (T : 𝓣.TensorIndex) : T ≈ T.contr := by
   apply congrArg
   rfl
 
-lemma smul_equiv {T₁ T₂ : 𝓣.TensorIndex} (h : T₁ ≈ T₂) (r : R) : r • T₁ ≈ r • T₂ := by
+
+/-!
+
+## Scalar multiplication of
+
+-/
+
+/-- The scalar multiplication of a `TensorIndex` by an element of `R`. -/
+instance : SMul R 𝓣.TensorIndex where
+  smul := fun r T => {
+    toColorIndexList := T.toColorIndexList
+    tensor := r • T.tensor}
+
+@[simp]
+lemma smul_index (r : R) (T : 𝓣.TensorIndex) : (r • T).toColorIndexList = T.toColorIndexList := rfl
+
+@[simp]
+lemma smul_tensor (r : R) (T : 𝓣.TensorIndex) : (r • T).tensor = r • T.tensor := rfl
+
+@[simp]
+lemma smul_contr (r : R) (T : 𝓣.TensorIndex) : (r • T).contr = r • T.contr := by
+  refine ext rfl ?_
+  simp only [contr, smul_index, smul_tensor, LinearMapClass.map_smul, Fin.castOrderIso_refl,
+    OrderIso.refl_toEquiv, mapIso_refl, LinearEquiv.refl_apply]
+
+lemma smul_rel {T₁ T₂ : 𝓣.TensorIndex} (h : T₁ ≈ T₂) (r : R) : r • T₁ ≈ r • T₂ := by
   apply And.intro h.1
   intro h1
   rw [tensor_eq_of_eq (smul_contr r T₁), tensor_eq_of_eq (smul_contr r T₂)]
@@ -521,14 +522,14 @@ lemma add_assoc {T₁ T₂ T₃ : 𝓣.TensorIndex} {h' : AddCond T₁ T₂} (h
     T₁ +[h'] T₂ +[h] T₃ = T₁ +[h'.add_right_of_add_left h] (T₂ +[h'.of_add_left h] T₃) := by
   rw [add_assoc']
 
-/-! TODO: Show that the product is well defined with respect to Rel. -/
-
 /-!
 
 ## Product of `TensorIndex` when allowed
 
 -/
 
+/-! TODO: Show that the product is well defined with respect to Rel. -/
+
 /-- The condition on two `TensorIndex` which is true if and only if their `ColorIndexList`s
   are related by the condition `AppendCond`. That is, they can be appended to form a
   `ColorIndexList`. -/
@@ -549,7 +550,9 @@ lemma symm (h : ProdCond T₁ T₂) : ProdCond T₂ T₁ := h.to_AppendCond.symm
 
 end ProdCond
 
-/-- The tensor product of two `TensorIndex`. -/
+/-- The tensor product of two `TensorIndex`.
+
+  Note: By defualt contraction is NOT done before taking the products. -/
 def prod (T₁ T₂ : 𝓣.TensorIndex) (h : ProdCond T₁ T₂) : 𝓣.TensorIndex where
   toColorIndexList := T₁ ++[h] T₂
   tensor := 𝓣.mapIso IndexList.appendEquiv (T₁.colorMap_sumELim T₂) <|