diff --git a/HepLean/SpaceTime/LorentzTensor/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Basic.lean index 7950fa1..f3c91b3 100644 --- a/HepLean/SpaceTime/LorentzTensor/Basic.lean +++ b/HepLean/SpaceTime/LorentzTensor/Basic.lean @@ -32,7 +32,8 @@ open TensorProduct variable {R : Type} [CommSemiring R] -/-- The index color data associated with a tensor structure. -/ +/-- The index color data associated with a tensor structure. + This corresponds to a type with an involution. -/ structure TensorColor where /-- The allowed colors of indices. For example for a real Lorentz tensor these are `{up, down}`. -/ diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean index 35b9810..7641b43 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean @@ -5,6 +5,7 @@ Authors: Joseph Tooby-Smith -/ import Mathlib.Data.Set.Finite import Mathlib.Data.Finset.Sort +import Mathlib.Logic.Equiv.Fin /-! # Index notation for a type @@ -236,8 +237,6 @@ instance : Fintype l.toPosSet where def toPosFinset (l : IndexList X) : Finset (Fin l.numIndices × Index X) := l.toPosSet.toFinset -instance : HAppend (IndexList X) (IndexList X) (IndexList X) := - @instHAppendOfAppend (List (Index X)) List.instAppend /-- The construction of a list of indices from a map from `Fin n` to `Index X`. -/ @@ -249,233 +248,47 @@ lemma fromFinMap_numIndices {n : ℕ} (f : Fin n → Index X) : (fromFinMap f).numIndices = n := by simp [fromFinMap, numIndices] -/-! - -## Contracted and non-contracting indices - --/ - -/-- The proposition on a element (or really index of element) of a index list - `s` which is ture iff does not share an id with any other element. - This tells us that it should not be contracted with any other element. -/ -def NoContr (i : Fin l.length) : Prop := - ∀ j, i ≠ j → l.idMap i ≠ l.idMap j - -instance (i : Fin l.length) : Decidable (l.NoContr i) := - Fintype.decidableForallFintype - -/-- The finset of indices of an index list corresponding to elements which do not contract. -/ -def noContrFinset : Finset (Fin l.length) := - Finset.univ.filter l.NoContr - -/-- An eqiuvalence between the subtype of indices of a index list `l` which do not contract and - `Fin l.noContrFinset.card`. -/ -def noContrSubtypeEquiv : {i : Fin l.length // l.NoContr i} ≃ Fin l.noContrFinset.card := - (Equiv.subtypeEquivRight (fun x => by simp [noContrFinset])).trans - (Finset.orderIsoOfFin l.noContrFinset rfl).toEquiv.symm - -@[simp] -lemma idMap_noContrSubtypeEquiv_neq (i j : Fin l.noContrFinset.card) (h : i ≠ j) : - l.idMap (l.noContrSubtypeEquiv.symm i).1 ≠ l.idMap (l.noContrSubtypeEquiv.symm j).1 := by - have hi := ((l.noContrSubtypeEquiv).symm i).2 - simp [NoContr] at hi - have hj := hi ((l.noContrSubtypeEquiv).symm j) - apply hj - rw [@SetCoe.ext_iff] - erw [Equiv.apply_eq_iff_eq] - exact h - -/-- The subtype of indices `l` which do contract. -/ -def contrSubtype : Type := {i : Fin l.length // ¬ l.NoContr i} - -instance : Fintype l.contrSubtype := - Subtype.fintype fun x => ¬ l.NoContr x - -instance : DecidableEq l.contrSubtype := - Subtype.instDecidableEq /-! -## Getting the index which contracts with a given index +## Appending index lists. -/ +instance : HAppend (IndexList X) (IndexList X) (IndexList X) := + @instHAppendOfAppend (List (Index X)) List.instAppend -/-- 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 j : Fin l.length) : Prop := - i ≠ j ∧ l.idMap i = l.idMap j - -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.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.1) = some (l.getDualFin i) := by - simp [getDualFin] - -lemma getDualFin_not_NoContr (i : l.contrSubtype) : ¬ l.NoContr (l.getDualFin i) := by - have h := l.some_getDualFin_eq_find i - rw [Fin.find_eq_some_iff] at h - simp [NoContr] - exact ⟨i.1, And.intro (fun a => h.1.1 a.symm) h.1.2.symm⟩ - -/-- The dual index of an element of `𝓒.contrSubtype s`, that is the index - contracting with it. -/ -def getDual (i : l.contrSubtype) : l.contrSubtype := - ⟨l.getDualFin i, l.getDualFin_not_NoContr i⟩ - -lemma getDual_id (i : l.contrSubtype) : l.idMap i.1 = l.idMap (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.2 - -lemma getDual_neq_self (i : l.contrSubtype) : i ≠ l.getDual i := by - have h1 := l.some_getDualFin_eq_find i - 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 - --/ - -/-- The proposition on a `IndexList` for it to have no contracting - indices. -/ -def HasNoContr : Prop := ∀ i, l.NoContr i - -lemma contrSubtype_is_empty_of_hasNoContr (h : l.HasNoContr) : IsEmpty l.contrSubtype := by - rw [_root_.isEmpty_iff] - intro a - exact h a.1 a.1 (fun _ => a.2 (h a.1)) rfl - -lemma hasNoContr_id_inj (h : l.HasNoContr) : Function.Injective l.idMap := fun i j => by - simpa using (h i j).mt - -lemma hasNoContr_color_eq_of_id_eq (h : l.HasNoContr) (i j : Fin l.length) : - l.idMap i = l.idMap j → l.colorMap i = l.colorMap j := by - intro h1 - apply l.hasNoContr_id_inj h at h1 - rw [h1] +def appendEquiv {l l2 : IndexList X} : Fin l.length ⊕ Fin l2.length ≃ Fin (l ++ l2).length := + finSumFinEquiv.trans (Fin.castOrderIso (List.length_append _ _).symm).toEquiv @[simp] -lemma hasNoContr_noContrFinset_card (h : l.HasNoContr) : - l.noContrFinset.card = List.length l := by - simp only [noContrFinset] - rw [Finset.filter_true_of_mem] - simp only [Finset.card_univ, Fintype.card_fin] - intro x _ - exact h x - -/-! - -## The contracted index list - --/ - -/-- The index list of those indices of `l` which do not contract. -/ -def contrIndexList : IndexList X := - IndexList.fromFinMap (fun i => l.get (l.noContrSubtypeEquiv.symm i)) +lemma idMap_append_inl {l l2 : IndexList X} (i : Fin l.length) : + (l ++ l2).idMap (appendEquiv (Sum.inl i)) = l.idMap i := by + simp [appendEquiv, idMap] + rw [List.getElem_append_left] @[simp] -lemma contrIndexList_numIndices : l.contrIndexList.numIndices = l.noContrFinset.card := by - simp [contrIndexList] +lemma idMap_append_inr {l l2 : IndexList X} (i : Fin l2.length) : + (l ++ l2).idMap (appendEquiv (Sum.inr i)) = l2.idMap i := by + simp [appendEquiv, idMap] + rw [List.getElem_append_right] + simp + omega + omega @[simp] -lemma contrIndexList_idMap_apply (i : Fin l.contrIndexList.numIndices) : - l.contrIndexList.idMap i = - l.idMap (l.noContrSubtypeEquiv.symm (Fin.cast (by simp) i)).1 := by - simp [contrIndexList, IndexList.fromFinMap, IndexList.idMap] - rfl +lemma colorMap_append_inl {l l2 : IndexList X} (i : Fin l.length) : + (l ++ l2).colorMap (appendEquiv (Sum.inl i)) = l.colorMap i := by + simp [appendEquiv, colorMap] + rw [List.getElem_append_left] -lemma contrIndexList_hasNoContr : HasNoContr l.contrIndexList := by - intro i - simp [NoContr] - intro j h - refine l.idMap_noContrSubtypeEquiv_neq _ _ ?_ - rw [@Fin.ne_iff_vne] - simp only [Fin.coe_cast, ne_eq] - exact Fin.val_ne_of_ne h - -/-- Contracting indices on a index list that has no contractions does nothing. -/ @[simp] -lemma contrIndexList_of_hasNoContr (h : HasNoContr l) : l.contrIndexList = l := by - simp only [contrIndexList, List.get_eq_getElem] - have hn : (@Finset.univ (Fin (List.length l)) (Fin.fintype (List.length l))).card = - (Finset.filter l.NoContr Finset.univ).card := by - rw [Finset.filter_true_of_mem (fun a _ => h a)] - have hx : (Finset.filter l.NoContr Finset.univ).card = (List.length l) := by - rw [← hn] - exact Finset.card_fin (List.length l) - apply List.ext_get - simpa [fromFinMap, noContrFinset] using hx - intro n h1 h2 - simp only [noContrFinset, noContrSubtypeEquiv, OrderIso.toEquiv_symm, Equiv.symm_trans_apply, - RelIso.coe_fn_toEquiv, Equiv.subtypeEquivRight_symm_apply_coe, fromFinMap, List.get_eq_getElem, - OrderIso.symm_symm, Finset.coe_orderIsoOfFin_apply, List.getElem_map, Fin.getElem_list, - Fin.cast_mk] - simp only [Finset.filter_true_of_mem (fun a _ => h a)] - congr - rw [(Finset.orderEmbOfFin_unique' _ - (fun x => Finset.mem_univ ((Fin.castOrderIso hx).toOrderEmbedding x))).symm] - rfl - -/-- Applying contrIndexlist is equivalent to applying it once. -/ -@[simp] -lemma contrIndexList_contrIndexList : l.contrIndexList.contrIndexList = l.contrIndexList := - l.contrIndexList.contrIndexList_of_hasNoContr (l.contrIndexList_hasNoContr) - -/-! - -## Pairs of contracting indices - --/ - -/-- The set of contracting ordered pairs of indices. -/ -def contrPairSet : Set (l.contrSubtype × l.contrSubtype) := - {p | p.1.1 < p.2.1 ∧ l.idMap p.1.1 = l.idMap p.2.1} - -instance : DecidablePred fun x => x ∈ l.contrPairSet := fun _ => - And.decidable - -instance : Fintype l.contrPairSet := setFintype _ - -lemma contrPairSet_isEmpty_of_hasNoContr (h : l.HasNoContr) : - IsEmpty l.contrPairSet := by - simp only [contrPairSet, Subtype.coe_lt_coe, Set.coe_setOf, isEmpty_subtype, not_and, Prod.forall] - refine fun a b h' => h a.1 b.1 (Fin.ne_of_lt h') - -lemma getDual_lt_self_mem_contrPairSet {i : l.contrSubtype} - (h : (l.getDual i).1 < i.1) : (l.getDual i, i) ∈ l.contrPairSet := - And.intro h (l.getDual_id i).symm - -lemma getDual_not_lt_self_mem_contrPairSet {i : l.contrSubtype} - (h : ¬ (l.getDual i).1 < i.1) : (i, l.getDual i) ∈ l.contrPairSet := by - apply And.intro - have h1 := l.getDual_neq_self i - simp only [Subtype.coe_lt_coe, gt_iff_lt] - simp at h - exact lt_of_le_of_ne h h1 - 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 +lemma colorMap_append_inr {l l2 : IndexList X} (i : Fin l2.length) : + (l ++ l2).colorMap (appendEquiv (Sum.inr i)) = l2.colorMap i := by + simp [appendEquiv, colorMap] + rw [List.getElem_append_right] + simp + omega + omega end IndexList diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/DualIndex.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/DualIndex.lean new file mode 100644 index 0000000..2bc0efd --- /dev/null +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/DualIndex.lean @@ -0,0 +1,840 @@ +/- +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.Basic +/-! + +# Dual indices + +-/ + +namespace IndexNotation + + +namespace IndexList + +variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X] +variable (l l2 : IndexList X) + +/-! + +## Are dual indices + +-/ + +/-- Two indices are dual if they are not equivalent, but have the same id. -/ +def AreDualInSelf (i j : Fin l.length) : Prop := + i ≠ j ∧ l.idMap i = l.idMap j + +instance (i j : Fin l.length) : Decidable (l.AreDualInSelf i j) := + instDecidableAnd + +def AreDualInOther {l : IndexList X} {l2 : IndexList X} (i : Fin l.length) (j : Fin l2.length) : + Prop := l.idMap i = l2.idMap j + +instance {l : IndexList X} {l2 : IndexList X} (i : Fin l.length) (j : Fin l2.length) : + Decidable (AreDualInOther i j) := (l.idMap i).decEq (l2.idMap j) + + +namespace AreDualInSelf + +variable {l l2 : IndexList X} {i j : Fin l.length} + +@[symm] +lemma symm (h : l.AreDualInSelf i j) : l.AreDualInSelf j i := by + simp only [AreDualInSelf] at h ⊢ + exact ⟨h.1.symm, h.2.symm⟩ + +@[simp] +lemma self_false (i : Fin l.length) : ¬ l.AreDualInSelf i i := by + simp [AreDualInSelf] + +@[simp] +lemma append_inl_inl : (l ++ l2).AreDualInSelf (appendEquiv (Sum.inl i)) (appendEquiv (Sum.inl j)) + ↔ l.AreDualInSelf i j := by + simp [AreDualInSelf] + +@[simp] +lemma append_inr_inr (l l2 : IndexList X) (i j : Fin l2.length) : + (l ++ l2).AreDualInSelf (appendEquiv (Sum.inr i)) (appendEquiv (Sum.inr j)) + ↔ l2.AreDualInSelf i j := by + simp [AreDualInSelf] + +@[simp] +lemma append_inl_inr (l l2 : IndexList X) (i : Fin l.length) (j : Fin l2.length) : + (l ++ l2).AreDualInSelf (appendEquiv (Sum.inl i)) (appendEquiv (Sum.inr j)) = + AreDualInOther i j := by + simp [AreDualInSelf, AreDualInOther] + +@[simp] +lemma append_inr_inl (l l2 : IndexList X) (i : Fin l2.length) (j : Fin l.length) : + (l ++ l2).AreDualInSelf (appendEquiv (Sum.inr i)) (appendEquiv (Sum.inl j)) = + AreDualInOther i j := by + simp [AreDualInSelf, AreDualInOther] + +end AreDualInSelf + +namespace AreDualInOther + +variable {l l2 : IndexList X} {i : Fin l.length} {j : Fin l2.length} + +@[symm] +lemma symm (h : AreDualInOther i j) : AreDualInOther j i := by + rw [AreDualInOther] at h ⊢ + exact h.symm + +end AreDualInOther + +/-! + +## Has a dual + +-/ + +def HasDualInSelf (i : Fin l.length) : Prop := ∃ j, AreDualInSelf l i j + +instance (i : Fin l.length) : Decidable (l.HasDualInSelf i) := Fintype.decidableExistsFintype + +def HasDualInOther (i : Fin l.length) : Prop := + ∃ (j : Fin l2.length), AreDualInOther i j + +instance (i : Fin l.length) : Decidable (l.HasDualInOther l2 i) := Fintype.decidableExistsFintype + +namespace HasDualInSelf + +variable {l l2 : IndexList X} {i : Fin l.length} + +@[simp] +lemma append_inl : (l ++ l2).HasDualInSelf (appendEquiv (Sum.inl i)) ↔ + (l.HasDualInSelf i ∨ l.HasDualInOther l2 i) := by + apply Iff.intro + · intro h + obtain ⟨j, hj⟩ := h + obtain ⟨k, hk⟩ := appendEquiv.surjective j + subst hk + match k with + | Sum.inl k => + apply Or.inl + simp only [AreDualInSelf, ne_eq, EmbeddingLike.apply_eq_iff_eq, Sum.inl.injEq, + idMap_append_inl] at hj + exact ⟨k, hj⟩ + | Sum.inr k => + apply Or.inr + simp only [AreDualInSelf, ne_eq, EmbeddingLike.apply_eq_iff_eq, not_false_eq_true, + idMap_append_inl, idMap_append_inr, true_and] at hj + exact ⟨k, hj⟩ + · intro h + cases h + · rename_i h + obtain ⟨j, hj⟩ := h + use appendEquiv (Sum.inl j) + simp only [AreDualInSelf, ne_eq, EmbeddingLike.apply_eq_iff_eq, Sum.inl.injEq, + idMap_append_inl] + exact hj + · rename_i h + obtain ⟨j, hj⟩ := h + use appendEquiv (Sum.inr j) + simp only [AreDualInSelf, ne_eq, EmbeddingLike.apply_eq_iff_eq, not_false_eq_true, + idMap_append_inl, idMap_append_inr, true_and] + exact hj + +@[simp] +lemma append_inr {i : Fin l2.length} : (l ++ l2).HasDualInSelf (appendEquiv (Sum.inr i)) ↔ + (l2.HasDualInSelf i ∨ l2.HasDualInOther l i) := by + apply Iff.intro + · intro h + obtain ⟨j, hj⟩ := h + obtain ⟨k, hk⟩ := appendEquiv.surjective j + subst hk + match k with + | Sum.inl k => + simp [AreDualInSelf, ne_eq, EmbeddingLike.apply_eq_iff_eq, Sum.inl.injEq, + idMap_append_inl] at hj + exact Or.inr ⟨k, hj⟩ + | Sum.inr k => + simp only [AreDualInSelf, ne_eq, EmbeddingLike.apply_eq_iff_eq, Sum.inr.injEq, + idMap_append_inr] at hj + exact Or.inl ⟨k, hj⟩ + · intro h + cases h + · rename_i h + obtain ⟨j, hj⟩ := h + use appendEquiv (Sum.inr j) + simp [AreDualInSelf] + exact hj + · rename_i h + obtain ⟨j, hj⟩ := h + use appendEquiv (Sum.inl j) + simp [AreDualInSelf] + exact hj + +def getFirst (h : l.HasDualInSelf i) : Fin l.length := + (Fin.find (l.AreDualInSelf i)).get (by simpa [Fin.isSome_find_iff] using h) + +lemma some_getFirst_eq_find (h : l.HasDualInSelf i) : + Fin.find (l.AreDualInSelf i) = some h.getFirst := by + simp [getFirst] + +lemma getFirst_hasDualInSelf (h : l.HasDualInSelf i) : + l.HasDualInSelf h.getFirst := by + have h := h.some_getFirst_eq_find + rw [Fin.find_eq_some_iff] at h + simp [HasDualInSelf] + exact ⟨i, And.intro (fun a => h.1.1 a.symm) h.1.2.symm⟩ + +lemma areDualInSelf_getFirst (h : l.HasDualInSelf i) : l.AreDualInSelf i h.getFirst := by + have h := h.some_getFirst_eq_find + rw [Fin.find_eq_some_iff] at h + simp [AreDualInSelf] + exact h.1 + +@[simp] +lemma getFirst_id (h : l.HasDualInSelf i) : l.idMap h.getFirst = l.idMap i := + h.areDualInSelf_getFirst.2.symm + +end HasDualInSelf + +namespace HasDualInOther + +variable {l l2 : IndexList X} {i : Fin l.length} + +def getFirst {l : IndexList X} {l2 : IndexList X} (i : Fin l.length) (h : l.HasDualInOther l2 i) : + Fin l2.length := + (Fin.find (l.AreDualInOther i)).get (by simpa [Fin.isSome_find_iff] using h) + +lemma some_getFirst_eq_find (h : l.HasDualInOther l2 i) : + Fin.find (l.AreDualInOther i) = some h.getFirst := by + simp [getFirst] + +lemma getFirst_hasDualInOther (h : l.HasDualInOther l2 i) : + l2.HasDualInOther l h.getFirst := by + have h := h.some_getFirst_eq_find + rw [Fin.find_eq_some_iff] at h + simp only [HasDualInOther] + exact ⟨i, h.1.symm⟩ + +lemma areDualInOther_getFirst (h : l.HasDualInOther l2 i) : + l.AreDualInOther i h.getFirst := by + have h := h.some_getFirst_eq_find + rw [Fin.find_eq_some_iff] at h + simp [AreDualInOther] + exact h.1 + +@[simp] +lemma getFirst_id (h : l.HasDualInOther l2 i) : l2.idMap h.getFirst = l.idMap i := + h.areDualInOther_getFirst.symm + +end HasDualInOther + +namespace HasDualInSelf + + +@[simp] +lemma getFirst_append_inl_of_hasDualInSelf (h : (l ++ l2).HasDualInSelf (appendEquiv (Sum.inl i))) + (hi : l.HasDualInSelf i) : h.getFirst = appendEquiv (Sum.inl hi.getFirst) := by + have h1 : Fin.find ((l ++ l2).AreDualInSelf (appendEquiv (Sum.inl i))) = + some (appendEquiv (Sum.inl hi.getFirst)) := by + rw [Fin.find_eq_some_iff] + simp + apply And.intro hi.areDualInSelf_getFirst + intro j hj + obtain ⟨k, hk⟩ := appendEquiv.surjective j + subst hk + match k with + | Sum.inl k => + simp [appendEquiv] + rw [Fin.le_def] + simp + have h2 := hi.some_getFirst_eq_find + rw [Fin.find_eq_some_iff] at h2 + simp only [AreDualInSelf.append_inl_inl] at hj + exact h2.2 k hj + | Sum.inr k => + simp [appendEquiv] + rw [Fin.le_def] + simp + omega + rw [h.some_getFirst_eq_find] at h1 + simpa only [Option.some.injEq] using h1 + +@[simp] +lemma getFirst_append_inl_of_not_hasDualInSelf + (h : (l ++ l2).HasDualInSelf (appendEquiv (Sum.inl i))) + (hi : ¬ l.HasDualInSelf i) (hn : l.HasDualInOther l2 i) : + h.getFirst = appendEquiv (Sum.inr hn.getFirst) := by + have h1 : Fin.find ((l ++ l2).AreDualInSelf (appendEquiv (Sum.inl i))) = + some (appendEquiv (Sum.inr hn.getFirst)) := by + rw [Fin.find_eq_some_iff] + simp + apply And.intro hn.areDualInOther_getFirst + intro j hj + obtain ⟨k, hk⟩ := appendEquiv.surjective j + subst hk + match k with + | Sum.inl k => + simp at hj + exact False.elim (hi ⟨k, hj⟩) + | Sum.inr k => + simp [appendEquiv] + rw [Fin.le_def] + simp + have h2 := hn.some_getFirst_eq_find + rw [Fin.find_eq_some_iff] at h2 + simp only [AreDualInSelf.append_inl_inr] at hj + exact h2.2 k hj + rw [h.some_getFirst_eq_find] at h1 + simpa only [Option.some.injEq] using h1 + +@[simp] +lemma getFirst_append_inr_of_hasDualInOther {i : Fin l2.length} + (h : (l ++ l2).HasDualInSelf (appendEquiv (Sum.inr i))) (hi : l2.HasDualInOther l i) : + h.getFirst = appendEquiv (Sum.inl hi.getFirst) := by + have h1 : Fin.find ((l ++ l2).AreDualInSelf (appendEquiv (Sum.inr i))) = + some (appendEquiv (Sum.inl hi.getFirst)) := by + rw [Fin.find_eq_some_iff] + simp + apply And.intro hi.areDualInOther_getFirst + intro j hj + obtain ⟨k, hk⟩ := appendEquiv.surjective j + subst hk + match k with + | Sum.inl k => + simp [appendEquiv] + rw [Fin.le_def] + simp + have h2 := hi.some_getFirst_eq_find + rw [Fin.find_eq_some_iff] at h2 + simp only [AreDualInSelf.append_inr_inl] at hj + exact h2.2 k hj + | Sum.inr k => + simp [appendEquiv] + rw [Fin.le_def] + simp + omega + rw [h.some_getFirst_eq_find] at h1 + simpa only [Option.some.injEq] using h1 + +@[simp] +lemma getFirst_append_inr_of_not_hasDualInOther {i : Fin l2.length} + (h : (l ++ l2).HasDualInSelf (appendEquiv (Sum.inr i))) (hi : ¬ l2.HasDualInOther l i) + (hn : l2.HasDualInSelf i) : h.getFirst = appendEquiv (Sum.inr hn.getFirst) := by + have h1 : Fin.find ((l ++ l2).AreDualInSelf (appendEquiv (Sum.inr i))) = + some (appendEquiv (Sum.inr hn.getFirst)) := by + rw [Fin.find_eq_some_iff] + simp + apply And.intro hn.areDualInSelf_getFirst + intro j hj + obtain ⟨k, hk⟩ := appendEquiv.surjective j + subst hk + match k with + | Sum.inl k => + simp at hj + exact False.elim (hi ⟨k, hj⟩) + | Sum.inr k => + simp [appendEquiv] + rw [Fin.le_def] + simp + have h2 := hn.some_getFirst_eq_find + rw [Fin.find_eq_some_iff] at h2 + simp only [AreDualInSelf.append_inr_inr] at hj + exact h2.2 k hj + rw [h.some_getFirst_eq_find] at h1 + simpa only [Option.some.injEq] using h1 + +end HasDualInSelf +/-! + +## Has single dual + +-/ + +def HasSingDualInSelf (i : Fin l.length) : Prop := + l.HasDualInSelf i ∧ ∀ (h : l.HasDualInSelf i) j, l.AreDualInSelf i j → j = h.getFirst + +instance (i : Fin l.length) : Decidable (l.HasSingDualInSelf i) := instDecidableAnd + +def HasSingDualInOther (l l2 : IndexList X) (i : Fin l.length) : Prop := + l.HasDualInOther l2 i ∧ ∀ (h : l.HasDualInOther l2 i) j, l.AreDualInOther i j → j = h.getFirst + +instance (i : Fin l.length) : Decidable (l.HasSingDualInOther l2 i) := instDecidableAnd + +namespace HasSingDualInSelf + +variable {l l2 : IndexList X} {i : Fin l.length} + +def toHasDualInSelf (h : l.HasSingDualInSelf i) : l.HasDualInSelf i := h.1 + +def get (h : l.HasSingDualInSelf i) : Fin l.length := h.1.getFirst + +lemma eq_get_iff (h : l.HasSingDualInSelf i) (j : Fin l.length) : + j = h.get ↔ l.AreDualInSelf i j := by + apply Iff.intro + · intro h1 + subst h1 + exact h.1.areDualInSelf_getFirst + · intro h1 + exact h.2 h.1 j h1 + +@[simp] +lemma get_id (h : l.HasSingDualInSelf i) : l.idMap h.get = l.idMap i := h.1.getFirst_id + +lemma get_hasSingDualInSelf (h : l.HasSingDualInSelf i) : l.HasSingDualInSelf h.get := by + refine And.intro h.1.getFirst_hasDualInSelf (fun hj j hji => ?_) + have h1 : i = j := by + by_contra hn + have h' : l.AreDualInSelf i j := by + simp [AreDualInSelf, hn] + simp_all [AreDualInSelf, get] + rw [← h.eq_get_iff] at h' + subst h' + simp at hji + subst h1 + have h2 : i = hj.getFirst := by + by_contra hn + have h' : l.AreDualInSelf i hj.getFirst := by + simp [AreDualInSelf, hn] + rw [← h.eq_get_iff] at h' + have hx := hj.areDualInSelf_getFirst + simp [AreDualInSelf, h'] at hx + rw [← h2] + +@[simp] +lemma get_get (h : l.HasSingDualInSelf i) : h.get_hasSingDualInSelf.get = i := by + symm + rw [h.get_hasSingDualInSelf.eq_get_iff] + exact h.1.areDualInSelf_getFirst.symm + +/-! + +### Relations regarding append for HasSingDualInSelf + +-/ + +lemma get_append_inl (h : (l ++ l2).HasSingDualInSelf (appendEquiv (Sum.inl i))) + (hi : l.HasDualInSelf i) : h.get = appendEquiv (Sum.inl hi.getFirst) := by + symm + rw [h.eq_get_iff] + simp only [AreDualInSelf.append_inl_inl] + exact HasDualInSelf.areDualInSelf_getFirst hi + +lemma get_append_inl_other (h : (l ++ l2).HasSingDualInSelf (appendEquiv (Sum.inl i))) + (hi : l.HasDualInOther l2 i) : h.get = appendEquiv (Sum.inr hi.getFirst) := by + symm + rw [h.eq_get_iff] + simp only [AreDualInSelf.append_inl_inr] + exact HasDualInOther.areDualInOther_getFirst hi + +lemma get_append_inr {i : Fin l2.length} + (h : (l ++ l2).HasSingDualInSelf (appendEquiv (Sum.inr i))) (hi : l2.HasDualInSelf i) : + h.get = appendEquiv (Sum.inr hi.getFirst) := by + symm + rw [h.eq_get_iff] + simp only [AreDualInSelf.append_inr_inr] + exact HasDualInSelf.areDualInSelf_getFirst hi + +lemma get_append_inr_other {i : Fin l2.length} + (h : (l ++ l2).HasSingDualInSelf (appendEquiv (Sum.inr i))) (hi : l2.HasDualInOther l i) : + h.get = appendEquiv (Sum.inl hi.getFirst) := by + symm + rw [h.eq_get_iff] + simp only [AreDualInSelf.append_inr_inl] + exact HasDualInOther.areDualInOther_getFirst hi + +lemma hasDualInSelf_iff_of_append_inl (h : (l ++ l2).HasSingDualInSelf (appendEquiv (Sum.inl i))) : + l.HasDualInSelf i ↔ l.HasSingDualInSelf i := by + refine Iff.intro (fun hi => ?_) (fun hi => hi.1) + apply And.intro hi + intro _ j hji + simpa [get_append_inl h hi] using + (h.eq_get_iff (appendEquiv (Sum.inl j))).mpr (by simpa using hji) + +lemma hasDualInSelf_iff_of_append_inr {i : Fin l2.length} + (h : (l ++ l2).HasSingDualInSelf (appendEquiv (Sum.inr i))) : + l2.HasDualInSelf i ↔ l2.HasSingDualInSelf i := by + refine Iff.intro (fun hi => ?_) (fun hi => hi.1) + apply And.intro hi + intro _ j hji + simpa [get_append_inr h hi] using + (h.eq_get_iff (appendEquiv (Sum.inr j))).mpr (by simpa using hji) + +lemma hasDualInOther_iff_of_append_inl + (h : (l ++ l2).HasSingDualInSelf (appendEquiv (Sum.inl i))) : + l.HasDualInOther l2 i ↔ l.HasSingDualInOther l2 i := by + refine Iff.intro (fun hi => ?_) (fun hi => hi.1) + apply And.intro hi + intro _ j hji + simpa [get_append_inl_other h hi] using + (h.eq_get_iff (appendEquiv (Sum.inr j))).mpr (by simpa using hji) + +lemma hasDualInOther_iff_of_append_inr {i : Fin l2.length} + (h : (l ++ l2).HasSingDualInSelf (appendEquiv (Sum.inr i))) : + l2.HasDualInOther l i ↔ l2.HasSingDualInOther l i := by + refine Iff.intro (fun hi => ?_) (fun hi => hi.1) + apply And.intro hi + intro _ j hji + simpa [get_append_inr_other h hi] using + (h.eq_get_iff (appendEquiv (Sum.inl j))).mpr (by simpa using hji) + +lemma hasSingInSelf_iff_not_hasSingDualInOther_of_append_inl + (h : (l ++ l2).HasSingDualInSelf (appendEquiv (Sum.inl i))) : + l.HasSingDualInSelf i ↔ ¬ l.HasSingDualInOther l2 i := by + rw [← hasDualInOther_iff_of_append_inl h, ← hasDualInSelf_iff_of_append_inl h] + refine Iff.intro (fun hi => ?_) (fun hi => ?_) + · simp only [HasDualInOther, not_exists] + intro j + by_contra hn + have h' := h.eq_get_iff (appendEquiv (Sum.inr j)) + rw [AreDualInSelf.append_inl_inr] at h' + simpa [get_append_inl h hi] using h'.mpr hn + · obtain ⟨j, hj⟩ := h.1 + obtain ⟨k, hk⟩ := appendEquiv.surjective j + subst hk + match k with + | Sum.inl k => + simp only [AreDualInSelf.append_inl_inl] at hj + exact ⟨k, hj⟩ + | Sum.inr k => + simp only [AreDualInSelf.append_inl_inr] at hj + simp only [HasDualInOther, not_exists] at hi + exact False.elim (hi k hj) + +lemma hasSingInSelf_iff_not_hasSingDualInOther_of_append_inr {i : Fin l2.length} + (h : (l ++ l2).HasSingDualInSelf (appendEquiv (Sum.inr i))) : + l2.HasSingDualInSelf i ↔ ¬ l2.HasSingDualInOther l i := by + rw [← hasDualInOther_iff_of_append_inr h, ← hasDualInSelf_iff_of_append_inr h] + refine Iff.intro (fun hi => ?_) (fun hi => ?_) + · simp only [HasDualInOther, not_exists] + intro j + by_contra hn + have h' := h.eq_get_iff (appendEquiv (Sum.inl j)) + rw [AreDualInSelf.append_inr_inl] at h' + simpa [get_append_inr h hi] using h'.mpr hn + · obtain ⟨j, hj⟩ := h.1 + obtain ⟨k, hk⟩ := appendEquiv.surjective j + subst hk + match k with + | Sum.inl k => + simp only [AreDualInSelf.append_inr_inl] at hj + simp only [HasDualInOther, not_exists] at hi + exact False.elim (hi k hj) + | Sum.inr k => + simp only [AreDualInSelf.append_inr_inr] at hj + exact ⟨k, hj⟩ + +lemma append_inl_of_hasSingDualInSelf (h1 : l.HasSingDualInSelf i) (h2 : ¬ l.HasDualInOther l2 i) : + (l ++ l2).HasSingDualInSelf (appendEquiv (Sum.inl i)) := by + simp only [HasSingDualInSelf, HasDualInSelf.append_inl] + apply And.intro (Or.inl h1.toHasDualInSelf) + intro h j hji + obtain ⟨k, hk⟩ := appendEquiv.surjective j + subst hk + rw [HasDualInSelf.getFirst_append_inl_of_hasDualInSelf l l2 (HasDualInSelf.append_inl.mpr h) + h1.toHasDualInSelf] + match k with + | Sum.inl k => + simp only [AreDualInSelf.append_inl_inl] at hji + simp only [EmbeddingLike.apply_eq_iff_eq, Sum.inl.injEq] + exact h1.2 h1.1 k hji + | Sum.inr k => + simp only [AreDualInSelf.append_inl_inr] at hji + exact False.elim (h2 ⟨k, hji⟩) + +lemma append_inr_of_hasSingDualInSelf {i : Fin l2.length} (h1 : l2.HasSingDualInSelf i) + (h2 : ¬ l2.HasDualInOther l i) : (l ++ l2).HasSingDualInSelf (appendEquiv (Sum.inr i)) := by + simp only [HasSingDualInSelf, HasDualInSelf.append_inr] + refine And.intro (Or.inl h1.toHasDualInSelf) ?_ + intro h j hji + obtain ⟨k, hk⟩ := appendEquiv.surjective j + subst hk + rw [HasDualInSelf.getFirst_append_inr_of_not_hasDualInOther l l2 + (HasDualInSelf.append_inr.mpr h) h2 h1.1] + match k with + | Sum.inl k => + simp only [AreDualInSelf.append_inr_inl] at hji + exact False.elim (h2 ⟨k, hji⟩) + | Sum.inr k => + simp only [EmbeddingLike.apply_eq_iff_eq, Sum.inr.injEq] + simp only [AreDualInSelf.append_inr_inr] at hji + exact h1.2 h1.1 k hji + +lemma append_inl_of_not_hasSingDualInSelf (h1 : ¬ l.HasDualInSelf i) (h2 : l.HasSingDualInOther l2 i) : + (l ++ l2).HasSingDualInSelf (appendEquiv (Sum.inl i)) := by + simp only [HasSingDualInSelf, HasDualInSelf.append_inl] + apply And.intro (Or.inr h2.1) + intro h j hji + obtain ⟨k, hk⟩ := appendEquiv.surjective j + subst hk + rw [HasDualInSelf.getFirst_append_inl_of_not_hasDualInSelf l l2 + (HasDualInSelf.append_inl.mpr h) h1 h2.1] + match k with + | Sum.inl k => + simp at hji + exact False.elim (h1 ⟨k, hji⟩) + | Sum.inr k => + simp + simp at hji + exact h2.2 h2.1 k hji + +lemma append_inr_of_not_hasSingDualInSelf {i : Fin l2.length} (h1 : ¬ l2.HasDualInSelf i) + (h2 : l2.HasSingDualInOther l i) : (l ++ l2).HasSingDualInSelf (appendEquiv (Sum.inr i)) := by + simp only [HasSingDualInSelf, HasDualInSelf.append_inr] + refine And.intro (Or.inr h2.1) ?_ + intro h j hji + obtain ⟨k, hk⟩ := appendEquiv.surjective j + subst hk + rw [HasDualInSelf.getFirst_append_inr_of_hasDualInOther l l2 + (HasDualInSelf.append_inr.mpr h) h2.1] + match k with + | Sum.inl k => + simp + simp at hji + exact h2.2 h2.1 k hji + | Sum.inr k => + simp only [AreDualInSelf.append_inr_inr] at hji + exact False.elim (h1 ⟨k, hji⟩) + +@[simp] +lemma append_inl : (l ++ l2).HasSingDualInSelf (appendEquiv (Sum.inl i)) ↔ + (l.HasSingDualInSelf i ∧ ¬ l.HasDualInOther l2 i) ∨ + (¬ l.HasDualInSelf i ∧ l.HasSingDualInOther l2 i) := by + refine Iff.intro (fun h => ?_) (fun h => ?_) + · by_cases hl : l.HasDualInSelf i + · have hl2 := (hasDualInSelf_iff_of_append_inl h).mp hl + simp_all + exact (hasDualInOther_iff_of_append_inl h).mp.mt + ((hasSingInSelf_iff_not_hasSingDualInOther_of_append_inl h).mp hl2) + · have hl2 := (hasDualInSelf_iff_of_append_inl h).mpr.mt hl + simp_all + have h' := (hasSingInSelf_iff_not_hasSingDualInOther_of_append_inl h).mpr.mt + simp at h' + exact h' hl2 + · cases h <;> rename_i h + · exact append_inl_of_hasSingDualInSelf h.1 h.2 + · exact append_inl_of_not_hasSingDualInSelf h.1 h.2 + +@[simp] +lemma append_inr {i : Fin l2.length} : (l ++ l2).HasSingDualInSelf (appendEquiv (Sum.inr i)) ↔ + (l2.HasSingDualInSelf i ∧ ¬ l2.HasDualInOther l i) ∨ + (¬ l2.HasDualInSelf i ∧ l2.HasSingDualInOther l i) := by + refine Iff.intro (fun h => ?_) (fun h => ?_) + · by_cases hl : l2.HasDualInSelf i + · have hl2 := (hasDualInSelf_iff_of_append_inr h).mp hl + simp_all + exact (hasDualInOther_iff_of_append_inr h).mp.mt + ((hasSingInSelf_iff_not_hasSingDualInOther_of_append_inr h).mp hl2) + · have hl2 := (hasDualInSelf_iff_of_append_inr h).mpr.mt hl + simp_all + have h' := (hasSingInSelf_iff_not_hasSingDualInOther_of_append_inr h).mpr.mt + simp at h' + exact h' hl2 + · cases h <;> rename_i h + · exact append_inr_of_hasSingDualInSelf h.1 h.2 + · exact append_inr_of_not_hasSingDualInSelf h.1 h.2 + +lemma append_symm : (l ++ l2).HasSingDualInSelf (appendEquiv (Sum.inl i)) ↔ + (l2 ++ l).HasSingDualInSelf (appendEquiv (Sum.inr i)) := by + simp + +end HasSingDualInSelf + +namespace HasSingDualInOther + +variable {l l2 : IndexList X} {i : Fin l.length} + +def toHasDualInOther (h : l.HasSingDualInOther l2 i) : l.HasDualInOther l2 i := h.1 + +def get (h : l.HasSingDualInOther l2 i) : Fin l2.length := h.1.getFirst + +lemma eq_get_iff (h : l.HasSingDualInOther l2 i) (j : Fin l2.length) : + j = h.get ↔ AreDualInOther i j := by + apply Iff.intro + · intro h1 + subst h1 + exact h.1.areDualInOther_getFirst + · intro h1 + exact h.2 h.1 j h1 + +end HasSingDualInOther + + +/-! + +## Lists with no duals + +-/ + +def HasNoDualsSelf : Prop := ∀ i, ¬ l.HasDualInSelf i + +instance : Decidable (HasNoDualsSelf l) := Nat.decidableForallFin fun i => ¬l.HasDualInSelf i + +namespace HasNoDualsSelf + +variable {l : IndexList X} + +lemma idMap_inje (h : l.HasNoDualsSelf) : Function.Injective l.idMap := by + intro i j + have h1 := h i + simp only [HasDualInSelf, AreDualInSelf, ne_eq, not_exists, not_and] at h1 + simpa using (h1 j).mt + +lemma eq_of_id_eq (h : l.HasNoDualsSelf) {i j : Fin l.length} (h' : l.idMap i = l.idMap j) : + i = j := h.idMap_inje h' + +lemma color_eq_of_id_eq (h : l.HasNoDualsSelf) (i j : Fin l.length) : + l.idMap i = l.idMap j → l.colorMap i = l.colorMap j := by + intro h' + rw [h.eq_of_id_eq h'] + +end HasNoDualsSelf + +section Color + +variable {𝓒 : TensorColor} +variable [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color] +variable (l l2 : IndexList 𝓒.Color) +/-! + +## Has single dual of correct color + +-/ + + +def HasSingColorDualInSelf (i : Fin l.length) : Prop := + l.HasSingDualInSelf i ∧ ∀ (h : l.HasSingDualInSelf i), l.colorMap i = 𝓒.τ (l.colorMap h.get) + +instance (i : Fin l.length) : Decidable (l.HasSingColorDualInSelf i) := instDecidableAnd + +def HasSingColorDualInOther (i : Fin l.length) : Prop := + l.HasSingDualInOther l2 i ∧ ∀ (h : l.HasSingDualInOther l2 i), l.colorMap i = + 𝓒.τ (l2.colorMap h.get) + +instance (i : Fin l.length) : Decidable (l.HasSingColorDualInOther l2 i) := instDecidableAnd + +namespace HasSingColorDualInSelf + +variable {l l2 : IndexList 𝓒.Color} {i : Fin l.length} + +def get (h : l.HasSingColorDualInSelf i) : Fin l.length := h.1.get + +@[simp] +lemma get_color (h : l.HasSingColorDualInSelf i) : l.colorMap h.get = 𝓒.τ (l.colorMap i) := by + rw [h.2 h.1] + exact (𝓒.τ_involutive (l.colorMap h.get)).symm + +@[simp] +lemma get_id (h : l.HasSingColorDualInSelf i) : l.idMap h.get = l.idMap i := h.1.get_id + +lemma get_hasSingColorDualInSelf (h : l.HasSingColorDualInSelf i) : + l.HasSingColorDualInSelf h.get := by + refine And.intro h.1.get_hasSingDualInSelf ?_ + intro _ + simp only [get_color, HasSingDualInSelf.get_get] + +@[simp] +lemma get_get (h : l.HasSingColorDualInSelf i) : h.get_hasSingColorDualInSelf.get = i := by + simp [get] + +lemma areDualInSelf_get (h : l.HasSingColorDualInSelf i) : l.AreDualInSelf i h.get := by + exact h.1.1.areDualInSelf_getFirst + +/-! + +### Append lemmas regarding HasSingColorDualInSelf + +-/ + +@[simp] +lemma append_inl : (l ++ l2).HasSingColorDualInSelf (appendEquiv (Sum.inl i)) ↔ + (l.HasSingColorDualInSelf i ∧ ¬ l.HasDualInOther l2 i) ∨ + (¬ l.HasDualInSelf i ∧ l.HasSingColorDualInOther l2 i) := by + refine Iff.intro (fun h => ?_) (fun h => ?_) + · have h1 := h.1 + have h2 := h.2 h.1 + simp [HasSingColorDualInSelf] at h1 + simp at h2 + cases h1 <;> rename_i h1 + · refine Or.inl (And.intro ⟨h1.1, fun h' => ?_⟩ h1.2) + rw [HasSingDualInSelf.get_append_inl h.1 h1.1.1] at h2 + simpa using h2 + · refine Or.inr (And.intro h1.1 ⟨h1.2, fun h' => ?_⟩) + rw [HasSingDualInSelf.get_append_inl_other h.1 h1.2.1] at h2 + simpa using h2 + · have h1 : (l ++ l2).HasSingDualInSelf (appendEquiv (Sum.inl i)) := by + simp [HasSingColorDualInSelf] + cases h <;> rename_i h + · exact Or.inl ⟨h.1.1, h.2⟩ + · exact Or.inr ⟨h.1, h.2.1⟩ + apply And.intro h1 + intro h' + simp + cases h <;> rename_i h + · simpa [HasSingDualInSelf.get_append_inl h1 h.1.1.1] using h.1.2 h.1.1 + · simpa [HasSingDualInSelf.get_append_inl_other h1 h.2.1.1] using h.2.2 h.2.1 + +@[simp] +lemma append_inr {i : Fin l2.length} : (l ++ l2).HasSingColorDualInSelf (appendEquiv (Sum.inr i)) ↔ + (l2.HasSingColorDualInSelf i ∧ ¬ l2.HasDualInOther l i) ∨ + (¬ l2.HasDualInSelf i ∧ l2.HasSingColorDualInOther l i) := by + refine Iff.intro (fun h => ?_) (fun h => ?_) + · have h1 := h.1 + have h2 := h.2 h.1 + simp [HasSingColorDualInSelf] at h1 + simp at h2 + cases h1 <;> rename_i h1 + · refine Or.inl (And.intro ⟨h1.1, fun h' => ?_⟩ h1.2) + rw [HasSingDualInSelf.get_append_inr h.1 h1.1.1] at h2 + simpa using h2 + · refine Or.inr (And.intro h1.1 ⟨h1.2, fun h' => ?_⟩) + rw [HasSingDualInSelf.get_append_inr_other h.1 h1.2.1] at h2 + simpa using h2 + · have h1 : (l ++ l2).HasSingDualInSelf (appendEquiv (Sum.inr i)) := by + simp [HasSingColorDualInSelf] + cases h <;> rename_i h + · exact Or.inl ⟨h.1.1, h.2⟩ + · exact Or.inr ⟨h.1, h.2.1⟩ + apply And.intro h1 + intro h' + simp + cases h <;> rename_i h + · simpa [HasSingDualInSelf.get_append_inr h1 h.1.1.1] using h.1.2 h.1.1 + · simpa [HasSingDualInSelf.get_append_inr_other h1 h.2.1.1] using h.2.2 h.2.1 + +lemma append_symm : (l ++ l2).HasSingColorDualInSelf (appendEquiv (Sum.inl i)) ↔ + (l2 ++ l).HasSingColorDualInSelf (appendEquiv (Sum.inr i)) := by + simp + +end HasSingColorDualInSelf + +def HasSingColorDualsInSelf : Prop := ∀ i, l.HasSingColorDualInSelf i ∨ ¬ l.HasDualInSelf i + +namespace HasSingColorDualsInSelf + +variable {l : IndexList 𝓒.Color} + +lemma not_hasDualInSelf_iff_not_hasSingColorDualInSelf (h : l.HasSingColorDualsInSelf) + (i : Fin l.length) : ¬ l.HasDualInSelf i ↔ ¬ l.HasSingColorDualInSelf i := by + apply Iff.intro + · intro h' + by_contra hn + exact h' hn.1.1 + · intro h' + have h1 := h i + simp_all + +lemma _root_.IndexNotation.IndexList.HasNoDualsSelf.toHasSingColorDualsInSelf + (h : l.HasNoDualsSelf) : l.HasSingColorDualsInSelf := + fun i => Or.inr (h i) + +end HasSingColorDualsInSelf +def HasSingColorDualsInOther : Prop := ∀ i, l.HasSingColorDualInOther l2 i ∨ ¬ l.HasDualInOther l2 i + + +end Color + + +end IndexList + +end IndexNotation diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/GetDual.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/GetDual.lean new file mode 100644 index 0000000..fe6ff6a --- /dev/null +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/GetDual.lean @@ -0,0 +1,113 @@ +/- +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.DualIndex +/-! + +# Dual indices + +-/ + +namespace IndexNotation + + +namespace IndexList + +variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X] +variable (l l2 : IndexList X) + + +def getDual (i : Fin l.length) : Option (Fin l.length) := + if h : l.HasDualInSelf i then + some h.getFirst + else + none + +lemma getDual_of_hasDualInSelf {i : Fin l.length} (h : l.HasDualInSelf i) : + l.getDual i = some h.getFirst := by + simp [getDual, h] + +lemma getDual_of_not_hasDualInSelf {i : Fin l.length} (h : ¬l.HasDualInSelf i) : + l.getDual i = none := by + simp [getDual, h] + +def getDualOther (i : Fin l.length) : Option (Fin l2.length) := + if h : l.HasDualInOther l2 i then + some h.getFirst + else + none + +lemma getDualOther_of_hasDualInOther {i : Fin l.length} (h : l.HasDualInOther l2 i) : + l.getDualOther l2 i = some h.getFirst := by + simp [getDualOther, h] + +lemma getDualOther_of_not_hasDualInOther {i : Fin l.length} (h : ¬l.HasDualInOther l2 i) : + l.getDualOther l2 i = none := by + simp [getDualOther, h] + +/-! + +## Append relations + +-/ + +@[simp] +lemma getDual_append_inl (i : Fin l.length) : (l ++ l2).getDual (appendEquiv (Sum.inl i)) = + Option.or (Option.map (appendEquiv ∘ Sum.inl) (l.getDual i)) + (Option.map (appendEquiv ∘ Sum.inr) (l.getDualOther l2 i)) := by + by_cases h : (l ++ l2).HasDualInSelf (appendEquiv (Sum.inl i)) + · rw [(l ++ l2).getDual_of_hasDualInSelf h] + by_cases hl : l.HasDualInSelf i + · rw [l.getDual_of_hasDualInSelf hl] + simp + exact HasDualInSelf.getFirst_append_inl_of_hasDualInSelf l l2 h hl + · rw [l.getDual_of_not_hasDualInSelf hl] + simp at h hl + simp_all + rw [l.getDualOther_of_hasDualInOther l2 h] + simp only [Option.map_some', Function.comp_apply] + · rw [(l ++ l2).getDual_of_not_hasDualInSelf h] + simp at h + rw [l.getDual_of_not_hasDualInSelf h.1] + rw [l.getDualOther_of_not_hasDualInOther l2 h.2] + rfl + +@[simp] +lemma getDual_append_inr (i : Fin l2.length) : (l ++ l2).getDual (appendEquiv (Sum.inr i)) = + Option.or (Option.map (appendEquiv ∘ Sum.inl) (l2.getDualOther l i)) + (Option.map (appendEquiv ∘ Sum.inr) (l2.getDual i)) := by + by_cases h : (l ++ l2).HasDualInSelf (appendEquiv (Sum.inr i)) + · rw [(l ++ l2).getDual_of_hasDualInSelf h] + by_cases hl1 : l2.HasDualInOther l i + · rw [l2.getDualOther_of_hasDualInOther l hl1] + simp + exact HasDualInSelf.getFirst_append_inr_of_hasDualInOther l l2 h hl1 + · rw [l2.getDualOther_of_not_hasDualInOther l hl1] + simp at h hl1 + simp_all + rw [l2.getDual_of_hasDualInSelf h] + simp only [Option.map_some', Function.comp_apply] + · rw [(l ++ l2).getDual_of_not_hasDualInSelf h] + simp at h + rw [l2.getDual_of_not_hasDualInSelf h.1] + rw [l2.getDualOther_of_not_hasDualInOther l h.2] + rfl + +def HasSingDualsInSelf : Prop := + ∀ i, (l.getDual i).bind l.getDual = some i + +def HasSingDualsInOther : Prop := + (∀ i, (l.getDualOther l2 i).bind (l2.getDualOther l) = some i) + ∧ (∀ i, (l2.getDualOther l i).bind (l.getDualOther l2) = some i) + +def HasNoDualsInSelf : Prop := l.getDual = fun _ => none + +lemma hasSingDualsInSelf_append : + (l ++ l2).HasSingDualsInSelf ↔ + l.HasSingDualsInSelf ∧ l2.HasSingDualsInSelf ∧ HasSingDualsInOther l1 l2 := by + sorry +end IndexList + +end IndexNotation diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColor.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColor.lean index 8c552b7..87d5c69 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColor.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColor.lean @@ -26,7 +26,7 @@ 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.1 j.1 → j = l.getDual i) ∧ + (∀ (i j : l.contrSubtype), l.AreDual 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 @@ -63,7 +63,7 @@ def colorPropFstBool (l : IndexList 𝓒.Color) : Bool := 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 + ∀ (i j : l.contrSubtype), l.AreDual i.1 j.1 → j = l.getDual i := by simp [colorPropFstBool] at hl rw [List.filterMap_eq_nil] at hl simp at hl @@ -118,7 +118,7 @@ lemma colorPropBool_indexListColorProp {l : IndexList 𝓒.Color} (hl : colorPro lemma getDual_getDual (i : l.1.contrSubtype) : l.1.getDual (l.1.getDual i) = i := by refine (l.prop.1 (l.1.getDual i) i ?_).symm - simp [getDualProp] + simp [AreDual] apply And.intro exact Subtype.coe_ne_coe.mpr (l.1.getDual_neq_self i).symm exact (l.1.getDual_id i).symm @@ -210,23 +210,23 @@ lemma splitContr_symm_apply_of_hasNoContr (h : l.1.HasNoContr) (x : Fin (l.1.noC /-- The contracted index list as a `IndexListColor`. -/ def contr : IndexListColor 𝓒 := - ⟨l.1.contrIndexList, indexListColorProp_of_hasNoContr l.1.contrIndexList_hasNoContr⟩ + ⟨l.1.contr, indexListColorProp_of_hasNoContr l.1.contr_hasNoContr⟩ /-- Contracting twice is equivalent to contracting once. -/ @[simp] lemma contr_contr : l.contr.contr = l.contr := by apply Subtype.ext - exact l.1.contrIndexList_contrIndexList + exact l.1.contr_contr @[simp] lemma contr_numIndices : l.contr.1.numIndices = l.1.noContrFinset.card := - l.1.contrIndexList_numIndices + l.1.contr_numIndices lemma contr_colorMap : l.1.colorMap ∘ l.splitContr.symm ∘ Sum.inr = l.contr.1.colorMap ∘ (Fin.castOrderIso l.contr_numIndices.symm).toEquiv.toFun := by funext x - simp only [Function.comp_apply, colorMap, List.get_eq_getElem, contr, contrIndexList, fromFinMap, + simp only [Function.comp_apply, colorMap, List.get_eq_getElem, contr, IndexList.contr, fromFinMap, Equiv.toFun_as_coe, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Fin.coe_cast, List.getElem_map, Fin.getElem_list, Fin.cast_mk, Fin.eta] rfl @@ -252,7 +252,7 @@ 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 + have h1 : l.contr.1.HasNoContr := l.1.contr_hasNoContr exact fun i j a => hasNoContr_color_eq_of_id_eq (↑l.contr) h1 i j a lemma symm : Symmetric (@PermContr 𝓒 _) := @@ -297,7 +297,7 @@ lemma get_unique {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) (hij : s1.contr.1.idMap i = s2.contr.1.idMap j) : j = h.get i := by by_contra hn - refine (?_ : ¬ s2.contr.1.NoContr j) (s2.1.contrIndexList_hasNoContr j) + refine (?_ : ¬ s2.contr.1.NoContr j) (s2.1.contr_hasNoContr j) simp [NoContr] use PermContr.get h i apply And.intro hn @@ -351,7 +351,7 @@ lemma toEquiv_refl' {s : IndexListColor 𝓒} (h : PermContr s s) : 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 + have h2 := s.1.contr_hasNoContr x simp only [true_and] intro j hj by_cases hjx : j = x @@ -394,7 +394,7 @@ lemma of_contr_eq {s1 s2 : IndexListColor 𝓒} (hc : s1.contr = s2.contr) : simp [PermContr] rw [hc] simp only [List.Perm.refl, true_and] - refine hasNoContr_color_eq_of_id_eq s2.contr.1 (s2.1.contrIndexList_hasNoContr) + refine hasNoContr_color_eq_of_id_eq s2.contr.1 (s2.1.contr_hasNoContr) lemma of_contr {s1 s2 : IndexListColor 𝓒} (hc : PermContr s1.contr s2.contr) : PermContr s1 s2 := by @@ -418,7 +418,7 @@ lemma toEquiv_contr_eq {s1 s2 : IndexListColor 𝓒} (hc : s1.contr = s2.contr) rfl intro j hj rw [idMap_cast (congrArg Subtype.val hc)] at hj - have h2 := s2.contr.1.hasNoContr_id_inj (s2.1.contrIndexList_hasNoContr) hj + have h2 := s2.contr.1.hasNoContr_id_inj (s2.1.contr_hasNoContr) hj subst h2 rfl simp only [h1, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Option.get_some] diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColorV2.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColorV2.lean new file mode 100644 index 0000000..325412e --- /dev/null +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColorV2.lean @@ -0,0 +1,511 @@ +/- +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.DualIndex +import HepLean.SpaceTime.LorentzTensor.Basic +import Init.Data.List.Lemmas +/-! + +# Index lists with color conditions + +Here we consider `IndexListColor` which is a subtype of all lists of indices +on those where the elements to be contracted have consistent colors with respect to +a Tensor Color structure. + +-/ + +namespace IndexNotation + +def IndexListColor (𝓒 : TensorColor) [IndexNotation 𝓒.Color] : Type := + {l // (l : IndexList 𝓒.Color).HasSingColorDualsInSelf} + +namespace IndexListColor + +variable {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color] +variable (l : IndexListColor 𝓒) + +def length : ℕ := l.1.length + +def HasNoDualsSelf : Prop := l.1.HasNoDualsSelf + +def getDual? (i : Fin l.length) : Option (Fin l.length) := + if h : l.1.HasSingColorDualInSelf i then + some h.get + else none + +def withDualFinset : Finset (Fin l.length) := Finset.filter l.1.HasSingColorDualInSelf Finset.univ + +lemma withDualFinset_prop {l : IndexListColor 𝓒} (i : l.withDualFinset) : + l.1.HasSingColorDualInSelf i.1 := by + simpa [withDualFinset] using i.2 + +def withDualFinsetLT : Finset l.withDualFinset := + Finset.filter (fun i => i.1 < (withDualFinset_prop i).get) Finset.univ + +def withDualFinsetGT : Finset l.withDualFinset := + Finset.filter (fun i => (withDualFinset_prop i).get < i.1) Finset.univ + +def withDualFinsetLTGTEquiv : l.withDualFinsetLT ≃ l.withDualFinsetGT where + toFun x := ⟨⟨(withDualFinset_prop x.1).get, + by simpa [withDualFinset] using (withDualFinset_prop x.1).get_hasSingColorDualInSelf⟩, by + simpa [withDualFinsetGT, withDualFinsetLT] using x.2⟩ + invFun x := ⟨⟨(withDualFinset_prop x.1).get, + by simpa [withDualFinset] using (withDualFinset_prop x.1).get_hasSingColorDualInSelf⟩, by + simpa [withDualFinsetGT, withDualFinsetLT] using x.2⟩ + left_inv x := by + apply Subtype.ext + apply Subtype.ext + simp only [length, IndexList.HasSingColorDualInSelf.get_get] + right_inv x := by + apply Subtype.ext + apply Subtype.ext + simp only [length, IndexList.HasSingColorDualInSelf.get_get] + +lemma withDualFinsetLT_disjoint_withDualFinsetGT : + Disjoint l.withDualFinsetLT l.withDualFinsetGT := by + rw [Finset.disjoint_iff_ne] + intro a ha b hb + by_contra hn + subst hn + simp [withDualFinsetLT, withDualFinsetGT] at ha hb + omega + +lemma mem_withDualFinsetLT_union_withDualFinsetGT (x : l.withDualFinset) : + x ∈ l.withDualFinsetLT ∪ l.withDualFinsetGT := by + simpa [withDualFinsetLT, withDualFinsetGT] using (withDualFinset_prop x).areDualInSelf_get.1 + +def withDualEquiv : l.withDualFinsetLT ⊕ l.withDualFinsetLT ≃ l.withDualFinset := + (Equiv.sumCongr (Equiv.refl _) l.withDualFinsetLTGTEquiv).trans <| + (Equiv.Finset.union _ _ l.withDualFinsetLT_disjoint_withDualFinsetGT).trans <| + Equiv.subtypeUnivEquiv l.mem_withDualFinsetLT_union_withDualFinsetGT + +def withoutDualFinset : Finset (Fin l.length) := + Finset.filter (fun i => ¬ l.1.HasDualInSelf i) Finset.univ + +lemma mem_withoutDualFinset_iff_not_hasSingColorDualInSelf (i : Fin l.length) : + i ∈ l.withoutDualFinset ↔ ¬ l.1.HasSingColorDualInSelf i := by + simp [withoutDualFinset] + exact l.2.not_hasDualInSelf_iff_not_hasSingColorDualInSelf i + +lemma mem_withoutDualFinset_of_hasNoDualsSelf (h : l.HasNoDualsSelf) (i : Fin l.length) : + i ∈ l.withoutDualFinset := by + simpa [withoutDualFinset] using h i + +lemma withoutDualFinset_of_hasNoDualsSelf (h : l.HasNoDualsSelf) : + l.withoutDualFinset = Finset.univ := by + rw [@Finset.eq_univ_iff_forall] + exact l.mem_withoutDualFinset_of_hasNoDualsSelf h + +lemma withDualFinset_disjoint_withoutDualFinset : + Disjoint l.withDualFinset l.withoutDualFinset := by + rw [Finset.disjoint_iff_ne] + intro a ha b hb + by_contra hn + subst hn + rw [mem_withoutDualFinset_iff_not_hasSingColorDualInSelf] at hb + simp [withDualFinset, withoutDualFinset] at ha hb + exact hb ha + +lemma mem_withDualFinset_union_withoutDualFinset (x : Fin l.length) : + x ∈ l.withDualFinset ∪ l.withoutDualFinset := by + simp [withDualFinset] + rw [mem_withoutDualFinset_iff_not_hasSingColorDualInSelf] + exact Decidable.em (l.1.HasSingColorDualInSelf x) + +def dualEquiv : l.withDualFinset ⊕ l.withoutDualFinset ≃ Fin l.length := + (Equiv.Finset.union _ _ l.withDualFinset_disjoint_withoutDualFinset).trans <| + Equiv.subtypeUnivEquiv l.mem_withDualFinset_union_withoutDualFinset + +def withoutDualEquiv : Fin l.withoutDualFinset.card ≃ l.withoutDualFinset := + (Finset.orderIsoOfFin _ rfl).toEquiv + + +def withoutDualIndexList : IndexList 𝓒.Color := + (Fin.list l.withoutDualFinset.card).map (fun i => l.1.get (l.withoutDualEquiv i).1) + +@[simp] +lemma withoutDualIndexList_idMap (i : Fin (List.length l.withoutDualIndexList)) : + l.withoutDualIndexList.idMap i = + l.1.idMap (l.withoutDualEquiv (Fin.cast (by simp [withoutDualIndexList]) i)).1 := by + simp [withoutDualIndexList, IndexList.idMap] + rfl + +lemma withoutDualIndexList_hasNoDualsSelf : l.withoutDualIndexList.HasNoDualsSelf := by + intro i + simp [IndexList.HasDualInSelf, IndexList.AreDualInSelf] + intro x hx + have h1 : l.withoutDualEquiv (Fin.cast (by simp [withoutDualIndexList]) i) ≠ + l.withoutDualEquiv (Fin.cast (by simp [withoutDualIndexList]) x) := by + simp + rw [Fin.ext_iff] at hx ⊢ + simpa using hx + have hx' := (l.withoutDualEquiv (Fin.cast (by simp [withoutDualIndexList]) i)).2 + simp [withoutDualFinset, IndexList.HasDualInSelf, IndexList.AreDualInSelf] at hx' + refine hx' (l.withoutDualEquiv (Fin.cast (by simp [withoutDualIndexList]) x)).1 ?_ + simp only [length] + rw [← Subtype.eq_iff] + exact h1 + +lemma withoutDualIndexList_of_hasNoDualsSelf (h : l.1.HasNoDualsSelf ) : + l.withoutDualIndexList = l.1 := by + simp [withoutDualIndexList, List.get_eq_getElem] + apply List.ext_get + · simp only [List.length_map, Fin.length_list] + rw [l.withoutDualFinset_of_hasNoDualsSelf h] + simp only [Finset.card_univ, Fintype.card_fin] + rfl + intro n h1 h2 + simp + congr + simp [withoutDualEquiv] + have h1 : l.withoutDualFinset.orderEmbOfFin rfl = + (Fin.castOrderIso (by + rw [l.withoutDualFinset_of_hasNoDualsSelf h] + simp only [Finset.card_univ, Fintype.card_fin])).toOrderEmbedding := by + symm + refine Finset.orderEmbOfFin_unique' (Eq.refl l.withoutDualFinset.card) + (fun x => mem_withoutDualFinset_of_hasNoDualsSelf l h _) + rw [h1] + rfl + +def contr : IndexListColor 𝓒 := + ⟨l.withoutDualIndexList, l.withoutDualIndexList_hasNoDualsSelf.toHasSingColorDualsInSelf⟩ + +lemma contr_length : l.contr.1.length = l.withoutDualFinset.card := by + simp [contr, withoutDualIndexList] + +@[simp] +lemma contr_id (i : Fin l.contr.length) : l.contr.1.idMap i = + l.1.idMap (l.withoutDualEquiv (Fin.cast l.contr_length i)).1 := by + simp [contr] + +lemma contr_hasNoDualsSelf : l.contr.1.HasNoDualsSelf := + l.withoutDualIndexList_hasNoDualsSelf + +lemma contr_of_hasNoDualsSelf (h : l.1.HasNoDualsSelf) : + l.contr = l := by + apply Subtype.ext + exact l.withoutDualIndexList_of_hasNoDualsSelf h + +@[simp] +lemma contr_contr : l.contr.contr = l.contr := + l.contr.contr_of_hasNoDualsSelf l.contr_hasNoDualsSelf + +/-! + +# Relations on IndexListColor + +-/ + +def Relabel (l1 l2 : IndexListColor 𝓒) : Prop := + l1.length = l2.length ∧ + ∀ (h : l1.length = l2.length), + Option.map (Fin.cast h) ∘ l1.getDual? = l2.getDual? ∘ Fin.cast h ∧ + l1.1.colorMap = l2.1.colorMap ∘ Fin.cast h + +def PermAfterContr (l1 l2 : IndexListColor 𝓒) : Prop := + List.Perm (l1.contr.1.map Index.id) (l2.contr.1.map Index.id) + ∧ ∀ (i : Fin l1.contr.1.length) (j : Fin l2.contr.1.length), + l1.contr.1.idMap i = l2.contr.1.idMap j → + l1.contr.1.colorMap i = l2.contr.1.colorMap j + +def AppendHasSingColorDualsInSelf (l1 l2 : IndexListColor 𝓒) : Prop := + (l1.contr.1 ++ l2.contr.1).HasSingColorDualsInSelf + + +end IndexListColor + +/-- A proposition which is true if an index has at most one dual. -/ +def HasSubSingeDualSelf (i : Fin l.length) : Prop := + ∀ (h : l.HasDualSelf i) j, l.AreDualSelf i j → j = l.getDualSelf i h + +lemma HasSubSingeDualSelf.eq_dual_iff {l : IndexList X} {i : Fin l.length} + (h : l.HasSubSingeDualSelf i) (hi : l.HasDualSelf i) (j : Fin l.length) : + j = l.getDualSelf i hi ↔ l.AreDualSelf i j := by + have h1 := h hi j + apply Iff.intro + intro h + subst h + exact l.areDualSelf_of_getDualSelf i hi + exact h1 + +@[simp] +lemma getDualSelf_append_inl {l l2 : IndexList X} (i : Fin l.length) + (h : (l ++ l2).HasSubSingeDualSelf (appendEquiv (Sum.inl i))) (hi : l.HasDualSelf i) : + (l ++ l2).getDualSelf (appendEquiv (Sum.inl i)) ((hasDualSelf_append_inl l l2 i).mpr (Or.inl hi)) = + appendEquiv (Sum.inl (l.getDualSelf i hi)) := by + symm + rw [HasSubSingeDualSelf.eq_dual_iff h] + simp + exact areDualSelf_of_getDualSelf l i hi + +lemma HasSubSingeDualSelf.of_append_inl_of_hasDualSelf {l l2 : IndexList X} (i : Fin l.length) + (h : (l ++ l2).HasSubSingeDualSelf (appendEquiv (Sum.inl i))) (hi : l.HasDualSelf i) : + l.HasSubSingeDualSelf i := by + intro hj j + have h1 := h ((hasDualSelf_append_inl l l2 i).mpr (Or.inl hi)) (appendEquiv (Sum.inl j)) + intro hij + simp at h1 + have h2 := h1 hij + apply Sum.inl_injective + apply appendEquiv.injective + rw [h2, l.getDualSelf_append_inl _ h] + + +lemma HasSubSingeDualSelf.not_hasDualOther_of_append_inl_of_hasDualSelf + {l l2 : IndexList X} (i : Fin l.length) + (h : (l ++ l2).HasSubSingeDualSelf (appendEquiv (Sum.inl i))) (hi : l.HasDualSelf i) : + ¬ l.HasDualOther l2 i := by + simp [HasDualOther] + intro j + simp [AreDualOther] + simp [HasSubSingeDualSelf] at h + have h' := h ((hasDualSelf_append_inl l l2 i).mpr (Or.inl hi)) (appendEquiv (Sum.inr j)) + simp [AreDualSelf] at h' + by_contra hn + have h'' := h' hn + rw [l.getDualSelf_append_inl _ h hi] at h'' + simp at h'' + + +lemma HasSubSingeDualSelf.of_append_inr_of_hasDualSelf {l l2 : IndexList X} (i : Fin l2.length) + (h : (l ++ l2).HasSubSingeDualSelf (appendEquiv (Sum.inr i))) (hi : l2.HasDualSelf i) : + l2.HasSubSingeDualSelf i := by + intro hj j + have h1 := h ((hasDualSelf_append_inr l i).mpr (Or.inl hi)) (appendEquiv (Sum.inr j)) + intro hij + simp at h1 + have h2 := h1 hij + apply Sum.inr_injective + apply appendEquiv.injective + rw [h2] + symm + rw [eq_dual_iff h] + simp only [AreDualSelf.append_inr_inr] + exact areDualSelf_of_getDualSelf l2 i hj + + +lemma HasSubSingeDualSelf.append_inl (i : Fin l.length) : + (l ++ l2).HasSubSingeDualSelf (appendEquiv (Sum.inl i)) ↔ + (l.HasSubSingeDualSelf i ∧ ¬ l.HasDualOther l2 i) ∨ + (¬ l.HasDualSelf i ∧ l.HasSubSingeDualOther l2 i) := by + apply Iff.intro + · intro h + by_cases h1 : (l ++ l2).HasDualSelf (appendEquiv (Sum.inl i)) + rw [hasDualSelf_append_inl] at h1 + cases h1 <;> rename_i h1 + · exact Or.inl ⟨of_append_inl_of_hasDualSelf i h h1, + (not_hasDualOther_of_append_inl_of_hasDualSelf i h h1)⟩ + · sorry + + +def HasSubSingeDuals : Prop := ∀ i, l.HasSubSingeDual i + +def HasNoDual (i : Fin l.length) : Prop := ¬ l.HasDual i + +def HasNoDuals : Prop := ∀ i, l.HasNoDual i + + +lemma hasSubSingeDuals_of_hasNoDuals (h : l.HasNoDuals) : l.HasSubSingeDuals := by + intro i h1 j h2 + exfalso + apply h i + simp only [HasDual] + exact ⟨j, h2⟩ + +/-- The proposition on a element (or really index of element) of a index list + `s` which is ture iff does not share an id with any other element. + This tells us that it should not be contracted with any other element. -/ +def NoContr (i : Fin l.length) : Prop := + ∀ j, i ≠ j → l.idMap i ≠ l.idMap j + +instance (i : Fin l.length) : Decidable (l.NoContr i) := + Fintype.decidableForallFintype + +/-- The finset of indices of an index list corresponding to elements which do not contract. -/ +def noContrFinset : Finset (Fin l.length) := + Finset.univ.filter l.NoContr + +/-- An eqiuvalence between the subtype of indices of a index list `l` which do not contract and + `Fin l.noContrFinset.card`. -/ +def noContrSubtypeEquiv : {i : Fin l.length // l.NoContr i} ≃ Fin l.noContrFinset.card := + (Equiv.subtypeEquivRight (fun x => by simp [noContrFinset])).trans + (Finset.orderIsoOfFin l.noContrFinset rfl).toEquiv.symm + +@[simp] +lemma idMap_noContrSubtypeEquiv_neq (i j : Fin l.noContrFinset.card) (h : i ≠ j) : + l.idMap (l.noContrSubtypeEquiv.symm i).1 ≠ l.idMap (l.noContrSubtypeEquiv.symm j).1 := by + have hi := ((l.noContrSubtypeEquiv).symm i).2 + simp [NoContr] at hi + have hj := hi ((l.noContrSubtypeEquiv).symm j) + apply hj + rw [@SetCoe.ext_iff] + erw [Equiv.apply_eq_iff_eq] + exact h + +/-- The subtype of indices `l` which do contract. -/ +def contrSubtype : Type := {i : Fin l.length // ¬ l.NoContr i} + +instance : Fintype l.contrSubtype := + Subtype.fintype fun x => ¬ l.NoContr x + +instance : DecidableEq l.contrSubtype := + Subtype.instDecidableEq + +/-! + +## Getting the index which contracts with a given index + +-/ + +lemma getDual_id (i : l.contrSubtype) : l.idMap i.1 = l.idMap (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 [AreDual, ne_eq, and_imp] at h1 + exact h1.1.2 + +lemma getDual_neq_self (i : l.contrSubtype) : i ≠ l.getDual i := by + have h1 := l.some_getDualFin_eq_find i + 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.AreDual 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 [AreDual, ne_eq, and_imp] at h1 + exact h1.1 + +/-! + +## Index lists with no contracting indices + +-/ + +/-- The proposition on a `IndexList` for it to have no contracting + indices. -/ +def HasNoContr : Prop := ∀ i, l.NoContr i + +lemma contrSubtype_is_empty_of_hasNoContr (h : l.HasNoContr) : IsEmpty l.contrSubtype := by + rw [_root_.isEmpty_iff] + intro a + exact h a.1 a.1 (fun _ => a.2 (h a.1)) rfl + +lemma hasNoContr_id_inj (h : l.HasNoContr) : Function.Injective l.idMap := fun i j => by + simpa using (h i j).mt + +lemma hasNoContr_color_eq_of_id_eq (h : l.HasNoContr) (i j : Fin l.length) : + l.idMap i = l.idMap j → l.colorMap i = l.colorMap j := by + intro h1 + apply l.hasNoContr_id_inj h at h1 + rw [h1] + +@[simp] +lemma hasNoContr_noContrFinset_card (h : l.HasNoContr) : + l.noContrFinset.card = List.length l := by + simp only [noContrFinset] + rw [Finset.filter_true_of_mem] + simp only [Finset.card_univ, Fintype.card_fin] + intro x _ + exact h x + +/-! + +## The contracted index list + +-/ + +/-- The index list of those indices of `l` which do not contract. -/ +def contr : IndexList X := + IndexList.fromFinMap (fun i => l.get (l.noContrSubtypeEquiv.symm i)) + +@[simp] +lemma contr_numIndices : l.contr.numIndices = l.noContrFinset.card := by + simp [contr] + +@[simp] +lemma contr_idMap_apply (i : Fin l.contr.numIndices) : + l.contr.idMap i = + l.idMap (l.noContrSubtypeEquiv.symm (Fin.cast (by simp) i)).1 := by + simp [contr, IndexList.fromFinMap, IndexList.idMap] + rfl + +lemma contr_hasNoContr : HasNoContr l.contr := by + intro i + simp [NoContr] + intro j h + refine l.idMap_noContrSubtypeEquiv_neq _ _ ?_ + rw [@Fin.ne_iff_vne] + simp only [Fin.coe_cast, ne_eq] + exact Fin.val_ne_of_ne h + +/-- Contracting indices on a index list that has no contractions does nothing. -/ +@[simp] +lemma contr_of_hasNoContr (h : HasNoContr l) : l.contr = l := by + simp only [contr, List.get_eq_getElem] + have hn : (@Finset.univ (Fin (List.length l)) (Fin.fintype (List.length l))).card = + (Finset.filter l.NoContr Finset.univ).card := by + rw [Finset.filter_true_of_mem (fun a _ => h a)] + have hx : (Finset.filter l.NoContr Finset.univ).card = (List.length l) := by + rw [← hn] + exact Finset.card_fin (List.length l) + apply List.ext_get + simpa [fromFinMap, noContrFinset] using hx + intro n h1 h2 + simp only [noContrFinset, noContrSubtypeEquiv, OrderIso.toEquiv_symm, Equiv.symm_trans_apply, + RelIso.coe_fn_toEquiv, Equiv.subtypeEquivRight_symm_apply_coe, fromFinMap, List.get_eq_getElem, + OrderIso.symm_symm, Finset.coe_orderIsoOfFin_apply, List.getElem_map, Fin.getElem_list, + Fin.cast_mk] + simp only [Finset.filter_true_of_mem (fun a _ => h a)] + congr + rw [(Finset.orderEmbOfFin_unique' _ + (fun x => Finset.mem_univ ((Fin.castOrderIso hx).toOrderEmbedding x))).symm] + rfl + +/-- Applying contrIndexlist is equivalent to applying it once. -/ +@[simp] +lemma contr_contr : l.contr.contr = l.contr := + l.contr.contr_of_hasNoContr (l.contr_hasNoContr) + +/-! + +## Pairs of contracting indices + +-/ + +/-- The set of contracting ordered pairs of indices. -/ +def contrPairSet : Set (l.contrSubtype × l.contrSubtype) := + {p | p.1.1 < p.2.1 ∧ l.idMap p.1.1 = l.idMap p.2.1} + +instance : DecidablePred fun x => x ∈ l.contrPairSet := fun _ => + And.decidable + +instance : Fintype l.contrPairSet := setFintype _ + +lemma contrPairSet_isEmpty_of_hasNoContr (h : l.HasNoContr) : + IsEmpty l.contrPairSet := by + simp only [contrPairSet, Subtype.coe_lt_coe, Set.coe_setOf, isEmpty_subtype, not_and, Prod.forall] + refine fun a b h' => h a.1 b.1 (Fin.ne_of_lt h') + +lemma getDual_lt_self_mem_contrPairSet {i : l.contrSubtype} + (h : (l.getDual i).1 < i.1) : (l.getDual i, i) ∈ l.contrPairSet := + And.intro h (l.getDual_id i).symm + +lemma getDual_not_lt_self_mem_contrPairSet {i : l.contrSubtype} + (h : ¬ (l.getDual i).1 < i.1) : (i, l.getDual i) ∈ l.contrPairSet := by + apply And.intro + have h1 := l.getDual_neq_self i + simp only [Subtype.coe_lt_coe, gt_iff_lt] + simp at h + exact lt_of_le_of_ne h h1 + 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.AreDual i j then some (i, j) else none +end IndexNotation diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean index 430646d..5440c44 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean @@ -13,6 +13,9 @@ import HepLean.SpaceTime.LorentzTensor.Contraction -/ +/-! TODO: Introduce a way to change an index from e.g. `ᵘ¹` to `ᵘ²`. + Would be nice to have a tactic that did this automatically. -/ + namespace TensorStructure noncomputable section @@ -103,7 +106,7 @@ def contr (T : 𝓣.TensorIndex) : 𝓣.TensorIndex where lemma contr_of_hasNoContr (T : 𝓣.TensorIndex) (h : T.index.1.HasNoContr) : T.contr = T := by refine ext _ _ ?_ ?_ - exact Subtype.eq (T.index.1.contrIndexList_of_hasNoContr h) + exact Subtype.eq (T.index.1.contr_of_hasNoContr h) simp only [contr] have h1 : IsEmpty T.index.1.contrPairSet := T.index.1.contrPairSet_isEmpty_of_hasNoContr h cases T @@ -129,31 +132,11 @@ lemma contr_of_hasNoContr (T : 𝓣.TensorIndex) (h : T.index.1.HasNoContr) : @[simp] lemma contr_contr (T : 𝓣.TensorIndex) : T.contr.contr = T.contr := - T.contr.contr_of_hasNoContr T.index.1.contrIndexList_hasNoContr + T.contr.contr_of_hasNoContr T.index.1.contr_hasNoContr @[simp] lemma contr_index (T : 𝓣.TensorIndex) : T.contr.index = T.index.contr := rfl -/-! - -## 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 - index := T₁.index.prod T₂.index h - tensor := - 𝓣.mapIso ((Fin.castOrderIso (IndexListColor.prod_numIndices)).toEquiv.trans - (finSumFinEquiv.symm)).symm - (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 /-! @@ -251,7 +234,7 @@ lemma rel_contr (T : 𝓣.TensorIndex) : T ≈ T.contr := by apply And.intro simp only [PermContr, contr_index, IndexListColor.contr_contr, List.Perm.refl, true_and] rw [IndexListColor.contr_contr] - exact T.index.contr.1.hasNoContr_color_eq_of_id_eq T.index.1.contrIndexList_hasNoContr + exact T.index.contr.1.hasNoContr_color_eq_of_id_eq T.index.1.contr_hasNoContr intro h rw [tensor_eq_of_eq T.contr_contr] simp only [contr_index, mapIso_mapIso] @@ -394,7 +377,7 @@ lemma smul_add (r : R) (T₁ T₂ : 𝓣.TensorIndex) (h : AddCond T₁ T₂) : lemma add_hasNoContr (T₁ T₂ : 𝓣.TensorIndex) (h : AddCond T₁ T₂) : (T₁ +[h] T₂).index.1.HasNoContr := by - simpa using T₂.index.1.contrIndexList_hasNoContr + simpa using T₂.index.1.contr_hasNoContr @[simp] lemma contr_add (T₁ T₂ : 𝓣.TensorIndex) (h : AddCond T₁ T₂) : @@ -467,6 +450,50 @@ lemma add_assoc {T₁ T₂ T₃ : 𝓣.TensorIndex} {h' : AddCond T₁ T₂} (h /-! TODO: Show that the product is well defined with respect to Rel. -/ +/-! + +## Product of `TensorIndex` allowed + +-/ + +/-- The condition on two tensors with indices determining if it possible to + take their product. + + This condition says that the indices of the two tensors can contract nicely, + after the contraction of indivdual indices has taken place. Note that + it is required to take the contraction of indivdual tensors before taking the product + to ensure that the product is well-defined under the `Rel` equivalence relation. + + For example, indices with the same id have dual colors, and no more then two indices + have the same id (after contraction). For example, the product of `ψᵘ¹ᵤ₂ᵘ²` could be taken with + `φᵤ₁ᵤ₃ᵘ³` or `φᵤ₄ᵤ₃ᵘ³` or `φᵤ₁ᵤ₂ᵘ²` or `φᵤ₂ᵤ₁ᵘ¹` + (since contraction is done before taking the product) + but not with `φᵤ₁ᵤ₃ᵘ³` or `φᵤ₁ᵤ₂ᵘ²` or `φᵤ₃ᵤ₂ᵘ²`. -/ +def ProdCond (T₁ T₂ : 𝓣.TensorIndex) : Prop := + IndexListColorProp 𝓣.toTensorColor (T₁.contr.index.1 ++ T₂.contr.index.1) + +namespace ProdCond + +lemma to_indexListColorProp {T₁ T₂ : 𝓣.TensorIndex} (h : ProdCond T₁ T₂) : + IndexListColorProp 𝓣.toTensorColor (T₁.contr.index.1 ++ T₂.contr.index.1) := h + +end ProdCond + +/-- The tensor product of two `TensorIndex`. -/ +def prod (T₁ T₂ : 𝓣.TensorIndex) + (h : ProdCond T₁ T₂) : 𝓣.TensorIndex where + index := T₁.contr.index.prod T₂.contr.index h.to_indexListColorProp + tensor := + 𝓣.mapIso ((Fin.castOrderIso (IndexListColor.prod_numIndices)).toEquiv.trans + (finSumFinEquiv.symm)).symm + (IndexListColor.prod_colorMap h) <| + 𝓣.tensoratorEquiv _ _ (T₁.contr.tensor ⊗ₜ[R] T₂.contr.tensor) + +@[simp] +lemma prod_index (T₁ T₂ : 𝓣.TensorIndex) (h : ProdCond T₁ T₂) : + (prod T₁ T₂ h).index = T₁.contr.index.prod T₂.contr.index h.to_indexListColorProp := rfl + + end TensorIndex end end TensorStructure