Merge pull request #115 from HEPLean/Index-notation

Docs: Index notation

HepLean/SpaceTime/LorentzTensor/IndexNotation/AreDual.lean

@@ -8,6 +8,15 @@ import HepLean.SpaceTime.LorentzTensor.IndexNotation.Basic
 
 # Indices which are dual in an index list
 
+Given an list of indices we say two indices are dual if they have the same id.
+
+For example the `0`, `2` and `3` index in `l₁ := ['ᵘ¹', 'ᵘ²', 'ᵤ₁', 'ᵘ¹']` are pairwise dual to
+  one another. The `1` (`'ᵘ²'`) index is not dual to any other index in the list.
+
+We also define the notion of dual indices in different lists. For example,
+  the `1` index in `l₁` is dual to the `1` and the `4` indices in
+  `l₂ := ['ᵘ³', 'ᵘ²', 'ᵘ⁴', 'ᵤ₂']`.
+
 -/
 
 namespace IndexNotation

HepLean/SpaceTime/LorentzTensor/IndexNotation/Color.lean

@@ -10,11 +10,17 @@ import Init.Data.List.Lemmas
 import HepLean.SpaceTime.LorentzTensor.Contraction
 /-!
 
-# Index lists with color conditions
+# Index lists and color
 
-Here we consider `IndexListColor` which is a subtype of all lists of indices
+In this file we look at the interaction of index lists with color.
-on those where the elements to be contracted have consistent colors with respect to
+
-a Tensor Color structure.
+The main definiton of this file is `ColorIndexList`. This type defines the
+permissible index lists which can be used for a tensor. These are lists of indices for which
+every index with a dual has a unique dual, and the color of that dual (when it exists) is dual
+to the color of the index.
+
+We also define `AppendCond`, which is a condition on two `ColorIndexList`s which allows them to be
+appended to form a new `ColorIndexList`.
 
 -/
 

HepLean/SpaceTime/LorentzTensor/IndexNotation/Contraction.lean

@@ -8,7 +8,25 @@ import Mathlib.Algebra.Order.Ring.Nat
 import Mathlib.Data.Finset.Sort
 /-!
 
-# Contraction of Dual indices
+# Contraction of an index list.
+
+In this file we define the contraction of an index list `l` to be the index list formed by
+by the subset of indices of `l` which do not have a dual in `l`.
+
+For example, the contraction of the index list `['ᵘ¹', 'ᵘ²', 'ᵤ₁', 'ᵘ¹']` is the index list
+`['ᵘ²']`.
+
+We also define the following finite sets
+- `l.withoutDual` the finite set of indices of `l` which do not have a dual in `l`.
+- `l.withUniqueDualLT` the finite set of those indices of `l` which have a unique dual, and
+  for which that dual is greater-then (determined by the ordering on `Fin`) then the index itself.
+- `l.withUniqueDualGT` the finite set of those indices of `l` which have a unique dual, and
+  for which that dual is less-then (determined by the ordering on `Fin`) then the index itself.
+
+We define an equivalence `l.withUniqueDualLT ⊕ l.withUniqueDualLT ≃ l.withUniqueDual`.
+
+We prove properties related to when `l.withUniqueDualInOther l2 = Finset.univ` for two
+index lists `l` and `l2`.
 
 -/
 

HepLean/SpaceTime/LorentzTensor/IndexNotation/GetDual.lean

@@ -7,10 +7,25 @@ import HepLean.SpaceTime.LorentzTensor.IndexNotation.AreDual
 import Mathlib.Algebra.Order.Ring.Nat
 /-!
 
-# Get dual index
+# Getting dual index
 
