From e458300359c1fb58058211450933cba53bc0e7ad Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 15 Aug 2024 07:30:12 -0400 Subject: [PATCH] refactor: Delete unused files --- HepLean.lean | 4 +- .../IndexNotation/{Indices => }/Basic.lean | 0 .../IndexNotation/{Indices => }/Color.lean | 14 +- .../IndexNotation/{Indices => }/Dual.lean | 3 +- .../LorentzTensor/IndexNotation/GetDual.lean | 223 ---- .../IndexNotation/IndexListColor.lean | 462 --------- .../IndexNotation/IndexListColorV2.lean | 515 ---------- .../{Indices => }/IndexString.lean | 0 .../IndexNotation/Indices/Append.lean | 952 ------------------ .../IndexNotation/Indices/DualInOther.lean | 105 -- .../IndexNotation/Indices/UniqueDual.lean | 439 -------- .../Indices/UniqueDualInOther.lean | 141 --- .../{Indices => }/Relations.lean | 2 +- .../IndexNotation/TensorIndex.lean | 11 +- .../LorentzTensor/Real/IndexNotation.lean | 54 +- 15 files changed, 37 insertions(+), 2888 deletions(-) rename HepLean/SpaceTime/LorentzTensor/IndexNotation/{Indices => }/Basic.lean (100%) rename HepLean/SpaceTime/LorentzTensor/IndexNotation/{Indices => }/Color.lean (97%) rename HepLean/SpaceTime/LorentzTensor/IndexNotation/{Indices => }/Dual.lean (99%) delete mode 100644 HepLean/SpaceTime/LorentzTensor/IndexNotation/GetDual.lean delete mode 100644 HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColor.lean delete mode 100644 HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColorV2.lean rename HepLean/SpaceTime/LorentzTensor/IndexNotation/{Indices => }/IndexString.lean (100%) delete mode 100644 HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Append.lean delete mode 100644 HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/DualInOther.lean delete mode 100644 HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/UniqueDual.lean delete mode 100644 HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/UniqueDualInOther.lean rename HepLean/SpaceTime/LorentzTensor/IndexNotation/{Indices => }/Relations.lean (98%) diff --git a/HepLean.lean b/HepLean.lean index 72a54e4..9bb97ff 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -73,8 +73,10 @@ import HepLean.SpaceTime.LorentzGroup.Rotations import HepLean.SpaceTime.LorentzTensor.Basic import HepLean.SpaceTime.LorentzTensor.Contraction import HepLean.SpaceTime.LorentzTensor.IndexNotation.Basic -import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexListColor +import HepLean.SpaceTime.LorentzTensor.IndexNotation.Color +import HepLean.SpaceTime.LorentzTensor.IndexNotation.Dual import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexString +import HepLean.SpaceTime.LorentzTensor.IndexNotation.Relations import HepLean.SpaceTime.LorentzTensor.IndexNotation.TensorIndex import HepLean.SpaceTime.LorentzTensor.MulActionTensor import HepLean.SpaceTime.LorentzTensor.Real.Basic diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Basic.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean similarity index 100% rename from HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Basic.lean rename to HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Color.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Color.lean similarity index 97% rename from HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Color.lean rename to HepLean/SpaceTime/LorentzTensor/IndexNotation/Color.lean index 0a19b2f..7f1de72 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Color.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Color.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ -import HepLean.SpaceTime.LorentzTensor.IndexNotation.Indices.Dual +import HepLean.SpaceTime.LorentzTensor.IndexNotation.Dual import HepLean.SpaceTime.LorentzTensor.Basic import Init.Data.List.Lemmas import HepLean.SpaceTime.LorentzTensor.Contraction @@ -505,13 +505,17 @@ lemma appendCond_of_eq (h1 : l.withUniqueDual = l.withDual) 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 +def bool (l l2 : IndexList 𝓒.Color) : Bool := + if ¬ (l ++ l2).withUniqueDual = (l ++ l2).withDual then false else - ColorCond.bool (l.toIndexList ++ l2.toIndexList) + ColorCond.bool (l ++ l2) -lemma iff_bool (l l2 : ColorIndexList 𝓒) : AppendCond l l2 ↔ bool l l2 := by +lemma bool_iff (l l2 : IndexList 𝓒.Color) : + bool l l2 ↔ (l ++ l2).withUniqueDual = (l ++ l2).withDual ∧ ColorCond.bool (l ++ l2) := by + simp [bool] + +lemma iff_bool (l l2 : ColorIndexList 𝓒) : AppendCond l l2 ↔ bool l.toIndexList l2.toIndexList := by rw [AppendCond] simp [bool] rw [ColorCond.iff_bool] diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Dual.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Dual.lean similarity index 99% rename from HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Dual.lean rename to HepLean/SpaceTime/LorentzTensor/IndexNotation/Dual.lean index 3d982da..d4d692b 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Dual.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Dual.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ -import HepLean.SpaceTime.LorentzTensor.IndexNotation.Indices.Basic +import HepLean.SpaceTime.LorentzTensor.IndexNotation.Basic import HepLean.SpaceTime.LorentzTensor.Basic /-! @@ -2088,7 +2088,6 @@ lemma withUniqueDualInOther_eq_univ_contr_refl : 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 diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/GetDual.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/GetDual.lean deleted file mode 100644 index 21d63df..0000000 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/GetDual.lean +++ /dev/null @@ -1,223 +0,0 @@ -/- -Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joseph Tooby-Smith --/ -import HepLean.SpaceTime.LorentzTensor.IndexNotation.DualIndex -/-! - -# Dual indices - --/ - -namespace IndexNotation - - -namespace IndexList - -variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X] -variable (l l2 : IndexList X) - -def getDual? (i : Fin l.length) : Option (Fin l.length) := - Fin.find (fun j => i ≠ j ∧ l.idMap i = l.idMap j) - -def getDualInOther? (i : Fin l.length) : Option (Fin l2.length) := - Fin.find (fun j => l.idMap i = l2.idMap j) - -/-! - -## Finite sets of duals - --/ - -def withDual : Finset (Fin l.length) := - Finset.filter (fun i => (l.getDual? i).isSome) Finset.univ - -def getDual (i : l.withDual) : Fin l.length := - (l.getDual? i).get (by simpa [withDual] using i.2) - -def withoutDual : Finset (Fin l.length) := - Finset.filter (fun i => (l.getDual? i).isNone) Finset.univ - -def withDualOther : Finset (Fin l.length) := - Finset.filter (fun i => (l.getDualInOther? l2 i).isSome) Finset.univ - -def withoutDualOther : Finset (Fin l.length) := - Finset.filter (fun i => (l.getDualInOther? l2 i).isNone) Finset.univ - -lemma withDual_disjoint_withoutDual : Disjoint l.withDual l.withoutDual := by - rw [Finset.disjoint_iff_ne] - intro a ha b hb - by_contra hn - subst hn - simp_all only [withDual, Finset.mem_filter, Finset.mem_univ, true_and, withoutDual, - Option.isNone_iff_eq_none, Option.isSome_none, Bool.false_eq_true] - -lemma withDual_union_withoutDual : l.withDual ∪ l.withoutDual = Finset.univ := by - rw [Finset.eq_univ_iff_forall] - intro i - by_cases h : (l.getDual? i).isSome - · simp [withDual, Finset.mem_filter, Finset.mem_univ, h] - · simp at h - simp [withoutDual, Finset.mem_filter, Finset.mem_univ, h] - -lemma withDualOther_disjoint_withoutDualOther : - Disjoint (l.withDualOther l2) (l.withoutDualOther l2) := by - rw [Finset.disjoint_iff_ne] - intro a ha b hb - by_contra hn - subst hn - simp_all only [withDualOther, Finset.mem_filter, Finset.mem_univ, true_and, withoutDualOther, - Option.isNone_iff_eq_none, Option.isSome_none, Bool.false_eq_true] - -lemma withDualOther_union_withoutDualOther : - l.withDualOther l2 ∪ l.withoutDualOther l2 = Finset.univ := by - rw [Finset.eq_univ_iff_forall] - intro i - by_cases h : (l.getDualInOther? l2 i).isSome - · simp [withDualOther, Finset.mem_filter, Finset.mem_univ, h] - · simp at h - simp [withoutDualOther, Finset.mem_filter, Finset.mem_univ, h] - -def dualEquiv : l.withDual ⊕ l.withoutDual ≃ Fin l.length := - (Equiv.Finset.union _ _ l.withDual_disjoint_withoutDual).trans <| - Equiv.subtypeUnivEquiv (Finset.eq_univ_iff_forall.mp l.withDual_union_withoutDual) - -def dualEquivOther : l.withDualOther l2 ⊕ l.withoutDualOther l2 ≃ Fin l.length := - (Equiv.Finset.union _ _ (l.withDualOther_disjoint_withoutDualOther l2)).trans - (Equiv.subtypeUnivEquiv - (Finset.eq_univ_iff_forall.mp (l.withDualOther_union_withoutDualOther l2))) - -/-! - -## Index lists where `getDual?` is invertiable. --/ - -def InverDual : Prop := - ∀ i, (l.getDual? i).bind l.getDual? = some i - -namespace InverDual - -variable {l : IndexList X} (h : l.InverDual) (i : Fin l.length) - - -end InverDual - -def InverDualOther : Prop := - ∀ i, (l.getDualInOther? l2 i).bind (l2.getDualInOther? l) = some i - ∧ ∀ i, (l2.getDualInOther? l i).bind (l.getDualInOther? l2) = some i - - -section Color - -variable {𝓒 : TensorColor} -variable [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color] -variable (l l2 : IndexList 𝓒.Color) -/-! - -## Has single dual of correct color - --/ - -def IndexListColor (𝓒 : TensorColor) [IndexNotation 𝓒.Color] : Type := {l : IndexList X // - ∀ i, (l.getDual? i).bind l.getDual? = some i ∧ - Option.map (l.colorMap) ∘ l.getDual? = Option.map () - } - -end color -/-! - -## Append relations - --/ - -@[simp] -lemma getDual_append_inl (i : Fin l.length) : (l ++ l2).getDual (appendEquiv (Sum.inl i)) = - Option.or (Option.map (appendEquiv ∘ Sum.inl) (l.getDual i)) - (Option.map (appendEquiv ∘ Sum.inr) (l.getDualOther l2 i)) := by - by_cases h : (l ++ l2).HasDualInSelf (appendEquiv (Sum.inl i)) - · rw [(l ++ l2).getDual_of_hasDualInSelf h] - by_cases hl : l.HasDualInSelf i - · rw [l.getDual_of_hasDualInSelf hl] - simp - exact HasDualInSelf.getFirst_append_inl_of_hasDualInSelf l l2 h hl - · rw [l.getDual_of_not_hasDualInSelf hl] - simp at h hl - simp_all - rw [l.getDualOther_of_hasDualInOther l2 h] - simp only [Option.map_some', Function.comp_apply] - · rw [(l ++ l2).getDual_of_not_hasDualInSelf h] - simp at h - rw [l.getDual_of_not_hasDualInSelf h.1] - rw [l.getDualOther_of_not_hasDualInOther l2 h.2] - rfl - -@[simp] -lemma getDual_append_inr (i : Fin l2.length) : (l ++ l2).getDual (appendEquiv (Sum.inr i)) = - Option.or (Option.map (appendEquiv ∘ Sum.inl) (l2.getDualOther l i)) - (Option.map (appendEquiv ∘ Sum.inr) (l2.getDual i)) := by - by_cases h : (l ++ l2).HasDualInSelf (appendEquiv (Sum.inr i)) - · rw [(l ++ l2).getDual_of_hasDualInSelf h] - by_cases hl1 : l2.HasDualInOther l i - · rw [l2.getDualOther_of_hasDualInOther l hl1] - simp - exact HasDualInSelf.getFirst_append_inr_of_hasDualInOther l l2 h hl1 - · rw [l2.getDualOther_of_not_hasDualInOther l hl1] - simp at h hl1 - simp_all - rw [l2.getDual_of_hasDualInSelf h] - simp only [Option.map_some', Function.comp_apply] - · rw [(l ++ l2).getDual_of_not_hasDualInSelf h] - simp at h - rw [l2.getDual_of_not_hasDualInSelf h.1] - rw [l2.getDualOther_of_not_hasDualInOther l h.2] - rfl - -def HasSingDualsInSelf : Prop := - ∀ i, (l.getDual i).bind l.getDual = some i - -def HasSingDualsInOther : Prop := - (∀ i, (l.getDualOther l2 i).bind (l2.getDualOther l) = some i) - ∧ (∀ i, (l2.getDualOther l i).bind (l.getDualOther l2) = some i) - -def HasNoDualsInSelf : Prop := l.getDual = fun _ => none - -lemma hasSingDualsInSelf_append (h1 : l.HasNoDualsInSelf) (h2 : l2.HasNoDualsInSelf) : - (l ++ l2).HasSingDualsInSelf ↔ HasSingDualsInOther l l2 := by - apply Iff.intro - · intro h - simp [HasSingDualsInOther] - apply And.intro - · intro i - have h3 := h (appendEquiv (Sum.inl i)) - simp at h3 - rw [h1] at h3 - simp at h3 - by_cases hn : l.HasDualInOther l2 i - · rw [l.getDualOther_of_hasDualInOther l2 hn] at h3 ⊢ - simp only [Option.map_some', Function.comp_apply, Option.some_bind, getDual_append_inr] at h3 - rw [h2] at h3 - simpa using h3 - · rw [l.getDualOther_of_not_hasDualInOther l2 hn] at h3 ⊢ - simp at h3 - · intro i - have h3 := h (appendEquiv (Sum.inr i)) - simp at h3 - rw [h2] at h3 - simp at h3 - by_cases hn : l2.HasDualInOther l i - · rw [l2.getDualOther_of_hasDualInOther l hn] at h3 ⊢ - simp only [Option.map_some', Function.comp_apply, Option.some_bind, getDual_append_inl] at h3 - rw [h1] at h3 - simpa using h3 - · rw [l2.getDualOther_of_not_hasDualInOther l hn] at h3 ⊢ - simp at h3 - · intro h - intro i - obtain ⟨k, hk⟩ := appendEquiv.surjective i - - sorry - -end IndexList - -end IndexNotation diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColor.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColor.lean deleted file mode 100644 index 87d5c69..0000000 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColor.lean +++ /dev/null @@ -1,462 +0,0 @@ -/- -Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joseph Tooby-Smith --/ -import HepLean.SpaceTime.LorentzTensor.IndexNotation.Basic -import HepLean.SpaceTime.LorentzTensor.Basic -import Init.Data.List.Lemmas -/-! - -# Index lists with color conditions - -Here we consider `IndexListColor` which is a subtype of all lists of indices -on those where the elements to be contracted have consistent colors with respect to -a Tensor Color structure. - --/ - -namespace IndexNotation - -open IndexNotation - -variable (𝓒 : TensorColor) -variable [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color] - -/-- An index list is allowed if every contracting index has exactly one dual, - and the color of the dual is dual to the color of the index. -/ -def IndexListColorProp (l : IndexList 𝓒.Color) : Prop := - (∀ (i j : l.contrSubtype), l.AreDual i.1 j.1 → j = l.getDual i) ∧ - (∀ (i : l.contrSubtype), l.colorMap i.1 = 𝓒.τ (l.colorMap (l.getDual i).1)) - -instance : DecidablePred (IndexListColorProp 𝓒) := fun _ => And.decidable - -/-- The type of index lists which satisfy `IndexListColorProp`. -/ -def IndexListColor : Type := {s : IndexList 𝓒.Color // IndexListColorProp 𝓒 s} - -namespace IndexListColor - -open IndexList - -variable {𝓒 : TensorColor} -variable [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color] -variable (l : IndexListColor 𝓒) -instance : Coe (IndexListColor 𝓒) (IndexList 𝓒.Color) := ⟨fun x => x.val⟩ - -lemma indexListColorProp_of_hasNoContr {s : IndexList 𝓒.Color} (h : s.HasNoContr) : - IndexListColorProp 𝓒 s := by - simp [IndexListColorProp] - haveI : IsEmpty (s.contrSubtype) := s.contrSubtype_is_empty_of_hasNoContr h - simp - -/-! - -## Conditions related to IndexListColorProp - --/ - -/-- The bool which is true if ever index appears at most once in the first element of entries of - `l.contrPairList`. I.e. If every element contracts with at most one other element. -/ -def colorPropFstBool (l : IndexList 𝓒.Color) : Bool := - let l' := List.product l.contrPairList l.contrPairList - let l'' := l'.filterMap fun (i, j) => if i.1 = j.1 ∧ i.2 ≠ j.2 then some i else none - List.isEmpty l'' - -lemma colorPropFstBool_indexListColorProp_fst (l : IndexList 𝓒.Color) (hl : colorPropFstBool l) : - ∀ (i j : l.contrSubtype), l.AreDual i.1 j.1 → j = l.getDual i := by - simp [colorPropFstBool] at hl - rw [List.filterMap_eq_nil] at hl - simp at hl - intro i j hij - have hl' := hl i.1 j.1 i.1 (l.getDual i).1 - simp [contrPairList] at hl' - have h1 {n : ℕ} (m : Fin n) : m ∈ Fin.list n := by - have h1' : (Fin.list n)[m] = m := by - erw [Fin.getElem_list] - rfl - rw [← h1'] - apply List.getElem_mem - apply Subtype.ext (hl' (h1 _) (h1 _) hij (h1 _) (h1 _) (l.getDual_getDualProp i)) - -/-- The bool which is true if the pairs in `l.contrPairList` have dual colors. -/ -def colorPropSndBool (l : IndexList 𝓒.Color) : Bool := - List.all l.contrPairList (fun (i, j) => l.colorMap i = 𝓒.τ (l.colorMap j)) - -lemma colorPropSndBool_indexListColorProp_snd (l : IndexList 𝓒.Color) - (hl2 : colorPropSndBool l) : - ∀ (i : l.contrSubtype), l.colorMap i.1 = 𝓒.τ (l.colorMap (l.getDual i).1) := by - simp [colorPropSndBool] at hl2 - intro i - have h2 := hl2 i.1 (l.getDual i).1 - simp [contrPairList] at h2 - have h1 {n : ℕ} (m : Fin n) : m ∈ Fin.list n := by - have h1' : (Fin.list n)[m] = m := by - erw [Fin.getElem_list] - rfl - rw [← h1'] - apply List.getElem_mem - exact h2 (h1 _) (h1 _) (l.getDual_getDualProp i) - -/-- The bool which is true if both `colorPropFstBool` and `colorPropSndBool` are true. -/ -def colorPropBool (l : IndexList 𝓒.Color) : Bool := - colorPropFstBool l && colorPropSndBool l - -lemma colorPropBool_indexListColorProp {l : IndexList 𝓒.Color} (hl : colorPropBool l) : - IndexListColorProp 𝓒 l := by - simp [colorPropBool] at hl - exact And.intro (colorPropFstBool_indexListColorProp_fst l hl.1) - (colorPropSndBool_indexListColorProp_snd l hl.2) - -/-! - -## Contraction pairs for IndexListColor - --/ - -/-! TODO: Would be nice to get rid of all of the `.1` which appear here. -/ -@[simp] -lemma getDual_getDual (i : l.1.contrSubtype) : - l.1.getDual (l.1.getDual i) = i := by - refine (l.prop.1 (l.1.getDual i) i ?_).symm - simp [AreDual] - apply And.intro - exact Subtype.coe_ne_coe.mpr (l.1.getDual_neq_self i).symm - exact (l.1.getDual_id i).symm - -lemma contrPairSet_fst_eq_dual_snd (x : l.1.contrPairSet) : x.1.1 = l.1.getDual x.1.2 := - (l.prop.1 (x.1.2) x.1.1 (And.intro (Fin.ne_of_gt x.2.1) x.2.2.symm)) - -lemma contrPairSet_snd_eq_dual_fst (x : l.1.contrPairSet) : x.1.2 = l.1.getDual x.1.1 := by - rw [contrPairSet_fst_eq_dual_snd, getDual_getDual] - -lemma contrPairSet_dual_snd_lt_self (x : l.1.contrPairSet) : - (l.1.getDual x.1.2).1 < x.1.2.1 := by - rw [← l.contrPairSet_fst_eq_dual_snd] - exact x.2.1 - -/-- An equivalence between two coppies of `l.1.contrPairSet` and `l.1.contrSubtype`. - This equivalence exists due to the ordering on pairs in `𝓒.contrPairSet s`. -/ -def contrPairEquiv : l.1.contrPairSet ⊕ l.1.contrPairSet ≃ l.1.contrSubtype where - toFun x := - match x with - | Sum.inl p => p.1.2 - | Sum.inr p => p.1.1 - invFun x := - if h : (l.1.getDual x).1 < x.1 then - Sum.inl ⟨(l.1.getDual x, x), l.1.getDual_lt_self_mem_contrPairSet h⟩ - else - Sum.inr ⟨(x, l.1.getDual x), l.1.getDual_not_lt_self_mem_contrPairSet h⟩ - left_inv x := by - match x with - | Sum.inl x => - simp only [Subtype.coe_lt_coe] - rw [dif_pos] - simp [← l.contrPairSet_fst_eq_dual_snd] - exact l.contrPairSet_dual_snd_lt_self _ - | Sum.inr x => - simp only [Subtype.coe_lt_coe] - rw [dif_neg] - simp only [← l.contrPairSet_snd_eq_dual_fst, Prod.mk.eta, Subtype.coe_eta] - rw [← l.contrPairSet_snd_eq_dual_fst] - have h1 := x.2.1 - simp only [not_lt, ge_iff_le] - exact le_of_lt h1 - right_inv x := by - by_cases h1 : (l.1.getDual x).1 < x.1 - simp only [h1, ↓reduceDIte] - simp only [h1, ↓reduceDIte] - -@[simp] -lemma contrPairEquiv_apply_inr (x : l.1.contrPairSet) : l.contrPairEquiv (Sum.inr x) = x.1.1 := by - simp [contrPairEquiv] - -@[simp] -lemma contrPairEquiv_apply_inl(x : l.1.contrPairSet) : l.contrPairEquiv (Sum.inl x) = x.1.2 := by - simp [contrPairEquiv] - -/-- An equivalence between `Fin s.length` and - `(𝓒.contrPairSet s ⊕ 𝓒.contrPairSet s) ⊕ Fin (𝓒.noContrFinset s).card`, which - can be used for contractions. -/ -def splitContr : Fin l.1.length ≃ - (l.1.contrPairSet ⊕ l.1.contrPairSet) ⊕ Fin (l.1.noContrFinset).card := - (Equiv.sumCompl l.1.NoContr).symm.trans <| - (Equiv.sumComm { i // l.1.NoContr i} { i // ¬ l.1.NoContr i}).trans <| - Equiv.sumCongr l.contrPairEquiv.symm l.1.noContrSubtypeEquiv - -lemma splitContr_map : - l.1.colorMap ∘ l.splitContr.symm ∘ Sum.inl ∘ Sum.inl = - 𝓒.τ ∘ l.1.colorMap ∘ l.splitContr.symm ∘ Sum.inl ∘ Sum.inr := by - funext x - simp [splitContr, contrPairEquiv_apply_inr] - erw [contrPairEquiv_apply_inr, contrPairEquiv_apply_inl] - rw [contrPairSet_fst_eq_dual_snd _ _] - exact l.prop.2 _ - -lemma splitContr_symm_apply_of_hasNoContr (h : l.1.HasNoContr) (x : Fin (l.1.noContrFinset).card) : - l.splitContr.symm (Sum.inr x) = Fin.castOrderIso (l.1.hasNoContr_noContrFinset_card h) x := by - simp [splitContr, noContrSubtypeEquiv, noContrFinset] - trans (Finset.univ.orderEmbOfFin (by rw [l.1.hasNoContr_noContrFinset_card h]; simp)) x - congr - rw [Finset.filter_true_of_mem (fun x _ => h x)] - rw [@Finset.orderEmbOfFin_apply] - simp only [List.get_eq_getElem, Fin.sort_univ, List.getElem_finRange] - rfl - -/-! - -## The contracted index list - --/ - -/-- The contracted index list as a `IndexListColor`. -/ -def contr : IndexListColor 𝓒 := - ⟨l.1.contr, indexListColorProp_of_hasNoContr l.1.contr_hasNoContr⟩ - -/-- Contracting twice is equivalent to contracting once. -/ -@[simp] -lemma contr_contr : l.contr.contr = l.contr := by - apply Subtype.ext - exact l.1.contr_contr - -@[simp] -lemma contr_numIndices : l.contr.1.numIndices = l.1.noContrFinset.card := - l.1.contr_numIndices - -lemma contr_colorMap : - l.1.colorMap ∘ l.splitContr.symm ∘ Sum.inr = l.contr.1.colorMap ∘ - (Fin.castOrderIso l.contr_numIndices.symm).toEquiv.toFun := by - funext x - simp only [Function.comp_apply, colorMap, List.get_eq_getElem, contr, IndexList.contr, fromFinMap, - Equiv.toFun_as_coe, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Fin.coe_cast, - List.getElem_map, Fin.getElem_list, Fin.cast_mk, Fin.eta] - rfl - -/-! TODO: Prove applying contr twice equals applying it once. -/ -/-! - -## Equivalence relation on IndexListColor due to permutation - --/ - -/-- Two index lists are related if there contracted lists have the same id's for indices, - and the color of indices with the same id sit are the same. - This will allow us to add and compare tensors. -/ -def PermContr (s1 s2 : IndexListColor 𝓒) : Prop := - List.Perm (s1.contr.1.map Index.id) (s2.contr.1.map Index.id) - ∧ ∀ (i : Fin s1.contr.1.length) (j : Fin s2.contr.1.length), - s1.contr.1.idMap i = s2.contr.1.idMap j → - s1.contr.1.colorMap i = s2.contr.1.colorMap j - -namespace PermContr - -lemma refl : Reflexive (@PermContr 𝓒 _) := by - intro l - simp only [PermContr, List.Perm.refl, true_and] - have h1 : l.contr.1.HasNoContr := l.1.contr_hasNoContr - exact fun i j a => hasNoContr_color_eq_of_id_eq (↑l.contr) h1 i j a - -lemma symm : Symmetric (@PermContr 𝓒 _) := - fun _ _ h => And.intro (List.Perm.symm h.1) fun i j hij => (h.2 j i hij.symm).symm - -/-- Given an index in `s1` the index in `s2` related by `PermContr` with the same id. -/ -def get {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) (i : Fin s1.contr.1.length) : - Fin s2.contr.1.length := - (Fin.find (fun j => s1.contr.1.idMap i = s2.contr.1.idMap j)).get (by - rw [Fin.isSome_find_iff] - have h2 : s1.contr.1.idMap i ∈ (List.map Index.id s2.contr.1) := by - rw [← List.Perm.mem_iff h.1] - simp only [List.mem_map] - use s1.contr.1.get i - simp_all only [true_and, List.get_eq_getElem] - apply And.intro - · exact List.getElem_mem (s1.contr.1) (↑i) i.isLt - · rfl - simp only [List.mem_map] at h2 - obtain ⟨j, hj1, hj2⟩ := h2 - obtain ⟨j', hj'⟩ := List.mem_iff_get.mp hj1 - use j' - rw [← hj2] - simp [idMap, hj'] - change _ = (s2.contr.1.get j').id - rw [hj']) - -lemma some_get_eq_find {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) - (i : Fin s1.contr.1.length) : - Fin.find (fun j => s1.contr.1.idMap i = s2.contr.1.idMap j) = some (h.get i) := by - simp [PermContr.get] - -lemma get_id {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) - (i : Fin s1.contr.1.length) : - s2.contr.1.idMap (h.get i) = s1.contr.1.idMap i := by - have h1 := h.some_get_eq_find i - rw [Fin.find_eq_some_iff] at h1 - exact h1.1.symm - -lemma get_unique {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) - {i : Fin s1.contr.1.length} {j : Fin s2.contr.1.length} - (hij : s1.contr.1.idMap i = s2.contr.1.idMap j) : - j = h.get i := by - by_contra hn - refine (?_ : ¬ s2.contr.1.NoContr j) (s2.1.contr_hasNoContr j) - simp [NoContr] - use PermContr.get h i - apply And.intro hn - rw [← hij, PermContr.get_id] - -lemma get_color {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) - (i : Fin s1.contr.1.length) : - s1.contr.1.colorMap i = s2.contr.1.colorMap (h.get i) := - h.2 i (h.get i) (h.get_id i).symm - -@[simp] -lemma get_symm_apply_get_apply {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) - (i : Fin s1.contr.1.length) : h.symm.get (h.get i) = i := - (h.symm.get_unique (h.get_id i)).symm - -lemma get_apply_get_symm_apply {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) - (i : Fin s2.contr.1.length) : h.get (h.symm.get i) = i := - (h.get_unique (h.symm.get_id i)).symm - -lemma trans {s1 s2 s3 : IndexListColor 𝓒} (h1 : PermContr s1 s2) (h2 : PermContr s2 s3) : - PermContr s1 s3 := by - apply And.intro (h1.1.trans h2.1) - intro i j hij - rw [h1.get_color i] - have hj : j = h2.get (h1.get i) := by - apply h2.get_unique - rw [get_id] - exact hij - rw [hj, h2.get_color] - -lemma get_trans {s1 s2 s3 : IndexListColor 𝓒} (h1 : PermContr s1 s2) (h2 : PermContr s2 s3) - (i : Fin s1.contr.1.length) : - (h1.trans h2).get i = h2.get (h1.get i) := by - apply h2.get_unique - rw [get_id, get_id] - -/-- Equivalence of indexing types for two `IndexListColor` related by `PermContr`. -/ -def toEquiv {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) : - Fin s1.contr.1.length ≃ Fin s2.contr.1.length where - toFun := h.get - invFun := h.symm.get - left_inv x := by - simp - right_inv x := by - simp - -lemma toEquiv_refl' {s : IndexListColor 𝓒} (h : PermContr s s) : - h.toEquiv = Equiv.refl _ := by - apply Equiv.ext - intro x - simp [toEquiv, get] - have h1 : Fin.find fun j => s.contr.1.idMap x = s.contr.1.idMap j = some x := by - rw [Fin.find_eq_some_iff] - have h2 := s.1.contr_hasNoContr x - simp only [true_and] - intro j hj - by_cases hjx : j = x - subst hjx - rfl - exact False.elim (h2 j (fun a => hjx a.symm) hj) - simp only [h1, Option.get_some] - -@[simp] -lemma toEquiv_refl {s : IndexListColor 𝓒} : - PermContr.toEquiv (PermContr.refl s) = Equiv.refl _ := by - exact PermContr.toEquiv_refl' _ - -lemma toEquiv_symm {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) : - h.toEquiv.symm = h.symm.toEquiv := by - rfl - -lemma toEquiv_colorMap {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) : - s2.contr.1.colorMap = s1.contr.1.colorMap ∘ h.toEquiv.symm := by - funext x - refine (h.2 _ _ ?_).symm - simp [← h.get_id, toEquiv] - -lemma toEquiv_colorMap' {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) : - s1.contr.1.colorMap = s2.contr.1.colorMap ∘ h.toEquiv := by - rw [toEquiv_colorMap h] - funext x - simp - -@[simp] -lemma toEquiv_trans {s1 s2 s3 : IndexListColor 𝓒} (h1 : PermContr s1 s2) (h2 : PermContr s2 s3) : - h1.toEquiv.trans h2.toEquiv = (h1.trans h2).toEquiv := by - apply Equiv.ext - intro x - simp [toEquiv] - rw [← get_trans] - -lemma of_contr_eq {s1 s2 : IndexListColor 𝓒} (hc : s1.contr = s2.contr) : - PermContr s1 s2 := by - simp [PermContr] - rw [hc] - simp only [List.Perm.refl, true_and] - refine hasNoContr_color_eq_of_id_eq s2.contr.1 (s2.1.contr_hasNoContr) - -lemma of_contr {s1 s2 : IndexListColor 𝓒} (hc : PermContr s1.contr s2.contr) : - PermContr s1 s2 := by - apply And.intro - simpa using hc.1 - have h2 := hc.2 - simp at h2 - rw [contr_contr, contr_contr] at h2 - exact h2 - -lemma toEquiv_contr_eq {s1 s2 : IndexListColor 𝓒} (hc : s1.contr = s2.contr) : - (of_contr_eq hc).toEquiv = (Fin.castOrderIso (by rw [hc])).toEquiv := by - apply Equiv.ext - intro x - simp [toEquiv, of_contr_eq, hc, get] - have h1 : (Fin.find fun j => (s1.contr).1.idMap x = (s2.contr).1.idMap j) = - some ((Fin.castOrderIso (by rw [hc]; rfl)).toEquiv x) := by - rw [Fin.find_eq_some_iff] - apply And.intro - rw [idMap_cast (congrArg Subtype.val hc)] - rfl - intro j hj - rw [idMap_cast (congrArg Subtype.val hc)] at hj - have h2 := s2.contr.1.hasNoContr_id_inj (s2.1.contr_hasNoContr) hj - subst h2 - rfl - simp only [h1, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Option.get_some] - -end PermContr - -/-! TODO: Show that `rel` is indeed an equivalence relation. -/ - -/-! - -## Appending two IndexListColor - --/ - -/-- Appending two `IndexListColor` whose correpsonding appended index list - satisfies `IndexListColorProp`. -/ -def prod (s1 s2 : IndexListColor 𝓒) (h : IndexListColorProp 𝓒 (s1.1 ++ s2.1)) : - IndexListColor 𝓒 := ⟨s1.1 ++ s2.1, h⟩ - -lemma prod_numIndices {s1 s2 : IndexListColor 𝓒} : - (s1.1 ++ s2.1).numIndices = s1.1.numIndices + s2.1.numIndices := - List.length_append s1.1 s2.1 - -lemma prod_colorMap {s1 s2 : IndexListColor 𝓒} (h : IndexListColorProp 𝓒 (s1.1 ++ s2.1)) : - Sum.elim s1.1.colorMap s2.1.colorMap = - (s1.prod s2 h).1.colorMap ∘ ((Fin.castOrderIso prod_numIndices).toEquiv.trans - finSumFinEquiv.symm).symm := by - funext x - match x with - | Sum.inl x => - simp [prod, colorMap, fromFinMap] - rw [List.getElem_append_left] - | Sum.inr x => - simp [prod, colorMap, fromFinMap] - rw [List.getElem_append_right] - simp [numIndices] - simp [numIndices] - simp [numIndices] -end IndexListColor - -end IndexNotation diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColorV2.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColorV2.lean deleted file mode 100644 index b0bd78c..0000000 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColorV2.lean +++ /dev/null @@ -1,515 +0,0 @@ -/- -Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joseph Tooby-Smith --/ -import HepLean.SpaceTime.LorentzTensor.IndexNotation.DualIndex -import HepLean.SpaceTime.LorentzTensor.Basic -import Init.Data.List.Lemmas -/-! - -# Index lists with color conditions - -Here we consider `IndexListColor` which is a subtype of all lists of indices -on those where the elements to be contracted have consistent colors with respect to -a Tensor Color structure. - --/ - -namespace IndexNotation - -def IndexListColor (𝓒 : TensorColor) [IndexNotation 𝓒.Color] : Type := - {l // (l : IndexList 𝓒.Color).HasSingColorDualsInSelf} - -namespace IndexListColor - -variable {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color] -variable (l : IndexListColor 𝓒) - -def length : ℕ := l.1.length - -def HasNoDualsSelf : Prop := l.1.HasNoDualsSelf - -def getDual? (i : Fin l.length) : Option (Fin l.length) := - if h : l.1.HasSingColorDualInSelf i then - some h.get - else none - -def withDualFinset : Finset (Fin l.length) := Finset.filter l.1.HasSingColorDualInSelf Finset.univ - -lemma withDualFinset_prop {l : IndexListColor 𝓒} (i : l.withDualFinset) : - l.1.HasSingColorDualInSelf i.1 := by - simpa [withDualFinset] using i.2 - -def withDualFinsetLT : Finset l.withDualFinset := - Finset.filter (fun i => i.1 < (withDualFinset_prop i).get) Finset.univ - -def withDualFinsetGT : Finset l.withDualFinset := - Finset.filter (fun i => (withDualFinset_prop i).get < i.1) Finset.univ - -def withDualFinsetLTGTEquiv : l.withDualFinsetLT ≃ l.withDualFinsetGT where - toFun x := ⟨⟨(withDualFinset_prop x.1).get, - by simpa [withDualFinset] using (withDualFinset_prop x.1).get_hasSingColorDualInSelf⟩, by - simpa [withDualFinsetGT, withDualFinsetLT] using x.2⟩ - invFun x := ⟨⟨(withDualFinset_prop x.1).get, - by simpa [withDualFinset] using (withDualFinset_prop x.1).get_hasSingColorDualInSelf⟩, by - simpa [withDualFinsetGT, withDualFinsetLT] using x.2⟩ - left_inv x := by - apply Subtype.ext - apply Subtype.ext - simp only [length, IndexList.HasSingColorDualInSelf.get_get] - right_inv x := by - apply Subtype.ext - apply Subtype.ext - simp only [length, IndexList.HasSingColorDualInSelf.get_get] - -lemma withDualFinsetLT_disjoint_withDualFinsetGT : - Disjoint l.withDualFinsetLT l.withDualFinsetGT := by - rw [Finset.disjoint_iff_ne] - intro a ha b hb - by_contra hn - subst hn - simp [withDualFinsetLT, withDualFinsetGT] at ha hb - omega - -lemma mem_withDualFinsetLT_union_withDualFinsetGT (x : l.withDualFinset) : - x ∈ l.withDualFinsetLT ∪ l.withDualFinsetGT := by - simpa [withDualFinsetLT, withDualFinsetGT] using (withDualFinset_prop x).areDualInSelf_get.1 - -def withDualEquiv : l.withDualFinsetLT ⊕ l.withDualFinsetLT ≃ l.withDualFinset := - (Equiv.sumCongr (Equiv.refl _) l.withDualFinsetLTGTEquiv).trans <| - (Equiv.Finset.union _ _ l.withDualFinsetLT_disjoint_withDualFinsetGT).trans <| - Equiv.subtypeUnivEquiv l.mem_withDualFinsetLT_union_withDualFinsetGT - -def withoutDualFinset : Finset (Fin l.length) := - Finset.filter (fun i => ¬ l.1.HasDualInSelf i) Finset.univ - -lemma mem_withoutDualFinset_iff_not_hasSingColorDualInSelf (i : Fin l.length) : - i ∈ l.withoutDualFinset ↔ ¬ l.1.HasSingColorDualInSelf i := by - simp [withoutDualFinset] - exact l.2.not_hasDualInSelf_iff_not_hasSingColorDualInSelf i - -lemma mem_withoutDualFinset_of_hasNoDualsSelf (h : l.HasNoDualsSelf) (i : Fin l.length) : - i ∈ l.withoutDualFinset := by - simpa [withoutDualFinset] using h i - -lemma withoutDualFinset_of_hasNoDualsSelf (h : l.HasNoDualsSelf) : - l.withoutDualFinset = Finset.univ := by - rw [@Finset.eq_univ_iff_forall] - exact l.mem_withoutDualFinset_of_hasNoDualsSelf h - -lemma withDualFinset_disjoint_withoutDualFinset : - Disjoint l.withDualFinset l.withoutDualFinset := by - rw [Finset.disjoint_iff_ne] - intro a ha b hb - by_contra hn - subst hn - rw [mem_withoutDualFinset_iff_not_hasSingColorDualInSelf] at hb - simp [withDualFinset, withoutDualFinset] at ha hb - exact hb ha - -lemma mem_withDualFinset_union_withoutDualFinset (x : Fin l.length) : - x ∈ l.withDualFinset ∪ l.withoutDualFinset := by - simp [withDualFinset] - rw [mem_withoutDualFinset_iff_not_hasSingColorDualInSelf] - exact Decidable.em (l.1.HasSingColorDualInSelf x) - -def dualEquiv : l.withDualFinset ⊕ l.withoutDualFinset ≃ Fin l.length := - (Equiv.Finset.union _ _ l.withDualFinset_disjoint_withoutDualFinset).trans <| - Equiv.subtypeUnivEquiv l.mem_withDualFinset_union_withoutDualFinset - -def withoutDualEquiv : Fin l.withoutDualFinset.card ≃ l.withoutDualFinset := - (Finset.orderIsoOfFin _ rfl).toEquiv - - -def withoutDualIndexList : IndexList 𝓒.Color := - (Fin.list l.withoutDualFinset.card).map (fun i => l.1.get (l.withoutDualEquiv i).1) - -@[simp] -lemma withoutDualIndexList_idMap (i : Fin (List.length l.withoutDualIndexList)) : - l.withoutDualIndexList.idMap i = - l.1.idMap (l.withoutDualEquiv (Fin.cast (by simp [withoutDualIndexList]) i)).1 := by - simp [withoutDualIndexList, IndexList.idMap] - rfl - -lemma withoutDualIndexList_hasNoDualsSelf : l.withoutDualIndexList.HasNoDualsSelf := by - intro i - simp [IndexList.HasDualInSelf, IndexList.AreDualInSelf] - intro x hx - have h1 : l.withoutDualEquiv (Fin.cast (by simp [withoutDualIndexList]) i) ≠ - l.withoutDualEquiv (Fin.cast (by simp [withoutDualIndexList]) x) := by - simp - rw [Fin.ext_iff] at hx ⊢ - simpa using hx - have hx' := (l.withoutDualEquiv (Fin.cast (by simp [withoutDualIndexList]) i)).2 - simp [withoutDualFinset, IndexList.HasDualInSelf, IndexList.AreDualInSelf] at hx' - refine hx' (l.withoutDualEquiv (Fin.cast (by simp [withoutDualIndexList]) x)).1 ?_ - simp only [length] - rw [← Subtype.eq_iff] - exact h1 - -lemma withoutDualIndexList_of_hasNoDualsSelf (h : l.1.HasNoDualsSelf ) : - l.withoutDualIndexList = l.1 := by - simp [withoutDualIndexList, List.get_eq_getElem] - apply List.ext_get - · simp only [List.length_map, Fin.length_list] - rw [l.withoutDualFinset_of_hasNoDualsSelf h] - simp only [Finset.card_univ, Fintype.card_fin] - rfl - intro n h1 h2 - simp - congr - simp [withoutDualEquiv] - have h1 : l.withoutDualFinset.orderEmbOfFin rfl = - (Fin.castOrderIso (by - rw [l.withoutDualFinset_of_hasNoDualsSelf h] - simp only [Finset.card_univ, Fintype.card_fin])).toOrderEmbedding := by - symm - refine Finset.orderEmbOfFin_unique' (Eq.refl l.withoutDualFinset.card) - (fun x => mem_withoutDualFinset_of_hasNoDualsSelf l h _) - rw [h1] - rfl - -def contr : IndexListColor 𝓒 := - ⟨l.withoutDualIndexList, l.withoutDualIndexList_hasNoDualsSelf.toHasSingColorDualsInSelf⟩ - -lemma contr_length : l.contr.1.length = l.withoutDualFinset.card := by - simp [contr, withoutDualIndexList] - -@[simp] -lemma contr_id (i : Fin l.contr.length) : l.contr.1.idMap i = - l.1.idMap (l.withoutDualEquiv (Fin.cast l.contr_length i)).1 := by - simp [contr] - -lemma contr_hasNoDualsSelf : l.contr.1.HasNoDualsSelf := - l.withoutDualIndexList_hasNoDualsSelf - -lemma contr_of_hasNoDualsSelf (h : l.1.HasNoDualsSelf) : - l.contr = l := by - apply Subtype.ext - exact l.withoutDualIndexList_of_hasNoDualsSelf h - -@[simp] -lemma contr_contr : l.contr.contr = l.contr := - l.contr.contr_of_hasNoDualsSelf l.contr_hasNoDualsSelf - -/-! - -# Relations on IndexListColor - --/ -/- - l.getDual? ∘ Option.guard l.HasDualInSelf = - l.getDual? --/ -def Relabel (l1 l2 : IndexListColor 𝓒) : Prop := - l1.length = l2.length ∧ - ∀ (h : l1.length = l2.length), - l1.getDual? = Option.map (Fin.cast h.symm) ∘ l2.getDual? ∘ Fin.cast h ∧ - l1.1.colorMap = l2.1.colorMap ∘ Fin.cast h - -/-! TODO: Rewrite in terms of HasSingDualInOther. -/ -def PermAfterContr (l1 l2 : IndexListColor 𝓒) : Prop := - List.Perm (l1.contr.1.map Index.id) (l2.contr.1.map Index.id) - ∧ ∀ (i : Fin l1.contr.1.length) (j : Fin l2.contr.1.length), - l1.contr.1.idMap i = l2.contr.1.idMap j → - l1.contr.1.colorMap i = l2.contr.1.colorMap j - -def AppendHasSingColorDualsInSelf (l1 l2 : IndexListColor 𝓒) : Prop := - (l1.contr.1 ++ l2.contr.1).HasSingColorDualsInSelf - - -end IndexListColor - -/-- A proposition which is true if an index has at most one dual. -/ -def HasSubSingeDualSelf (i : Fin l.length) : Prop := - ∀ (h : l.HasDualSelf i) j, l.AreDualSelf i j → j = l.getDualSelf i h - -lemma HasSubSingeDualSelf.eq_dual_iff {l : IndexList X} {i : Fin l.length} - (h : l.HasSubSingeDualSelf i) (hi : l.HasDualSelf i) (j : Fin l.length) : - j = l.getDualSelf i hi ↔ l.AreDualSelf i j := by - have h1 := h hi j - apply Iff.intro - intro h - subst h - exact l.areDualSelf_of_getDualSelf i hi - exact h1 - -@[simp] -lemma getDualSelf_append_inl {l l2 : IndexList X} (i : Fin l.length) - (h : (l ++ l2).HasSubSingeDualSelf (appendEquiv (Sum.inl i))) (hi : l.HasDualSelf i) : - (l ++ l2).getDualSelf (appendEquiv (Sum.inl i)) ((hasDualSelf_append_inl l l2 i).mpr (Or.inl hi)) = - appendEquiv (Sum.inl (l.getDualSelf i hi)) := by - symm - rw [HasSubSingeDualSelf.eq_dual_iff h] - simp - exact areDualSelf_of_getDualSelf l i hi - -lemma HasSubSingeDualSelf.of_append_inl_of_hasDualSelf {l l2 : IndexList X} (i : Fin l.length) - (h : (l ++ l2).HasSubSingeDualSelf (appendEquiv (Sum.inl i))) (hi : l.HasDualSelf i) : - l.HasSubSingeDualSelf i := by - intro hj j - have h1 := h ((hasDualSelf_append_inl l l2 i).mpr (Or.inl hi)) (appendEquiv (Sum.inl j)) - intro hij - simp at h1 - have h2 := h1 hij - apply Sum.inl_injective - apply appendEquiv.injective - rw [h2, l.getDualSelf_append_inl _ h] - - -lemma HasSubSingeDualSelf.not_hasDualOther_of_append_inl_of_hasDualSelf - {l l2 : IndexList X} (i : Fin l.length) - (h : (l ++ l2).HasSubSingeDualSelf (appendEquiv (Sum.inl i))) (hi : l.HasDualSelf i) : - ¬ l.HasDualOther l2 i := by - simp [HasDualOther] - intro j - simp [AreDualOther] - simp [HasSubSingeDualSelf] at h - have h' := h ((hasDualSelf_append_inl l l2 i).mpr (Or.inl hi)) (appendEquiv (Sum.inr j)) - simp [AreDualSelf] at h' - by_contra hn - have h'' := h' hn - rw [l.getDualSelf_append_inl _ h hi] at h'' - simp at h'' - - -lemma HasSubSingeDualSelf.of_append_inr_of_hasDualSelf {l l2 : IndexList X} (i : Fin l2.length) - (h : (l ++ l2).HasSubSingeDualSelf (appendEquiv (Sum.inr i))) (hi : l2.HasDualSelf i) : - l2.HasSubSingeDualSelf i := by - intro hj j - have h1 := h ((hasDualSelf_append_inr l i).mpr (Or.inl hi)) (appendEquiv (Sum.inr j)) - intro hij - simp at h1 - have h2 := h1 hij - apply Sum.inr_injective - apply appendEquiv.injective - rw [h2] - symm - rw [eq_dual_iff h] - simp only [AreDualSelf.append_inr_inr] - exact areDualSelf_of_getDualSelf l2 i hj - - -lemma HasSubSingeDualSelf.append_inl (i : Fin l.length) : - (l ++ l2).HasSubSingeDualSelf (appendEquiv (Sum.inl i)) ↔ - (l.HasSubSingeDualSelf i ∧ ¬ l.HasDualOther l2 i) ∨ - (¬ l.HasDualSelf i ∧ l.HasSubSingeDualOther l2 i) := by - apply Iff.intro - · intro h - by_cases h1 : (l ++ l2).HasDualSelf (appendEquiv (Sum.inl i)) - rw [hasDualSelf_append_inl] at h1 - cases h1 <;> rename_i h1 - · exact Or.inl ⟨of_append_inl_of_hasDualSelf i h h1, - (not_hasDualOther_of_append_inl_of_hasDualSelf i h h1)⟩ - · sorry - - -def HasSubSingeDuals : Prop := ∀ i, l.HasSubSingeDual i - -def HasNoDual (i : Fin l.length) : Prop := ¬ l.HasDual i - -def HasNoDuals : Prop := ∀ i, l.HasNoDual i - - -lemma hasSubSingeDuals_of_hasNoDuals (h : l.HasNoDuals) : l.HasSubSingeDuals := by - intro i h1 j h2 - exfalso - apply h i - simp only [HasDual] - exact ⟨j, h2⟩ - -/-- The proposition on a element (or really index of element) of a index list - `s` which is ture iff does not share an id with any other element. - This tells us that it should not be contracted with any other element. -/ -def NoContr (i : Fin l.length) : Prop := - ∀ j, i ≠ j → l.idMap i ≠ l.idMap j - -instance (i : Fin l.length) : Decidable (l.NoContr i) := - Fintype.decidableForallFintype - -/-- The finset of indices of an index list corresponding to elements which do not contract. -/ -def noContrFinset : Finset (Fin l.length) := - Finset.univ.filter l.NoContr - -/-- An eqiuvalence between the subtype of indices of a index list `l` which do not contract and - `Fin l.noContrFinset.card`. -/ -def noContrSubtypeEquiv : {i : Fin l.length // l.NoContr i} ≃ Fin l.noContrFinset.card := - (Equiv.subtypeEquivRight (fun x => by simp [noContrFinset])).trans - (Finset.orderIsoOfFin l.noContrFinset rfl).toEquiv.symm - -@[simp] -lemma idMap_noContrSubtypeEquiv_neq (i j : Fin l.noContrFinset.card) (h : i ≠ j) : - l.idMap (l.noContrSubtypeEquiv.symm i).1 ≠ l.idMap (l.noContrSubtypeEquiv.symm j).1 := by - have hi := ((l.noContrSubtypeEquiv).symm i).2 - simp [NoContr] at hi - have hj := hi ((l.noContrSubtypeEquiv).symm j) - apply hj - rw [@SetCoe.ext_iff] - erw [Equiv.apply_eq_iff_eq] - exact h - -/-- The subtype of indices `l` which do contract. -/ -def contrSubtype : Type := {i : Fin l.length // ¬ l.NoContr i} - -instance : Fintype l.contrSubtype := - Subtype.fintype fun x => ¬ l.NoContr x - -instance : DecidableEq l.contrSubtype := - Subtype.instDecidableEq - -/-! - -## Getting the index which contracts with a given index - --/ - -lemma getDual_id (i : l.contrSubtype) : l.idMap i.1 = l.idMap (l.getDual i).1 := by - simp [getDual] - have h1 := l.some_getDualFin_eq_find i - rw [Fin.find_eq_some_iff] at h1 - simp only [AreDual, ne_eq, and_imp] at h1 - exact h1.1.2 - -lemma getDual_neq_self (i : l.contrSubtype) : i ≠ l.getDual i := by - have h1 := l.some_getDualFin_eq_find i - rw [Fin.find_eq_some_iff] at h1 - exact ne_of_apply_ne Subtype.val h1.1.1 - -lemma getDual_getDualProp (i : l.contrSubtype) : l.AreDual i.1 (l.getDual i).1 := by - simp [getDual] - have h1 := l.some_getDualFin_eq_find i - rw [Fin.find_eq_some_iff] at h1 - simp only [AreDual, ne_eq, and_imp] at h1 - exact h1.1 - -/-! - -## Index lists with no contracting indices - --/ - -/-- The proposition on a `IndexList` for it to have no contracting - indices. -/ -def HasNoContr : Prop := ∀ i, l.NoContr i - -lemma contrSubtype_is_empty_of_hasNoContr (h : l.HasNoContr) : IsEmpty l.contrSubtype := by - rw [_root_.isEmpty_iff] - intro a - exact h a.1 a.1 (fun _ => a.2 (h a.1)) rfl - -lemma hasNoContr_id_inj (h : l.HasNoContr) : Function.Injective l.idMap := fun i j => by - simpa using (h i j).mt - -lemma hasNoContr_color_eq_of_id_eq (h : l.HasNoContr) (i j : Fin l.length) : - l.idMap i = l.idMap j → l.colorMap i = l.colorMap j := by - intro h1 - apply l.hasNoContr_id_inj h at h1 - rw [h1] - -@[simp] -lemma hasNoContr_noContrFinset_card (h : l.HasNoContr) : - l.noContrFinset.card = List.length l := by - simp only [noContrFinset] - rw [Finset.filter_true_of_mem] - simp only [Finset.card_univ, Fintype.card_fin] - intro x _ - exact h x - -/-! - -## The contracted index list - --/ - -/-- The index list of those indices of `l` which do not contract. -/ -def contr : IndexList X := - IndexList.fromFinMap (fun i => l.get (l.noContrSubtypeEquiv.symm i)) - -@[simp] -lemma contr_numIndices : l.contr.numIndices = l.noContrFinset.card := by - simp [contr] - -@[simp] -lemma contr_idMap_apply (i : Fin l.contr.numIndices) : - l.contr.idMap i = - l.idMap (l.noContrSubtypeEquiv.symm (Fin.cast (by simp) i)).1 := by - simp [contr, IndexList.fromFinMap, IndexList.idMap] - rfl - -lemma contr_hasNoContr : HasNoContr l.contr := by - intro i - simp [NoContr] - intro j h - refine l.idMap_noContrSubtypeEquiv_neq _ _ ?_ - rw [@Fin.ne_iff_vne] - simp only [Fin.coe_cast, ne_eq] - exact Fin.val_ne_of_ne h - -/-- Contracting indices on a index list that has no contractions does nothing. -/ -@[simp] -lemma contr_of_hasNoContr (h : HasNoContr l) : l.contr = l := by - simp only [contr, List.get_eq_getElem] - have hn : (@Finset.univ (Fin (List.length l)) (Fin.fintype (List.length l))).card = - (Finset.filter l.NoContr Finset.univ).card := by - rw [Finset.filter_true_of_mem (fun a _ => h a)] - have hx : (Finset.filter l.NoContr Finset.univ).card = (List.length l) := by - rw [← hn] - exact Finset.card_fin (List.length l) - apply List.ext_get - simpa [fromFinMap, noContrFinset] using hx - intro n h1 h2 - simp only [noContrFinset, noContrSubtypeEquiv, OrderIso.toEquiv_symm, Equiv.symm_trans_apply, - RelIso.coe_fn_toEquiv, Equiv.subtypeEquivRight_symm_apply_coe, fromFinMap, List.get_eq_getElem, - OrderIso.symm_symm, Finset.coe_orderIsoOfFin_apply, List.getElem_map, Fin.getElem_list, - Fin.cast_mk] - simp only [Finset.filter_true_of_mem (fun a _ => h a)] - congr - rw [(Finset.orderEmbOfFin_unique' _ - (fun x => Finset.mem_univ ((Fin.castOrderIso hx).toOrderEmbedding x))).symm] - rfl - -/-- Applying contrIndexlist is equivalent to applying it once. -/ -@[simp] -lemma contr_contr : l.contr.contr = l.contr := - l.contr.contr_of_hasNoContr (l.contr_hasNoContr) - -/-! - -## Pairs of contracting indices - --/ - -/-- The set of contracting ordered pairs of indices. -/ -def contrPairSet : Set (l.contrSubtype × l.contrSubtype) := - {p | p.1.1 < p.2.1 ∧ l.idMap p.1.1 = l.idMap p.2.1} - -instance : DecidablePred fun x => x ∈ l.contrPairSet := fun _ => - And.decidable - -instance : Fintype l.contrPairSet := setFintype _ - -lemma contrPairSet_isEmpty_of_hasNoContr (h : l.HasNoContr) : - IsEmpty l.contrPairSet := by - simp only [contrPairSet, Subtype.coe_lt_coe, Set.coe_setOf, isEmpty_subtype, not_and, Prod.forall] - refine fun a b h' => h a.1 b.1 (Fin.ne_of_lt h') - -lemma getDual_lt_self_mem_contrPairSet {i : l.contrSubtype} - (h : (l.getDual i).1 < i.1) : (l.getDual i, i) ∈ l.contrPairSet := - And.intro h (l.getDual_id i).symm - -lemma getDual_not_lt_self_mem_contrPairSet {i : l.contrSubtype} - (h : ¬ (l.getDual i).1 < i.1) : (i, l.getDual i) ∈ l.contrPairSet := by - apply And.intro - have h1 := l.getDual_neq_self i - simp only [Subtype.coe_lt_coe, gt_iff_lt] - simp at h - exact lt_of_le_of_ne h h1 - simp only - exact l.getDual_id i - -/-- The list of elements of `l` which contract together. -/ -def contrPairList : List (Fin l.length × Fin l.length) := - (List.product (Fin.list l.length) (Fin.list l.length)).filterMap fun (i, j) => if - l.AreDual i j then some (i, j) else none -end IndexNotation diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/IndexString.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexString.lean similarity index 100% rename from HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/IndexString.lean rename to HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexString.lean diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Append.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Append.lean deleted file mode 100644 index 7e72ebe..0000000 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Append.lean +++ /dev/null @@ -1,952 +0,0 @@ -/- -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.UniqueDualInOther -import HepLean.SpaceTime.LorentzTensor.IndexNotation.Indices.UniqueDual -import HepLean.SpaceTime.LorentzTensor.Basic -/-! - -# Appending index lists and consquences thereof. - --/ - -namespace IndexNotation - - -namespace IndexList - -variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X] -variable (l l2 l3 : IndexList X) - -/-! - -## Appending index lists. - --/ - -instance : HAppend (IndexList X) (IndexList X) (IndexList X) where - hAppend := fun l l2 => {val := 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) - exact List.append_assoc l.val l2.val l3.val - -def appendEquiv {l l2 : IndexList X} : Fin l.length ⊕ Fin l2.length ≃ Fin (l ++ l2).length := - finSumFinEquiv.trans (Fin.castOrderIso (List.length_append _ _).symm).toEquiv - -def appendInl : Fin l.length ↪ Fin (l ++ l2).length where - toFun := appendEquiv ∘ Sum.inl - inj' := by - intro i j h - simp [Function.comp] at h - exact h - -def appendInr : Fin l2.length ↪ Fin (l ++ l2).length where - toFun := appendEquiv ∘ Sum.inr - inj' := by - intro i j h - simp [Function.comp] at h - exact h - -@[simp] -lemma appendInl_appendEquiv : - (l.appendInl l2).trans appendEquiv.symm.toEmbedding = - {toFun := Sum.inl, inj' := Sum.inl_injective} := by - ext i - simp [appendInl] - -@[simp] -lemma appendInr_appendEquiv : - (l.appendInr l2).trans appendEquiv.symm.toEmbedding = - {toFun := Sum.inr, inj' := Sum.inr_injective} := by - ext i - simp [appendInr] - -@[simp] -lemma append_val {l l2 : IndexList X} : (l ++ l2).val = l.val ++ l2.val := by - rfl - -@[simp] -lemma idMap_append_inl {l l2 : IndexList X} (i : Fin l.length) : - (l ++ l2).idMap (appendEquiv (Sum.inl i)) = l.idMap i := by - simp [appendEquiv, idMap] - rw [List.getElem_append_left] - rfl - -@[simp] -lemma idMap_append_inr {l l2 : IndexList X} (i : Fin l2.length) : - (l ++ l2).idMap (appendEquiv (Sum.inr i)) = l2.idMap i := by - simp [appendEquiv, idMap, IndexList.length] - rw [List.getElem_append_right] - simp - omega - omega - -@[simp] -lemma colorMap_append_inl {l l2 : IndexList X} (i : Fin l.length) : - (l ++ l2).colorMap (appendEquiv (Sum.inl i)) = l.colorMap i := by - simp [appendEquiv, colorMap, IndexList.length] - rw [List.getElem_append_left] - -@[simp] -lemma colorMap_append_inl' : - (l ++ l2).colorMap ∘ appendEquiv ∘ Sum.inl = l.colorMap := by - funext i - simp - -@[simp] -lemma colorMap_append_inr {l l2 : IndexList X} (i : Fin l2.length) : - (l ++ l2).colorMap (appendEquiv (Sum.inr i)) = l2.colorMap i := by - simp [appendEquiv, colorMap, IndexList.length] - rw [List.getElem_append_right] - simp - omega - omega - -@[simp] -lemma colorMap_append_inr' : - (l ++ l2).colorMap ∘ appendEquiv ∘ Sum.inr = l2.colorMap := by - funext i - simp - -/-! - -## AreDualInSelf - --/ - -namespace AreDualInSelf - -@[simp] -lemma append_inl_inl : (l ++ l2).AreDualInSelf (appendEquiv (Sum.inl i)) (appendEquiv (Sum.inl j)) - ↔ l.AreDualInSelf i j := by - simp [AreDualInSelf] - -@[simp] -lemma append_inr_inr (l l2 : IndexList X) (i j : Fin l2.length) : - (l ++ l2).AreDualInSelf (appendEquiv (Sum.inr i)) (appendEquiv (Sum.inr j)) - ↔ l2.AreDualInSelf i j := by - simp [AreDualInSelf] - -@[simp] -lemma append_inl_inr (l l2 : IndexList X) (i : Fin l.length) (j : Fin l2.length) : - (l ++ l2).AreDualInSelf (appendEquiv (Sum.inl i)) (appendEquiv (Sum.inr j)) = - l.AreDualInOther l2 i j := by - simp [AreDualInSelf, AreDualInOther] - -@[simp] -lemma append_inr_inl (l l2 : IndexList X) (i : Fin l2.length) (j : Fin l.length) : - (l ++ l2).AreDualInSelf (appendEquiv (Sum.inr i)) (appendEquiv (Sum.inl j)) = - l2.AreDualInOther l i j := by - simp [AreDualInSelf, AreDualInOther] - -end AreDualInSelf - - -/-! - -## Member withDual append conditions - --/ - -lemma inl_mem_withDual_append_iff (i : Fin l.length) : - appendEquiv (Sum.inl i) ∈ (l ++ l2).withDual ↔ (i ∈ l.withDual ∨ i ∈ l.withDualInOther l2) := by - simp only [mem_withDual_iff_exists, mem_withInDualOther_iff_exists] - refine Iff.intro (fun h => ?_) (fun h => ?_) - · obtain ⟨j, hj⟩ := h - obtain ⟨k, hk⟩ := appendEquiv.surjective j - subst hk - match k with - | Sum.inl k => - exact Or.inl ⟨k, by simpa using hj⟩ - | Sum.inr k => - exact Or.inr ⟨k, by simpa using hj⟩ - · cases' h with h h <;> - obtain ⟨j, hj⟩ := h - · use appendEquiv (Sum.inl j) - simpa using hj - · use appendEquiv (Sum.inr j) - simpa using hj - -@[simp] -lemma inl_getDual?_isSome_iff (i : Fin l.length) : - ((l ++ l2).getDual? (appendEquiv (Sum.inl i))).isSome ↔ - ((l.getDual? i).isSome ∨ (l.getDualInOther? l2 i).isSome) := by - simpa using l.inl_mem_withDual_append_iff l2 i - -@[simp] -lemma inl_getDual?_eq_none_iff (i : Fin l.length) : - (l ++ l2).getDual? (appendEquiv (Sum.inl i)) = none ↔ - (l.getDual? i = none ∧ l.getDualInOther? l2 i = none) := by - apply Iff.intro - · intro h - have h1 := (l.inl_getDual?_isSome_iff l2 i).mpr.mt - simp only [not_or, Bool.not_eq_true, Option.not_isSome, - Option.isNone_iff_eq_none, imp_self] at h1 - exact h1 h - · intro h - have h1 := (l.inl_getDual?_isSome_iff l2 i).mp.mt - simp only [not_or, Bool.not_eq_true, Option.not_isSome, - Option.isNone_iff_eq_none, imp_self] at h1 - exact h1 h - -@[simp] -lemma inr_mem_withDual_append_iff (i : Fin l2.length) : - appendEquiv (Sum.inr i) ∈ (l ++ l2).withDual - ↔ (i ∈ l2.withDual ∨ i ∈ l2.withDualInOther l) := by - simp only [mem_withDual_iff_exists, mem_withInDualOther_iff_exists] - refine Iff.intro (fun h => ?_) (fun h => ?_) - · obtain ⟨j, hj⟩ := h - obtain ⟨k, hk⟩ := appendEquiv.surjective j - subst hk - match k with - | Sum.inl k => - exact Or.inr ⟨k, by simpa using hj⟩ - | Sum.inr k => - exact Or.inl ⟨k, by simpa using hj⟩ - · cases' h with h h <;> - obtain ⟨j, hj⟩ := h - · use appendEquiv (Sum.inr j) - simpa using hj - · use appendEquiv (Sum.inl j) - simpa using hj -@[simp] -lemma inr_getDual?_isSome_iff (i : Fin l2.length) : - ((l ++ l2).getDual? (appendEquiv (Sum.inr i))).isSome ↔ - ((l2.getDual? i).isSome ∨ (l2.getDualInOther? l i).isSome) := by - simpa using l.inr_mem_withDual_append_iff l2 i - -@[simp] -lemma inr_getDual?_eq_none_iff (i : Fin l2.length) : - (l ++ l2).getDual? (appendEquiv (Sum.inr i)) = none ↔ - (l2.getDual? i = none ∧ l2.getDualInOther? l i = none) := by - apply Iff.intro - · intro h - have h1 := (l.inr_getDual?_isSome_iff l2 i).mpr.mt - simp only [not_or, Bool.not_eq_true, Option.not_isSome, - Option.isNone_iff_eq_none, imp_self] at h1 - exact h1 h - · intro h - have h1 := (l.inr_getDual?_isSome_iff l2 i).mp.mt - simp only [not_or, Bool.not_eq_true, Option.not_isSome, - Option.isNone_iff_eq_none, imp_self] at h1 - exact h1 h - -lemma append_getDual?_isSome_symm (i : Fin l.length) : - ((l ++ l2).getDual? (appendEquiv (Sum.inl i))).isSome ↔ - ((l2 ++ l).getDual? (appendEquiv (Sum.inr i))).isSome := by - simp - -@[simp] -lemma getDual?_inl_of_getDual?_isSome (i : Fin l.length) (h : (l.getDual? i).isSome) : - (l ++ l2).getDual? (appendEquiv (Sum.inl i)) = - some (appendEquiv (Sum.inl ((l.getDual? i).get h))) := by - rw [getDual?, Fin.find_eq_some_iff, AreDualInSelf.append_inl_inl] - apply And.intro (getDual?_get_areDualInSelf l i h).symm - intro j hj - obtain ⟨k, hk⟩ := appendEquiv.surjective j - subst hk - match k with - | Sum.inl k => - simp only [appendEquiv, Equiv.trans_apply, finSumFinEquiv_apply_left, RelIso.coe_fn_toEquiv, - Fin.castOrderIso_apply, ge_iff_le] - rw [Fin.le_def] - have h2 : l.getDual? i = some (((l.getDual? i).get h)) := by simp - nth_rewrite 1 [getDual?] at h2 - rw [Fin.find_eq_some_iff] at h2 - exact h2.2 k (by simpa using hj) - | Sum.inr k => - simp only [appendEquiv, Equiv.trans_apply, finSumFinEquiv_apply_left, RelIso.coe_fn_toEquiv, - Fin.castOrderIso_apply, finSumFinEquiv_apply_right, ge_iff_le] - rw [Fin.le_def] - simp only [length, append_val, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Fin.coe_cast, - Fin.coe_castAdd, Fin.coe_natAdd] - omega - -@[simp] -lemma getDual?_inl_of_getDual?_isNone_getDualInOther?_isSome (i : Fin l.length) - (hi : (l.getDual? i).isNone) (h : (l.getDualInOther? l2 i).isSome) : - (l ++ l2).getDual? (appendEquiv (Sum.inl i)) = some - (appendEquiv (Sum.inr ((l.getDualInOther? l2 i).get h))) := by - rw [getDual?, Fin.find_eq_some_iff, AreDualInSelf.append_inl_inr] - apply And.intro (l.areDualInOther_getDualInOther! l2 ⟨i, by simp_all⟩) - intro j hj - obtain ⟨k, hk⟩ := appendEquiv.surjective j - subst hk - match k with - | Sum.inl k => - rw [AreDualInSelf.append_inl_inl] at hj - simp only [withDual, getDual?, Finset.mem_filter, Finset.mem_univ, true_and, Bool.not_eq_true, - Option.not_isSome, Option.isNone_iff_eq_none, Fin.find_eq_none_iff] at hi - exact False.elim (hi k hj) - | Sum.inr k => - simp [appendEquiv] - rw [Fin.le_def] - have h1 : l.getDualInOther? l2 i = some (((l.getDualInOther? l2 i).get h)) := by simp - nth_rewrite 1 [getDualInOther?] at h1 - rw [Fin.find_eq_some_iff] at h1 - simp only [length, append_val, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Fin.coe_cast, - Fin.coe_natAdd, add_le_add_iff_left, Fin.val_fin_le, ge_iff_le] - refine h1.2 k (by simpa using hj) - -lemma getDual?_append_inl (i : Fin l.length) : (l ++ l2).getDual? (appendEquiv (Sum.inl i)) = - Option.or (Option.map (appendEquiv ∘ Sum.inl) (l.getDual? i)) - (Option.map (appendEquiv ∘ Sum.inr) (l.getDualInOther? l2 i)) := by - by_cases h : (l.getDual? i).isSome - · simp_all - rw [congrArg (Option.map (appendEquiv ∘ Sum.inl)) (Option.eq_some_of_isSome h)] - rfl - by_cases ho : (l.getDualInOther? l2 i).isSome - · simp_all - rw [congrArg (Option.map (appendEquiv ∘ Sum.inr)) (Option.eq_some_of_isSome ho)] - rfl - simp_all - -@[simp] -lemma getDual?_append_inr_getDualInOther?_isSome (i : Fin l2.length) - (h : (l2.getDualInOther? l i).isSome) : - (l ++ l2).getDual? (appendEquiv (Sum.inr i)) = - some (appendEquiv (Sum.inl ((l2.getDualInOther? l i).get h))) := by - rw [getDual?, Fin.find_eq_some_iff, AreDualInSelf.append_inr_inl] - apply And.intro (l2.areDualInOther_getDualInOther! l ⟨i, by simp_all⟩) - intro j hj - obtain ⟨k, hk⟩ := appendEquiv.surjective j - subst hk - match k with - | Sum.inl k => - simp only [appendEquiv, Equiv.trans_apply, finSumFinEquiv_apply_left, RelIso.coe_fn_toEquiv, - Fin.castOrderIso_apply, ge_iff_le] - rw [Fin.le_def] - have h1 : l2.getDualInOther? l i = some (((l2.getDualInOther? l i).get h)) := by simp - nth_rewrite 1 [getDualInOther?] at h1 - rw [Fin.find_eq_some_iff] at h1 - simp only [Fin.coe_cast, Fin.coe_natAdd, add_le_add_iff_left, Fin.val_fin_le, ge_iff_le] - refine h1.2 k (by simpa using hj) - | Sum.inr k => - simp only [appendEquiv, Equiv.trans_apply, finSumFinEquiv_apply_left, RelIso.coe_fn_toEquiv, - Fin.castOrderIso_apply, finSumFinEquiv_apply_right, ge_iff_le] - rw [Fin.le_def] - simp only [length, append_val, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Fin.coe_cast, - Fin.coe_castAdd, Fin.coe_natAdd] - omega - -@[simp] -lemma getDual?_inr_getDualInOther?_isNone_getDual?_isSome (i : Fin l2.length) - (h : (l2.getDualInOther? l i).isNone) (hi : (l2.getDual? i).isSome) : - (l ++ l2).getDual? (appendEquiv (Sum.inr i)) = some - (appendEquiv (Sum.inr ((l2.getDual? i).get hi))) := by - rw [getDual?, Fin.find_eq_some_iff, AreDualInSelf.append_inr_inr] - apply And.intro (l2.areDualInSelf_getDual! ⟨i, by simp_all⟩) - intro j hj - obtain ⟨k, hk⟩ := appendEquiv.surjective j - subst hk - match k with - | Sum.inl k => - simp at hj - simp only [getDualInOther?, Option.isNone_iff_eq_none, Fin.find_eq_none_iff] at h - exact False.elim (h k hj) - | Sum.inr k => - simp [appendEquiv, IndexList.length] - rw [Fin.le_def] - simp - have h2 : l2.getDual? i = some ((l2.getDual? i).get hi) := by simp - nth_rewrite 1 [getDual?] at h2 - rw [Fin.find_eq_some_iff] at h2 - simp only [AreDualInSelf.append_inr_inr] at hj - exact h2.2 k hj - -lemma getDual?_append_inr (i : Fin l2.length) : - (l ++ l2).getDual? (appendEquiv (Sum.inr i)) = - Option.or (Option.map (appendEquiv ∘ Sum.inl) (l2.getDualInOther? l i)) - (Option.map (appendEquiv ∘ Sum.inr) (l2.getDual? i)) := by - by_cases h : (l2.getDualInOther? l i).isSome - · simp_all - rw [congrArg (Option.map (appendEquiv ∘ Sum.inl)) (Option.eq_some_of_isSome h)] - rfl - by_cases ho : (l2.getDual? i).isSome - · simp_all - rw [congrArg (Option.map (appendEquiv ∘ Sum.inr)) (Option.eq_some_of_isSome ho)] - rfl - simp_all - - -/-! - -## Properties of the finite set withDual. - --/ - -def appendInlWithDual (i : l.withDual) : (l ++ l2).withDual := - ⟨appendEquiv (Sum.inl i), by simp⟩ - -lemma append_withDual : (l ++ l2).withDual = - (Finset.map (l.appendInl l2) (l.withDual ∪ l.withDualInOther l2)) ∪ - (Finset.map (l.appendInr l2) (l2.withDual ∪ l2.withDualInOther l)) := by - ext i - obtain ⟨k, hk⟩ := appendEquiv.surjective i - subst hk - match k with - | Sum.inl k => - simp - apply Iff.intro - intro h - · apply Or.inl - use k - simp_all [appendInl] - · intro h - cases' h with h h - · obtain ⟨j, hj⟩ := h - simp [appendInl] at hj - have hj2 := hj.2 - subst hj2 - exact hj.1 - · obtain ⟨j, hj⟩ := h - simp [appendInr] at hj - | Sum.inr k => - simp - apply Iff.intro - intro h - · apply Or.inr - use k - simp_all [appendInr] - · intro h - cases' h with h h - · obtain ⟨j, hj⟩ := h - simp [appendInl] at hj - · obtain ⟨j, hj⟩ := h - simp [appendInr] at hj - have hj2 := hj.2 - subst hj2 - exact hj.1 - -lemma append_withDual_disjSum : (l ++ l2).withDual = - Equiv.finsetCongr appendEquiv - ((l.withDual ∪ l.withDualInOther l2).disjSum - (l2.withDual ∪ l2.withDualInOther l)) := by - rw [← Equiv.symm_apply_eq] - simp [append_withDual] - rw [Finset.map_union] - rw [Finset.map_map, Finset.map_map] - ext1 a - cases a with - | inl val => simp - | inr val_1 => simp - - -/-! - -## withUniqueDualInOther append conditions - --/ - -lemma append_inl_not_mem_withDual_of_withDualInOther (i : Fin l.length) - (h : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual) : - i ∈ l.withDual ↔ ¬ i ∈ l.withDualInOther l2 := by - refine Iff.intro (fun hs => ?_) (fun ho => ?_) - · by_contra ho - obtain ⟨j, hj⟩ := (l.mem_withDual_iff_exists).mp hs - obtain ⟨k, hk⟩ := (l.mem_withInDualOther_iff_exists l2).mp ho - have h1 : appendEquiv (Sum.inl j) = appendEquiv (Sum.inr k) := by - refine (l ++ l2).eq_of_areDualInSelf_withUniqueDual ⟨appendEquiv (Sum.inl i), h⟩ ?_ ?_ - simpa using hj - simpa using hk - simp at h1 - · have ht : ((l ++ l2).getDual? (appendEquiv (Sum.inl i))).isSome := by simp [h] - simp only [inl_getDual?_isSome_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 [inr_getDual?_isSome_iff] at ht - simp_all - -/-! - -## getDual? apply symmetry. - --/ -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] - -/-! - -## mem withUniqueDual symmetry - --/ - -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, - inl_getDual?_isSome_iff, true_and, inr_getDual?_isSome_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, inl_getDual?_isSome_iff, - implies_true, and_self, mem_withUniqueDual_isSome, eq_getDual?_get_of_withUniqueDual_iff, - Option.some_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_inr, imp_self, withUniqueDual, - mem_withDual_iff_isSome, Finset.mem_filter, Finset.mem_univ, inl_getDual?_isSome_iff, - implies_true, and_self, mem_withUniqueDual_isSome, eq_getDual?_get_of_withUniqueDual_iff, - Option.some_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, inr_getDual?_isSome_iff, - implies_true, and_self, mem_withUniqueDual_isSome, eq_getDual?_get_of_withUniqueDual_iff, - Option.some_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_inr, imp_self, withUniqueDual, - mem_withDual_iff_isSome, Finset.mem_filter, Finset.mem_univ, inr_getDual?_isSome_iff, - implies_true, and_self, mem_withUniqueDual_isSome, eq_getDual?_get_of_withUniqueDual_iff, - Option.some_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, - inl_getDual?_isSome_iff, true_and] at h ⊢ - apply And.intro hi - intro j hj - have hj' := h.2 (appendEquiv (Sum.inl j)) - simp 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, - inl_getDual?_isSome_iff, true_and] at h - have hj' := h.2 (appendEquiv (Sum.inr j)) - simp only [AreDualInSelf.append_inl_inr] 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, - inl_getDual?_isSome_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 - erw [← l.eq_getDualInOther_of_withUniqueDual_iff l2 ⟨i, ho⟩ k] - simpa using hj - -@[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 - -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, append_withDual_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] - -/-! - -## AreDualInOther append conditions --/ -namespace AreDualInOther -variable {l l2 l3 : IndexList X} - -@[simp] -lemma append_of_inl (i : Fin l.length) (j : Fin l3.length) : - (l ++ l2).AreDualInOther l3 (appendEquiv (Sum.inl i)) j ↔ l.AreDualInOther l3 i j := by - simp [AreDualInOther] - -@[simp] -lemma append_of_inr (i : Fin l2.length) (j : Fin l3.length) : - (l ++ l2).AreDualInOther l3 (appendEquiv (Sum.inr i)) j ↔ l2.AreDualInOther l3 i j := by - simp [AreDualInOther] - -@[simp] -lemma of_append_inl (i : Fin l.length) (j : Fin l2.length) : - l.AreDualInOther (l2 ++ l3) i (appendEquiv (Sum.inl j)) ↔ l.AreDualInOther l2 i j := by - simp [AreDualInOther] - -@[simp] -lemma of_append_inr (i : Fin l.length) (j : Fin l3.length) : - l.AreDualInOther (l2 ++ l3) i (appendEquiv (Sum.inr j)) ↔ l.AreDualInOther l3 i j := by - simp [AreDualInOther] - -end AreDualInOther -/-! - -## Append and getDualInOther? - --/ -variable (l3 : IndexList X) - -@[simp] -lemma getDualInOther?_append_inl (i : Fin l.length) : - (l ++ l2).getDualInOther? l3 (appendEquiv (Sum.inl i)) = l.getDualInOther? l3 i := by - simp [getDualInOther?] - -/-! - -## append in other - --/ - - -lemma append_withDualInOther_eq : - (l ++ l2).withDualInOther l3 = - Equiv.finsetCongr appendEquiv ((l.withDualInOther l3).disjSum (l2.withDualInOther l3)) := by - rw [Finset.ext_iff] - intro i - simp - - sorry - -lemma withDualInOther_append_eq : - l.withDualInOther (l2 ++ l3) = - l.withDualInOther l2 ∪ l.withDualInOther l3 := by - sorry - -end IndexList - -end IndexNotation diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/DualInOther.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/DualInOther.lean deleted file mode 100644 index 2dc4ba5..0000000 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/DualInOther.lean +++ /dev/null @@ -1,105 +0,0 @@ -/- -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.Basic -import HepLean.SpaceTime.LorentzTensor.Basic -/-! - -# Dual in other list - --/ -namespace IndexNotation - - -namespace IndexList - -variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X] -variable (l l2 : IndexList X) - -def AreDualInOther (i : Fin l.length) (j : Fin l2.length) : - Prop := l.idMap i = l2.idMap j - -instance {l : IndexList X} {l2 : IndexList X} (i : Fin l.length) (j : Fin l2.length) : - Decidable (l.AreDualInOther l2 i j) := (l.idMap i).decEq (l2.idMap j) - -namespace AreDualInOther - -variable {l l2 : IndexList X} {i : Fin l.length} {j : Fin l2.length} - -@[symm] -lemma symm (h : l.AreDualInOther l2 i j) : l2.AreDualInOther l j i := by - rw [AreDualInOther] at h ⊢ - exact h.symm - -end AreDualInOther - -/-- Given an `i`, if a dual exists in the other list, - outputs the first such dual, otherwise outputs `none`. -/ -def getDualInOther? (i : Fin l.length) : Option (Fin l2.length) := - Fin.find (fun j => l.AreDualInOther l2 i j) - - -/-! - -## With dual other. - --/ - -def withDualInOther : Finset (Fin l.length) := - Finset.filter (fun i => (l.getDualInOther? l2 i).isSome) Finset.univ - -@[simp] -lemma mem_withInDualOther_iff_isSome (i : Fin l.length) : - i ∈ l.withDualInOther l2 ↔ (l.getDualInOther? l2 i).isSome := by - simp only [withDualInOther, getDualInOther?, Finset.mem_filter, Finset.mem_univ, true_and] - -lemma mem_withInDualOther_iff_exists : - i ∈ l.withDualInOther l2 ↔ ∃ (j : Fin l2.length), l.AreDualInOther l2 i j := by - simp [withDualInOther, Finset.mem_filter, Finset.mem_univ, getDualInOther?] - rw [Fin.isSome_find_iff] - -def getDualInOther! (i : l.withDualInOther l2) : Fin l2.length := - (l.getDualInOther? l2 i).get (by simpa [withDualInOther] using i.2) - - -lemma getDualInOther?_eq_some_getDualInOther! (i : l.withDualInOther l2) : - l.getDualInOther? l2 i = some (l.getDualInOther! l2 i) := by - simp [getDualInOther!] - -lemma getDualInOther?_eq_none_on_not_mem (i : Fin l.length) (h : i ∉ l.withDualInOther l2) : - l.getDualInOther? l2 i = none := by - simpa [getDualInOther?, Fin.find_eq_none_iff, mem_withInDualOther_iff_exists] using h - - -lemma areDualInOther_getDualInOther! (i : l.withDualInOther l2) : - l.AreDualInOther l2 i (l.getDualInOther! l2 i) := by - have h := l.getDualInOther?_eq_some_getDualInOther! l2 i - rw [getDualInOther?, Fin.find_eq_some_iff] at h - exact h.1 - -@[simp] -lemma getDualInOther!_id (i : l.withDualInOther l2) : - l2.idMap (l.getDualInOther! l2 i) = l.idMap i := by - simpa using (l.areDualInOther_getDualInOther! l2 i).symm - -lemma getDualInOther_mem_withDualInOther (i : l.withDualInOther l2) : - l.getDualInOther! l2 i ∈ l2.withDualInOther l := - (l2.mem_withInDualOther_iff_exists l).mpr ⟨i, (areDualInOther_getDualInOther! l l2 i).symm⟩ - -def getDualInOther (i : l.withDualInOther l2) : l2.withDualInOther l := - ⟨l.getDualInOther! l2 i, l.getDualInOther_mem_withDualInOther l2 i⟩ - -@[simp] -lemma getDualInOther_id (i : l.withDualInOther l2) : - l2.idMap (l.getDualInOther l2 i) = l.idMap i := by - simp [getDualInOther] - -lemma getDualInOther_coe (i : l.withDualInOther l2) : - (l.getDualInOther l2 i).1 = l.getDualInOther! l2 i := by - rfl - -end IndexList - -end IndexNotation diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/UniqueDual.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/UniqueDual.lean deleted file mode 100644 index 43b60e1..0000000 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/UniqueDual.lean +++ /dev/null @@ -1,439 +0,0 @@ -/- -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.Dual -import HepLean.SpaceTime.LorentzTensor.Basic -/-! - -# Unique Dual indices - --/ - -namespace IndexNotation - - -namespace IndexList - -variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X] -variable (l l2 : IndexList X) - - -/-! - -## Has single dual in self. - --/ - - -def withUniqueDual : Finset (Fin l.length) := - Finset.filter (fun i => i ∈ l.withDual ∧ - ∀ j, l.AreDualInSelf i j → j = l.getDual? i) Finset.univ - -@[simp] -lemma mem_withDual_of_mem_withUniqueDual (i : Fin l.length) (h : i ∈ l.withUniqueDual) : - i ∈ l.withDual := by - simp only [withUniqueDual, mem_withDual_iff_isSome, Finset.mem_filter, Finset.mem_univ, - true_and] at h - simpa using h.1 - -@[simp] -lemma mem_withUniqueDual_isSome (i : Fin l.length) (h : i ∈ l.withUniqueDual) : - (l.getDual? i).isSome := by - simpa using mem_withDual_of_mem_withUniqueDual l i h - -lemma mem_withDual_of_withUniqueDual (i : l.withUniqueDual) : - i.1 ∈ l.withDual := by - have hi := i.2 - simp only [withUniqueDual, Finset.mem_filter, Finset.mem_univ] at hi - exact hi.2.1 - -def fromWithUnique (i : l.withUniqueDual) : l.withDual := - ⟨i.1, l.mem_withDual_of_withUniqueDual i⟩ - -instance : Coe l.withUniqueDual l.withDual where - coe i := ⟨i.1, l.mem_withDual_of_withUniqueDual i⟩ - -@[simp] -lemma fromWithUnique_coe (i : l.withUniqueDual) : (l.fromWithUnique i).1 = i.1 := by - rfl - -lemma all_dual_eq_getDual_of_withUniqueDual (i : l.withUniqueDual) : - ∀ j, l.AreDualInSelf i j → j = l.getDual! i := by - have hi := i.2 - simp [withUniqueDual] at hi - intro j hj - simpa [getDual!, fromWithUnique] using (Option.get_of_mem _ (hi.2 j hj ).symm).symm - -lemma eq_of_areDualInSelf_withUniqueDual {j k : Fin l.length} (i : l.withUniqueDual) - (hj : l.AreDualInSelf i j) (hk : l.AreDualInSelf i k) : - j = k := by - have hj' := all_dual_eq_getDual_of_withUniqueDual l i j hj - have hk' := all_dual_eq_getDual_of_withUniqueDual l i k hk - rw [hj', hk'] - -/-! - -## Properties of getDual? - --/ - -lemma all_dual_eq_getDual?_of_mem_withUniqueDual (i : Fin l.length) (h : i ∈ l.withUniqueDual) : - ∀ j, l.AreDualInSelf i j → j = l.getDual? i := by - simp [withUniqueDual] at h - exact fun j hj => h.2 j hj - -lemma some_eq_getDual?_of_withUniqueDual_iff (i j : Fin l.length) (h : i ∈ l.withUniqueDual) : - l.AreDualInSelf i j ↔ some j = l.getDual? i := by - apply Iff.intro - intro h' - exact all_dual_eq_getDual?_of_mem_withUniqueDual l i h j h' - intro h' - have hj : j = (l.getDual? i).get (mem_withUniqueDual_isSome l i h) := - Eq.symm (Option.get_of_mem (mem_withUniqueDual_isSome l i h) (id (Eq.symm h'))) - subst hj - exact (getDual?_get_areDualInSelf l i (mem_withUniqueDual_isSome l i h)).symm - -@[simp] -lemma eq_getDual?_get_of_withUniqueDual_iff (i j : Fin l.length) (h : i ∈ l.withUniqueDual) : - l.AreDualInSelf i j ↔ j = (l.getDual? i).get (mem_withUniqueDual_isSome l i h) := by - rw [l.some_eq_getDual?_of_withUniqueDual_iff i j h] - refine Iff.intro (fun h' => ?_) (fun h' => ?_) - exact Eq.symm (Option.get_of_mem (mem_withUniqueDual_isSome l i h) (id (Eq.symm h'))) - simp [h'] - -@[simp] -lemma getDual?_get_getDual?_get_of_withUniqueDual (i : Fin l.length) (h : i ∈ l.withUniqueDual) : - (l.getDual? ((l.getDual? i).get (mem_withUniqueDual_isSome l i h))).get - (l.getDual?_getDual?_get_isSome i (mem_withUniqueDual_isSome l i h)) = i := by - by_contra hn - have h' : l.AreDualInSelf i ((l.getDual? ((l.getDual? i).get (mem_withUniqueDual_isSome l i h))).get ( - getDual?_getDual?_get_isSome l i (mem_withUniqueDual_isSome l i h))) := by - simp [AreDualInSelf, hn] - exact fun a => hn (id (Eq.symm a)) - simp [h] at h' - -@[simp] -lemma getDual?_getDual?_get_of_withUniqueDual (i : Fin l.length) (h : i ∈ l.withUniqueDual) : - l.getDual? ((l.getDual? i).get (mem_withUniqueDual_isSome l i h)) = some i := by - nth_rewrite 3 [← l.getDual?_get_getDual?_get_of_withUniqueDual i h] - simp - -@[simp] -lemma getDual?_getDual?_of_withUniqueDual (i : Fin l.length) (h : i ∈ l.withUniqueDual) : - (l.getDual? i).bind l.getDual? = some i := by - have h1 : (l.getDual? i) = some ((l.getDual? i).get (mem_withUniqueDual_isSome l i h)) := by simp - nth_rewrite 1 [h1] - 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, getDual, fromWithUnique] - simp [h] at h' - subst h' - simp_all [getDual] - subst h1 - exact Eq.symm (getDual?_getDual?_get_of_withUniqueDual l i h) - -/-! - -## 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⟩ - 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, fromWithUnique] - - -/-! - -## Properties of getDual! etc. - --/ -lemma eq_getDual_of_withUniqueDual_iff (i : l.withUniqueDual) (j : Fin l.length) : - l.AreDualInSelf i j ↔ j = l.getDual! i := by - apply Iff.intro - intro h - exact (l.all_dual_eq_getDual_of_withUniqueDual i) j h - intro h - subst h - exact areDualInSelf_getDual! l i - -@[simp] -lemma getDual!_getDual_of_withUniqueDual (i : l.withUniqueDual) : - l.getDual! (l.getDual i) = i := by - by_contra hn - have h' : l.AreDualInSelf i (l.getDual! (l.getDual i)) := by - simp [AreDualInSelf, hn] - simp_all [AreDualInSelf, getDual, fromWithUnique] - exact fun a => hn (id (Eq.symm a)) - rw [eq_getDual_of_withUniqueDual_iff] at h' - have hx := l.areDualInSelf_getDual! (l.getDual i) - simp_all [getDual] - -@[simp] -lemma getDual_getDual_of_withUniqueDual (i : l.withUniqueDual) : - l.getDual (l.getDual i) = l.fromWithUnique i := - SetCoe.ext (getDual!_getDual_of_withUniqueDual l i) - -@[simp] -lemma getDual?_getDual!_of_withUniqueDual (i : l.withUniqueDual) : - l.getDual? (l.getDual! i) = some i := by - change l.getDual? (l.getDual i) = some i - rw [getDual?_eq_some_getDual!] - simp - -@[simp] -lemma getDual?_getDual_of_withUniqueDual (i : l.withUniqueDual) : - l.getDual? (l.getDual i) = some i := by - change l.getDual? (l.getDual i) = some i - rw [getDual?_eq_some_getDual!] - simp - -/-! - -## Equality of withUnqiueDual and withDual - --/ - -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⟩ - · rw [getDual?_eq_none_on_not_mem l i hi] - simp - symm - simpa [Option.guard, ite_eq_right_iff, imp_false] using 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' - -/-! - -## 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])) - -end IndexList - -end IndexNotation diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/UniqueDualInOther.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/UniqueDualInOther.lean deleted file mode 100644 index 2b95007..0000000 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/UniqueDualInOther.lean +++ /dev/null @@ -1,141 +0,0 @@ -/- -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.DualInOther -import HepLean.SpaceTime.LorentzTensor.IndexNotation.Indices.Dual -import HepLean.SpaceTime.LorentzTensor.Basic -/-! - -# Unique Dual indices - --/ - -namespace IndexNotation - - -namespace IndexList - -variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X] -variable (l l2 : IndexList X) - - -/-! - -## Has single in other. - --/ - -def withUniqueDualInOther : Finset (Fin l.length) := - Finset.filter (fun i => i ∉ l.withDual ∧ i ∈ l.withDualInOther l2 - ∧ (∀ j, l.AreDualInOther l2 i j → j = l.getDualInOther? l2 i)) Finset.univ - -lemma not_mem_withDual_of_withUniqueDualInOther (i : l.withUniqueDualInOther l2) : - i.1 ∉ l.withDual := by - have hi := i.2 - simp only [withUniqueDualInOther, Finset.univ_eq_attach, Finset.mem_filter, Finset.mem_attach, - true_and] at hi - exact hi.2.1 - -lemma mem_withDualInOther_of_withUniqueDualInOther (i : l.withUniqueDualInOther l2) : - i.1 ∈ l.withDualInOther l2 := by - have hi := i.2 - simp only [withUniqueDualInOther, Finset.univ_eq_attach, Finset.mem_filter, Finset.mem_attach, - true_and] at hi - exact hi.2.2.1 - -@[simp] -lemma mem_withUniqueDualInOther_isSome (i : Fin l.length) (hi : i ∈ l.withUniqueDualInOther l2) : - (l.getDualInOther? l2 i).isSome := by - simp only [withUniqueDualInOther, Finset.mem_filter, Finset.mem_univ, true_and] at hi - have hi2 := hi.2.1 - simpa using hi2 - - -def fromWithUniqueDualInOther (i : l.withUniqueDualInOther l2) : l.withDualInOther l2 := - ⟨i.1, l.mem_withDualInOther_of_withUniqueDualInOther l2 i⟩ - -instance : Coe (l.withUniqueDualInOther l2) (l.withDualInOther l2) where - coe i := ⟨i.1, l.mem_withDualInOther_of_withUniqueDualInOther l2 i⟩ - -lemma all_dual_eq_of_withUniqueDualInOther (i : l.withUniqueDualInOther l2) : - ∀ j, l.AreDualInOther l2 i j → j = l.getDualInOther! l2 i := by - have hi := i.2 - simp only [withUniqueDualInOther, Finset.univ_eq_attach, Finset.mem_filter, Finset.mem_attach, - true_and] at hi - intro j hj - refine (Option.get_of_mem _ (hi.2.2.2 j hj).symm).symm - -lemma eq_getDualInOther_of_withUniqueDual_iff (i : l.withUniqueDualInOther l2) (j : Fin l2.length) : - l.AreDualInOther l2 i j ↔ j = l.getDualInOther! l2 i := by - apply Iff.intro - intro h - exact l.all_dual_eq_of_withUniqueDualInOther l2 i j h - intro h - subst h - exact areDualInOther_getDualInOther! l l2 i - -@[simp] -lemma getDualInOther!_getDualInOther_of_withUniqueDualInOther (i : l.withUniqueDualInOther l2) : - l2.getDualInOther! l (l.getDualInOther l2 i) = i := by - by_contra hn - refine (l.not_mem_withDual_of_withUniqueDualInOther l2 i) - (l.mem_withDual_iff_exists.mpr ⟨(l2.getDualInOther! l (l.getDualInOther l2 i)), ?_⟩ ) - simp [AreDualInSelf, hn] - exact (fun a => hn (id (Eq.symm a))) - -@[simp] -lemma getDualInOther_getDualInOther_of_withUniqueDualInOther (i : l.withUniqueDualInOther l2) : - l2.getDualInOther l (l.getDualInOther l2 i) = i := - SetCoe.ext (getDualInOther!_getDualInOther_of_withUniqueDualInOther l l2 i) - -@[simp] -lemma getDualInOther?_getDualInOther!_of_withUniqueDualInOther (i : l.withUniqueDualInOther l2) : - l2.getDualInOther? l (l.getDualInOther! l2 i) = some i := by - change l2.getDualInOther? l (l.getDualInOther l2 i) = some i - rw [getDualInOther?_eq_some_getDualInOther!] - simp - -lemma getDualInOther_of_withUniqueDualInOther_not_mem_of_withDual (i : l.withUniqueDualInOther l2) : - (l.getDualInOther l2 i).1 ∉ l2.withDual := by - rw [mem_withDual_iff_exists] - simp - intro j - simp [AreDualInSelf] - intro hj - by_contra hn - have hn' : l.AreDualInOther l2 i j := by - simp [AreDualInOther, hn, hj] - rw [eq_getDualInOther_of_withUniqueDual_iff] at hn' - simp_all - simp only [getDualInOther_coe, not_true_eq_false] at hj - -lemma getDualInOther_of_withUniqueDualInOther_mem (i : l.withUniqueDualInOther l2) : - (l.getDualInOther l2 i).1 ∈ l2.withUniqueDualInOther l := by - simp only [withUniqueDualInOther, Finset.mem_filter, Finset.mem_univ, true_and] - apply And.intro (l.getDualInOther_of_withUniqueDualInOther_not_mem_of_withDual l2 i) - apply And.intro - exact Finset.coe_mem - (l.getDualInOther l2 ⟨↑i, mem_withDualInOther_of_withUniqueDualInOther l l2 i⟩) - intro j hj - by_contra hn - have h' : l.AreDualInSelf i j := by - simp [AreDualInSelf, hn] - simp_all [AreDualInOther, getDual] - simp [getDualInOther_coe] at hn - exact fun a => hn (id (Eq.symm a)) - have hi := l.not_mem_withDual_of_withUniqueDualInOther l2 i - rw [mem_withDual_iff_exists] at hi - simp_all - -def getDualInOtherEquiv : l.withUniqueDualInOther l2 ≃ l2.withUniqueDualInOther l where - toFun x := ⟨l.getDualInOther l2 x, l.getDualInOther_of_withUniqueDualInOther_mem l2 x⟩ - invFun x := ⟨l2.getDualInOther l x, l2.getDualInOther_of_withUniqueDualInOther_mem l x⟩ - left_inv x := SetCoe.ext (by simp) - right_inv x := SetCoe.ext (by simp) - - -end IndexList - -end IndexNotation diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Relations.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Relations.lean similarity index 98% rename from HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Relations.lean rename to HepLean/SpaceTime/LorentzTensor/IndexNotation/Relations.lean index 171a4dc..55bf676 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Relations.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Relations.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ -import HepLean.SpaceTime.LorentzTensor.IndexNotation.Indices.Color +import HepLean.SpaceTime.LorentzTensor.IndexNotation.Color import HepLean.SpaceTime.LorentzTensor.Basic import Init.Data.List.Lemmas /-! diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean index 8234958..040641f 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean @@ -3,8 +3,8 @@ 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.Color -import HepLean.SpaceTime.LorentzTensor.IndexNotation.Indices.Relations +import HepLean.SpaceTime.LorentzTensor.IndexNotation.Color +import HepLean.SpaceTime.LorentzTensor.IndexNotation.Relations import HepLean.SpaceTime.LorentzTensor.Basic import HepLean.SpaceTime.LorentzTensor.RisingLowering import HepLean.SpaceTime.LorentzTensor.Contraction @@ -484,7 +484,7 @@ lemma add_assoc {T₁ T₂ T₃ : 𝓣.TensorIndex} {h' : AddCond T₁ T₂} (h def ProdCond (T₁ T₂ : 𝓣.TensorIndex) : Prop := - T₁.AppendCond T₂ + AppendCond T₁.toColorIndexList T₂.toColorIndexList namespace ProdCond @@ -504,6 +504,11 @@ def prod (T₁ T₂ : 𝓣.TensorIndex) lemma prod_toColorIndexList (T₁ T₂ : 𝓣.TensorIndex) (h : ProdCond T₁ T₂) : (prod T₁ T₂ h).toColorIndexList = T₁.toColorIndexList ++[h] T₂.toColorIndexList := rfl +@[simp] +lemma prod_toIndexList (T₁ T₂ : 𝓣.TensorIndex) (h : ProdCond T₁ T₂) : + (prod T₁ T₂ h).toIndexList = T₁.toIndexList ++ T₂.toIndexList := rfl + + end TensorIndex end end TensorStructure diff --git a/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean b/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean index 7eee821..31330d3 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.Indices.IndexString +import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexString import HepLean.SpaceTime.LorentzTensor.Real.Basic /-! @@ -87,37 +87,8 @@ noncomputable def fromIndexStringColor {cn : Fin n → realTensorColor.Color} 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| { - 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 => `(tactic| { @@ -128,19 +99,24 @@ macro "dualMapTactic" : tactic => Conditions are checked automatically. -/ 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 (by prodTactic) -/-(IndexListColor.colorPropBool_indexListColorProp - (by prodTactic))-/ +/-- A tactics used to prove `colorPropBool` for real Lorentz tensors. -/ +macro "prodTactic" : tactic => + `(tactic| { + apply (ColorIndexList.AppendCond.iff_bool _ _).mpr + change @ColorIndexList.AppendCond.bool realTensorColor instIndexNotationColorRealTensorColor instDecidableEqColorRealTensorColor + _ _ + simp only [prod_toIndexList, indexNotation_eq_color, fromIndexStringColor, mkDualMap, toTensorColor_eq, + decidableEq_eq_color] + rfl}) + +/-- The product of Real Lorentz tensors. Conditions on indices are checked automatically. -/ +notation:10 T "⊗ᵀ" S:11 => TensorIndex.prod T S (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 _ := fromIndexStringColor T "ᵤ₁ᵤ₂" (by rfl) (by rfl) (by rfl) (by - rfl) (by dualMapTactic) - let _ := T|"ᵤ₁ᵤ₂" ⊗ᵀ T|"ᵘ³ᵤ₄" ⊗ᵀ T|"ᵘ¹ᵘ⁴" + let _ := T|"ᵤ₁ᵤ₂" ⊗ᵀ T|"ᵘ³ᵤ₄" ⊗ᵀ T|"ᵘ⁴ᵤ₃" + let _ := T|"ᵤ₁ᵤ₂" ⊗ᵀ T|"ᵘ³ᵤ₄" ⊗ᵀ T|"ᵘ¹ᵘ²" ⊗ᵀ T|"ᵘ⁴ᵤ₃" exact trivial end realLorentzTensor