From d419a17448f19bd077a4a0584d24ca7fb6627161 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 14 Aug 2024 16:55:13 -0400 Subject: [PATCH] refactor: Working refactor --- HepLean/SpaceTime/LorentzTensor/Basic.lean | 3 + .../IndexNotation/Indices/Basic.lean | 14 + .../IndexNotation/Indices/Color.lean | 302 ++++- .../IndexNotation/Indices/Dual.lean | 1130 ++++++++++++++++- .../IndexNotation/Indices/IndexString.lean | 21 +- .../IndexNotation/Indices/Relations.lean | 145 ++- .../IndexNotation/TensorIndex.lean | 283 ++--- .../LorentzTensor/Real/IndexNotation.lean | 68 +- 8 files changed, 1763 insertions(+), 203 deletions(-) diff --git a/HepLean/SpaceTime/LorentzTensor/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Basic.lean index f3c91b3..bcbe5e1 100644 --- a/HepLean/SpaceTime/LorentzTensor/Basic.lean +++ b/HepLean/SpaceTime/LorentzTensor/Basic.lean @@ -126,6 +126,9 @@ lemma symm (h : cX.MapIso e cY) : cY.MapIso e.symm cX := by rw [MapIso] at h exact (Equiv.eq_comp_symm e cY cX).mpr h.symm +lemma symm' : cX.MapIso e cY ↔ cY.MapIso e.symm cX := by + refine ⟨symm, symm⟩ + lemma trans (h : cX.MapIso e cY) (h' : cY.MapIso e' cZ) : cX.MapIso (e.trans e') cZ:= by funext a diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Basic.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Basic.lean index 8c6fac2..10a562f 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Basic.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Basic.lean @@ -268,6 +268,11 @@ 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 append_length : (l ++ l2).length = l.length + l2.length := by + simp [IndexList.length] + exact List.length_append l.val l2.val + lemma append_assoc : l ++ l2 ++ l3 = l ++ (l2 ++ l3) := by apply ext change l.val ++ l2.val ++ l3.val = l.val ++ (l2.val ++ l3.val) @@ -351,6 +356,15 @@ lemma colorMap_append_inr' : funext i simp +lemma colorMap_sumELim (l1 l2 : IndexList X) : + Sum.elim l1.colorMap l2.colorMap = + (l1 ++ l2).colorMap ∘ appendEquiv := by + funext x + match x with + | Sum.inl i => simp + | Sum.inr i => simp + + end append end IndexList diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Color.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Color.lean index 1af94ec..0a19b2f 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Color.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Color.lean @@ -3,10 +3,10 @@ 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.Indices.UniqueDual -import HepLean.SpaceTime.LorentzTensor.IndexNotation.Indices.Append +import HepLean.SpaceTime.LorentzTensor.IndexNotation.Indices.Dual import HepLean.SpaceTime.LorentzTensor.Basic import Init.Data.List.Lemmas +import HepLean.SpaceTime.LorentzTensor.Contraction /-! # Index lists with color conditions @@ -31,7 +31,9 @@ def ColorCond : Prop := Option.map l.colorMap ∘ Option.guard fun i => (l.getDual? i).isSome namespace ColorCond + variable {l l2 l3 : IndexList 𝓒.Color} + lemma iff_withDual : l.ColorCond ↔ ∀ (i : l.withDual), 𝓒.τ (l.colorMap ((l.getDual? i).get (l.withDual_isSome i))) = l.colorMap i := by @@ -77,7 +79,6 @@ lemma inl (h : ColorCond (l ++ l2)) : ColorCond l := by rw [iff_withDual] at h ⊢ intro i have hi' := h ⟨appendEquiv (Sum.inl i), by - rw [inl_mem_withDual_append_iff] simp_all⟩ have hn : (Option.map (appendEquiv ∘ Sum.inl) (l.getDual? ↑i) : Option (Fin (l ++ l2).length)) = some (appendEquiv (Sum.inl ((l.getDual? i).get (l.withDual_isSome i)))) := by @@ -99,16 +100,27 @@ lemma symm (hu : (l ++ l2).withUniqueDual = (l ++ l2).withDual) (h : ColorCond ( | Sum.inl k => have hn := l2.append_inl_not_mem_withDual_of_withDualInOther l k hj by_cases hk' : (l2.getDual? k).isSome - · simp_all + · simp_all only [mem_withDual_iff_isSome, getDual?_append_inl_of_getDual?_isSome, + Option.isSome_some, mem_withInDualOther_iff_isSome, Bool.not_eq_true, Option.not_isSome, + Option.isNone_iff_eq_none, true_iff, Option.get_some, colorMap_append_inl] have hk'' := h (appendEquiv (Sum.inr k)) simp at hk'' - simp_all - · simp_all + simp_all only [getDual?_append_inl_of_getDual?_isSome, Option.isSome_some, Option.isSome_none, + Bool.false_eq_true, or_false, Option.isNone_none, + getDual?_inr_getDualInOther?_isNone_getDual?_isSome, Option.get_some, colorMap_append_inr, + true_implies] + · simp_all only [mem_withDual_iff_isSome, Bool.false_eq_true, mem_withInDualOther_iff_isSome, + Bool.not_eq_true, Option.not_isSome, Option.isNone_iff_eq_none, false_iff, Option.isNone_none, + colorMap_append_inl] have hn' : (l2.getDualInOther? l k).isSome := by - simp_all + simp_all only [Option.isNone_none, getDual?_isSome_append_inl_iff, Option.isSome_none, + Bool.false_eq_true, false_or] have hk'' := h (appendEquiv (Sum.inr k)) - simp at hk'' - simp_all + simp only [getDual?_isSome_append_inr_iff, colorMap_append_inr] at hk'' + simp_all only [Option.isSome_none, Bool.false_eq_true, or_true, + getDual?_append_inr_getDualInOther?_isSome, Option.get_some, colorMap_append_inl, + true_implies, Option.isNone_none, getDual?_inl_of_getDual?_isNone_getDualInOther?_isSome, + colorMap_append_inr] | Sum.inr k => have hn := l2.append_inr_not_mem_withDual_of_withDualInOther l k hj by_cases hk' : (l.getDual? k).isSome @@ -126,6 +138,123 @@ lemma symm (hu : (l ++ l2).withUniqueDual = (l ++ l2).withDual) (h : ColorCond ( lemma inr (hu : (l ++ l2).withUniqueDual = (l ++ l2).withDual) (h : ColorCond (l ++ l2)) : ColorCond l2 := inl (symm hu h) +lemma triple_right (hu : (l ++ l2 ++ l3).withUniqueDual = (l ++ l2 ++ l3).withDual) + (h : ColorCond (l ++ l2 ++ l3)) : ColorCond (l2 ++ l3) := by + have h1 := assoc h + rw [append_assoc] at hu + exact h1.inr hu + +lemma triple_drop_mid (hu : (l ++ l2 ++ l3).withUniqueDual = (l ++ l2 ++ l3).withDual) + (h : ColorCond (l ++ l2 ++ l3)) : ColorCond (l ++ l3) := by + rw [append_assoc] at hu + refine ((((assoc h).symm hu).assoc).inr ?_).symm ?_ + rw [append_withDual_eq_withUniqueDual_symm, append_assoc] at hu + exact hu + rw [append_withDual_eq_withUniqueDual_symm, append_assoc] at hu + exact append_withDual_eq_withUniqueDual_inr _ _ hu + + +lemma swap (hu : (l ++ l2 ++ l3).withUniqueDual = (l ++ l2 ++ l3).withDual) + (h : ColorCond (l ++ l2 ++ l3)) : + ColorCond (l2 ++ l ++ l3) := by + have hC := h + have hu' := hu + rw [iff_on_isSome] at h ⊢ + intro j hj + obtain ⟨k, hk⟩ := appendEquiv.surjective j + subst hk + match k with + | Sum.inl k => + have hj' := hj + rw [append_withDual_eq_withUniqueDual_swap] at hu + rw [← mem_withDual_iff_isSome, ← hu] at hj' + have hn := (l2 ++ l).append_inl_not_mem_withDual_of_withDualInOther l3 k hj' + simp only [mem_withDual_iff_isSome, mem_withInDualOther_iff_isSome, Bool.not_eq_true, + Option.not_isSome, Option.isNone_iff_eq_none] at hn + simp only [getDual?_isSome_append_inl_iff] at hj + by_cases hk' : ((l2 ++ l).getDual? k).isSome + · simp only [hk', getDual?_append_inl_of_getDual?_isSome, Option.get_some, colorMap_append_inl] + have hu' := append_withDual_eq_withUniqueDual_inl (l2 ++ l) l3 hu + have hC' := hC.inl.symm ((append_withDual_eq_withUniqueDual_symm l2 l).mp hu') + rw [iff_on_isSome] at hC' + exact hC' k hk' + · simp only [hk', Bool.false_eq_true, false_iff] at hn + rw [← @Option.not_isSome_iff_eq_none, not_not] at hn + simp_all only [mem_withDual_iff_isSome, Bool.false_eq_true, or_true, Bool.not_eq_true, + Option.not_isSome, Option.isNone_iff_eq_none, Option.isNone_none, + getDual?_inl_of_getDual?_isNone_getDualInOther?_isSome, Option.get_some, + colorMap_append_inr, colorMap_append_inl] + obtain ⟨k', hk'⟩ := appendEquiv.surjective k + subst hk' + match k' with + | Sum.inl k' => + simp at hn + simp + have hL := triple_right hu' hC + rw [iff_on_isSome] at hL + have hL' := hL (appendEquiv (Sum.inl k')) (by simp [hn]) + simp_all only [Option.isNone_none, getDualInOther?_append_of_inl, + getDual?_inl_of_getDual?_isNone_getDualInOther?_isSome, Option.isSome_some, + getDual?_eq_none_append_inl_iff, Option.get_some, colorMap_append_inr, + colorMap_append_inl] + | Sum.inr k' => + simp at hn + simp + have hR := triple_drop_mid hu' hC + rw [iff_on_isSome] at hR + have hR' := hR (appendEquiv (Sum.inl k')) (by simp [hn]) + simp_all only [Option.isNone_none, getDualInOther?_append_of_inr, + getDual?_inl_of_getDual?_isNone_getDualInOther?_isSome, Option.isSome_some, + getDual?_eq_none_append_inr_iff, Option.get_some, colorMap_append_inr, + colorMap_append_inl] + | Sum.inr k => + have hj' := hj + rw [append_withDual_eq_withUniqueDual_swap] at hu + rw [← mem_withDual_iff_isSome, ← hu] at hj' + have hn := (l2 ++ l).append_inr_not_mem_withDual_of_withDualInOther l3 k hj' + simp only [mem_withDual_iff_isSome, mem_withInDualOther_iff_isSome, + getDualInOther?_isSome_of_append_iff, not_or, Bool.not_eq_true, Option.not_isSome, + Option.isNone_iff_eq_none] at hn + by_cases hk' : (l3.getDual? k).isSome + · simp_all only [mem_withDual_iff_isSome, true_iff, Option.isNone_iff_eq_none, + getDualInOther?_eq_none_of_append_iff, and_self, + getDual?_inr_getDualInOther?_isNone_getDual?_isSome, Option.get_some, colorMap_append_inr] + have hRR := hC.inr hu' + rw [iff_on_isSome] at hRR + exact hRR k hk' + · simp_all only [mem_withDual_iff_isSome, Bool.false_eq_true, false_iff, not_and, + Bool.not_eq_true, Option.not_isSome, Option.isNone_iff_eq_none, colorMap_append_inr] + by_cases hk'' : (l3.getDualInOther? l2 k).isSome + · simp_all only [getDualInOther?_of_append_of_isSome, Option.isSome_some, + getDual?_append_inr_getDualInOther?_isSome, Option.get_some, colorMap_append_inl] + have hL := triple_right hu' hC + rw [iff_on_isSome] at hL + have hL' := hL (appendEquiv (Sum.inr k)) (by simp [hk'']) + simp_all only [getDualInOther?_of_append_of_isSome, Option.isSome_some, + getDual?_append_inr_getDualInOther?_isSome, Option.get_some, colorMap_append_inl, + colorMap_append_inr] + · simp_all + rw [← @Option.not_isSome_iff_eq_none, not_not] at hn + simp_all + have hR := triple_drop_mid hu' hC + rw [iff_on_isSome] at hR + have hR' := hR (appendEquiv (Sum.inr k)) (by simp [hn]) + simp_all only [getDualInOther?_of_append_of_isNone_isSome, Option.isSome_some, + getDual?_append_inr_getDualInOther?_isSome, Option.get_some, colorMap_append_inl, + colorMap_append_inr] + +/- l.getDual? = Option.map (𝓒.τ ∘ l.colorMap) ∘ + Option.guard fun i => (l.getDual? i).isSome -/ +def bool (l : IndexList 𝓒.Color) : Bool := + if (∀ (i : l.withDual), 𝓒.τ + (l.colorMap ((l.getDual? i).get (l.withDual_isSome i))) = l.colorMap i) then + true + else false + +lemma iff_bool : l.ColorCond ↔ bool l := by + rw [iff_withDual, bool] + simp + end ColorCond @@ -145,8 +274,9 @@ namespace ColorIndexList variable {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color] variable (l l2 : ColorIndexList 𝓒) -open IndexList +open IndexList TensorColor +instance : Coe (ColorIndexList 𝓒) (IndexList 𝓒.Color) := ⟨fun l => l.toIndexList⟩ def empty : ColorIndexList 𝓒 where val := ∅ unique_duals := by @@ -154,7 +284,6 @@ def empty : ColorIndexList 𝓒 where dual_color := by rfl -@[simp] def colorMap' : 𝓒.ColorMap (Fin l.length) := l.colorMap @@ -166,6 +295,21 @@ lemma ext {l l' : ColorIndexList 𝓒} (h : l.val = l'.val) : l = l' := by apply IndexList.ext exact h + +/-! TODO: `orderEmbOfFin_univ` should be replaced with a mathlib lemma if possible. -/ +lemma orderEmbOfFin_univ (n m : ℕ) (h : n = m): + Finset.orderEmbOfFin (Finset.univ : Finset (Fin n)) (by simp [h]: Finset.univ.card = m) = + (Fin.castOrderIso h.symm).toOrderEmbedding := by + symm + have h1 : (Fin.castOrderIso h.symm).toFun = + ( Finset.orderEmbOfFin (Finset.univ : Finset (Fin n)) (by simp [h]: Finset.univ.card = m)).toFun := by + apply Finset.orderEmbOfFin_unique + intro x + exact Finset.mem_univ ((Fin.castOrderIso (Eq.symm h)).toFun x) + exact fun ⦃a b⦄ a => a + exact Eq.symm (Fin.orderEmbedding_eq (congrArg Set.range (id (Eq.symm h1)))) + + /-! ## Contracting an `ColorIndexList` @@ -185,6 +329,40 @@ lemma contr_contr : l.contr.contr = l.contr := by apply ext simp [contr] +@[simp] +lemma contr_contr_idMap (i : Fin l.contr.contr.length) : + l.contr.contr.idMap i = l.contr.idMap (Fin.cast (by simp) i) := by + simp [contr] + apply congrArg + simp [withoutDualEquiv] + have h1 : l.contrIndexList.withoutDual = Finset.univ := by + have hx := l.contrIndexList.withDual_union_withoutDual + have hx2 := l.contrIndexList_withDual + simp_all + simp [h1] + rw [orderEmbOfFin_univ] + rfl + rw [h1] + simp + +@[simp] +lemma contr_of_withDual_empty (h : l.withDual = ∅) : + l.contr = l := by + simp [contr] + apply ext + simp [l.contrIndexList_of_withDual_empty h] + +@[simp] +lemma contr_getDual?_eq_none (i : Fin l.contr.length) : + l.contr.getDual? i = none := by + simp only [contr, contrIndexList_getDual?] + +@[simp] +lemma contr_areDualInSelf (i j : Fin l.contr.length) : + l.contr.AreDualInSelf i j ↔ False := by + simp [contr] + + /-! ## Contract equiv @@ -197,6 +375,57 @@ def contrEquiv : (l.withUniqueDualLT ⊕ l.withUniqueDualLT) ⊕ Fin l.contr.len simp [l.unique_duals])) (Fin.castOrderIso l.contrIndexList_length).toEquiv).trans <| l.dualEquiv +lemma contrEquiv_inl_inl_isSome (i : l.withUniqueDualLT) : + (l.getDual? (l.contrEquiv (Sum.inl (Sum.inl i)))).isSome := by + change (l.getDual? i).isSome + have h1 : i.1 ∈ l.withUniqueDual := by + have hi2 := i.2 + simp [withUniqueDualLT] at hi2 + exact hi2.1 + exact mem_withUniqueDual_isSome l.toIndexList (↑i) h1 + +@[simp] +lemma contrEquiv_inl_inr_eq (i : l.withUniqueDualLT) : + (l.contrEquiv (Sum.inl (Sum.inr i))) = + (l.getDual? i.1).get (l.contrEquiv_inl_inl_isSome i) := by + rfl + +@[simp] +lemma contrEquiv_inl_inl_eq (i : l.withUniqueDualLT) : + (l.contrEquiv (Sum.inl (Sum.inl i))) = i := by + rfl + +lemma contrEquiv_colorMapIso : + ColorMap.MapIso (Equiv.refl (Fin l.contr.length)) + (ColorMap.contr l.contrEquiv l.colorMap) l.contr.colorMap := by + simp [ColorMap.MapIso, ColorMap.contr] + funext i + simp [contr] + rfl + +lemma contrEquiv_contrCond : ColorMap.ContrCond l.contrEquiv l.colorMap := by + simp [ColorMap.ContrCond] + funext i + simp + have h1 := l.dual_color + rw [ColorCond.iff_on_isSome] at h1 + exact (h1 i.1 _).symm + +@[simp] +lemma contrEquiv_on_withDual_empty (i : Fin l.contr.length) (h : l.withDual = ∅) : + l.contrEquiv (Sum.inr i) = Fin.cast (by simp [h]) i := by + simp [contrEquiv] + change l.dualEquiv (Sum.inr ((Fin.castOrderIso _).toEquiv i)) = _ + simp [dualEquiv, withoutDualEquiv] + have h : l.withoutDual = Finset.univ := by + have hx := l.withDual_union_withoutDual + simp_all + simp [h] + rw [orderEmbOfFin_univ] + rfl + rw [h] + simp + /-! ## Append @@ -208,17 +437,6 @@ def AppendCond : Prop := (l.toIndexList ++ l2.toIndexList).withUniqueDual = (l.toIndexList ++ l2.toIndexList).withDual ∧ ColorCond (l.toIndexList ++ l2.toIndexList) -namespace AppendCond - -variable {l l2 l3 : ColorIndexList 𝓒} - -lemma symm (h : AppendCond l l2) : AppendCond l2 l := by - apply And.intro _ (h.2.symm h.1) - rw [append_withDual_eq_withUniqueDual_symm] - exact h.1 - -end AppendCond - def append (h : AppendCond l l2) : ColorIndexList 𝓒 where toIndexList := l.toIndexList ++ l2.toIndexList unique_duals := h.1.symm @@ -235,6 +453,11 @@ namespace AppendCond variable {l l2 l3 : ColorIndexList 𝓒} +lemma symm (h : AppendCond l l2) : AppendCond l2 l := by + apply And.intro _ (h.2.symm h.1) + rw [append_withDual_eq_withUniqueDual_symm] + exact h.1 + lemma inr (h : AppendCond l l2) (h' : AppendCond (l ++[h] l2) l3) : AppendCond l2 l3 := by apply And.intro @@ -259,9 +482,44 @@ lemma assoc (h : AppendCond l l2) (h' : AppendCond (l ++[h] l2) l3) : rw [← append_assoc] exact h'.2 +lemma swap (h : AppendCond l l2) (h' : AppendCond (l ++[h] l2) l3) : + AppendCond (l2 ++[h.symm] l) l3:= by + apply And.intro + · simp + rw [← append_withDual_eq_withUniqueDual_swap] + simpa using h'.1 + · exact ColorCond.swap h'.1 h'.2 +/- +(l ++ l2).withUniqueDual = (l ++ l2).withDual ↔ + l.withUniqueDual = l.withDual ∧ l2.withUniqueDual = l2.withDual + ∧ l.withUniqueDualInOther l2 = l.withDualInOther l2 ∧ + l2.withUniqueDualInOther l = l2.withDualInOther l -/ +lemma appendCond_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) + (h5 : ColorCond.bool (l.toIndexList ++ l2.toIndexList)) : + AppendCond l l2 := by + rw [AppendCond] + rw [append_withDual_eq_withUniqueDual_iff'] + simp_all + exact ColorCond.iff_bool.mpr h5 + +def bool (l l2 : ColorIndexList 𝓒) : Bool := + if ¬ (l.toIndexList ++ l2.toIndexList).withUniqueDual = (l.toIndexList ++ l2.toIndexList).withDual then + false + else + ColorCond.bool (l.toIndexList ++ l2.toIndexList) + +lemma iff_bool (l l2 : ColorIndexList 𝓒) : AppendCond l l2 ↔ bool l l2 := by + rw [AppendCond] + simp [bool] + rw [ColorCond.iff_bool] + simp end AppendCond + end ColorIndexList end IndexNotation diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Dual.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Dual.lean index 0c17436..3d982da 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Dual.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Dual.lean @@ -256,6 +256,14 @@ lemma getDualInOther?_getDualInOther?_get_isSome (i : Fin l.length) rw [getDualInOther?, Fin.isSome_find_iff] exact ⟨i, by simp⟩ +@[simp] +lemma getDualInOther?_self_isSome (i : Fin l.length) : + (l.getDualInOther? l i).isSome := by + simp [getDualInOther?] + rw [@Fin.isSome_find_iff] + use i + simp [AreDualInOther] + /-! ## Append properties of getDual? @@ -675,6 +683,7 @@ lemma append_withDualInOther_eq : | Sum.inr k => simp + lemma withDualInOther_append_eq : l.withDualInOther (l2 ++ l3) = l.withDualInOther l2 ∪ l.withDualInOther l3 := by ext i @@ -806,6 +815,22 @@ lemma getDual?_getDual?_of_withUniqueDual (i : Fin l.length) (h : i ∈ l.withUn rw [Option.some_bind'] simp [h] +@[simp] +lemma getDual?_get_of_mem_withUnique_mem (i : Fin l.length) (h : i ∈ l.withUniqueDual) : + (l.getDual? i).get (l.mem_withUniqueDual_isSome i h) ∈ l.withUniqueDual := by + simp [withUniqueDual, h] + intro j hj + have h1 : i = j := by + by_contra hn + have h' : l.AreDualInSelf i j := by + simp [AreDualInSelf, hn] + simp_all [AreDualInSelf] + simp [h] at h' + subst h' + simp_all + subst h1 + exact Eq.symm (getDual?_getDual?_get_of_withUniqueDual l i h) + /-! @@ -872,6 +897,62 @@ lemma getDualInOther?_getDualInOther?_of_withUniqueDualInOther rw [Option.some_bind'] simp [h] +lemma eq_of_areDualInOther_withUniqueDualInOther {j k : Fin l2.length} (i : l.withUniqueDualInOther l2) + (hj : l.AreDualInOther l2 i j) (hk : l.AreDualInOther l2 i k) : j = k := by + simp at hj hk + exact hj.trans hk.symm + +lemma getDual?_of_getDualInOther?_of_mem_withUniqueInOther_eq_none (i : Fin l.length) + (h : i ∈ l.withUniqueDualInOther l2) : + l2.getDual? ((l.getDualInOther? l2 i).get (l.mem_withUniqueDualInOther_isSome l2 i h)) = none + := by + by_contra hn + rw [← @Option.not_isSome_iff_eq_none, not_not] at hn + rw [@getDual?_isSome_iff_exists] at hn + obtain ⟨j, hj⟩ := hn + have hx : l.AreDualInOther l2 i j := by + simp [AreDualInOther, hj] + simp [AreDualInSelf] at hj + exact hj.2 + have hn := l.eq_of_areDualInOther_withUniqueDualInOther l2 ⟨i, h⟩ hx + (getDualInOther?_areDualInOther_get l l2 i (mem_withUniqueDualInOther_isSome l l2 i h)) + subst hn + simp_all + +@[simp] +lemma getDualInOther?_get_of_mem_withUniqueInOther_mem (i : Fin l.length) + (h : i ∈ l.withUniqueDualInOther l2) : + (l.getDualInOther? l2 i).get (l.mem_withUniqueDualInOther_isSome l2 i h) ∈ l2.withUniqueDualInOther l := by + 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, + getDualInOther?_getDualInOther?_get_isSome, true_and] + apply And.intro + exact getDual?_of_getDualInOther?_of_mem_withUniqueInOther_eq_none l l2 i h + intro j hj + simp [h] + by_contra hn + have hx : l.AreDualInSelf i j := by + simp [AreDualInSelf, hn] + simp [AreDualInOther] at hj + simp [hj] + exact fun a => hn (id (Eq.symm a)) + simp only [withUniqueDualInOther, mem_withDual_iff_isSome, getDual?, 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 + rw [Fin.find_eq_none_iff] at h + simp_all only + + + +@[simp] +lemma getDualInOther?_self_of_mem_withUniqueInOther (i : Fin l.length) + (h : i ∈ l.withUniqueDualInOther l) : + l.getDualInOther? l i = some i := by + rw [all_dual_eq_of_withUniqueDualInOther l l i h i rfl] + + + + /-! ## Properties of getDual?, withUniqueDual and append @@ -894,6 +975,762 @@ lemma append_inl_not_mem_withDual_of_withDualInOther (i : Fin l.length) simp only [getDual?_isSome_append_inl_iff] at ht simp_all + +lemma append_inr_not_mem_withDual_of_withDualInOther (i : Fin l2.length) + (h : appendEquiv (Sum.inr i) ∈ (l ++ l2).withUniqueDual) : + i ∈ l2.withDual ↔ ¬ i ∈ l2.withDualInOther l := by + refine Iff.intro (fun hs => ?_) (fun ho => ?_) + · by_contra ho + obtain ⟨j, hj⟩ := (l2.mem_withDual_iff_exists).mp hs + obtain ⟨k, hk⟩ := (l2.mem_withInDualOther_iff_exists l).mp ho + have h1 : appendEquiv (Sum.inr j) = appendEquiv (Sum.inl k) := by + refine (l ++ l2).eq_of_areDualInSelf_withUniqueDual ⟨appendEquiv (Sum.inr i), h⟩ ?_ ?_ + simpa using hj + simpa using hk + simp at h1 + · have ht : ((l ++ l2).getDual? (appendEquiv (Sum.inr i))).isSome := by simp [h] + simp only [getDual?_isSome_append_inr_iff] at ht + simp_all + + +lemma getDual?_append_symm_of_withUniqueDual_of_inl (i : Fin l.length) (k : Fin l2.length) + (h : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual) : + (l ++ l2).getDual? (appendEquiv (Sum.inl i)) = some (appendEquiv (Sum.inr k)) + ↔ (l2 ++ l).getDual? (appendEquiv (Sum.inr i)) = some (appendEquiv (Sum.inl k)) := by + have h := l.append_inl_not_mem_withDual_of_withDualInOther l2 i h + by_cases hs : (l.getDual? i).isSome + <;> by_cases ho : (l.getDualInOther? l2 i).isSome + <;> simp_all [hs, ho] + +lemma getDual?_append_symm_of_withUniqueDual_of_inl' (i k : Fin l.length) + (h : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual) : + (l ++ l2).getDual? (appendEquiv (Sum.inl i)) = some (appendEquiv (Sum.inl k)) + ↔ (l2 ++ l).getDual? (appendEquiv (Sum.inr i)) = some (appendEquiv (Sum.inr k)) := by + have h := l.append_inl_not_mem_withDual_of_withDualInOther l2 i h + by_cases hs : (l.getDual? i).isSome + <;> by_cases ho : (l.getDualInOther? l2 i).isSome + <;> simp_all [hs, ho] + +lemma getDual?_append_symm_of_withUniqueDual_of_inr (i : Fin l2.length) (k : Fin l.length) + (h : appendEquiv (Sum.inr i) ∈ (l ++ l2).withUniqueDual) : + (l ++ l2).getDual? (appendEquiv (Sum.inr i)) = some (appendEquiv (Sum.inl k)) + ↔ (l2 ++ l).getDual? (appendEquiv (Sum.inl i)) = some (appendEquiv (Sum.inr k)) := by + have h := l.append_inr_not_mem_withDual_of_withDualInOther l2 i h + by_cases hs : (l2.getDual? i).isSome + <;> by_cases ho : (l2.getDualInOther? l i).isSome + <;> simp_all [hs, ho] + +lemma getDual?_append_symm_of_withUniqueDual_of_inr' (i k : Fin l2.length) + (h : appendEquiv (Sum.inr i) ∈ (l ++ l2).withUniqueDual) : + (l ++ l2).getDual? (appendEquiv (Sum.inr i)) = some (appendEquiv (Sum.inr k)) + ↔ (l2 ++ l).getDual? (appendEquiv (Sum.inl i)) = some (appendEquiv (Sum.inl k)) := by + have h := l.append_inr_not_mem_withDual_of_withDualInOther l2 i h + by_cases hs : (l2.getDual? i).isSome + <;> by_cases ho : (l2.getDualInOther? l i).isSome + <;> simp_all [hs, ho] + +lemma mem_withUniqueDual_append_symm (i : Fin l.length) : + appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual ↔ + appendEquiv (Sum.inr i) ∈ (l2 ++ l).withUniqueDual := by + simp only [withUniqueDual, mem_withDual_iff_isSome, Finset.mem_filter, Finset.mem_univ, + getDual?_isSome_append_inl_iff, true_and, getDual?_isSome_append_inr_iff, and_congr_right_iff] + intro h + refine Iff.intro (fun h' j hj => ?_) (fun h' j hj => ?_) + · obtain ⟨k, hk⟩ := appendEquiv.surjective j + subst hk + match k with + | Sum.inl k => + have hk' := h' (appendEquiv (Sum.inr k)) + simp only [AreDualInSelf.append_inl_inr] at hk' + simp only [AreDualInSelf.append_inr_inl] at hj + refine ((l.getDual?_append_symm_of_withUniqueDual_of_inl l2 _ _ ?_).mp (hk' hj).symm).symm + simp_all only [AreDualInSelf.append_inl_inr, imp_self, withUniqueDual, + mem_withDual_iff_isSome, Finset.mem_filter, Finset.mem_univ, getDual?_isSome_append_inl_iff, + implies_true, and_self, mem_withUniqueDual_isSome, eq_getDual?_get_of_withUniqueDual_iff, + getDual?_areDualInSelf_get] + | Sum.inr k => + have hk' := h' (appendEquiv (Sum.inl k)) + simp only [AreDualInSelf.append_inl_inl] at hk' + simp only [AreDualInSelf.append_inr_inr] at hj + refine ((l.getDual?_append_symm_of_withUniqueDual_of_inl' l2 _ _ ?_).mp (hk' hj).symm).symm + simp_all only [AreDualInSelf.append_inl_inl, imp_self, withUniqueDual, + mem_withDual_iff_isSome, Finset.mem_filter, Finset.mem_univ, getDual?_isSome_append_inl_iff, + implies_true, and_self, mem_withUniqueDual_isSome, eq_getDual?_get_of_withUniqueDual_iff, + getDual?_areDualInSelf_get] + · obtain ⟨k, hk⟩ := appendEquiv.surjective j + subst hk + match k with + | Sum.inl k => + have hk' := h' (appendEquiv (Sum.inr k)) + simp only [AreDualInSelf.append_inr_inr] at hk' + simp only [AreDualInSelf.append_inl_inl] at hj + refine ((l2.getDual?_append_symm_of_withUniqueDual_of_inr' l _ _ ?_).mp (hk' hj).symm).symm + simp_all only [AreDualInSelf.append_inr_inr, imp_self, withUniqueDual, + mem_withDual_iff_isSome, Finset.mem_filter, Finset.mem_univ, getDual?_isSome_append_inr_iff, + implies_true, and_self, mem_withUniqueDual_isSome, eq_getDual?_get_of_withUniqueDual_iff, + getDual?_areDualInSelf_get] + | Sum.inr k => + have hk' := h' (appendEquiv (Sum.inl k)) + simp only [AreDualInSelf.append_inr_inl] at hk' + simp only [AreDualInSelf.append_inl_inr] at hj + refine ((l2.getDual?_append_symm_of_withUniqueDual_of_inr l _ _ ?_).mp (hk' hj).symm).symm + simp_all only [AreDualInSelf.append_inr_inl, imp_self, withUniqueDual, + mem_withDual_iff_isSome, Finset.mem_filter, Finset.mem_univ, getDual?_isSome_append_inr_iff, + implies_true, and_self, mem_withUniqueDual_isSome, eq_getDual?_get_of_withUniqueDual_iff, + getDual?_areDualInSelf_get] + +@[simp] +lemma not_mem_withDualInOther_of_inl_mem_withUniqueDual (i : Fin l.length) + (h : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual) (hs : i ∈ l.withUniqueDual) : + ¬ i ∈ l.withUniqueDualInOther l2 := by + have hn := l.append_inl_not_mem_withDual_of_withDualInOther l2 i h + simp_all + by_contra ho + have ho' : (l.getDualInOther? l2 i).isSome := by + simp [ho] + simp_all [Option.isSome_none, Bool.false_eq_true] + +@[simp] +lemma not_mem_withUniqueDual_of_inl_mem_withUnqieuDual (i : Fin l.length) + (h : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual) (hi : i ∈ l.withUniqueDualInOther l2) : + ¬ i ∈ l.withUniqueDual := by + have hn := l.append_inl_not_mem_withDual_of_withDualInOther l2 i h + simp_all + by_contra hs + simp_all [Option.isSome_none, Bool.false_eq_true] + +@[simp] +lemma mem_withUniqueDual_of_inl (i : Fin l.length) + (h : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual) (hi : (l.getDual? i).isSome) : + i ∈ l.withUniqueDual := by + simp only [withUniqueDual, mem_withDual_iff_isSome, Finset.mem_filter, Finset.mem_univ, + getDual?_isSome_append_inl_iff, true_and] at h ⊢ + apply And.intro hi + intro j hj + have hj' := h.2 (appendEquiv (Sum.inl j)) + simp at hj' + have hj'' := hj' hj + simp [hi] at hj'' + simp_all + +@[simp] +lemma mem_withUniqueDualInOther_of_inl_withDualInOther (i : Fin l.length) + (h : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual) (hi : (l.getDualInOther? l2 i).isSome) : + i ∈ l.withUniqueDualInOther l2 := by + 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] + have hn := l.append_inl_not_mem_withDual_of_withDualInOther l2 i h + simp_all only [mem_withDual_iff_isSome, mem_withInDualOther_iff_isSome, not_true_eq_false, + iff_false, Bool.not_eq_true, Option.not_isSome, Option.isNone_iff_eq_none, true_and] + intro j hj + simp only [withUniqueDual, mem_withDual_iff_isSome, Finset.mem_filter, Finset.mem_univ, + getDual?_isSome_append_inl_iff, true_and] at h + have hj' := h.2 (appendEquiv (Sum.inr j)) + simp only [AreDualInSelf.append_inl_inr] at hj' + have hj'' := hj' hj + simp [hi, hn] at hj'' + simp_all + +lemma withUniqueDual_iff_not_withUniqueDualInOther_of_inl_withUniqueDualInOther + (i : Fin l.length) (h : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual) : + 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 + have hn := l.append_inl_not_mem_withDual_of_withDualInOther l2 i h + simp_all + simp [withUniqueDual] + simp_all + have hx : (l.getDualInOther? l2 i).isSome := by + rw [← @Option.isNone_iff_eq_none] at hn + rw [← @Option.not_isSome] at hn + exact Eq.symm ((fun {a b} => Bool.not_not_eq.mp) fun a => hn (id (Eq.symm a))) + simp_all + +lemma append_inl_mem_withUniqueDual_of_withUniqueDual (i : Fin l.length) + (h : i ∈ l.withUniqueDual) (hn : i ∉ l.withDualInOther l2) : + appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual := by + simp [withUniqueDual] + apply And.intro + simp_all + intro j hj + obtain ⟨k, hk⟩ := appendEquiv.surjective j + subst hk + match k with + | Sum.inl k => simp_all + | Sum.inr k => + simp at hj + refine False.elim (hn ?_) + exact (l.mem_withInDualOther_iff_exists _).mpr ⟨k, hj⟩ + +lemma append_inl_mem_of_withUniqueDualInOther (i : Fin l.length) + (ho : i ∈ l.withUniqueDualInOther l2) : + appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual := by + simp only [withUniqueDual, mem_withDual_iff_isSome, Finset.mem_filter, Finset.mem_univ, + getDual?_isSome_append_inl_iff, true_and] + apply And.intro + simp_all only [mem_withUniqueDualInOther_isSome, or_true] + intro j hj + obtain ⟨k, hk⟩ := appendEquiv.surjective j + subst hk + have hs := l.not_mem_withDual_of_withUniqueDualInOther l2 ⟨i, ho⟩ + match k with + | Sum.inl k => + refine False.elim (hs ?_) + simp at hj + exact (l.mem_withDual_iff_exists).mpr ⟨k, hj⟩ + | Sum.inr k => + simp_all + +@[simp] +lemma append_inl_mem_withUniqueDual_iff (i : Fin l.length) : + appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual ↔ + ((i ∈ l.withUniqueDual ∧ i ∉ l.withDualInOther l2) ↔ ¬ i ∈ l.withUniqueDualInOther l2) := by + apply Iff.intro + · intro h + apply Iff.intro + · intro hs + exact (l.withUniqueDual_iff_not_withUniqueDualInOther_of_inl_withUniqueDualInOther l2 i + h).mp hs.1 + · intro ho + have hs := ((l.withUniqueDual_iff_not_withUniqueDualInOther_of_inl_withUniqueDualInOther l2 i + h).mpr ho) + apply And.intro hs + refine (l.append_inl_not_mem_withDual_of_withDualInOther l2 i h).mp ?_ + exact (l.mem_withDual_of_withUniqueDual ⟨i, hs⟩) + · intro h + by_cases ho : i ∈ l.withUniqueDualInOther l2 + · exact append_inl_mem_of_withUniqueDualInOther l l2 i ho + · exact append_inl_mem_withUniqueDual_of_withUniqueDual l l2 i (h.mpr ho).1 (h.mpr ho).2 + +@[simp] +lemma append_inr_mem_withUniqueDual_iff (i : Fin l2.length) : + appendEquiv (Sum.inr i) ∈ (l ++ l2).withUniqueDual ↔ + ((i ∈ l2.withUniqueDual ∧ i ∉ l2.withDualInOther l) ↔ ¬ i ∈ l2.withUniqueDualInOther l) := by + rw [← mem_withUniqueDual_append_symm] + simp + +lemma append_withUniqueDual : (l ++ l2).withUniqueDual = + Finset.map (l.appendInl l2) ((l.withUniqueDual ∩ (l.withDualInOther l2)ᶜ) ∪ l.withUniqueDualInOther l2) + ∪ Finset.map (l.appendInr l2) ((l2.withUniqueDual ∩ (l2.withDualInOther l)ᶜ) ∪ l2.withUniqueDualInOther l) := by + rw [Finset.ext_iff] + intro j + obtain ⟨k, hk⟩ := appendEquiv.surjective j + subst hk + match k with + | Sum.inl k => + simp only [append_inl_mem_withUniqueDual_iff, Finset.mem_union] + apply Iff.intro + · intro h + apply Or.inl + simp only [Finset.mem_map, Finset.mem_union, Finset.mem_inter, Finset.mem_compl, + mem_withInDualOther_iff_isSome, Bool.not_eq_true, Option.not_isSome, + Option.isNone_iff_eq_none] + use k + simp only [appendInl, Function.Embedding.coeFn_mk, Function.comp_apply, and_true] + by_cases hk : k ∈ l.withUniqueDualInOther l2 + simp_all + have hk' := h.mpr hk + simp_all + · intro h + simp at h + cases' h with h h + · obtain ⟨j, hj⟩ := h + have hjk : j = k := by + simp [appendInl] at hj + exact hj.2 + subst hjk + have hj1 := hj.1 + cases' hj1 with hj1 hj1 + · simp_all + by_contra hn + have h' := l.mem_withDualInOther_of_withUniqueDualInOther l2 ⟨j, hn⟩ + simp_all only [mem_withInDualOther_iff_isSome, Option.isSome_none, Bool.false_eq_true] + · simp_all only [or_true, true_and, mem_withInDualOther_iff_isSome, + mem_withUniqueDualInOther_isSome, not_true_eq_false, and_false] + · obtain ⟨j, hj⟩ := h + simp [appendInr] at hj + | Sum.inr k => + simp only [append_inr_mem_withUniqueDual_iff, Finset.mem_union] + apply Iff.intro + · intro h + apply Or.inr + simp + use k + simp [appendInr] + by_cases hk : k ∈ l2.withUniqueDualInOther l + simp_all only [mem_withInDualOther_iff_isSome, mem_withUniqueDualInOther_isSome, + not_true_eq_false, and_false, or_true] + have hk' := h.mpr hk + simp_all only [not_false_eq_true, and_self, mem_withInDualOther_iff_isSome, Bool.not_eq_true, + Option.not_isSome, Option.isNone_iff_eq_none, or_false] + · intro h + simp at h + cases' h with h h + · obtain ⟨j, hj⟩ := h + simp [appendInl] at hj + · obtain ⟨j, hj⟩ := h + have hjk : j = k := by + simp [appendInr] at hj + exact hj.2 + subst hjk + have hj1 := hj.1 + cases' hj1 with hj1 hj1 + · simp_all + by_contra hn + have h' := l2.mem_withDualInOther_of_withUniqueDualInOther l ⟨j, hn⟩ + simp_all + · simp_all + +lemma append_withUniqueDual_disjSum : (l ++ l2).withUniqueDual = + Equiv.finsetCongr appendEquiv + (((l.withUniqueDual ∩ (l.withDualInOther l2)ᶜ) ∪ l.withUniqueDualInOther l2).disjSum + ((l2.withUniqueDual ∩ (l2.withDualInOther l)ᶜ) ∪ l2.withUniqueDualInOther l)) := by + rw [← Equiv.symm_apply_eq] + simp [append_withUniqueDual] + rw [Finset.map_union] + rw [Finset.map_map, Finset.map_map] + ext1 a + cases a with + | inl val => simp + | inr val_1 => simp + +/-! + +## Properties of getDualInOther?, withUniqueDualInOther and appendInOther + +-/ + + + +lemma mem_append_withUniqueDualInOther_symm (i : Fin l.length) : + appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDualInOther l3 ↔ + appendEquiv (Sum.inr i) ∈ (l2 ++ l).withUniqueDualInOther l3 := by + 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, + getDual?_eq_none_append_inl_iff, getDualInOther?_append_of_inl, AreDualInOther.append_of_inl, + true_and, getDual?_eq_none_append_inr_iff, getDualInOther?_append_of_inr, + AreDualInOther.append_of_inr] + +@[simp] +lemma withUniqueDualInOther_append_not_isSome_snd_of_isSome_fst (i : Fin l.length) + (h1 : i ∈ l.withUniqueDualInOther (l2 ++ l3)) (h2 : (l.getDualInOther? l2 i).isSome) : + (l.getDualInOther? l3 i) = none := by + by_contra hn + simp only [getDualInOther?] at h2 hn + rw [← @Option.not_isSome_iff_eq_none, not_not] at hn + rw [Fin.isSome_find_iff] at h2 hn + obtain ⟨j2, hj2⟩ := h2 + obtain ⟨j3, hj3⟩ := hn + have h1' : l.AreDualInOther (l2 ++ l3) i (appendEquiv (Sum.inl j2)) := by + simpa using hj2 + have h2 : l.AreDualInOther (l2 ++ l3) i (appendEquiv (Sum.inr j3)) := by + simpa using hj3 + have h3 := l.eq_of_areDualInOther_withUniqueDualInOther (l2 ++ l3) ⟨i, h1⟩ h1' h2 + simp only [EmbeddingLike.apply_eq_iff_eq] at h3 + +@[simp] +lemma withUniqueDualInOther_append_not_isSome_fst_of_isSome_snd (i : Fin l.length) + (h1 : i ∈ l.withUniqueDualInOther (l2 ++ l3)) (h2 : (l.getDualInOther? l3 i).isSome) : + (l.getDualInOther? l2 i) = none := by + by_contra hn + simp only [getDualInOther?] at h2 hn + rw [← @Option.not_isSome_iff_eq_none, not_not] at hn + rw [Fin.isSome_find_iff] at h2 hn + obtain ⟨j2, hj2⟩ := h2 + obtain ⟨j3, hj3⟩ := hn + have h1' : l.AreDualInOther (l2 ++ l3) i (appendEquiv (Sum.inr j2)) := by + simpa using hj2 + have h2 : l.AreDualInOther (l2 ++ l3) i (appendEquiv (Sum.inl j3)) := by + simpa using hj3 + have h3 := l.eq_of_areDualInOther_withUniqueDualInOther (l2 ++ l3) ⟨i, h1⟩ h1' h2 + simp only [EmbeddingLike.apply_eq_iff_eq] at h3 + +@[simp] +lemma withUniqueDualInOther_append_isSome_snd_of_not_isSome_fst (i : Fin l.length) + (h1 : i ∈ l.withUniqueDualInOther (l2 ++ l3)) (h2 : ¬ (l.getDualInOther? l2 i).isSome) : + (l.getDualInOther? l3 i).isSome := by + by_contra hn + simp only [withUniqueDualInOther, mem_withDual_iff_isSome, Bool.not_eq_true, Option.not_isSome, + Option.isNone_iff_eq_none, mem_withInDualOther_iff_isSome, getDualInOther?_isSome_of_append_iff, + Finset.mem_filter, Finset.mem_univ, true_and] at h1 + simp_all only [withUniqueDualInOther, Bool.not_eq_true, Option.not_isSome, Option.isNone_iff_eq_none, Option.isSome_none, + Bool.false_eq_true, or_self, false_and, and_false] + +lemma withUniqueDualInOther_append_isSome_fst_iff_not_isSome_snd (i : Fin l.length) + (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] + exact l.withUniqueDualInOther_append_not_isSome_snd_of_isSome_fst l2 l3 i h1 hs + simp [hs] + rw [← @Option.not_isSome_iff_eq_none, not_not] + exact withUniqueDualInOther_append_isSome_snd_of_not_isSome_fst l l2 l3 i h1 hs + +lemma getDualInOther?_append_symm_of_withUniqueDual_of_inl (i : Fin l.length) + (k : Fin l2.length) (h : i ∈ l.withUniqueDualInOther (l2 ++ l3)) : + l.getDualInOther? (l2 ++ l3) i = some (appendEquiv (Sum.inl k)) + ↔ l.getDualInOther? (l3 ++ l2) i = some (appendEquiv (Sum.inr k)) := by + have h := l.withUniqueDualInOther_append_isSome_fst_iff_not_isSome_snd l2 l3 i h + by_cases hs : (l.getDualInOther? l2 i).isSome + <;> by_cases ho : (l.getDualInOther? l3 i).isSome + <;> simp_all [hs] + +lemma getDualInOther?_append_symm_of_withUniqueDual_of_inr (i : Fin l.length) + (k : Fin l3.length) (h : i ∈ l.withUniqueDualInOther (l2 ++ l3)) : + l.getDualInOther? (l2 ++ l3) i = some (appendEquiv (Sum.inr k)) + ↔ l.getDualInOther? (l3 ++ l2) i = some (appendEquiv (Sum.inl k)) := by + have h := l.withUniqueDualInOther_append_isSome_fst_iff_not_isSome_snd l2 l3 i h + by_cases hs : (l.getDualInOther? l2 i).isSome + <;> by_cases ho : (l.getDualInOther? l3 i).isSome + <;> simp_all [hs] + + +lemma mem_withUniqueDualInOther_symm' (i : Fin l.length) + (h : i ∈ l.withUniqueDualInOther (l2 ++ l3)): + i ∈ l.withUniqueDualInOther (l3 ++ l2) := by + have h' := h + simp only [withUniqueDualInOther, mem_withDual_iff_isSome, Bool.not_eq_true, + Option.not_isSome, Option.isNone_iff_eq_none, mem_withInDualOther_iff_isSome, + getDualInOther?_isSome_of_append_iff, Finset.mem_filter, Finset.mem_univ, true_and, + implies_true, and_self, eq_getDualInOther?_get_of_withUniqueDualInOther_iff, + getDualInOther?_areDualInOther_get] at h ⊢ + apply And.intro h.1 + have hc := l.withUniqueDualInOther_append_isSome_fst_iff_not_isSome_snd l2 l3 i h' + by_cases h1 : (l.getDualInOther? l2 i).isSome <;> + 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 [h1, or_true, true_and] + intro j + obtain ⟨k, hk⟩ := appendEquiv.surjective j + subst hk + match k with + | Sum.inl k => + simp only [AreDualInOther.of_append_inl] + have hk'' := h.2.2 (appendEquiv (Sum.inr k)) + simp 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 => + simp only [AreDualInOther.of_append_inr] + have hk'' := h.2.2 (appendEquiv (Sum.inl k)) + simp at hk'' + exact fun h'' => ((getDualInOther?_append_symm_of_withUniqueDual_of_inl l l2 l3 i k h').mp + (hk'' h'').symm).symm + · simp only [h2, true_or, Option.some.injEq, true_and] + intro j + obtain ⟨k, hk⟩ := appendEquiv.surjective j + subst hk + match k with + | Sum.inl k => + simp only [AreDualInOther.of_append_inl] + have hk'' := h.2.2 (appendEquiv (Sum.inr k)) + simp 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 => + simp only [AreDualInOther.of_append_inr] + have hk'' := h.2.2 (appendEquiv (Sum.inl k)) + simp at hk'' + exact fun h'' => ((getDualInOther?_append_symm_of_withUniqueDual_of_inl l l2 l3 i k h').mp + (hk'' h'').symm).symm + · simp [h1] at hc + simp_all + +lemma mem_withUniqueDualInOther_symm (i : Fin l.length) : + i ∈ l.withUniqueDualInOther (l2 ++ l3) ↔ i ∈ l.withUniqueDualInOther (l3 ++ l2) := + Iff.intro (l.mem_withUniqueDualInOther_symm' l2 l3 i) + (l.mem_withUniqueDualInOther_symm' l3 l2 i) + +/-! + +## withDual equal to withUniqueDual + +-/ + + +lemma withUnqiueDual_eq_withDual_iff_unique_forall : + l.withUniqueDual = l.withDual ↔ + ∀ (i : l.withDual) j, l.AreDualInSelf i j → j = l.getDual? i := by + apply Iff.intro + · intro h i j hj + rw [@Finset.ext_iff] at h + simp [withUniqueDual] at h + refine h i ?_ j hj + simp + · intro h + apply Finset.ext + intro i + apply Iff.intro + · intro hi + simp [withUniqueDual] at hi + simpa using hi.1 + · intro hi + simp [withUniqueDual] + apply And.intro + simpa using hi + intro j hj + exact h ⟨i, hi⟩ j hj + +lemma withUnqiueDual_eq_withDual_iff : + l.withUniqueDual = l.withDual ↔ + ∀ i, (l.getDual? i).bind l.getDual? = Option.guard (fun i => i ∈ l.withDual) i := by + apply Iff.intro + · intro h i + by_cases hi : i ∈ l.withDual + · have hii : i ∈ l.withUniqueDual := by + simp_all only + change (l.getDual? i).bind l.getDual? = _ + simp [hii] + symm + rw [Option.guard_eq_some] + exact ⟨rfl, by simpa using hi⟩ + · simp at hi + simp [Option.guard, hi] + · intro h + rw [withUnqiueDual_eq_withDual_iff_unique_forall] + intro i j hj + rcases l.getDual?_of_areDualInSelf hj with hi | hi | hi + · have hj' := h j + rw [hi] at hj' + simp at hj' + rw [hj'] + symm + rw [Option.guard_eq_some, hi] + exact ⟨rfl, rfl⟩ + · exact hi.symm + · have hj' := h j + rw [hi] at hj' + rw [h i] at hj' + have hi : Option.guard (fun i => i ∈ l.withDual) ↑i = some i := by + apply Option.guard_eq_some.mpr + simp + rw [hi] at hj' + simp at hj' + have hj'' := Option.guard_eq_some.mp hj'.symm + have hj''' := hj''.1 + rw [hj'''] at hj + simp at hj + +lemma withUnqiueDual_eq_withDual_iff_list_apply : + l.withUniqueDual = l.withDual ↔ + (Fin.list l.length).map (fun i => (l.getDual? i).bind l.getDual?) = + (Fin.list l.length).map (fun i => Option.guard (fun i => i ∈ l.withDual) i) := by + rw [withUnqiueDual_eq_withDual_iff] + apply Iff.intro + intro h + apply congrFun + apply congrArg + exact (Set.eqOn_univ (fun i => (l.getDual? i).bind l.getDual?) fun i => + Option.guard (fun i => i ∈ l.withDual) i).mp fun ⦃x⦄ _ => h x + intro h + intro i + simp only [List.map_inj_left] at h + have h1 {n : ℕ} (m : Fin n) : m ∈ Fin.list n := by + have h1' : (Fin.list n)[m] = m := Fin.getElem_list _ _ + exact h1' ▸ List.getElem_mem _ _ _ + exact h i (h1 i) + +def withUnqiueDualEqWithDualBool : Bool := + if (Fin.list l.length).map (fun i => (l.getDual? i).bind l.getDual?) = + (Fin.list l.length).map (fun i => Option.guard (fun i => i ∈ l.withDual) i) then + true + else + false + +lemma withUnqiueDual_eq_withDual_iff_list_apply_bool : + l.withUniqueDual = l.withDual ↔ l.withUnqiueDualEqWithDualBool := by + rw [withUnqiueDual_eq_withDual_iff_list_apply] + apply Iff.intro + intro h + simp [withUnqiueDualEqWithDualBool, h] + intro h + simpa [withUnqiueDualEqWithDualBool] using h + +@[simp] +lemma withUnqiueDual_eq_withDual_of_empty (h : l.withDual = ∅) : + l.withUniqueDual = l.withDual := by + rw [h, Finset.eq_empty_iff_forall_not_mem] + intro x + by_contra hx + have x' : l.withDual := ⟨x, l.mem_withDual_of_withUniqueDual ⟨x, hx⟩⟩ + have hx' := x'.2 + simp [h] at hx' + +/-! + +## withUniqueDualInOther equal to withDualInOther append conditions + +-/ + +lemma withUniqueDualInOther_eq_withDualInOther_append_of_symm' + (h : (l ++ l2).withUniqueDualInOther l3 = (l ++ l2).withDualInOther l3) : + (l2 ++ l).withUniqueDualInOther l3 = (l2 ++ l).withDualInOther l3 := by + rw [Finset.ext_iff] at h ⊢ + intro j + obtain ⟨k, hk⟩ := appendEquiv.surjective j + subst hk + match k with + | Sum.inl k => + rw [mem_append_withUniqueDualInOther_symm] + simpa using h (appendEquiv (Sum.inr k)) + | Sum.inr k => + rw [← mem_append_withUniqueDualInOther_symm] + simpa using h (appendEquiv (Sum.inl k)) + +lemma withUniqueDualInOther_eq_withDualInOther_append_of_symm : + (l ++ l2).withUniqueDualInOther l3 = (l ++ l2).withDualInOther l3 ↔ + (l2 ++ l).withUniqueDualInOther l3 = (l2 ++ l).withDualInOther l3 := by + apply Iff.intro + exact l.withUniqueDualInOther_eq_withDualInOther_append_of_symm' l2 l3 + exact l2.withUniqueDualInOther_eq_withDualInOther_append_of_symm' l l3 + +lemma withUniqueDualInOther_eq_withDualInOther_of_append_symm' + (h : l.withUniqueDualInOther (l2 ++ l3) = l.withDualInOther (l2 ++ l3)) : + l.withUniqueDualInOther (l3 ++ l2) = l.withDualInOther (l3 ++ l2) := by + rw [Finset.ext_iff] at h ⊢ + intro j + rw [mem_withUniqueDualInOther_symm] + rw [h j] + simp + simp_all only [mem_withInDualOther_iff_isSome, getDualInOther?_isSome_of_append_iff] + apply Iff.intro + · intro a + cases a with + | inl h_1 => simp_all only [or_true] + | inr h_2 => simp_all only [true_or] + · intro a + cases a with + | inl h_1 => simp_all only [or_true] + | inr h_2 => simp_all only [true_or] + +lemma withUniqueDualInOther_eq_withDualInOther_of_append_symm : + l.withUniqueDualInOther (l2 ++ l3) = l.withDualInOther (l2 ++ l3) ↔ + l.withUniqueDualInOther (l3 ++ l2) = l.withDualInOther (l3 ++ l2) := by + apply Iff.intro + exact l.withUniqueDualInOther_eq_withDualInOther_of_append_symm' l2 l3 + exact l.withUniqueDualInOther_eq_withDualInOther_of_append_symm' l3 l2 + + +/-! + +## withDual equal to withUniqueDual append conditions + +-/ + + +lemma append_withDual_eq_withUniqueDual_iff : + (l ++ l2).withUniqueDual = (l ++ l2).withDual ↔ + ((l.withUniqueDual ∩ (l.withDualInOther l2)ᶜ) ∪ l.withUniqueDualInOther l2) + = l.withDual ∪ l.withDualInOther l2 + ∧ (l2.withUniqueDual ∩ (l2.withDualInOther l)ᶜ) ∪ l2.withUniqueDualInOther l + = l2.withDual ∪ l2.withDualInOther l := by + rw [append_withUniqueDual_disjSum, withDual_append_eq_disjSum] + simp + have h (s s' : Finset (Fin l.length)) (t t' : Finset (Fin l2.length)) : + s.disjSum t = s'.disjSum t' ↔ s = s' ∧ t = t' := by + simp [Finset.ext_iff] + rw [h] + +lemma append_withDual_eq_withUniqueDual_symm : + (l ++ l2).withUniqueDual = (l ++ l2).withDual ↔ + (l2 ++ l).withUniqueDual = (l2 ++ l).withDual := by + rw [append_withDual_eq_withUniqueDual_iff, append_withDual_eq_withUniqueDual_iff] + apply Iff.intro + · intro a + simp_all only [and_self] + · intro a + simp_all only [and_self] + + +@[simp] +lemma append_withDual_eq_withUniqueDual_inl (h : (l ++ l2).withUniqueDual = (l ++ l2).withDual) : + l.withUniqueDual = l.withDual := by + rw [Finset.ext_iff] + intro i + refine Iff.intro (fun h' => ?_) (fun h' => ?_) + · simp [h'] + · have hn : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual := by + rw [h] + simp_all + refine l.mem_withUniqueDual_of_inl l2 i hn ?_ + simp_all + +@[simp] +lemma append_withDual_eq_withUniqueDual_inr (h : (l ++ l2).withUniqueDual = (l ++ l2).withDual) : + l2.withUniqueDual = l2.withDual := by + rw [append_withDual_eq_withUniqueDual_symm] at h + exact append_withDual_eq_withUniqueDual_inl l2 l h + +@[simp] +lemma append_withDual_eq_withUniqueDual_withUniqueDualInOther_inl + (h : (l ++ l2).withUniqueDual = (l ++ l2).withDual) : + l.withUniqueDualInOther l2 = l.withDualInOther l2 := by + rw [Finset.ext_iff] + intro i + refine Iff.intro (fun h' => ?_) (fun h' => ?_) + · simp [h'] + · have hn : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual := by + rw [h] + simp_all + refine l.mem_withUniqueDualInOther_of_inl_withDualInOther l2 i hn ?_ + simp_all + +@[simp] +lemma append_withDual_eq_withUniqueDual_withUniqueDualInOther_inr + (h : (l ++ l2).withUniqueDual = (l ++ l2).withDual) : + l2.withUniqueDualInOther l = l2.withDualInOther l := by + rw [append_withDual_eq_withUniqueDual_symm] at h + exact append_withDual_eq_withUniqueDual_withUniqueDualInOther_inl l2 l h + +lemma append_withDual_eq_withUniqueDual_iff' : + (l ++ l2).withUniqueDual = (l ++ l2).withDual ↔ + l.withUniqueDual = l.withDual ∧ l2.withUniqueDual = l2.withDual + ∧ l.withUniqueDualInOther l2 = l.withDualInOther l2 ∧ + l2.withUniqueDualInOther l = l2.withDualInOther l := by + apply Iff.intro + intro h + exact ⟨append_withDual_eq_withUniqueDual_inl l l2 h, append_withDual_eq_withUniqueDual_inr l l2 h, + append_withDual_eq_withUniqueDual_withUniqueDualInOther_inl l l2 h, + append_withDual_eq_withUniqueDual_withUniqueDualInOther_inr l l2 h⟩ + intro h + rw [append_withDual_eq_withUniqueDual_iff] + rw [h.1, h.2.1, h.2.2.1, h.2.2.2] + have h1 : l.withDual ∩ (l.withDualInOther l2)ᶜ = l.withDual := by + rw [Finset.inter_eq_left] + rw [Finset.subset_iff] + rw [← h.1, ← h.2.2.1] + intro i hi + simp only [withUniqueDualInOther, mem_withDual_iff_isSome, Bool.not_eq_true, Option.not_isSome, + Option.isNone_iff_eq_none, mem_withInDualOther_iff_isSome, Finset.compl_filter, not_and, + not_forall, Classical.not_imp, Finset.mem_filter, Finset.mem_univ, true_and] + intro hn + simp_all + have h2 : l2.withDual ∩ (l2.withDualInOther l)ᶜ = l2.withDual := by + rw [Finset.inter_eq_left] + rw [Finset.subset_iff] + rw [← h.2.1, ← h.2.2.2] + intro i hi + simp only [withUniqueDualInOther, mem_withDual_iff_isSome, Bool.not_eq_true, Option.not_isSome, + Option.isNone_iff_eq_none, mem_withInDualOther_iff_isSome, Finset.compl_filter, not_and, + not_forall, Classical.not_imp, Finset.mem_filter, Finset.mem_univ, true_and] + intro hn + simp_all + rw [h1, h2] + simp only [and_self] + +lemma append_withDual_eq_withUniqueDual_swap : + (l ++ l2 ++ l3).withUniqueDual = (l ++ l2 ++ l3).withDual + ↔ (l2 ++ l ++ l3).withUniqueDual = (l2 ++ l ++ l3).withDual := by + rw [append_withDual_eq_withUniqueDual_iff'] + rw [append_withDual_eq_withUniqueDual_iff' (l2 ++ l) l3] + rw [append_withDual_eq_withUniqueDual_symm] + rw [withUniqueDualInOther_eq_withDualInOther_of_append_symm] + rw [withUniqueDualInOther_eq_withDualInOther_append_of_symm] + /-! ## Indices which do not have duals. @@ -932,6 +1769,7 @@ def dualEquiv : l.withDual ⊕ Fin l.withoutDual.card ≃ Fin l.length := (Equiv.Finset.union _ _ l.withDual_disjoint_withoutDual).trans <| Equiv.subtypeUnivEquiv (by simp [withDual_union_withoutDual]) + /-! ## The contraction list @@ -957,7 +1795,6 @@ lemma contrIndexList_colorMap (i : Fin l.contrIndexList.length) : l.contrIndexLi simp [contrIndexList, colorMap] rfl -@[simp] lemma contrIndexList_areDualInSelf (i j : Fin l.contrIndexList.length) : l.contrIndexList.AreDualInSelf i j ↔ l.AreDualInSelf (l.withoutDualEquiv (Fin.cast l.contrIndexList_length i)).1 @@ -974,11 +1811,11 @@ lemma contrIndexList_areDualInSelf (i j : Fin l.contrIndexList.length) : lemma contrIndexList_getDual? (i : Fin l.contrIndexList.length) : l.contrIndexList.getDual? i = none := by rw [← Option.not_isSome_iff_eq_none, ← mem_withDual_iff_isSome, mem_withDual_iff_exists] - simp + simp [contrIndexList_areDualInSelf] have h1 := (l.withoutDualEquiv (Fin.cast l.contrIndexList_length i)).2 have h1' := Finset.disjoint_right.mp l.withDual_disjoint_withoutDual h1 rw [mem_withDual_iff_exists] at h1' - simp at h1' + simp [contrIndexList_areDualInSelf] at h1' exact fun x => h1' ↑(l.withoutDualEquiv (Fin.cast (contrIndexList_length l) x)) @[simp] @@ -987,6 +1824,16 @@ lemma contrIndexList_withDual : l.contrIndexList.withDual = ∅ := by intro x simp [withDual] +@[simp] +lemma contrIndexList_areDualInSelf_false (i j : Fin l.contrIndexList.length) : + l.contrIndexList.AreDualInSelf i j ↔ False := by + refine Iff.intro (fun h => ?_) (fun h => ?_) + have h1 : i ∈ l.contrIndexList.withDual := by + rw [@mem_withDual_iff_exists] + use j + simp_all + simp_all + @[simp] lemma contrIndexList_of_withDual_empty (h : l.withDual = ∅) : l.contrIndexList = l := by have h1 := l.withDual_union_withoutDual @@ -1010,6 +1857,283 @@ lemma contrIndexList_of_withDual_empty (h : l.withDual = ∅) : l.contrIndexList lemma contrIndexList_contrIndexList : l.contrIndexList.contrIndexList = l.contrIndexList := by simp +@[simp] +lemma contrIndexList_getDualInOther?_self (i : Fin l.contrIndexList.length) : + l.contrIndexList.getDualInOther? l.contrIndexList i = some i := by + simp [getDualInOther?] + rw [@Fin.find_eq_some_iff] + simp [AreDualInOther] + intro j hj + have h1 : i = j := by + by_contra hn + have h : l.contrIndexList.AreDualInSelf i j := by + simp only [AreDualInSelf] + simp [hj] + exact hn + simp at h + subst h1 + rfl + +/-! + +## The equivalence defined by getDual? + +-/ + +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⟩ + left_inv x := SetCoe.ext (by simp) + right_inv x := SetCoe.ext (by simp) + +@[simp] +lemma getDualEquiv_involutive : Function.Involutive l.getDualEquiv := by + intro x + simp [getDualEquiv] + +/-! + +## Equivalence for withUniqueDualInOther + +-/ + +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⟩ + invFun x := ⟨(l2.getDualInOther? l x).get (l2.mem_withUniqueDualInOther_isSome l x.1 x.2), + by simp⟩ + left_inv x := SetCoe.ext (by simp) + right_inv x := SetCoe.ext (by simp) + +@[simp] +lemma getDualInOtherEquiv_self_refl : l.getDualInOtherEquiv l = Equiv.refl _ := by + apply Equiv.ext + intro x + simp [getDualInOtherEquiv] + +/-! + +## Splitting withUniqueDual + +-/ + +instance (i j : Option (Fin l.length)) : Decidable (i < j) := + match i, j with + | none, none => isFalse (fun a => a) + | none, some _ => isTrue (by trivial) + | some _, none => isFalse (fun a => a) + | some i, some j => Fin.decLt i j + +def withUniqueDualLT : Finset (Fin l.length) := + Finset.filter (fun i => i < l.getDual? i) l.withUniqueDual + +def withUniqueDualLTToWithUniqueDual (i : l.withUniqueDualLT) : l.withUniqueDual := + ⟨i.1, by + have hi := i.2 + simp only [withUniqueDualLT, Finset.mem_filter] at hi + exact hi.1⟩ + +instance : Coe l.withUniqueDualLT l.withUniqueDual where + coe := l.withUniqueDualLTToWithUniqueDual + +def withUniqueDualGT : Finset (Fin l.length) := + Finset.filter (fun i => ¬ i < l.getDual? i) l.withUniqueDual + +def withUniqueDualGTToWithUniqueDual (i : l.withUniqueDualGT) : l.withUniqueDual := + ⟨i.1, by + have hi := i.2 + simp only [withUniqueDualGT, Finset.mem_filter] at hi + exact hi.1⟩ + +instance : Coe l.withUniqueDualGT l.withUniqueDual where + coe := l.withUniqueDualGTToWithUniqueDual + +lemma withUniqueDualLT_disjoint_withUniqueDualGT : + Disjoint l.withUniqueDualLT l.withUniqueDualGT := by + rw [Finset.disjoint_iff_inter_eq_empty] + exact @Finset.filter_inter_filter_neg_eq (Fin l.length) _ _ _ _ _ + +lemma withUniqueDualLT_union_withUniqueDualGT : + l.withUniqueDualLT ∪ l.withUniqueDualGT = l.withUniqueDual := + Finset.filter_union_filter_neg_eq _ _ + +/-! TODO: Replace with a mathlib lemma. -/ +lemma option_not_lt (i j : Option (Fin l.length)) : i < j → i ≠ j → ¬ j < i := by + match i, j with + | none, none => + intro _ + simp + | none, some k => + intro _ + exact fun _ a => a + | some i, none => + intro h + exact fun _ _ => h + | some i, some j => + intro h h' + simp_all + change i < j at h + change ¬ j < i + exact Fin.lt_asymm h + +/-! TODO: Replace with a mathlib lemma. -/ +lemma lt_option_of_not (i j : Option (Fin l.length)) : ¬ j < i → i ≠ j → i < j := by + match i, j with + | none, none => + intro _ + simp + | none, some k => + intro _ + exact fun _ => trivial + | some i, none => + intro h + exact fun _ => h trivial + | some i, some j => + intro h h' + simp_all + change ¬ j < i at h + change i < j + omega + +def withUniqueDualLTEquivGT : l.withUniqueDualLT ≃ l.withUniqueDualGT where + toFun i := ⟨l.getDualEquiv i, by + have hi := i.2 + simp [withUniqueDualGT] + simp [getDualEquiv] + simp [withUniqueDualLT] at hi + apply option_not_lt + simpa [withUniqueDualLTToWithUniqueDual] using hi.2 + exact Ne.symm (getDual?_neq_self l i)⟩ + invFun i := ⟨l.getDualEquiv.symm i, by + have hi := i.2 + simp [withUniqueDualLT] + simp [getDualEquiv] + simp [withUniqueDualGT] at hi + apply lt_option_of_not + simpa [withUniqueDualLTToWithUniqueDual] using hi.2 + exact (getDual?_neq_self l i)⟩ + left_inv x := SetCoe.ext (by simp [withUniqueDualGTToWithUniqueDual, + withUniqueDualLTToWithUniqueDual]) + right_inv x := SetCoe.ext (by simp [withUniqueDualGTToWithUniqueDual, + withUniqueDualLTToWithUniqueDual]) + +def withUniqueLTGTEquiv : l.withUniqueDualLT ⊕ l.withUniqueDualLT ≃ l.withUniqueDual := by + apply (Equiv.sumCongr (Equiv.refl _ ) l.withUniqueDualLTEquivGT).trans + apply (Equiv.Finset.union _ _ l.withUniqueDualLT_disjoint_withUniqueDualGT).trans + apply (Equiv.subtypeEquivRight (by simp [l.withUniqueDualLT_union_withUniqueDualGT])) + +/-! + +## withUniqueDualInOther equal univ + +-/ + +lemma withUniqueDualInOther_eq_univ_fst_withDual_empty + (h : l.withUniqueDualInOther l2 = Finset.univ) : l.withDual = ∅ := by + rw [@Finset.eq_empty_iff_forall_not_mem] + intro x + have hx : x ∈ l.withUniqueDualInOther l2 := by + rw [h] + simp + rw [withUniqueDualInOther] at hx + simp only [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 hx + simpa using hx.1 + +lemma withUniqueDualInOther_eq_univ_fst_eq_contrIndexList (h : l.withUniqueDualInOther l2 = Finset.univ) : + l = l.contrIndexList := by + refine Eq.symm (contrIndexList_of_withDual_empty l ?h) + exact withUniqueDualInOther_eq_univ_fst_withDual_empty l l2 h + +lemma withUniqueDualInOther_eq_univ_symm (hl : l.length = l2.length) + (h : l.withUniqueDualInOther l2 = Finset.univ) : + l2.withUniqueDualInOther l = Finset.univ := by + let S' : Finset (Fin l2.length) := + Finset.map ⟨Subtype.val, Subtype.val_injective⟩ + (Equiv.finsetCongr + (l.getDualInOtherEquiv l2) Finset.univ ) + have hSCard : S'.card = l2.length := by + rw [Finset.card_map] + simp + rw [h, ← hl] + simp + have hsCardUn : S'.card = (@Finset.univ (Fin l2.length)).card := by + rw [hSCard] + simp + have hS'Eq : S' = (l2.withUniqueDualInOther l) := by + rw [@Finset.ext_iff] + intro a + simp [S'] + rw [hS'Eq] at hsCardUn + exact (Finset.card_eq_iff_eq_univ (l2.withUniqueDualInOther l)).mp hsCardUn + +lemma withUniqueDualInOther_eq_univ_contr_refl : + l.contrIndexList.withUniqueDualInOther l.contrIndexList = Finset.univ := by + rw [@Finset.eq_univ_iff_forall] + intro x + simp only [withUniqueDualInOther, mem_withDual_iff_isSome, + Option.isSome_none, Bool.false_eq_true, not_false_eq_true, mem_withInDualOther_iff_isSome, + getDualInOther?_self_isSome, true_and, Finset.mem_filter, Finset.mem_univ] + simp only [contrIndexList_getDual?, Option.isSome_none, Bool.false_eq_true, not_false_eq_true, + contrIndexList_getDualInOther?_self, Option.some.injEq, true_and] + intro j hj + have h1 : j = x := by + by_contra hn + have hj : l.contrIndexList.AreDualInSelf x j := by + simp [AreDualInOther] at hj + simp only [AreDualInSelf, ne_eq, contrIndexList_idMap, hj, and_true] + exact fun a => hn (id (Eq.symm a)) + simp at hj + simpa using h1 + +set_option maxHeartbeats 0 +lemma withUniqueDualInOther_eq_univ_trans (h : l.withUniqueDualInOther l2 = Finset.univ) + (h' : l2.withUniqueDualInOther l3 = Finset.univ) : + l.withUniqueDualInOther l3 = Finset.univ := by + rw [Finset.eq_univ_iff_forall] + intro i + 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] + have hi : i ∈ l.withUniqueDualInOther l2 := by + rw [h] + simp + 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 hi + have hi2 : ((l.getDualInOther? l2 i).get hi.2.1) ∈ l2.withUniqueDualInOther l3 := by + rw [h'] + simp + 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 hi2 + apply And.intro hi.1 + apply And.intro + · rw [@getDualInOther?_isSome_iff_exists] + use (l2.getDualInOther? l3 ((l.getDualInOther? l2 i).get hi.2.1)).get hi2.2.1 + simp [AreDualInOther] + intro j hj + have hj' : j = (l2.getDualInOther? l3 ((l.getDualInOther? l2 i).get hi.2.1)).get hi2.2.1 := by + rw [← eq_getDualInOther?_get_of_withUniqueDualInOther_iff] + simpa [AreDualInOther] using hj + rw [h'] + simp + have hs : (l.getDualInOther? l3 i).isSome := by + rw [@getDualInOther?_isSome_iff_exists] + exact Exists.intro j hj + have hs' : (l.getDualInOther? l3 i).get hs = (l2.getDualInOther? l3 ((l.getDualInOther? l2 i).get hi.2.1)).get hi2.2.1 := by + rw [← eq_getDualInOther?_get_of_withUniqueDualInOther_iff] + simp [AreDualInOther] + rw [h'] + simp + rw [← hj'] at hs' + rw [← hs'] + simp + + + end IndexList end IndexNotation diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/IndexString.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/IndexString.lean index e90a776..346b240 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/IndexString.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/IndexString.lean @@ -236,8 +236,11 @@ lemma listCharIndexString (s : IndexString X) : listCharIndexString X s.toCharLi /-- The indices associated to an index string. -/ def toIndexList (s : IndexString X) : IndexList X := - (listCharIndexStringTolistCharIndex X s.toCharList (listCharIndexString s)).map - fun x => Index.ofCharList x.1 x.2 + {val := (listCharIndexStringTolistCharIndex X s.toCharList (listCharIndexString s)).map + fun x => Index.ofCharList x.1 x.2} + +def toIndexList' (s : String) (hs : listCharIndexStringBool X s.toList = true) : IndexList X := + toIndexList ⟨s, hs⟩ end IndexString @@ -255,20 +258,18 @@ variable {R : Type} [CommSemiring R] (𝓣 : TensorStructure R) variable {𝓣 : TensorStructure R} [IndexNotation 𝓣.Color] [Fintype 𝓣.Color] [DecidableEq 𝓣.Color] variable {n m : ℕ} {cn : Fin n → 𝓣.Color} {cm : Fin m → 𝓣.Color} -open IndexNotation IndexListColor +open IndexNotation ColorIndexList IndexString /-- The construction of a tensor index from a tensor and a string satisfing conditions which are easy to check automatically. -/ noncomputable def fromIndexString (T : 𝓣.Tensor cn) (s : String) (hs : listCharIndexStringBool 𝓣.toTensorColor.Color s.toList = true) - (hn : n = (IndexString.toIndexList (⟨s, hs⟩ : IndexString 𝓣.Color)).length) - (hc : IndexListColorProp 𝓣.toTensorColor ( - IndexString.toIndexList (⟨s, hs⟩ : IndexString 𝓣.Color))) - (hd : TensorColor.ColorMap.DualMap - (IndexString.toIndexList (⟨s, hs⟩ : IndexString 𝓣.Color)).colorMap + (hn : n = (toIndexList' s hs).length) + (hD : (toIndexList' s hs).withDual = (toIndexList' s hs).withUniqueDual) + (hC : IndexList.ColorCond (toIndexList' s hs)) + (hd : TensorColor.ColorMap.DualMap (toIndexList' s hs).colorMap (cn ∘ Fin.cast hn.symm)) : 𝓣.TensorIndex := - TensorStructure.TensorIndex.mkDualMap T - ⟨(IndexString.toIndexList (⟨s, hs⟩ : IndexString 𝓣.Color)), hc⟩ hn hd + TensorStructure.TensorIndex.mkDualMap T ⟨(toIndexList' s hs), hD, hC⟩ hn hd end TensorIndex diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Relations.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Relations.lean index ae9952c..171a4dc 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Relations.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Relations.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.SpaceTime.LorentzTensor.IndexNotation.Indices.Color -import HepLean.SpaceTime.LorentzTensor.IndexNotation.Indices.UniqueDualInOther import HepLean.SpaceTime.LorentzTensor.Basic import Init.Data.List.Lemmas /-! @@ -25,7 +24,7 @@ namespace ColorIndexList variable {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color] variable (l l' : ColorIndexList 𝓒) - +open IndexList TensorColor /-! ## Reindexing @@ -45,12 +44,146 @@ To prevent choice problems, this has to be done after contraction. -/ -def ContrPerm : Prop := l.contr.length = l'.contr.length ∧ - l.contr.withUniqueDualInOther l'.contr.toIndexList = Finset.univ ∧ - l'.contr.colorMap ∘ Subtype.val ∘ (l.contr.getDualInOtherEquiv l'.contr.toIndexList) - = l.contr.colorMap ∘ Subtype.val +def ContrPerm : Prop := + l.contr.length = l'.contr.length ∧ + l.contr.withUniqueDualInOther l'.contr = Finset.univ ∧ + l'.contr.colorMap' ∘ Subtype.val ∘ (l.contr.getDualInOtherEquiv l'.contr) + = l.contr.colorMap' ∘ Subtype.val + +namespace ContrPerm + +variable {l l' l2 l3 : ColorIndexList 𝓒} +@[symm] +lemma symm (h : ContrPerm l l') : ContrPerm l' l := by + rw [ContrPerm] at h ⊢ + apply And.intro h.1.symm + apply And.intro (l.contr.withUniqueDualInOther_eq_univ_symm l'.contr h.1 h.2.1) + rw [← Function.comp.assoc, ← h.2.2, Function.comp.assoc, Function.comp.assoc] + rw [show (l.contr.getDualInOtherEquiv l'.contr) = + (l'.contr.getDualInOtherEquiv l.contr).symm from rfl] + simp + +@[simp] +lemma refl : 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] + +@[trans] +lemma trans (h1 : ContrPerm l l2) (h2 : ContrPerm l2 l3) : ContrPerm l l3 := by + apply And.intro (h1.1.trans h2.1) + apply And.intro (l.contr.withUniqueDualInOther_eq_univ_trans l2.contr l3.contr h1.2.1 h2.2.1) + funext i + simp + have h1' := congrFun h1.2.2 ⟨i, by simp [h1.2.1]⟩ + simp at h1' + rw [← h1'] + have h2' := congrFun h2.2.2 ⟨ + ↑((l.contr.getDualInOtherEquiv l2.contr.toIndexList) ⟨↑i, by simp [h1.2.1]⟩), by simp [h2.2.1]⟩ + simp at h2' + rw [← h2'] + apply congrArg + simp only [getDualInOtherEquiv, Equiv.coe_fn_mk] + rw [← eq_getDualInOther?_get_of_withUniqueDualInOther_iff] + simp [AreDualInOther] + rw [h2.2.1] + simp + +@[simp] +lemma symm_trans (h1 : ContrPerm l l2) (h2 : ContrPerm l2 l3) : + (h1.trans h2).symm = h2.symm.trans h1.symm := by + rfl + +@[simp] +lemma contr_self : ContrPerm l l.contr := by + rw [ContrPerm] + simp + have h1 := @refl _ _ l + apply And.intro h1.2.1 + erw [contr_contr] + exact h1.2.2 + +@[simp] +lemma self_contr : ContrPerm l.contr l := by + symm + simp + +end ContrPerm + +def contrPermEquiv {l l' : ColorIndexList 𝓒} (h : ContrPerm l l') : + Fin l.contr.length ≃ Fin l'.contr.length := + (Equiv.subtypeUnivEquiv (by simp [h.2])).symm.trans <| + (l.contr.getDualInOtherEquiv l'.contr.toIndexList).trans <| + Equiv.subtypeUnivEquiv (by simp [h.symm.2]) + +lemma contrPermEquiv_colorMap_iso {l l' : ColorIndexList 𝓒} (h : ContrPerm l l') : + ColorMap.MapIso (contrPermEquiv h).symm l'.contr.colorMap' l.contr.colorMap' := by + simp [ColorMap.MapIso] + funext i + simp [contrPermEquiv, getDualInOtherEquiv] + have h' := h.symm.2.2 + have hi : i ∈ (l'.contr.withUniqueDualInOther l.contr.toIndexList) := by + rw [h.symm.2.1] + exact Finset.mem_univ i + have hn := congrFun h' ⟨i, hi⟩ + simp at hn + rw [← hn] + rfl + +lemma contrPermEquiv_colorMap_iso' {l l' : ColorIndexList 𝓒} (h : ContrPerm l l') : + ColorMap.MapIso (contrPermEquiv h) l.contr.colorMap' l'.contr.colorMap' := by + rw [ColorMap.MapIso.symm'] + exact contrPermEquiv_colorMap_iso h + + +@[simp] +lemma contrPermEquiv_refl : contrPermEquiv (@ContrPerm.refl 𝓒 _ l) = Equiv.refl _ := by + simp [contrPermEquiv, ContrPerm.refl] + +@[simp] +lemma contrPermEquiv_symm {l l' : ColorIndexList 𝓒} (h : ContrPerm l l') : + (contrPermEquiv h).symm = contrPermEquiv h.symm := by + simp only [contrPermEquiv] + rfl + +@[simp] +lemma contrPermEquiv_trans {l l2 l3 : ColorIndexList 𝓒} + (h1 : ContrPerm l l2) (h2 : ContrPerm l2 l3) : + (contrPermEquiv h1).trans (contrPermEquiv h2) = contrPermEquiv (h1.trans h2) := by + simp [contrPermEquiv] + ext x + simp only [getDualInOtherEquiv, Equiv.trans_apply, Equiv.subtypeUnivEquiv_symm_apply, + Equiv.coe_fn_mk, Equiv.subtypeUnivEquiv_apply] + apply congrArg + rw [← eq_getDualInOther?_get_of_withUniqueDualInOther_iff] + simp [AreDualInOther] + rw [(h1.trans h2).2.1] + simp + +@[simp] +lemma contrPermEquiv_self_contr {l : ColorIndexList 𝓒} : + contrPermEquiv (by simp : ContrPerm l l.contr) = + (Fin.castOrderIso (by simp)).toEquiv := by + simp [contrPermEquiv] + ext1 x + simp only [getDualInOtherEquiv, Equiv.trans_apply, Equiv.subtypeUnivEquiv_symm_apply, + Equiv.coe_fn_mk, Equiv.subtypeUnivEquiv_apply, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, + Fin.coe_cast] + symm + rw [← eq_getDualInOther?_get_of_withUniqueDualInOther_iff] + simp only [AreDualInOther, contr_contr_idMap, Fin.cast_trans, Fin.cast_eq_self] + have h1 : ContrPerm l l.contr := by simp + rw [h1.2.1] + simp + +@[simp] +lemma contrPermEquiv_contr_self {l : ColorIndexList 𝓒} : + contrPermEquiv (by simp : ContrPerm l.contr l) = + (Fin.castOrderIso (by simp)).toEquiv := by + rw [← contrPermEquiv_symm, contrPermEquiv_self_contr] + simp end ColorIndexList diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean index 0a80f0d..8234958 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.SpaceTime.LorentzTensor.IndexNotation.Indices.Color +import HepLean.SpaceTime.LorentzTensor.IndexNotation.Indices.Relations import HepLean.SpaceTime.LorentzTensor.Basic import HepLean.SpaceTime.LorentzTensor.RisingLowering import HepLean.SpaceTime.LorentzTensor.Contraction @@ -34,7 +35,7 @@ variable [IndexNotation 𝓣.Color] [Fintype 𝓣.Color] [DecidableEq 𝓣.Color /-- The structure an tensor with a index specification e.g. `ᵘ¹ᵤ₂`. -/ structure TensorIndex extends ColorIndexList 𝓣.toTensorColor where /-- The underlying tensor. -/ - tensor : 𝓣.Tensor toIndexList.colorMap + tensor : 𝓣.Tensor toColorIndexList.colorMap' namespace TensorIndex @@ -43,9 +44,12 @@ open TensorColor ColorIndexList variable {𝓣 : TensorStructure R} [IndexNotation 𝓣.Color] [Fintype 𝓣.Color] [DecidableEq 𝓣.Color] variable {n m : ℕ} {cn : Fin n → 𝓣.Color} {cm : Fin m → 𝓣.Color} +instance : Coe 𝓣.TensorIndex (ColorIndexList 𝓣.toTensorColor) where + coe T := T.toColorIndexList + lemma colormap_mapIso {T₁ T₂ : 𝓣.TensorIndex} (hi : T₁.toColorIndexList = T₂.toColorIndexList) : ColorMap.MapIso (Fin.castOrderIso (by simp [IndexList.length, hi])).toEquiv - T₁.colorMap T₂.colorMap := by + T₁.colorMap' T₂.colorMap' := by cases T₁; cases T₂ simp [ColorMap.MapIso] simp at hi @@ -90,12 +94,12 @@ lemma tensor_eq_of_eq {T₁ T₂ : 𝓣.TensorIndex} (h : T₁ = T₂) : T₁.te /-- The construction of a `TensorIndex` from a tensor, a IndexListColor, and a condition on the dual maps. -/ def mkDualMap (T : 𝓣.Tensor cn) (l : ColorIndexList 𝓣.toTensorColor) (hn : n = l.1.length) - (hd : ColorMap.DualMap l.1.colorMap (cn ∘ Fin.cast hn.symm)) : + (hd : ColorMap.DualMap l.colorMap' (cn ∘ Fin.cast hn.symm)) : 𝓣.TensorIndex where toColorIndexList := l tensor := - 𝓣.mapIso (Equiv.refl _) (ColorMap.DualMap.split_dual' (by simp [hd])) <| - 𝓣.dualize (ColorMap.DualMap.split l.1.colorMap (cn ∘ Fin.cast hn.symm)) <| + 𝓣.mapIso (Equiv.refl _) (ColorMap.DualMap.split_dual' (by simpa using hd)) <| + 𝓣.dualize (ColorMap.DualMap.split l.colorMap' (cn ∘ Fin.cast hn.symm)) <| (𝓣.mapIso (Fin.castOrderIso hn).toEquiv rfl T : 𝓣.Tensor (cn ∘ Fin.cast hn.symm)) /-! @@ -106,49 +110,61 @@ def mkDualMap (T : 𝓣.Tensor cn) (l : ColorIndexList 𝓣.toTensorColor) (hn : /-- The contraction of indices in a `TensorIndex`. -/ def contr (T : 𝓣.TensorIndex) : 𝓣.TensorIndex where - index := T.index.contr - tensor := - 𝓣.mapIso (Fin.castOrderIso T.index.contr_numIndices.symm).toEquiv - T.index.contr_colorMap <| - 𝓣.contr (T.index.splitContr).symm T.index.splitContr_map T.tensor + toColorIndexList := T.toColorIndexList.contr + tensor := 𝓣.mapIso (Equiv.refl _) T.contrEquiv_colorMapIso <| + 𝓣.contr T.toColorIndexList.contrEquiv T.contrEquiv_contrCond T.tensor /-- Applying contr to a tensor whose indices has no contracts does not do anything. -/ @[simp] -lemma contr_of_hasNoContr (T : 𝓣.TensorIndex) (h : T.index.1.HasNoContr) : +lemma contr_of_withDual_empty (T : 𝓣.TensorIndex) (h : T.withDual = ∅) : T.contr = T := by - refine ext _ _ ?_ ?_ - 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 - rename_i i T - simp only - refine PiTensorProduct.induction_on' T ?_ (by - intro a b hx hy - simp [map_add, add_mul, hx, hy]) - intro r f - simp only [PiTensorProduct.tprodCoeff_eq_smul_tprod, LinearMapClass.map_smul, mapIso_tprod, id_eq, - eq_mpr_eq_cast, OrderIso.toEquiv_symm, RelIso.coe_fn_toEquiv] - apply congrArg - erw [TensorStructure.contr_tprod_isEmpty] - erw [mapIso_tprod] - apply congrArg - funext l - rw [← LinearEquiv.symm_apply_eq] - simp only [colorModuleCast, Equiv.cast_symm, OrderIso.toEquiv_symm, RelIso.coe_fn_toEquiv, - Function.comp_apply, LinearEquiv.coe_mk, Equiv.cast_apply, LinearEquiv.coe_symm_mk, cast_cast] - apply cast_eq_iff_heq.mpr - rw [splitContr_symm_apply_of_hasNoContr _ h] - rfl + refine ext ?_ ?_ + · simp [contr, ColorIndexList.contr] + have hx := T.contrIndexList_of_withDual_empty h + apply ColorIndexList.ext + simp [hx] + · simp only [contr] + cases T + rename_i i T + simp only + refine PiTensorProduct.induction_on' T ?_ (by + intro a b hx hy + simp [map_add, add_mul, hx, hy]) + intro r f + simp only [PiTensorProduct.tprodCoeff_eq_smul_tprod, LinearMapClass.map_smul, mapIso_tprod, id_eq, + eq_mpr_eq_cast, OrderIso.toEquiv_symm, RelIso.coe_fn_toEquiv] + apply congrArg + have hEm : IsEmpty { x // x ∈ i.withUniqueDualLT } := by + rw [Finset.isEmpty_coe_sort] + rw [Finset.eq_empty_iff_forall_not_mem] + intro x hx + have hx' : x ∈ i.withUniqueDual := by + exact Finset.mem_of_mem_filter x hx + rw [i.unique_duals] at h + rw [h] at hx' + simp_all + erw [TensorStructure.contr_tprod_isEmpty] + erw [mapIso_tprod] + simp only [Equiv.refl_symm, Equiv.refl_apply, colorMap', mapIso_tprod, id_eq, + OrderIso.toEquiv_symm, RelIso.coe_fn_toEquiv] + apply congrArg + funext l + rw [← LinearEquiv.symm_apply_eq] + simp only [colorModuleCast, Equiv.cast_symm, OrderIso.toEquiv_symm, RelIso.coe_fn_toEquiv, + Function.comp_apply, LinearEquiv.coe_mk, Equiv.cast_apply, LinearEquiv.coe_symm_mk, cast_cast] + apply cast_eq_iff_heq.mpr + let hl := i.contrEquiv_on_withDual_empty l h + exact let_value_heq f hl @[simp] lemma contr_contr (T : 𝓣.TensorIndex) : T.contr.contr = T.contr := - T.contr.contr_of_hasNoContr T.index.1.contr_hasNoContr + T.contr.contr_of_withDual_empty (by simp [contr, ColorIndexList.contr]) @[simp] -lemma contr_index (T : 𝓣.TensorIndex) : T.contr.index = T.index.contr := rfl - +lemma contr_toColorIndexList (T : 𝓣.TensorIndex) : T.contr.toColorIndexList = T.toColorIndexList.contr := rfl +@[simp] +lemma contr_toIndexList (T : 𝓣.TensorIndex) : T.contr.toIndexList = T.toIndexList.contrIndexList := rfl /-! ## Scalar multiplication of @@ -158,18 +174,18 @@ lemma contr_index (T : 𝓣.TensorIndex) : T.contr.index = T.index.contr := rfl /-- The scalar multiplication of a `TensorIndex` by an element of `R`. -/ instance : SMul R 𝓣.TensorIndex where smul := fun r T => { - index := T.index + toColorIndexList := T.toColorIndexList tensor := r • T.tensor} @[simp] -lemma smul_index (r : R) (T : 𝓣.TensorIndex) : (r • T).index = T.index := rfl +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 ?_ + refine ext rfl ?_ simp only [contr, smul_index, smul_tensor, LinearMapClass.map_smul, Fin.castOrderIso_refl, OrderIso.refl_toEquiv, mapIso_refl, LinearEquiv.refl_apply] @@ -179,22 +195,23 @@ lemma smul_contr (r : R) (T : 𝓣.TensorIndex) : (r • T).contr = r • T.cont -/ + + /-- An (equivalence) relation on two `TensorIndex`. The point in this equivalence relation is that certain things (like the permutation of indices, the contraction of indices, or rising or lowering indices) can be placed in the indices or moved to the tensor itself. These two descriptions are equivalent. -/ def Rel (T₁ T₂ : 𝓣.TensorIndex) : Prop := - T₁.index.PermContr T₂.index ∧ ∀ (h : T₁.index.PermContr T₂.index), - T₁.contr.tensor = 𝓣.mapIso h.toEquiv.symm h.toEquiv_colorMap T₂.contr.tensor + T₁.ContrPerm T₂ ∧ ∀ (h : T₁.ContrPerm T₂), + T₁.contr.tensor = 𝓣.mapIso (contrPermEquiv h).symm (contrPermEquiv_colorMap_iso h) T₂.contr.tensor namespace Rel /-- Rel is reflexive. -/ lemma refl (T : 𝓣.TensorIndex) : Rel T T := by apply And.intro - exact IndexListColor.PermContr.refl T.index - intro h - simp [PermContr.toEquiv_refl'] + simp + simp /-- Rel is symmetric. -/ lemma symm {T₁ T₂ : 𝓣.TensorIndex} (h : Rel T₁ T₂) : Rel T₂ T₁ := by @@ -210,15 +227,17 @@ lemma symm {T₁ T₂ : 𝓣.TensorIndex} (h : Rel T₁ T₂) : Rel T₂ T₁ := /-- Rel is transitive. -/ lemma trans {T₁ T₂ T₃ : 𝓣.TensorIndex} (h1 : Rel T₁ T₂) (h2 : Rel T₂ T₃) : Rel T₁ T₃ := by - apply And.intro (h1.1.trans h2.1) + apply And.intro ((h1.1.trans h2.1)) intro h - change _ = (𝓣.mapIso (h1.1.trans h2.1).toEquiv.symm _) T₃.contr.tensor - trans (𝓣.mapIso ((h1.1).toEquiv.trans (h2.1).toEquiv).symm (by - rw [PermContr.toEquiv_trans] - exact proof_2 T₁ T₃ h)) T₃.contr.tensor + change _ = (𝓣.mapIso (contrPermEquiv (h1.1.trans h2.1)).symm _) T₃.contr.tensor + trans (𝓣.mapIso ((contrPermEquiv h1.1).trans (contrPermEquiv h2.1)).symm (by + simp + have h1 := contrPermEquiv_colorMap_iso (ContrPerm.symm (ContrPerm.trans h1.left h2.left)) + rw [← ColorMap.MapIso.symm'] at h1 + exact h1)) T₃.contr.tensor swap - congr - rw [PermContr.toEquiv_trans] + congr 1 + simp only [contrPermEquiv_trans, contrPermEquiv_symm] erw [← mapIso_trans] simp only [LinearEquiv.trans_apply] apply (h1.2 h1.1).trans @@ -233,7 +252,7 @@ lemma isEquivalence : Equivalence (@Rel _ _ 𝓣 _) where /-- The equality of tensors corresponding to related tensor indices. -/ lemma to_eq {T₁ T₂ : 𝓣.TensorIndex} (h : Rel T₁ T₂) : - T₁.contr.tensor = 𝓣.mapIso h.1.toEquiv.symm h.1.toEquiv_colorMap T₂.contr.tensor := h.2 h.1 + T₁.contr.tensor = 𝓣.mapIso (contrPermEquiv h.1).symm (contrPermEquiv_colorMap_iso h.1) T₂.contr.tensor := h.2 h.1 end Rel @@ -243,26 +262,21 @@ instance asSetoid : Setoid 𝓣.TensorIndex := ⟨Rel, Rel.isEquivalence⟩ /-- A tensor index is equivalent to its contraction. -/ 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.contr_hasNoContr + simp intro h rw [tensor_eq_of_eq T.contr_contr] - simp only [contr_index, mapIso_mapIso] + simp only [contr_toColorIndexList, colorMap', contrPermEquiv_self_contr, OrderIso.toEquiv_symm, + Fin.symm_castOrderIso, mapIso_mapIso] trans 𝓣.mapIso (Equiv.refl _) (by rfl) T.contr.tensor - simp only [contr_index, mapIso_refl, LinearEquiv.refl_apply] - congr - apply Equiv.ext - intro x - rw [PermContr.toEquiv_contr_eq T.index.contr_contr.symm] + simp only [contr_toColorIndexList, mapIso_refl, LinearEquiv.refl_apply] rfl lemma smul_equiv {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₂)] - simp only [contr_index, smul_index, Fin.castOrderIso_refl, OrderIso.refl_toEquiv, mapIso_refl, - smul_tensor, LinearMapClass.map_smul, LinearEquiv.refl_apply] + simp only [contr_toColorIndexList, smul_index, Fin.castOrderIso_refl, OrderIso.refl_toEquiv, + mapIso_refl, smul_tensor, map_smul, LinearEquiv.refl_apply, contrPermEquiv_symm] apply congrArg exact h.2 h1 @@ -278,20 +292,19 @@ lemma smul_equiv {T₁ T₂ : 𝓣.TensorIndex} (h : T₁ ≈ T₂) (r : R) : r This condition is general enough to allow addition of e.g. `ψᵤ₁ᵤ₂ + φᵤ₂ᵤ₁`, but will NOT allow e.g. `ψᵤ₁ᵤ₂ + φᵘ²ᵤ₁`. -/ -def AddCond (T₁ T₂ : 𝓣.TensorIndex) : Prop := - T₁.index.PermContr T₂.index +def AddCond (T₁ T₂ : 𝓣.TensorIndex) : Prop := T₁.ContrPerm T₂ namespace AddCond -lemma to_PermContr {T₁ T₂ : 𝓣.TensorIndex} (h : AddCond T₁ T₂) : T₁.index.PermContr T₂.index := h +lemma to_PermContr {T₁ T₂ : 𝓣.TensorIndex} (h : AddCond T₁ T₂) : + T₁.toColorIndexList.ContrPerm T₂.toColorIndexList := h @[symm] lemma symm {T₁ T₂ : 𝓣.TensorIndex} (h : AddCond T₁ T₂) : AddCond T₂ T₁ := by rw [AddCond] at h exact h.symm -lemma refl (T : 𝓣.TensorIndex) : AddCond T T := by - exact PermContr.refl _ +lemma refl (T : 𝓣.TensorIndex) : AddCond T T := ContrPerm.refl lemma trans {T₁ T₂ T₃ : 𝓣.TensorIndex} (h1 : AddCond T₁ T₂) (h2 : AddCond T₂ T₃) : AddCond T₁ T₃ := by @@ -304,23 +317,25 @@ lemma rel_left {T₁ T₁' T₂ : 𝓣.TensorIndex} (h : AddCond T₁ T₂) (h' lemma rel_right {T₁ T₂ T₂' : 𝓣.TensorIndex} (h : AddCond T₁ T₂) (h' : T₂ ≈ T₂') : AddCond T₁ T₂' := h.trans h'.1 -/-- The equivalence between indices after contraction given a `AddCond`. -/ -@[simp] -def toEquiv {T₁ T₂ : 𝓣.TensorIndex} (h : AddCond T₁ T₂) : - Fin T₁.contr.index.1.length ≃ Fin T₂.contr.index.1.length := h.to_PermContr.toEquiv - -lemma toEquiv_colorMap {T₁ T₂ : 𝓣.TensorIndex} (h : AddCond T₁ T₂) : - ColorMap.MapIso h.toEquiv (T₁.contr.index).1.colorMap (T₂.contr.index).1.colorMap := - h.to_PermContr.toEquiv_colorMap' end AddCond + +/-- The equivalence between indices after contraction given a `AddCond`. -/ +@[simp] +def addCondEquiv {T₁ T₂ : 𝓣.TensorIndex} (h : AddCond T₁ T₂) : + Fin T₁.contr.length ≃ Fin T₂.contr.length := contrPermEquiv h + +lemma addCondEquiv_colorMap {T₁ T₂ : 𝓣.TensorIndex} (h : AddCond T₁ T₂) : + ColorMap.MapIso (addCondEquiv h) T₁.contr.colorMap' T₂.contr.colorMap' := + contrPermEquiv_colorMap_iso' h + /-- The addition of two `TensorIndex` given the condition that, after contraction, their index lists are the same. -/ def add (T₁ T₂ : 𝓣.TensorIndex) (h : AddCond T₁ T₂) : 𝓣.TensorIndex where - index := T₂.index.contr - tensor := (𝓣.mapIso h.toEquiv h.toEquiv_colorMap T₁.contr.tensor) + T₂.contr.tensor + toColorIndexList := T₂.toColorIndexList.contr + tensor := (𝓣.mapIso (addCondEquiv h) (addCondEquiv_colorMap h) T₁.contr.tensor) + T₂.contr.tensor /-- Notation for addition of tensor indices. -/ notation:71 T₁ "+["h"]" T₂:72 => add T₁ T₂ h @@ -329,7 +344,7 @@ namespace AddCond lemma add_right {T₁ T₂ T₃ : 𝓣.TensorIndex} (h : AddCond T₁ T₃) (h' : AddCond T₂ T₃) : AddCond T₁ (T₂ +[h'] T₃) := by - simpa only [AddCond, add, contr_index] using h.rel_right T₃.rel_contr + simpa only [AddCond, add] using h.rel_right T₃.rel_contr lemma add_left {T₁ T₂ T₃ : 𝓣.TensorIndex} (h : AddCond T₁ T₂) (h' : AddCond T₂ T₃) : AddCond (T₁ +[h] T₂) T₃ := @@ -369,70 +384,72 @@ lemma add_comm {T₁ T₂ : 𝓣.TensorIndex} (h : AddCond T₁ T₂) : end AddCond @[simp] -lemma add_index (T₁ T₂ : 𝓣.TensorIndex) (h : AddCond T₁ T₂) : - (add T₁ T₂ h).index = T₂.index.contr := rfl +lemma add_toColorIndexList (T₁ T₂ : 𝓣.TensorIndex) (h : AddCond T₁ T₂) : + (add T₁ T₂ h).toColorIndexList = T₂.toColorIndexList.contr := rfl @[simp] lemma add_tensor (T₁ T₂ : 𝓣.TensorIndex) (h : AddCond T₁ T₂) : (add T₁ T₂ h).tensor = - (𝓣.mapIso h.toEquiv h.toEquiv_colorMap T₁.contr.tensor) + T₂.contr.tensor := by rfl + (𝓣.mapIso (addCondEquiv h) (addCondEquiv_colorMap h) T₁.contr.tensor) + T₂.contr.tensor := by rfl /-- Scalar multiplication commutes with addition. -/ lemma smul_add (r : R) (T₁ T₂ : 𝓣.TensorIndex) (h : AddCond T₁ T₂) : r • (T₁ +[h] T₂) = r • T₁ +[h] r • T₂ := by - refine ext _ _ rfl ?_ + refine ext rfl ?_ simp [add] rw [tensor_eq_of_eq (smul_contr r T₁), tensor_eq_of_eq (smul_contr r T₂)] - simp only [smul_index, contr_index, Fin.castOrderIso_refl, OrderIso.refl_toEquiv, mapIso_refl, - smul_tensor, AddCond.toEquiv, LinearMapClass.map_smul, LinearEquiv.refl_apply] + simp only [smul_index, contr_toColorIndexList, Fin.castOrderIso_refl, OrderIso.refl_toEquiv, + mapIso_refl, smul_tensor, map_smul, LinearEquiv.refl_apply] -lemma add_hasNoContr (T₁ T₂ : 𝓣.TensorIndex) (h : AddCond T₁ T₂) : - (T₁ +[h] T₂).index.1.HasNoContr := by - simpa using T₂.index.1.contr_hasNoContr +lemma add_withDual_empty (T₁ T₂ : 𝓣.TensorIndex) (h : AddCond T₁ T₂) : + (T₁ +[h] T₂).withDual = ∅ := by + simp [contr] + change T₂.toColorIndexList.contr.withDual = ∅ + simp [ColorIndexList.contr] @[simp] lemma contr_add (T₁ T₂ : 𝓣.TensorIndex) (h : AddCond T₁ T₂) : (T₁ +[h] T₂).contr = T₁ +[h] T₂ := - contr_of_hasNoContr (T₁ +[h] T₂) (add_hasNoContr T₁ T₂ h) + contr_of_withDual_empty (T₁ +[h] T₂) (add_withDual_empty T₁ T₂ h) @[simp] lemma contr_add_tensor (T₁ T₂ : 𝓣.TensorIndex) (h : AddCond T₁ T₂) : (T₁ +[h] T₂).contr.tensor = 𝓣.mapIso (Fin.castOrderIso (by rw [index_eq_of_eq (contr_add T₁ T₂ h)])).toEquiv - (index_eq_colorMap_eq (index_eq_of_eq (contr_add T₁ T₂ h))) (T₁ +[h] T₂).tensor := + (colormap_mapIso (by simp)) (T₁ +[h] T₂).tensor := tensor_eq_of_eq (contr_add T₁ T₂ h) lemma add_comm {T₁ T₂ : 𝓣.TensorIndex} (h : AddCond T₁ T₂) : T₁ +[h] T₂ ≈ T₂ +[h.symm] T₁ := by apply And.intro h.add_comm intro h - simp only [contr_index, add_index, contr_add_tensor, add_tensor, AddCond.toEquiv, map_add, - mapIso_mapIso] + simp only [contr_toColorIndexList, add_toColorIndexList, contr_add_tensor, add_tensor, + addCondEquiv, map_add, mapIso_mapIso, colorMap', contrPermEquiv_symm] rw [_root_.add_comm] congr 1 - all_goals - apply congrFun + · apply congrFun apply congrArg congr 1 - rw [← PermContr.toEquiv_contr_eq, ← PermContr.toEquiv_contr_eq, - PermContr.toEquiv_trans, PermContr.toEquiv_symm, PermContr.toEquiv_trans] - simp only [IndexListColor.contr_contr] - simp only [IndexListColor.contr_contr] + rw [← contrPermEquiv_self_contr, ← contrPermEquiv_self_contr, contrPermEquiv_trans, + contrPermEquiv_trans] + · apply congrFun + apply congrArg + congr 1 + rw [← contrPermEquiv_self_contr, ← contrPermEquiv_self_contr, contrPermEquiv_trans, + contrPermEquiv_trans] open AddCond in lemma add_rel_left {T₁ T₁' T₂ : 𝓣.TensorIndex} (h : AddCond T₁ T₂) (h' : T₁ ≈ T₁') : T₁ +[h] T₂ ≈ T₁' +[h.rel_left h'] T₂ := by - apply And.intro (PermContr.refl _) + apply And.intro ContrPerm.refl intro h - simp only [contr_index, add_index, contr_add_tensor, add_tensor, toEquiv, map_add, mapIso_mapIso, - PermContr.toEquiv_refl, Equiv.refl_symm, mapIso_refl, LinearEquiv.refl_apply] + simp only [contr_add_tensor, add_tensor, map_add] congr 1 rw [h'.to_eq] - simp only [mapIso_mapIso] - congr 1 - congr 1 - rw [PermContr.toEquiv_symm, ← PermContr.toEquiv_contr_eq, PermContr.toEquiv_trans, - PermContr.toEquiv_trans, PermContr.toEquiv_trans] - simp only [IndexListColor.contr_contr] + simp only [contr_toColorIndexList, add_toColorIndexList, colorMap', addCondEquiv, + contrPermEquiv_symm, mapIso_mapIso, contrPermEquiv_trans, contrPermEquiv_refl, Equiv.refl_symm, + mapIso_refl, LinearEquiv.refl_apply] + simp only [contr_toColorIndexList, add_toColorIndexList, colorMap', contrPermEquiv_refl, + Equiv.refl_symm, mapIso_refl, LinearEquiv.refl_apply] open AddCond in lemma add_rel_right {T₁ T₂ T₂' : 𝓣.TensorIndex} (h : AddCond T₁ T₂) (h' : T₂ ≈ T₂') : @@ -442,17 +459,15 @@ lemma add_rel_right {T₁ T₂ T₂' : 𝓣.TensorIndex} (h : AddCond T₁ T₂) open AddCond in lemma add_assoc' {T₁ T₂ T₃ : 𝓣.TensorIndex} {h' : AddCond T₂ T₃} (h : AddCond T₁ (T₂ +[h'] T₃)) : T₁ +[h] (T₂ +[h'] T₃) = T₁ +[h'.of_add_right h] T₂ +[h'.add_left_of_add_right h] T₃ := by - refine ext _ _ ?_ ?_ - simp only [add_index, IndexListColor.contr_contr] - simp only [add_index, add_tensor, contr_index, toEquiv, contr_add_tensor, map_add, mapIso_mapIso] + refine ext ?_ ?_ + simp only [add_toColorIndexList, ColorIndexList.contr_contr] + simp only [add_toColorIndexList, add_tensor, contr_toColorIndexList, addCondEquiv, + contr_add_tensor, map_add, mapIso_mapIso] rw [_root_.add_assoc] congr - rw [← PermContr.toEquiv_contr_eq, ← PermContr.toEquiv_contr_eq] - rw [PermContr.toEquiv_trans, PermContr.toEquiv_trans, PermContr.toEquiv_trans] - simp only [IndexListColor.contr_contr] - simp only [IndexListColor.contr_contr] - rw [← PermContr.toEquiv_contr_eq, PermContr.toEquiv_trans] - simp only [IndexListColor.contr_contr] + rw [← contrPermEquiv_self_contr, ← contrPermEquiv_self_contr] + rw [contrPermEquiv_trans, contrPermEquiv_trans, contrPermEquiv_trans] + erw [← contrPermEquiv_self_contr, contrPermEquiv_trans] open AddCond in lemma add_assoc {T₁ T₂ T₃ : 𝓣.TensorIndex} {h' : AddCond T₁ T₂} (h : AddCond (T₁ +[h'] T₂) T₃) : @@ -467,43 +482,27 @@ lemma add_assoc {T₁ T₂ T₃ : 𝓣.TensorIndex} {h' : AddCond T₁ T₂} (h -/ -/-- 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) + T₁.AppendCond T₂ namespace ProdCond -lemma to_indexListColorProp {T₁ T₂ : 𝓣.TensorIndex} (h : ProdCond T₁ T₂) : - IndexListColorProp 𝓣.toTensorColor (T₁.contr.index.1 ++ T₂.contr.index.1) := h +lemma to_AppendCond {T₁ T₂ : 𝓣.TensorIndex} (h : ProdCond T₁ T₂) : + T₁.AppendCond T₂ := 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) + toColorIndexList := T₁ ++[h] T₂ + tensor := 𝓣.mapIso IndexList.appendEquiv (T₁.colorMap_sumELim T₂) <| + 𝓣.tensoratorEquiv _ _ (T₁.tensor ⊗ₜ[R] T₂.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 - +lemma prod_toColorIndexList (T₁ T₂ : 𝓣.TensorIndex) (h : ProdCond T₁ T₂) : + (prod T₁ T₂ h).toColorIndexList = T₁.toColorIndexList ++[h] T₂.toColorIndexList := rfl end TensorIndex end diff --git a/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean b/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean index 4c9261f..7eee821 100644 --- a/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean +++ b/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.SpaceTime.LorentzTensor.IndexNotation.TensorIndex -import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexString +import HepLean.SpaceTime.LorentzTensor.IndexNotation.Indices.IndexString import HepLean.SpaceTime.LorentzTensor.Real.Basic /-! @@ -56,6 +56,11 @@ lemma indexNotation_eq_color : @realLorentzTensor.instIndexNotationColor d = instIndexNotationColorRealTensorColor := by rfl +@[simp] +lemma decidableEq_eq_color : @realLorentzTensor.instDecidableEqColor d = + instDecidableEqColorRealTensorColor := by + rfl + @[simp] lemma realLorentzTensor_color : (realLorentzTensor d).Color = realTensorColor.Color := by rfl @@ -74,24 +79,44 @@ open TensorStructure TensorIndex noncomputable def fromIndexStringColor {cn : Fin n → realTensorColor.Color} (T : (realLorentzTensor d).Tensor cn) (s : String) (hs : listCharIndexStringBool realTensorColor.Color s.toList = true) - (hn : n = (IndexString.toIndexList (⟨s, hs⟩ : IndexString realTensorColor.Color)).length) - (hc : IndexListColor.colorPropBool (IndexString.toIndexList ⟨s, hs⟩)) - (hd : TensorColor.ColorMap.DualMap.boolFin - (IndexString.toIndexList ⟨s, hs⟩).colorMap (cn ∘ Fin.cast hn.symm)) : + (hn : n = (toIndexList' s hs).length) + (hD : (toIndexList' s hs).withDual = (toIndexList' s hs).withUniqueDual) + (hC : IndexList.ColorCond.bool (toIndexList' s hs)) + (hd : TensorColor.ColorMap.DualMap.boolFin (toIndexList' s hs).colorMap (cn ∘ Fin.cast hn.symm)) : (realLorentzTensor d).TensorIndex := - TensorStructure.TensorIndex.mkDualMap T - ⟨(IndexString.toIndexList (⟨s, hs⟩ : IndexString realTensorColor.Color)), - IndexListColor.colorPropBool_indexListColorProp hc⟩ hn + TensorStructure.TensorIndex.mkDualMap T ⟨(toIndexList' s hs), hD, + IndexList.ColorCond.iff_bool.mpr hC⟩ hn (TensorColor.ColorMap.DualMap.boolFin_DualMap hd) +@[simp] +lemma fromIndexStringColor_toIndexColorList + {cn : Fin n → realTensorColor.Color} + (T : (realLorentzTensor d).Tensor cn) (s : String) + (hs : listCharIndexStringBool realTensorColor.Color s.toList = true) + (hn : n = (toIndexList' s hs).length) + (hD : (toIndexList' s hs).withDual = (toIndexList' s hs).withUniqueDual) + (hC : IndexList.ColorCond.bool (toIndexList' s hs)) + (hd : TensorColor.ColorMap.DualMap.boolFin (toIndexList' s hs).colorMap (cn ∘ Fin.cast hn.symm)) : + (fromIndexStringColor T s hs hn hD hC hd).toColorIndexList = + ⟨(toIndexList' s hs), hD, + IndexList.ColorCond.iff_bool.mpr hC⟩ := by + rfl + /-- A tactics used to prove `colorPropBool` for real Lorentz tensors. -/ macro "prodTactic" : tactic => `(tactic| { - change @IndexListColor.colorPropBool realTensorColor _ _ _ - simp only [toTensorColor_eq, indexNotation_eq_color, fromIndexStringColor, mkDualMap, - String.toList, ↓Char.isValue, Equiv.coe_refl, Function.comp_apply, id_eq, ne_eq, - Function.comp_id, RelIso.coe_fn_toEquiv, prod_index, IndexListColor.prod] - rfl}) + apply (ColorIndexList.AppendCond.iff_bool _ _).mpr + change @ColorIndexList.AppendCond.bool realTensorColor instIndexNotationColorRealTensorColor instDecidableEqColorRealTensorColor + _ _ + simp only [indexNotation_eq_color, fromIndexStringColor, mkDualMap, toTensorColor_eq, + String.toList, ne_eq, decidableEq_eq_color] + rw [ColorIndexList.AppendCond.bool] + rw [Bool.if_false_left, Bool.and_eq_true] + simp only [indexNotation_eq_color, decidableEq_eq_color, toTensorColor_eq, + prod_toColorIndexList, ColorIndexList.append_toIndexList, decide_not, Bool.not_not] + apply And.intro + · rfl + · rfl}) /-- A tactic used to prove `boolFin` for real Lornetz tensors. -/ macro "dualMapTactic" : tactic => @@ -101,18 +126,21 @@ macro "dualMapTactic" : tactic => /-- Notation for the construction of a tensor index from a tensor and a string. Conditions are checked automatically. -/ -notation:20 T "|" S:21 => fromIndexStringColor T S (by rfl) (by rfl) (by rfl) (by dualMapTactic) +notation:20 T "|" S:21 => fromIndexStringColor T S (by rfl) (by rfl) (by rfl) (by rfl) (by dualMapTactic) /-- Notation for the product of two tensor indices. Conditions are checked automatically. -/ -notation:10 T "⊗ᵀ" S:11 => TensorIndex.prod T S (IndexListColor.colorPropBool_indexListColorProp - (by prodTactic)) +notation:10 T "⊗ᵀ" S:11 => TensorIndex.prod T S (by prodTactic) +/-(IndexListColor.colorPropBool_indexListColorProp + (by prodTactic))-/ + +def colorIndexListCast (l : ColorIndexList realTensorColor) : ColorIndexList (realLorentzTensor d).toTensorColor := + l /-- An example showing the allowed constructions. -/ example (T : (realLorentzTensor d).Tensor ![ColorType.up, ColorType.down]) : True := by - let _ := T|"ᵤ₁ᵤ₂" - let _ := T|"ᵘ³ᵤ₄" - let _ := T|"ᵤ₁ᵤ₂" ⊗ᵀ T|"ᵘ³ᵤ₄" - let _ := T|"ᵤ₁ᵤ₂" ⊗ᵀ T|"ᵘ³ᵤ₄" ⊗ᵀ T|"ᵘ¹ᵘ²" ⊗ᵀ T|"ᵘ⁴ᵤ₃" + let _ := fromIndexStringColor T "ᵤ₁ᵤ₂" (by rfl) (by rfl) (by rfl) (by + rfl) (by dualMapTactic) + let _ := T|"ᵤ₁ᵤ₂" ⊗ᵀ T|"ᵘ³ᵤ₄" ⊗ᵀ T|"ᵘ¹ᵘ⁴" exact trivial end realLorentzTensor