-We define the functions `getDual?` and `getDualInOther?` which return the
+Using the option-monad we define two functions:
-  first dual index in an `IndexList`.
+- For a list of indices `l₁` the function `getDual?` takes in an index `i` in `l₁` and retruns
+  the the first index in `l₁` dual to `i`. If no such index exists, it returns `none`.
+- For two lists of indices `l₁` and `l₂` the function `getDualInOther?` takes in an index `i`
+  in `l₁` and returns the first index in `l₂` dual to `i`. If no such index exists,
+  it returns `none`.
+
+For example, given the lists `l₁ := ['ᵘ¹', 'ᵘ²', 'ᵤ₁', 'ᵘ¹']`, we have
+- `getDual? 0 = some 2`, `getDual? 1 = none`, `getDual? 2 = some 0`, `getDual? 3 = some 0`.
+
+Given the lists `l₁ := ['ᵘ¹', 'ᵘ²', 'ᵤ₁', 'ᵘ¹']` and `l₂ := ['ᵘ³', 'ᵘ²', 'ᵘ⁴', 'ᵤ₂']`, we have
+- `l₁.getDualInOther? l₂ 0 = none`, `l₁.getDualInOther? l₂ 1 = some 1`,
+  `l₁.getDualInOther? l₂ 2 = none`, `l₁.getDualInOther? l₂ 3 = none`.
+
+We prove some basic properties of `getDual?` and `getDualInOther?`. In particular,
+we prove lemmas related to how `getDual?` and `getDualInOther?` behave when we appending
+two index lists.
 
 -/
 

HepLean/SpaceTime/LorentzTensor/IndexNotation/OnlyUniqueDuals.lean

@@ -9,6 +9,11 @@ import Mathlib.Algebra.Order.Ring.Nat
 
 # withDuals equal to withUniqueDuals
 
+In a permissible list of indices every index which has a dual has a unique dual.
+This corresponds to the condition that `l.withDual = l.withUniqueDual`.
+
+We prove lemmas relating to this condition.
+
 -/
 
 namespace IndexNotation

HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean

@@ -477,7 +477,7 @@ lemma add_assoc {T₁ T₂ T₃ : 𝓣.TensorIndex} {h' : AddCond T₁ T₂} (h
 
 /-!
 
-## Product of `TensorIndex` allowed
+## Product of `TensorIndex` when allowed
 
 -/
 
@@ -489,14 +489,20 @@ def ProdCond (T₁ T₂ : 𝓣.TensorIndex) : Prop :=
 
 namespace ProdCond
 
-lemma to_AppendCond {T₁ T₂ : 𝓣.TensorIndex} (h : ProdCond T₁ T₂) :
+variable {T₁ T₁' T₂ T₂' : 𝓣.TensorIndex}
+
+lemma to_AppendCond (h : ProdCond T₁ T₂) :
     T₁.AppendCond T₂ := h
 
+@[symm]
+lemma symm (h : ProdCond T₁ T₂) : ProdCond T₂ T₁ := h.to_AppendCond.symm
+
+/-! TODO: Prove properties regarding the interaction of `ProdCond` and `Rel`. -/
+
 end ProdCond
 
 /-- The tensor product of two `TensorIndex`. -/
-def prod (T₁ T₂ : 𝓣.TensorIndex)
+def prod (T₁ T₂ : 𝓣.TensorIndex) (h : ProdCond T₁ T₂) : 𝓣.TensorIndex where
-    (h : ProdCond T₁ T₂) : 𝓣.TensorIndex where
   toColorIndexList := T₁ ++[h] T₂
   tensor := 𝓣.mapIso IndexList.appendEquiv (T₁.colorMap_sumELim T₂) <|
       𝓣.tensoratorEquiv _ _ (T₁.tensor ⊗ₜ[R] T₂.tensor)

HepLean/SpaceTime/LorentzTensor/IndexNotation/WithDual.lean

@@ -7,9 +7,22 @@ import HepLean.SpaceTime.LorentzTensor.IndexNotation.GetDual
 import Mathlib.Algebra.Order.Ring.Nat
 /-!
 
-# With dual
+# Indices with duals.
 
-We define the finite sets of indices in an index list which have a dual
+In this file we define the following finite sets:
+
+- Given an index list `l₁`, the finite set, `l₁.withDual`, of (positions in) `l₁`
+  corresponding to those indices which have a dual in `l₁`. This is equivalent to those indices
+  of `l₁` for which `getDual?` is `some`.
+- Given two index lists `l₁` and `l₂`, the finite set, `l₁.withDualInOther l₂` of (positions in)
+  `l₁` corresponding to those indices which have a dual in `l₂`. This is equivalent to those indices
+  of `l₁` for which `l₁.getDualInOther? l₂` is `some`.
+
+For example for `l₁ := ['ᵘ¹', 'ᵘ²', 'ᵤ₁', 'ᵘ¹']` and `l₂ := ['ᵘ³', 'ᵘ²', 'ᵘ⁴', 'ᵤ₂']` we have
+`l₁.withDual = {0, 2, 3}` and `l₁.withDualInOther l₂ = {1}`.
+
+We prove some properties of these finite sets. In particular, we prove properties
+related to how they interact with appending two index lists.
 
 -/
 

HepLean/SpaceTime/LorentzTensor/IndexNotation/WithUniqueDual.lean

@@ -7,12 +7,28 @@ import HepLean.SpaceTime.LorentzTensor.IndexNotation.WithDual
 import Mathlib.Algebra.Order.Ring.Nat
 /-!
 
-# With Unique Dual
+# Indices with a unique dual
 
-Finite sets of indices with a unique dual.
+In this file we define the following finite sets:
+
+- Given an index list `l₁`, the finite set, `l₁.withUniqueDual`, of (positions in) `l₁`
+  corresponding to those indices which have a unique dual in `l₁`.
+- Given two index lists `l₁` and `l₂`, the finite set, `l₁.withUniqueDualInOther l₂` of
+  (positions in) `l₁` corresponding to those indices which have a unique dual in `l₂`
+  and no duel in `l₁`.
+
+For example for `l₁ := ['ᵘ¹', 'ᵘ²', 'ᵤ₁', 'ᵘ¹', 'ᵘ²', 'ᵤ₃']` and
+`l₂ := ['ᵘ³', 'ᵘ²', 'ᵘ⁴', 'ᵤ₂']` we have
+`l₁.withUniqueDual = {1, 4}` and `l₁.withUniqueDualInOther l₂ = {5}`.
+
+The map `getDual?` defines an involution of `l₁.withUniqueDual`.
+The map `getDualInOther?` defines an equivalence from `l₁.withUniqueDualInOther l₂`
+to `l₂.withUniqueDualInOther l₁`.
+
+We prove some properties of these finite sets. In particular, we prove properties
+related to how they interact with appending two index lists.
 
 -/
-
 namespace IndexNotation
 
 namespace IndexList
@@ -93,7 +109,8 @@ lemma mem_withUniqueDualInOther_isSome (i : Fin l.length) (hi : i ∈ l.withUniq
 
 lemma all_dual_eq_getDual?_of_mem_withUniqueDual (i : Fin l.length) (h : i ∈ l.withUniqueDual) :
     ∀ j, l.AreDualInSelf i j → j = l.getDual? i := by
-  simp [withUniqueDual] at h
+  simp only [withUniqueDual, mem_withDual_iff_isSome, Finset.mem_filter, Finset.mem_univ,
+    true_and] at h
   exact fun j hj => h.2 j hj
 
 lemma some_eq_getDual?_of_withUniqueDual_iff (i j : Fin l.length) (h : i ∈ l.withUniqueDual) :
@@ -173,7 +190,9 @@ lemma getDual?_get_of_mem_withUnique_mem (i : Fin l.length) (h : i ∈ l.withUni
 lemma all_dual_eq_of_withUniqueDualInOther (i : Fin l.length)
     (h : i ∈ l.withUniqueDualInOther l2) :
     ∀ j, l.AreDualInOther l2 i j → j = l.getDualInOther? l2 i := by
-  simp [withUniqueDualInOther] at h
+  simp only [withUniqueDualInOther, mem_withDual_iff_isSome, Bool.not_eq_true, Option.not_isSome,
+    Option.isNone_iff_eq_none, mem_withInDualOther_iff_isSome, Finset.mem_filter, Finset.mem_univ,
+    true_and] at h
   exact fun j hj => h.2.2 j hj
 
 lemma some_eq_getDualInOther?_of_withUniqueDualInOther_iff (i : Fin l.length) (j : Fin l2.length)
@@ -471,11 +490,15 @@ lemma withUniqueDual_iff_not_withUniqueDualInOther_of_inl_withUniqueDualInOther
     i ∈ l.withUniqueDual ↔ ¬ i ∈ l.withUniqueDualInOther l2 := by
   by_cases h' : (l.getDual? i).isSome
   have hn : i ∈ l.withUniqueDual := mem_withUniqueDual_of_inl l l2 i h h'
-  simp_all
+  simp_all only [mem_withUniqueDual_isSome, not_mem_withDualInOther_of_inl_mem_withUniqueDual,
+    not_false_eq_true]
   have hn := l.append_inl_not_mem_withDual_of_withDualInOther l2 i h
-  simp_all
+  simp_all only [Bool.not_eq_true, Option.not_isSome, Option.isNone_iff_eq_none,
-  simp [withUniqueDual]
+    mem_withDual_iff_isSome, Option.isSome_none, Bool.false_eq_true, mem_withInDualOther_iff_isSome,
-  simp_all
+    false_iff]
+  simp only [withUniqueDual, mem_withDual_iff_isSome, Finset.mem_filter, Finset.mem_univ, true_and]
+  simp_all only [Option.isSome_none, Bool.false_eq_true, imp_false, false_and, false_iff,
+    Decidable.not_not]
   exact mem_withUniqueDualInOther_of_inl_withDualInOther l l2 i h (Option.ne_none_iff_isSome.mp hn)
 
 lemma append_inl_mem_withUniqueDual_of_withUniqueDual (i : Fin l.length)
@@ -599,7 +622,7 @@ lemma append_withUniqueDual : (l ++ l2).withUniqueDual =
         mem_withInDualOther_iff_isSome, Bool.not_eq_true, Option.not_isSome,
         Option.isNone_iff_eq_none]
       use k
-      simp [appendInr]
+      simp only [appendInr, Function.Embedding.coeFn_mk, Function.comp_apply, and_true]
       by_cases hk : k ∈ l2.withUniqueDualInOther l
       exact Or.inr hk
       have hk' := h.mpr hk
@@ -639,8 +662,14 @@ lemma append_withUniqueDual_disjSum : (l ++ l2).withUniqueDual =
   rw [Finset.map_map, Finset.map_map]
   ext1 a
   cases a with
-  | inl val => simp
+  | inl val => simp only [appendInl_appendEquiv, appendInr_appendEquiv, Finset.mem_union,
-  | inr val_1 => simp
+    Finset.mem_map, Finset.mem_inter, Finset.mem_compl, mem_withInDualOther_iff_isSome,
+    Bool.not_eq_true, Option.not_isSome, Option.isNone_iff_eq_none, Function.Embedding.coeFn_mk,
+    Sum.inl.injEq, exists_eq_right, and_false, exists_false, or_false, Finset.inl_mem_disjSum]
+  | inr val_1 => simp only [appendInl_appendEquiv, appendInr_appendEquiv, Finset.mem_union,
+    Finset.mem_map, Finset.mem_inter, Finset.mem_compl, mem_withInDualOther_iff_isSome,
+    Bool.not_eq_true, Option.not_isSome, Option.isNone_iff_eq_none, Function.Embedding.coeFn_mk,
+    and_false, exists_false, Sum.inr.injEq, exists_eq_right, false_or, Finset.inr_mem_disjSum]
 
 /-!
 
@@ -706,9 +735,9 @@ lemma withUniqueDualInOther_append_isSome_fst_iff_not_isSome_snd (i : Fin l.leng
     (h1 : i ∈ l.withUniqueDualInOther (l2 ++ l3)) :
     (l.getDualInOther? l2 i).isSome ↔ (l.getDualInOther? l3 i) = none := by
   by_cases hs : (l.getDualInOther? l2 i).isSome
-  simp [hs, h1]
+  simp only [hs, true_iff]
   exact l.withUniqueDualInOther_append_not_isSome_snd_of_isSome_fst l2 l3 i h1 hs
-  simp [hs]
+  simp only [hs, Bool.false_eq_true, false_iff]
   rw [← @Option.not_isSome_iff_eq_none, not_not]
   exact withUniqueDualInOther_append_isSome_snd_of_not_isSome_fst l l2 l3 i h1 hs
 
@@ -745,7 +774,7 @@ lemma mem_withUniqueDualInOther_symm' (i : Fin l.length)
   by_cases h2 : (l.getDualInOther? l3 i).isSome
   · simp only [h1, h2, not_true_eq_false, imp_false] at hc
     rw [← @Option.not_isSome_iff_eq_none] at hc
-    simp [h2] at hc
+    simp only [h2, not_true_eq_false, iff_false] at hc
   · simp only [h1, or_true, true_and]
     intro j
     obtain ⟨k, hk⟩ := appendEquiv.surjective j
@@ -754,7 +783,7 @@ lemma mem_withUniqueDualInOther_symm' (i : Fin l.length)
     | Sum.inl k =>
       simp only [AreDualInOther.of_append_inl]
       have hk'' := h.2.2 (appendEquiv (Sum.inr k))
-      simp at hk''
+      simp only [AreDualInOther.of_append_inr] at hk''
       exact fun h'' => ((getDualInOther?_append_symm_of_withUniqueDual_of_inr l l2 l3 i k h').mp
         (hk'' h'').symm).symm
     | Sum.inr k =>
@@ -771,7 +800,7 @@ lemma mem_withUniqueDualInOther_symm' (i : Fin l.length)
     | Sum.inl k =>
       simp only [AreDualInOther.of_append_inl]
       have hk'' := h.2.2 (appendEquiv (Sum.inr k))
-      simp at hk''
+      simp only [AreDualInOther.of_append_inr] at hk''
       exact fun h'' => ((getDualInOther?_append_symm_of_withUniqueDual_of_inr l l2 l3 i k h').mp
         (hk'' h'').symm).symm
     | Sum.inr k =>
@@ -798,7 +827,8 @@ lemma mem_withUniqueDualInOther_symm (i : Fin l.length) :
 def getDualEquiv : l.withUniqueDual ≃ l.withUniqueDual where
   toFun x := ⟨(l.getDual? x).get (l.mem_withUniqueDual_isSome x.1 x.2), by
     simp only [Finset.coe_mem, getDual?_get_of_mem_withUnique_mem]⟩
-  invFun x := ⟨(l.getDual? x).get (l.mem_withUniqueDual_isSome x.1 x.2), by simp⟩
+  invFun x := ⟨(l.getDual? x).get (l.mem_withUniqueDual_isSome x.1 x.2), by
+    simp only [Finset.coe_mem, getDual?_get_of_mem_withUnique_mem]⟩
   left_inv x := SetCoe.ext (by
     simp only [Finset.coe_mem, getDual?_getDual?_get_of_withUniqueDual, Option.get_some])
   right_inv x := SetCoe.ext (by
@@ -819,11 +849,19 @@ lemma getDualEquiv_involutive : Function.Involutive l.getDualEquiv := by
   obtained by taking the dual index. -/
 def getDualInOtherEquiv : l.withUniqueDualInOther l2 ≃ l2.withUniqueDualInOther l where
   toFun x := ⟨(l.getDualInOther? l2 x).get (l.mem_withUniqueDualInOther_isSome l2 x.1 x.2),
-    by simp⟩
+    by simp only [append_inl_mem_withUniqueDual_iff, mem_withInDualOther_iff_isSome, Finset.coe_mem,
+      getDualInOther?_getDualInOther?_get_of_withUniqueDualInOther, Option.isSome_some,
+      not_true_eq_false, and_false, getDualInOther?_get_of_mem_withUniqueInOther_mem,
+      mem_withUniqueDualInOther_of_inl_withDualInOther]⟩
   invFun x := ⟨(l2.getDualInOther? l x).get (l2.mem_withUniqueDualInOther_isSome l x.1 x.2),
-    by simp⟩
+    by simp only [append_inl_mem_withUniqueDual_iff, mem_withInDualOther_iff_isSome, Finset.coe_mem,
-  left_inv x := SetCoe.ext (by simp)
+      getDualInOther?_getDualInOther?_get_of_withUniqueDualInOther, Option.isSome_some,
-  right_inv x := SetCoe.ext (by simp)
+      not_true_eq_false, and_false, getDualInOther?_get_of_mem_withUniqueInOther_mem,
+      mem_withUniqueDualInOther_of_inl_withDualInOther]⟩
+  left_inv x := SetCoe.ext (by simp only [Finset.coe_mem,
+    getDualInOther?_getDualInOther?_get_of_withUniqueDualInOther, Option.get_some])
+  right_inv x := SetCoe.ext (by simp only [Finset.coe_mem,
+    getDualInOther?_getDualInOther?_get_of_withUniqueDualInOther, Option.get_some])
 
 @[simp]
 lemma getDualInOtherEquiv_self_refl : l.getDualInOtherEquiv l = Equiv.refl _ := by