DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor: Lint

Browse source
This commit is contained in:
jstoobysmith 2024-08-15 10:53:30 -04:00
parent 3693dee740
commit 1c9d66ee19
12 changed files with 79 additions and 138 deletions
Download patch file Download diff file Expand all files Collapse all files

13
HepLean/SpaceTime/LorentzTensor/IndexNotation/AreDual.lean
View file

@ -12,13 +12,11 @@ import HepLean.SpaceTime.LorentzTensor.IndexNotation.Basic
namespace IndexNotation namespace IndexNotation
namespace IndexList namespace IndexList
variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X] variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
variable (l l2 l3 : IndexList X) variable (l l2 l3 : IndexList X)
/-! /-!
## Are dual indices ## Are dual indices
@ -30,7 +28,7 @@ def AreDualInSelf (i j : Fin l.length) : Prop :=
i ≠ j ∧ l.idMap i = l.idMap j i ≠ j ∧ l.idMap i = l.idMap j
/-- Two indices in different `IndexLists` are dual to one another if they have the same `id`. -/ /-- Two indices in different `IndexLists` are dual to one another if they have the same `id`. -/
def AreDualInOther (i : Fin l.length) (j : Fin l2.length) : def AreDualInOther (i : Fin l.length) (j : Fin l2.length) :
Prop := l.idMap i = l2.idMap j Prop := l.idMap i = l2.idMap j
namespace AreDualInSelf namespace AreDualInSelf
@ -74,12 +72,11 @@ lemma append_inr_inl (l l2 : IndexList X) (i : Fin l2.length) (j : Fin l.length)
end AreDualInSelf end AreDualInSelf
namespace AreDualInOther namespace AreDualInOther
variable {l l2 l3 : IndexList X} {i : Fin l.length} {j : Fin l2.length} variable {l l2 l3 : IndexList X} {i : Fin l.length} {j : Fin l2.length}
instance {l : IndexList X} {l2 : IndexList X} (i : Fin l.length) (j : Fin l2.length) : 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) Decidable (l.AreDualInOther l2 i j) := (l.idMap i).decEq (l2.idMap j)
@[symm] @[symm]
@ -93,17 +90,17 @@ lemma append_of_inl (i : Fin l.length) (j : Fin l3.length) :
simp [AreDualInOther] simp [AreDualInOther]
@[simp] @[simp]
lemma append_of_inr (i : Fin l2.length) (j : Fin l3.length) : 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 (l ++ l2).AreDualInOther l3 (appendEquiv (Sum.inr i)) j ↔ l2.AreDualInOther l3 i j := by
simp [AreDualInOther] simp [AreDualInOther]
@[simp] @[simp]
lemma of_append_inl (i : Fin l.length) (j : Fin l2.length) : 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 l.AreDualInOther (l2 ++ l3) i (appendEquiv (Sum.inl j)) ↔ l.AreDualInOther l2 i j := by
simp [AreDualInOther] simp [AreDualInOther]
@[simp] @[simp]
lemma of_append_inr (i : Fin l.length) (j : Fin l3.length) : 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 l.AreDualInOther (l2 ++ l3) i (appendEquiv (Sum.inr j)) ↔ l.AreDualInOther l3 i j := by
simp [AreDualInOther] simp [AreDualInOther]

2
HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean
View file

@ -243,7 +243,6 @@ instance : Fintype l.toPosSet where
def toPosFinset (l : IndexList X) : Finset (Fin l.length × Index X) := def toPosFinset (l : IndexList X) : Finset (Fin l.length × Index X) :=
l.toPosSet.toFinset l.toPosSet.toFinset
/-- The construction of a list of indices from a map /-- The construction of a list of indices from a map
from `Fin n` to `Index X`. -/ from `Fin n` to `Index X`. -/
def fromFinMap {n : ℕ} (f : Fin n → Index X) : IndexList X where def fromFinMap {n : ℕ} (f : Fin n → Index X) : IndexList X where
@ -368,7 +367,6 @@ lemma colorMap_sumELim (l1 l2 : IndexList X) :
| Sum.inl i => simp | Sum.inl i => simp
| Sum.inr i => simp | Sum.inr i => simp
end append end append
end IndexList end IndexList

39
HepLean/SpaceTime/LorentzTensor/IndexNotation/Color.lean
View file

@ -20,7 +20,6 @@ a Tensor Color structure.
namespace IndexNotation namespace IndexNotation
namespace IndexList namespace IndexList
variable {𝓒 : TensorColor} variable {𝓒 : TensorColor}
@ -55,7 +54,7 @@ lemma iff_withDual :
· have h'' : (Option.guard (fun i => (l.getDual? i).isSome = true) ↑i) = i := by · have h'' : (Option.guard (fun i => (l.getDual? i).isSome = true) ↑i) = i := by
apply Option.guard_eq_some.mpr apply Option.guard_eq_some.mpr
simp only [true_and] simp only [true_and]
exact hi exact hi
simp only [Function.comp_apply, h'', Option.map_some'] simp only [Function.comp_apply, h'', Option.map_some']
rw [show l.getDual? ↑i = some ((l.getDual? i).get hi) by simp] rw [show l.getDual? ↑i = some ((l.getDual? i).get hi) by simp]
rw [Option.map_some'] rw [Option.map_some']
@ -140,10 +139,10 @@ lemma symm (hu : (l ++ l2).withUniqueDual = (l ++ l2).withDual) (h : ColorCond (
colorMap_append_inr, true_implies, getDual?_append_inr_getDualInOther?_isSome, colorMap_append_inr, true_implies, getDual?_append_inr_getDualInOther?_isSome,
colorMap_append_inl] colorMap_append_inl]
lemma inr (hu : (l ++ l2).withUniqueDual = (l ++ l2).withDual) (h : ColorCond (l ++ l2)) : lemma inr (hu : (l ++ l2).withUniqueDual = (l ++ l2).withDual) (h : ColorCond (l ++ l2)) :
ColorCond l2 := inl (symm hu h) ColorCond l2 := inl (symm hu h)
lemma triple_right (hu : (l ++ l2 ++ l3).withUniqueDual = (l ++ l2 ++ l3).withDual) lemma triple_right (hu : (l ++ l2 ++ l3).withUniqueDual = (l ++ l2 ++ l3).withDual)
(h : ColorCond (l ++ l2 ++ l3)) : ColorCond (l2 ++ l3) := by (h : ColorCond (l ++ l2 ++ l3)) : ColorCond (l2 ++ l3) := by
have h1 := assoc h have h1 := assoc h
rw [append_assoc] at hu rw [append_assoc] at hu
@ -158,8 +157,7 @@ lemma triple_drop_mid (hu : (l ++ l2 ++ l3).withUniqueDual = (l ++ l2 ++ l3).wit
rw [append_withDual_eq_withUniqueDual_symm, append_assoc] at hu rw [append_withDual_eq_withUniqueDual_symm, append_assoc] at hu
exact append_withDual_eq_withUniqueDual_inr _ _ hu exact append_withDual_eq_withUniqueDual_inr _ _ hu
lemma swap (hu : (l ++ l2 ++ l3).withUniqueDual = (l ++ l2 ++ l3).withDual)
lemma swap (hu : (l ++ l2 ++ l3).withUniqueDual = (l ++ l2 ++ l3).withDual)
(h : ColorCond (l ++ l2 ++ l3)) : (h : ColorCond (l ++ l2 ++ l3)) :
ColorCond (l2 ++ l ++ l3) := by ColorCond (l2 ++ l ++ l3) := by
have hC := h have hC := h
@ -222,7 +220,7 @@ lemma swap (hu : (l ++ l2 ++ l3).withUniqueDual = (l ++ l2 ++ l3).withDual)
simp only [mem_withDual_iff_isSome, mem_withInDualOther_iff_isSome, simp only [mem_withDual_iff_isSome, mem_withInDualOther_iff_isSome,
getDualInOther?_isSome_of_append_iff, not_or, Bool.not_eq_true, Option.not_isSome, getDualInOther?_isSome_of_append_iff, not_or, Bool.not_eq_true, Option.not_isSome,
Option.isNone_iff_eq_none] at hn Option.isNone_iff_eq_none] at hn
by_cases hk' : (l3.getDual? k).isSome by_cases hk' : (l3.getDual? k).isSome
· simp_all only [mem_withDual_iff_isSome, true_iff, Option.isNone_iff_eq_none, · simp_all only [mem_withDual_iff_isSome, true_iff, Option.isNone_iff_eq_none,
getDualInOther?_eq_none_of_append_iff, and_self, getDualInOther?_eq_none_of_append_iff, and_self,
getDual?_inr_getDualInOther?_isNone_getDual?_isSome, Option.get_some, colorMap_append_inr] getDual?_inr_getDualInOther?_isNone_getDual?_isSome, Option.get_some, colorMap_append_inr]
@ -256,8 +254,8 @@ lemma swap (hu : (l ++ l2 ++ l3).withUniqueDual = (l ++ l2 ++ l3).withDual)
/-- A bool which is true for an index list if and only if every index and its' dual, when it exists, /-- A bool which is true for an index list if and only if every index and its' dual, when it exists,
have dual colors. -/ have dual colors. -/
def bool (l : IndexList 𝓒.Color) : Bool := def bool (l : IndexList 𝓒.Color) : Bool :=
if (∀ (i : l.withDual), 𝓒.τ if (∀ (i : l.withDual), 𝓒.τ
(l.colorMap ((l.getDual? i).get (l.withDual_isSome i))) = l.colorMap i) then (l.colorMap ((l.getDual? i).get (l.withDual_isSome i))) = l.colorMap i) then
true true
else false else false
@ -268,11 +266,8 @@ lemma iff_bool : l.ColorCond ↔ bool l := by
end ColorCond end ColorCond
end IndexList end IndexList
variable (𝓒 : TensorColor) variable (𝓒 : TensorColor)
variable [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color] variable [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
@ -284,7 +279,7 @@ variable [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color
`['ᵘ¹', 'ᵤ₁', 'ᵤ₁']` cannot. -/ `['ᵘ¹', 'ᵤ₁', 'ᵤ₁']` cannot. -/
structure ColorIndexList (𝓒 : TensorColor) [IndexNotation 𝓒.Color] extends IndexList 𝓒.Color where structure ColorIndexList (𝓒 : TensorColor) [IndexNotation 𝓒.Color] extends IndexList 𝓒.Color where
/-- The condition that for index with a dual, that dual is the unique other index with /-- The condition that for index with a dual, that dual is the unique other index with
an identical `id`. -/ an identical `id`. -/
unique_duals : toIndexList.withDual = toIndexList.withUniqueDual unique_duals : toIndexList.withDual = toIndexList.withUniqueDual
/-- The condition that for an index with a dual, that dual has dual color to the index. -/ /-- The condition that for an index with a dual, that dual has dual color to the index. -/
dual_color : IndexList.ColorCond toIndexList dual_color : IndexList.ColorCond toIndexList
@ -305,7 +300,7 @@ def empty : ColorIndexList 𝓒 where
dual_color := rfl dual_color := rfl
/-- The colorMap of a `ColorIndexList` as a `𝓒.ColorMap`. /-- The colorMap of a `ColorIndexList` as a `𝓒.ColorMap`.
This is to be compared with `colorMap` which is a map `Fin l.length → 𝓒.Color`. -/ This is to be compared with `colorMap` which is a map `Fin l.length → 𝓒.Color`. -/
def colorMap' : 𝓒.ColorMap (Fin l.length) := def colorMap' : 𝓒.ColorMap (Fin l.length) :=
l.colorMap l.colorMap
@ -317,14 +312,13 @@ lemma ext {l l' : ColorIndexList 𝓒} (h : l.val = l'.val) : l = l' := by
apply IndexList.ext apply IndexList.ext
exact h exact h
/-! TODO: `orderEmbOfFin_univ` should be replaced with a mathlib lemma if possible. -/ /-! TODO: `orderEmbOfFin_univ` should be replaced with a mathlib lemma if possible. -/
lemma orderEmbOfFin_univ (n m : ℕ) (h : n = m): lemma orderEmbOfFin_univ (n m : ℕ) (h : n = m) :
Finset.orderEmbOfFin (Finset.univ : Finset (Fin n)) (by simp [h]: Finset.univ.card = m) = Finset.orderEmbOfFin (Finset.univ : Finset (Fin n)) (by simp [h]: Finset.univ.card = m) =
(Fin.castOrderIso h.symm).toOrderEmbedding := by (Fin.castOrderIso h.symm).toOrderEmbedding := by
symm symm
have h1 : (Fin.castOrderIso h.symm).toFun = have h1 : (Fin.castOrderIso h.symm).toFun =
( Finset.orderEmbOfFin (Finset.univ : Finset (Fin n)) (Finset.orderEmbOfFin (Finset.univ : Finset (Fin n))
(by simp [h]: Finset.univ.card = m)).toFun := by (by simp [h]: Finset.univ.card = m)).toFun := by
apply Finset.orderEmbOfFin_unique apply Finset.orderEmbOfFin_unique
intro x intro x
@ -332,7 +326,6 @@ lemma orderEmbOfFin_univ (n m : ℕ) (h : n = m):
exact fun ⦃a b⦄ a => a exact fun ⦃a b⦄ a => a
exact Eq.symm (Fin.orderEmbedding_eq (congrArg Set.range (id (Eq.symm h1)))) exact Eq.symm (Fin.orderEmbedding_eq (congrArg Set.range (id (Eq.symm h1))))
/-! /-!
## Contracting an `ColorIndexList` ## Contracting an `ColorIndexList`
@ -388,7 +381,6 @@ lemma contr_areDualInSelf (i j : Fin l.contr.length) :
l.contr.AreDualInSelf i j ↔ False := by l.contr.AreDualInSelf i j ↔ False := by
simp [contr] simp [contr]
/-! /-!
## Contract equiv ## Contract equiv
@ -397,7 +389,7 @@ lemma contr_areDualInSelf (i j : Fin l.contr.length) :
/-- An equivalence splitting the indices of `l` into /-- An equivalence splitting the indices of `l` into
a sum type of those indices and their duals (with choice determined by the ordering on `Fin`), a sum type of those indices and their duals (with choice determined by the ordering on `Fin`),
and those indices without duals. and those indices without duals.
This equivalence is used to contract the indices of tensors. -/ This equivalence is used to contract the indices of tensors. -/
def contrEquiv : (l.withUniqueDualLT ⊕ l.withUniqueDualLT) ⊕ Fin l.contr.length ≃ Fin l.length := def contrEquiv : (l.withUniqueDualLT ⊕ l.withUniqueDualLT) ⊕ Fin l.contr.length ≃ Fin l.length :=
@ -464,7 +456,7 @@ lemma contrEquiv_on_withDual_empty (i : Fin l.contr.length) (h : l.withDual =
-/ -/
/-- The condition on the `ColorIndexList`s `l` and `l2` so that on appending they form /-- The condition on the `ColorIndexList`s `l` and `l2` so that on appending they form
a `ColorIndexList`. -/ a `ColorIndexList`. -/
def AppendCond : Prop := def AppendCond : Prop :=
(l.toIndexList ++ l2.toIndexList).withUniqueDual = (l.toIndexList ++ l2.toIndexList).withDual (l.toIndexList ++ l2.toIndexList).withUniqueDual = (l.toIndexList ++ l2.toIndexList).withDual
@ -541,13 +533,13 @@ lemma appendCond_of_eq (h1 : l.withUniqueDual = l.withDual)
/-- A boolean which is true for two index lists `l` and `l2` if on appending /-- A boolean which is true for two index lists `l` and `l2` if on appending
they can form a `ColorIndexList`. -/ they can form a `ColorIndexList`. -/
def bool (l l2 : IndexList 𝓒.Color) : Bool := def bool (l l2 : IndexList 𝓒.Color) : Bool :=
if ¬ (l ++ l2).withUniqueDual = (l ++ l2).withDual then if ¬ (l ++ l2).withUniqueDual = (l ++ l2).withDual then
false false
else else
ColorCond.bool (l ++ l2) ColorCond.bool (l ++ l2)
lemma bool_iff (l l2 : IndexList 𝓒.Color) : lemma bool_iff (l l2 : IndexList 𝓒.Color) :
bool l l2 ↔ (l ++ l2).withUniqueDual = (l ++ l2).withDual ∧ ColorCond.bool (l ++ l2) := by bool l l2 ↔ (l ++ l2).withUniqueDual = (l ++ l2).withDual ∧ ColorCond.bool (l ++ l2) := by
simp [bool] simp [bool]
lemma iff_bool (l l2 : ColorIndexList 𝓒) : AppendCond l l2 ↔ bool l.toIndexList l2.toIndexList := by lemma iff_bool (l l2 : ColorIndexList 𝓒) : AppendCond l l2 ↔ bool l.toIndexList l2.toIndexList := by
@ -558,7 +550,6 @@ lemma iff_bool (l l2 : ColorIndexList 𝓒) : AppendCond l l2 ↔ bool l.toIndex
end AppendCond end AppendCond
end ColorIndexList end ColorIndexList
end IndexNotation end IndexNotation

32
HepLean/SpaceTime/LorentzTensor/IndexNotation/Contraction.lean
View file

@ -14,7 +14,6 @@ import Mathlib.Data.Finset.Sort
namespace IndexNotation namespace IndexNotation
namespace IndexList namespace IndexList
variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X] variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
@ -53,10 +52,10 @@ lemma withDual_union_withoutDual : l.withDual ∪ l.withoutDual = Finset.univ :=
/-- An equivalence from `Fin l.withoutDual.card` to `l.withoutDual` determined by /-- An equivalence from `Fin l.withoutDual.card` to `l.withoutDual` determined by
the order on `l.withoutDual` inherted from `Fin`. -/ the order on `l.withoutDual` inherted from `Fin`. -/
def withoutDualEquiv : Fin l.withoutDual.card ≃ l.withoutDual := def withoutDualEquiv : Fin l.withoutDual.card ≃ l.withoutDual :=
(Finset.orderIsoOfFin l.withoutDual (by rfl)).toEquiv (Finset.orderIsoOfFin l.withoutDual (by rfl)).toEquiv
/-- An equivalence splitting the indices of an index list `l` into those indices /-- An equivalence splitting the indices of an index list `l` into those indices
which have a dual in `l` and those which do not have a dual in `l`. -/ which have a dual in `l` and those which do not have a dual in `l`. -/
def dualEquiv : l.withDual ⊕ Fin l.withoutDual.card ≃ Fin l.length := def dualEquiv : l.withDual ⊕ Fin l.withoutDual.card ≃ Fin l.length :=
(Equiv.sumCongr (Equiv.refl _) l.withoutDualEquiv).trans <| (Equiv.sumCongr (Equiv.refl _) l.withoutDualEquiv).trans <|
@ -131,10 +130,10 @@ lemma contrIndexList_areDualInSelf_false (i j : Fin l.contrIndexList.length) :
@[simp] @[simp]
lemma contrIndexList_of_withDual_empty (h : l.withDual = ∅) : l.contrIndexList = l := by lemma contrIndexList_of_withDual_empty (h : l.withDual = ∅) : l.contrIndexList = l := by
have h1 := l.withDual_union_withoutDual have h1 := l.withDual_union_withoutDual
rw [h , Finset.empty_union] at h1 rw [h, Finset.empty_union] at h1
apply ext apply ext
rw [@List.ext_get_iff] rw [@List.ext_get_iff]
change l.contrIndexList.length = l.length ∧ _ change l.contrIndexList.length = l.length ∧ _
rw [contrIndexList_length, h1] rw [contrIndexList_length, h1]
simp only [Finset.card_univ, Fintype.card_fin, List.get_eq_getElem, true_and] simp only [Finset.card_univ, Fintype.card_fin, List.get_eq_getElem, true_and]
intro n h1' h2 intro n h1' h2
@ -152,7 +151,7 @@ lemma contrIndexList_contrIndexList : l.contrIndexList.contrIndexList = l.contrI
simp simp
@[simp] @[simp]
lemma contrIndexList_getDualInOther?_self (i : Fin l.contrIndexList.length) : lemma contrIndexList_getDualInOther?_self (i : Fin l.contrIndexList.length) :
l.contrIndexList.getDualInOther? l.contrIndexList i = some i := by l.contrIndexList.getDualInOther? l.contrIndexList i = some i := by
simp [getDualInOther?] simp [getDualInOther?]
rw [@Fin.find_eq_some_iff] rw [@Fin.find_eq_some_iff]
@ -160,14 +159,13 @@ lemma contrIndexList_getDualInOther?_self (i : Fin l.contrIndexList.length) :
intro j hj intro j hj
have h1 : i = j := by have h1 : i = j := by
by_contra hn by_contra hn
have h : l.contrIndexList.AreDualInSelf i j := by have h : l.contrIndexList.AreDualInSelf i j := by
simp only [AreDualInSelf] simp only [AreDualInSelf]
simp [hj] simp [hj]
exact hn exact hn
exact (contrIndexList_areDualInSelf_false l i j).mp h exact (contrIndexList_areDualInSelf_false l i j).mp h
exact Fin.ge_of_eq (id (Eq.symm h1)) exact Fin.ge_of_eq (id (Eq.symm h1))
/-! /-!
## Splitting withUniqueDual ## Splitting withUniqueDual
@ -231,7 +229,7 @@ lemma option_not_lt (i j : Option (Fin l.length)) : i < j → i ≠ j → ¬ j <
exact Fin.lt_asymm h exact Fin.lt_asymm h
/-! TODO: Replace with a mathlib lemma. -/ /-! TODO: Replace with a mathlib lemma. -/
lemma lt_option_of_not (i j : Option (Fin l.length)) : ¬ j < i → i ≠ j → i < j := by lemma lt_option_of_not (i j : Option (Fin l.length)) : ¬ j < i → i ≠ j → i < j := by
match i, j with match i, j with
| none, none => | none, none =>
exact fun a b => a (a (a (b rfl))) exact fun a b => a (a (a (b rfl)))
@ -243,7 +241,7 @@ lemma lt_option_of_not (i j : Option (Fin l.length)) : ¬ j < i → i ≠ j →
intro h h' intro h h'
simp_all simp_all
change ¬ j < i at h change ¬ j < i at h
change i < j change i < j
omega omega
/-- The equivalence between `l.withUniqueDualLT` and `l.withUniqueDualGT` obtained by /-- The equivalence between `l.withUniqueDualLT` and `l.withUniqueDualGT` obtained by
@ -273,16 +271,14 @@ def withUniqueDualLTEquivGT : l.withUniqueDualLT ≃ l.withUniqueDualGT where
withUniqueDualLTToWithUniqueDual]) withUniqueDualLTToWithUniqueDual])
/-- An equivalence from `l.withUniqueDualLT ⊕ l.withUniqueDualLT` to `l.withUniqueDual`. /-- An equivalence from `l.withUniqueDualLT ⊕ l.withUniqueDualLT` to `l.withUniqueDual`.
The first `l.withUniqueDualLT` are taken to themselves, whilst the second copy are The first `l.withUniqueDualLT` are taken to themselves, whilst the second copy are
taken to their dual. -/ taken to their dual. -/
def withUniqueLTGTEquiv : l.withUniqueDualLT ⊕ l.withUniqueDualLT ≃ l.withUniqueDual := by def withUniqueLTGTEquiv : l.withUniqueDualLT ⊕ l.withUniqueDualLT ≃ l.withUniqueDual := by
apply (Equiv.sumCongr (Equiv.refl _ ) l.withUniqueDualLTEquivGT).trans apply (Equiv.sumCongr (Equiv.refl _) l.withUniqueDualLTEquivGT).trans
apply (Equiv.Finset.union _ _ l.withUniqueDualLT_disjoint_withUniqueDualGT).trans apply (Equiv.Finset.union _ _ l.withUniqueDualLT_disjoint_withUniqueDualGT).trans
apply (Equiv.subtypeEquivRight (by simp only [l.withUniqueDualLT_union_withUniqueDualGT, apply (Equiv.subtypeEquivRight (by simp only [l.withUniqueDualLT_union_withUniqueDualGT,
implies_true])) implies_true]))
/-! /-!
## withUniqueDualInOther equal univ ## withUniqueDualInOther equal univ
@ -292,7 +288,7 @@ def withUniqueLTGTEquiv : l.withUniqueDualLT ⊕ l.withUniqueDualLT ≃ l.withUn
/-! TODO: There is probably a better place for this section. -/ /-! TODO: There is probably a better place for this section. -/
lemma withUniqueDualInOther_eq_univ_fst_withDual_empty lemma withUniqueDualInOther_eq_univ_fst_withDual_empty
(h : l.withUniqueDualInOther l2 = Finset.univ) : l.withDual = ∅ := by (h : l.withUniqueDualInOther l2 = Finset.univ) : l.withDual = ∅ := by
rw [@Finset.eq_empty_iff_forall_not_mem] rw [@Finset.eq_empty_iff_forall_not_mem]
intro x intro x
have hx : x ∈ l.withUniqueDualInOther l2 := by have hx : x ∈ l.withUniqueDualInOther l2 := by
@ -316,7 +312,7 @@ lemma withUniqueDualInOther_eq_univ_symm (hl : l.length = l2.length)
let S' : Finset (Fin l2.length) := let S' : Finset (Fin l2.length) :=
Finset.map ⟨Subtype.val, Subtype.val_injective⟩ Finset.map ⟨Subtype.val, Subtype.val_injective⟩
(Equiv.finsetCongr (Equiv.finsetCongr
(l.getDualInOtherEquiv l2) Finset.univ ) (l.getDualInOtherEquiv l2) Finset.univ)
have hSCard : S'.card = l2.length := by have hSCard : S'.card = l2.length := by
rw [Finset.card_map] rw [Finset.card_map]
simp only [Finset.univ_eq_attach, Equiv.finsetCongr_apply, Finset.card_map, Finset.card_attach] simp only [Finset.univ_eq_attach, Equiv.finsetCongr_apply, Finset.card_map, Finset.card_attach]
@ -325,7 +321,7 @@ lemma withUniqueDualInOther_eq_univ_symm (hl : l.length = l2.length)
have hsCardUn : S'.card = (@Finset.univ (Fin l2.length)).card := by have hsCardUn : S'.card = (@Finset.univ (Fin l2.length)).card := by
rw [hSCard] rw [hSCard]
exact Eq.symm (Finset.card_fin l2.length) exact Eq.symm (Finset.card_fin l2.length)
have hS'Eq : S' = (l2.withUniqueDualInOther l) := by have hS'Eq : S' = (l2.withUniqueDualInOther l) := by
rw [@Finset.ext_iff] rw [@Finset.ext_iff]
intro a intro a
simp only [S'] simp only [S']
@ -378,7 +374,7 @@ lemma withUniqueDualInOther_eq_univ_trans (h : l.withUniqueDualInOther l2 = Fins
use (l2.getDualInOther? l3 ((l.getDualInOther? l2 i).get hi.2.1)).get hi2.2.1 use (l2.getDualInOther? l3 ((l.getDualInOther? l2 i).get hi.2.1)).get hi2.2.1
simp only [AreDualInOther, getDualInOther?_id] simp only [AreDualInOther, getDualInOther?_id]
intro j hj intro j hj
have hj' : j = (l2.getDualInOther? l3 ((l.getDualInOther? l2 i).get hi.2.1)).get hi2.2.1 := by have hj' : j = (l2.getDualInOther? l3 ((l.getDualInOther? l2 i).get hi.2.1)).get hi2.2.1 := by
rw [← eq_getDualInOther?_get_of_withUniqueDualInOther_iff] rw [← eq_getDualInOther?_get_of_withUniqueDualInOther_iff]
simpa only [AreDualInOther, getDualInOther?_id] using hj simpa only [AreDualInOther, getDualInOther?_id] using hj
rw [h'] rw [h']

20
HepLean/SpaceTime/LorentzTensor/IndexNotation/GetDual.lean
View file

@ -16,13 +16,11 @@ We define the functions `getDual?` and `getDualInOther?` which return the
namespace IndexNotation namespace IndexNotation
namespace IndexList namespace IndexList
variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X] variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
variable (l l2 : IndexList X) variable (l l2 : IndexList X)
/-! /-!
## The getDual? Function ## The getDual? Function
@ -30,17 +28,15 @@ variable (l l2 : IndexList X)
-/ -/
/-- Given an `i`, if a dual exists in the same list, /-- Given an `i`, if a dual exists in the same list,
outputs the first such dual, otherwise outputs `none`. -/ outputs the first such dual, otherwise outputs `none`. -/
def getDual? (i : Fin l.length) : Option (Fin l.length) := def getDual? (i : Fin l.length) : Option (Fin l.length) :=
Fin.find (fun j => l.AreDualInSelf i j) Fin.find (fun j => l.AreDualInSelf i j)
/-- Given an `i`, if a dual exists in the other list, /-- Given an `i`, if a dual exists in the other list,
outputs the first such dual, otherwise outputs `none`. -/ outputs the first such dual, otherwise outputs `none`. -/
def getDualInOther? (i : Fin l.length) : Option (Fin l2.length) := def getDualInOther? (i : Fin l.length) : Option (Fin l2.length) :=
Fin.find (fun j => l.AreDualInOther l2 i j) Fin.find (fun j => l.AreDualInOther l2 i j)
/-! /-!
## Basic properties of getDual? ## Basic properties of getDual?
@ -65,7 +61,7 @@ lemma getDual?_of_areDualInSelf (h : l.AreDualInSelf i j) :
intro k' hk' intro k' hk'
by_cases hik' : i = k' by_cases hik' : i = k'
· exact Fin.ge_of_eq (id (Eq.symm hik')) · exact Fin.ge_of_eq (id (Eq.symm hik'))
· have hik'' : l.AreDualInSelf i k' := by · have hik'' : l.AreDualInSelf i k' := by
simp [AreDualInSelf, hik'] simp [AreDualInSelf, hik']
simp_all [AreDualInSelf] simp_all [AreDualInSelf]
have hk'' := hk.2 k' hik'' have hk'' := hk.2 k' hik''
@ -86,7 +82,7 @@ lemma getDual?_of_areDualInSelf (h : l.AreDualInSelf i j) :
by_cases hik' : i = k' by_cases hik' : i = k'
subst hik' subst hik'
exact Lean.Omega.Fin.le_of_not_lt hik exact Lean.Omega.Fin.le_of_not_lt hik
have hik'' : l.AreDualInSelf i k' := by have hik'' : l.AreDualInSelf i k' := by
simp [AreDualInSelf, hik'] simp [AreDualInSelf, hik']
simp_all [AreDualInSelf] simp_all [AreDualInSelf]
exact hk.2 k' hik'' exact hk.2 k' hik''
@ -124,7 +120,7 @@ lemma getDual?_get_areDualInSelf (i : Fin l.length) (h : (l.getDual? i).isSome)
@[simp] @[simp]
lemma getDual?_areDualInSelf_get (i : Fin l.length) (h : (l.getDual? i).isSome) : lemma getDual?_areDualInSelf_get (i : Fin l.length) (h : (l.getDual? i).isSome) :
l.AreDualInSelf i ((l.getDual? i).get h):= l.AreDualInSelf i ((l.getDual? i).get h) :=
AreDualInSelf.symm (getDual?_get_areDualInSelf l i h) AreDualInSelf.symm (getDual?_get_areDualInSelf l i h)
@[simp] @[simp]
@ -206,7 +202,7 @@ lemma getDual?_isSome_append_inl_iff (i : Fin l.length) :
@[simp] @[simp]
lemma getDual?_isSome_append_inr_iff (i : Fin l2.length) : lemma getDual?_isSome_append_inr_iff (i : Fin l2.length) :
((l ++ l2).getDual? (appendEquiv (Sum.inr i))).isSome ↔ ((l ++ l2).getDual? (appendEquiv (Sum.inr i))).isSome ↔
(l2.getDual? i).isSome ∨ (l2.getDualInOther? l i).isSome := by (l2.getDual? i).isSome ∨ (l2.getDualInOther? l i).isSome := by
rw [getDual?_isSome_iff_exists, getDual?_isSome_iff_exists, getDualInOther?_isSome_iff_exists] rw [getDual?_isSome_iff_exists, getDual?_isSome_iff_exists, getDualInOther?_isSome_iff_exists]
refine Iff.intro (fun h => ?_) (fun h => ?_) refine Iff.intro (fun h => ?_) (fun h => ?_)
· obtain ⟨j, hj⟩ := h · obtain ⟨j, hj⟩ := h
@ -245,7 +241,7 @@ lemma getDual?_eq_none_append_inl_iff (i : Fin l.length) :
exact h1 h exact h1 h
@[simp] @[simp]
lemma getDual?_eq_none_append_inr_iff (i : Fin l2.length) : lemma getDual?_eq_none_append_inr_iff (i : Fin l2.length) :
(l ++ l2).getDual? (appendEquiv (Sum.inr i)) = none ↔ (l ++ l2).getDual? (appendEquiv (Sum.inr i)) = none ↔
(l2.getDual? i = none ∧ l2.getDualInOther? l i = none) := by (l2.getDual? i = none ∧ l2.getDualInOther? l i = none) := by
apply Iff.intro apply Iff.intro
@ -290,7 +286,7 @@ lemma getDual?_append_inl_of_getDual?_isSome (i : Fin l.length) (h : (l.getDual?
lemma getDual?_inl_of_getDual?_isNone_getDualInOther?_isSome (i : Fin l.length) lemma getDual?_inl_of_getDual?_isNone_getDualInOther?_isSome (i : Fin l.length)
(hi : (l.getDual? i).isNone) (h : (l.getDualInOther? l2 i).isSome) : (hi : (l.getDual? i).isNone) (h : (l.getDualInOther? l2 i).isSome) :
(l ++ l2).getDual? (appendEquiv (Sum.inl i)) = some (l ++ l2).getDual? (appendEquiv (Sum.inl i)) = some
(appendEquiv (Sum.inr ((l.getDualInOther? l2 i).get h))) := by (appendEquiv (Sum.inr ((l.getDualInOther? l2 i).get h))) := by
rw [getDual?, Fin.find_eq_some_iff, AreDualInSelf.append_inl_inr] rw [getDual?, Fin.find_eq_some_iff, AreDualInSelf.append_inl_inr]
apply And.intro (getDualInOther?_areDualInOther_get l l2 i h) apply And.intro (getDualInOther?_areDualInOther_get l l2 i h)
intro j hj intro j hj

2
HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexString.lean
View file

@ -268,7 +268,7 @@ noncomputable def fromIndexString (T : 𝓣.Tensor cn) (s : String)
(hn : n = (toIndexList' s hs).length) (hn : n = (toIndexList' s hs).length)
(hD : (toIndexList' s hs).withDual = (toIndexList' s hs).withUniqueDual) (hD : (toIndexList' s hs).withDual = (toIndexList' s hs).withUniqueDual)
(hC : IndexList.ColorCond (toIndexList' s hs)) (hC : IndexList.ColorCond (toIndexList' s hs))
(hd : TensorColor.ColorMap.DualMap (toIndexList' s hs).colorMap (hd : TensorColor.ColorMap.DualMap (toIndexList' s hs).colorMap
(cn ∘ Fin.cast hn.symm)) : 𝓣.TensorIndex := (cn ∘ Fin.cast hn.symm)) : 𝓣.TensorIndex :=
TensorStructure.TensorIndex.mkDualMap T ⟨(toIndexList' s hs), hD, hC⟩ hn hd TensorStructure.TensorIndex.mkDualMap T ⟨(toIndexList' s hs), hD, hC⟩ hn hd

20
HepLean/SpaceTime/LorentzTensor/IndexNotation/OnlyUniqueDuals.lean
View file

@ -18,7 +18,6 @@ namespace IndexList
variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X] variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
variable (l l2 l3 : IndexList X) variable (l l2 l3 : IndexList X)
/-! /-!
## withDual equal to withUniqueDual ## withDual equal to withUniqueDual
@ -56,7 +55,7 @@ lemma withUnqiueDual_eq_withDual_iff :
by_cases hi : i ∈ l.withDual by_cases hi : i ∈ l.withDual
· have hii : i ∈ l.withUniqueDual := by · have hii : i ∈ l.withUniqueDual := by
simp_all only simp_all only
change (l.getDual? i).bind l.getDual? = _ change (l.getDual? i).bind l.getDual? = _
simp [hii] simp [hii]
symm symm
rw [Option.guard_eq_some] rw [Option.guard_eq_some]
@ -79,8 +78,8 @@ lemma withUnqiueDual_eq_withDual_iff :
rw [hi] at hj' rw [hi] at hj'
rw [h i] at hj' rw [h i] at hj'
have hi : Option.guard (fun i => i ∈ l.withDual) ↑i = some i := by have hi : Option.guard (fun i => i ∈ l.withDual) ↑i = some i := by
apply Option.guard_eq_some.mpr apply Option.guard_eq_some.mpr
simp simp
rw [hi] at hj' rw [hi] at hj'
simp at hj' simp at hj'
have hj'' := Option.guard_eq_some.mp hj'.symm have hj'' := Option.guard_eq_some.mp hj'.symm
@ -129,7 +128,7 @@ lemma withUnqiueDual_eq_withDual_of_empty (h : l.withDual = ∅) :
intro x intro x
by_contra hx by_contra hx
have x' : l.withDual := ⟨x, l.mem_withDual_of_withUniqueDual ⟨x, hx⟩⟩ have x' : l.withDual := ⟨x, l.mem_withDual_of_withUniqueDual ⟨x, hx⟩⟩
have hx' := x'.2 have hx' := x'.2
simp [h] at hx' simp [h] at hx'
/-! /-!
@ -140,7 +139,7 @@ lemma withUnqiueDual_eq_withDual_of_empty (h : l.withDual = ∅) :
lemma withUniqueDualInOther_eq_withDualInOther_append_of_symm' lemma withUniqueDualInOther_eq_withDualInOther_append_of_symm'
(h : (l ++ l2).withUniqueDualInOther l3 = (l ++ l2).withDualInOther l3) : (h : (l ++ l2).withUniqueDualInOther l3 = (l ++ l2).withDualInOther l3) :
(l2 ++ l).withUniqueDualInOther l3 = (l2 ++ l).withDualInOther l3 := by (l2 ++ l).withUniqueDualInOther l3 = (l2 ++ l).withDualInOther l3 := by
rw [Finset.ext_iff] at h ⊢ rw [Finset.ext_iff] at h ⊢
intro j intro j
obtain ⟨k, hk⟩ := appendEquiv.surjective j obtain ⟨k, hk⟩ := appendEquiv.surjective j
@ -179,20 +178,18 @@ lemma withUniqueDualInOther_eq_withDualInOther_of_append_symm :
exact l.withUniqueDualInOther_eq_withDualInOther_of_append_symm' l2 l3 exact l.withUniqueDualInOther_eq_withDualInOther_of_append_symm' l2 l3
exact l.withUniqueDualInOther_eq_withDualInOther_of_append_symm' l3 l2 exact l.withUniqueDualInOther_eq_withDualInOther_of_append_symm' l3 l2
/-! /-!
## withDual equal to withUniqueDual append conditions ## withDual equal to withUniqueDual append conditions
-/ -/
lemma append_withDual_eq_withUniqueDual_iff : lemma append_withDual_eq_withUniqueDual_iff :
(l ++ l2).withUniqueDual = (l ++ l2).withDual ↔ (l ++ l2).withUniqueDual = (l ++ l2).withDual ↔
((l.withUniqueDual ∩ (l.withDualInOther l2)ᶜ) ∪ l.withUniqueDualInOther l2) ((l.withUniqueDual ∩ (l.withDualInOther l2)ᶜ) ∪ l.withUniqueDualInOther l2)
= l.withDual ∪ l.withDualInOther l2 = l.withDual ∪ l.withDualInOther l2
∧ (l2.withUniqueDual ∩ (l2.withDualInOther l)ᶜ) ∪ l2.withUniqueDualInOther l ∧ (l2.withUniqueDual ∩ (l2.withDualInOther l)ᶜ) ∪ l2.withUniqueDualInOther l
= l2.withDual ∪ l2.withDualInOther l := by = l2.withDual ∪ l2.withDualInOther l := by
rw [append_withUniqueDual_disjSum, withDual_append_eq_disjSum] rw [append_withUniqueDual_disjSum, withDual_append_eq_disjSum]
simp only [Equiv.finsetCongr_apply, Finset.map_inj] simp only [Equiv.finsetCongr_apply, Finset.map_inj]
have h (s s' : Finset (Fin l.length)) (t t' : Finset (Fin l2.length)) : have h (s s' : Finset (Fin l.length)) (t t' : Finset (Fin l2.length)) :
@ -227,7 +224,7 @@ lemma append_withDual_eq_withUniqueDual_inr (h : (l ++ l2).withUniqueDual = (l +
@[simp] @[simp]
lemma append_withDual_eq_withUniqueDual_withUniqueDualInOther_inl lemma append_withDual_eq_withUniqueDual_withUniqueDualInOther_inl
(h : (l ++ l2).withUniqueDual = (l ++ l2).withDual) : (h : (l ++ l2).withUniqueDual = (l ++ l2).withDual) :
l.withUniqueDualInOther l2 = l.withDualInOther l2 := by l.withUniqueDualInOther l2 = l.withDualInOther l2 := by
rw [Finset.ext_iff] rw [Finset.ext_iff]
intro i intro i
@ -242,7 +239,7 @@ lemma append_withDual_eq_withUniqueDual_withUniqueDualInOther_inl
@[simp] @[simp]
lemma append_withDual_eq_withUniqueDual_withUniqueDualInOther_inr lemma append_withDual_eq_withUniqueDual_withUniqueDualInOther_inr
(h : (l ++ l2).withUniqueDual = (l ++ l2).withDual) : (h : (l ++ l2).withUniqueDual = (l ++ l2).withDual) :
l2.withUniqueDualInOther l = l2.withDualInOther l := by l2.withUniqueDualInOther l = l2.withDualInOther l := by
rw [append_withDual_eq_withUniqueDual_symm] at h rw [append_withDual_eq_withUniqueDual_symm] at h
exact append_withDual_eq_withUniqueDual_withUniqueDualInOther_inl l2 l h exact append_withDual_eq_withUniqueDual_withUniqueDualInOther_inl l2 l h
@ -292,7 +289,6 @@ lemma append_withDual_eq_withUniqueDual_swap :
rw [withUniqueDualInOther_eq_withDualInOther_of_append_symm] rw [withUniqueDualInOther_eq_withDualInOther_of_append_symm]
rw [withUniqueDualInOther_eq_withDualInOther_append_of_symm] rw [withUniqueDualInOther_eq_withDualInOther_append_of_symm]
end IndexList end IndexList
end IndexNotation end IndexNotation

7
HepLean/SpaceTime/LorentzTensor/IndexNotation/Relations.lean
View file

@ -18,7 +18,6 @@ a Tensor Color structure.
namespace IndexNotation namespace IndexNotation
namespace ColorIndexList namespace ColorIndexList
variable {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color] variable {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
@ -59,11 +58,10 @@ def ContrPerm : Prop :=
l'.contr.colorMap' ∘ Subtype.val ∘ (l.contr.getDualInOtherEquiv l'.contr) l'.contr.colorMap' ∘ Subtype.val ∘ (l.contr.getDualInOtherEquiv l'.contr)
= l.contr.colorMap' ∘ Subtype.val = l.contr.colorMap' ∘ Subtype.val
namespace ContrPerm namespace ContrPerm
variable {l l' l2 l3 : ColorIndexList 𝓒} variable {l l' l2 l3 : ColorIndexList 𝓒}
@[symm] @[symm]
lemma symm (h : ContrPerm l l') : ContrPerm l' l := by lemma symm (h : ContrPerm l l') : ContrPerm l' l := by
rw [ContrPerm] at h ⊢ rw [ContrPerm] at h ⊢
@ -148,7 +146,6 @@ lemma contrPermEquiv_colorMap_iso' {l l' : ColorIndexList 𝓒} (h : ContrPerm l
rw [ColorMap.MapIso.symm'] rw [ColorMap.MapIso.symm']
exact contrPermEquiv_colorMap_iso h exact contrPermEquiv_colorMap_iso h
@[simp] @[simp]
lemma contrPermEquiv_refl : contrPermEquiv (@ContrPerm.refl 𝓒 _ l) = Equiv.refl _ := by lemma contrPermEquiv_refl : contrPermEquiv (@ContrPerm.refl 𝓒 _ l) = Equiv.refl _ := by
simp [contrPermEquiv, ContrPerm.refl] simp [contrPermEquiv, ContrPerm.refl]
@ -185,7 +182,7 @@ lemma contrPermEquiv_self_contr {l : ColorIndexList 𝓒} :
symm symm
rw [← eq_getDualInOther?_get_of_withUniqueDualInOther_iff] rw [← eq_getDualInOther?_get_of_withUniqueDualInOther_iff]
simp only [AreDualInOther, contr_contr_idMap, Fin.cast_trans, Fin.cast_eq_self] simp only [AreDualInOther, contr_contr_idMap, Fin.cast_trans, Fin.cast_eq_self]
have h1 : ContrPerm l l.contr := by simp have h1 : ContrPerm l l.contr := by simp
rw [h1.2.1] rw [h1.2.1]
simp simp

15
HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean
View file

@ -74,7 +74,6 @@ lemma ext {T₁ T₂ : 𝓣.TensorIndex} (hi : T₁.toColorIndexList = T₂.toCo
subst hi subst hi
simp_all simp_all
lemma index_eq_of_eq {T₁ T₂ : 𝓣.TensorIndex} (h : T₁ = T₂) : lemma index_eq_of_eq {T₁ T₂ : 𝓣.TensorIndex} (h : T₁ = T₂) :
T₁.toColorIndexList = T₂.toColorIndexList := by T₁.toColorIndexList = T₂.toColorIndexList := by
cases h cases h
@ -134,7 +133,7 @@ lemma contr_of_withDual_empty (T : 𝓣.TensorIndex) (h : T.withDual = ∅) :
simp only [PiTensorProduct.tprodCoeff_eq_smul_tprod, LinearMapClass.map_smul, mapIso_tprod, simp only [PiTensorProduct.tprodCoeff_eq_smul_tprod, LinearMapClass.map_smul, mapIso_tprod,
id_eq, eq_mpr_eq_cast, OrderIso.toEquiv_symm, RelIso.coe_fn_toEquiv] id_eq, eq_mpr_eq_cast, OrderIso.toEquiv_symm, RelIso.coe_fn_toEquiv]
apply congrArg apply congrArg
have hEm : IsEmpty { x // x ∈ i.withUniqueDualLT } := by have hEm : IsEmpty { x // x ∈ i.withUniqueDualLT } := by
rw [Finset.isEmpty_coe_sort] rw [Finset.isEmpty_coe_sort]
rw [Finset.eq_empty_iff_forall_not_mem] rw [Finset.eq_empty_iff_forall_not_mem]
intro x hx intro x hx
@ -158,7 +157,7 @@ lemma contr_of_withDual_empty (T : 𝓣.TensorIndex) (h : T.withDual = ∅) :
@[simp] @[simp]
lemma contr_contr (T : 𝓣.TensorIndex) : T.contr.contr = T.contr := lemma contr_contr (T : 𝓣.TensorIndex) : T.contr.contr = T.contr :=
T.contr.contr_of_withDual_empty (by simp [contr, ColorIndexList.contr]) T.contr.contr_of_withDual_empty (by simp [contr, ColorIndexList.contr])
@[simp] @[simp]
lemma contr_toColorIndexList (T : 𝓣.TensorIndex) : lemma contr_toColorIndexList (T : 𝓣.TensorIndex) :
@ -197,8 +196,6 @@ lemma smul_contr (r : R) (T : 𝓣.TensorIndex) : (r • T).contr = r • T.cont
-/ -/
/-- An (equivalence) relation on two `TensorIndex`. /-- An (equivalence) relation on two `TensorIndex`.
The point in this equivalence relation is that certain things (like the The point in this equivalence relation is that certain things (like the
permutation of indices, the contraction of indices, or rising or lowering indices) can be placed permutation of indices, the contraction of indices, or rising or lowering indices) can be placed
@ -320,10 +317,8 @@ lemma rel_left {T₁ T₁' T₂ : 𝓣.TensorIndex} (h : AddCond T₁ T₂) (h'
lemma rel_right {T₁ T₂ T₂' : 𝓣.TensorIndex} (h : AddCond T₁ T₂) (h' : T₂ ≈ T₂') : lemma rel_right {T₁ T₂ T₂' : 𝓣.TensorIndex} (h : AddCond T₁ T₂) (h' : T₂ ≈ T₂') :
AddCond T₁ T₂' := h.trans h'.1 AddCond T₁ T₂' := h.trans h'.1
end AddCond end AddCond
/-- The equivalence between indices after contraction given a `AddCond`. -/ /-- The equivalence between indices after contraction given a `AddCond`. -/
@[simp] @[simp]
def addCondEquiv {T₁ T₂ : 𝓣.TensorIndex} (h : AddCond T₁ T₂) : def addCondEquiv {T₁ T₂ : 𝓣.TensorIndex} (h : AddCond T₁ T₂) :
@ -405,7 +400,7 @@ lemma smul_add (r : R) (T₁ T₂ : 𝓣.TensorIndex) (h : AddCond T₁ T₂) :
simp only [smul_index, contr_toColorIndexList, Fin.castOrderIso_refl, OrderIso.refl_toEquiv, simp only [smul_index, contr_toColorIndexList, Fin.castOrderIso_refl, OrderIso.refl_toEquiv,
mapIso_refl, smul_tensor, map_smul, LinearEquiv.refl_apply] mapIso_refl, smul_tensor, map_smul, LinearEquiv.refl_apply]
lemma add_withDual_empty (T₁ T₂ : 𝓣.TensorIndex) (h : AddCond T₁ T₂) : lemma add_withDual_empty (T₁ T₂ : 𝓣.TensorIndex) (h : AddCond T₁ T₂) :
(T₁ +[h] T₂).withDual = ∅ := by (T₁ +[h] T₂).withDual = ∅ := by
simp [contr] simp [contr]
change T₂.toColorIndexList.contr.withDual = ∅ change T₂.toColorIndexList.contr.withDual = ∅
@ -463,7 +458,7 @@ lemma add_rel_right {T₁ T₂ T₂' : 𝓣.TensorIndex} (h : AddCond T₁ T₂)
open AddCond in open AddCond in
lemma add_assoc' {T₁ T₂ T₃ : 𝓣.TensorIndex} {h' : AddCond T₂ T₃} (h : AddCond T₁ (T₂ +[h'] T₃)) : lemma add_assoc' {T₁ T₂ T₃ : 𝓣.TensorIndex} {h' : AddCond T₂ T₃} (h : AddCond T₁ (T₂ +[h'] T₃)) :
T₁ +[h] (T₂ +[h'] T₃) = T₁ +[h'.of_add_right h] T₂ +[h'.add_left_of_add_right h] T₃ := by T₁ +[h] (T₂ +[h'] T₃) = T₁ +[h'.of_add_right h] T₂ +[h'.add_left_of_add_right h] T₃ := by
refine ext ?_ ?_ refine ext ?_ ?_
simp only [add_toColorIndexList, ColorIndexList.contr_contr] simp only [add_toColorIndexList, ColorIndexList.contr_contr]
simp only [add_toColorIndexList, add_tensor, contr_toColorIndexList, addCondEquiv, simp only [add_toColorIndexList, add_tensor, contr_toColorIndexList, addCondEquiv,
contr_add_tensor, map_add, mapIso_mapIso] contr_add_tensor, map_add, mapIso_mapIso]
@ -486,7 +481,6 @@ lemma add_assoc {T₁ T₂ T₃ : 𝓣.TensorIndex} {h' : AddCond T₁ T₂} (h
-/ -/
/-- The condition on two `TensorIndex` which is true if and only if their `ColorIndexList`s /-- The condition on two `TensorIndex` which is true if and only if their `ColorIndexList`s
are related by the condition `AppendCond`. That is, they can be appended to form a are related by the condition `AppendCond`. That is, they can be appended to form a
`ColorIndexList`. -/ `ColorIndexList`. -/
@ -515,7 +509,6 @@ lemma prod_toColorIndexList (T₁ T₂ : 𝓣.TensorIndex) (h : ProdCond T₁ T
lemma prod_toIndexList (T₁ T₂ : 𝓣.TensorIndex) (h : ProdCond T₁ T₂) : lemma prod_toIndexList (T₁ T₂ : 𝓣.TensorIndex) (h : ProdCond T₁ T₂) :
(prod T₁ T₂ h).toIndexList = T₁.toIndexList ++ T₂.toIndexList := rfl (prod T₁ T₂ h).toIndexList = T₁.toIndexList ++ T₂.toIndexList := rfl
end TensorIndex end TensorIndex
end end
end TensorStructure end TensorStructure

4
HepLean/SpaceTime/LorentzTensor/IndexNotation/WithDual.lean
View file

@ -13,10 +13,8 @@ We define the finite sets of indices in an index list which have a dual
-/ -/
namespace IndexNotation namespace IndexNotation
namespace IndexList namespace IndexList
variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X] variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
@ -65,7 +63,6 @@ lemma mem_withDual_iff_exists : i ∈ l.withDual ↔ ∃ j, l.AreDualInSelf i j
-/ -/
@[simp] @[simp]
lemma mem_withInDualOther_iff_isSome (i : Fin l.length) : lemma mem_withInDualOther_iff_isSome (i : Fin l.length) :
i ∈ l.withDualInOther l2 ↔ (l.getDualInOther? l2 i).isSome := by i ∈ l.withDualInOther l2 ↔ (l.getDualInOther? l2 i).isSome := by
@ -114,7 +111,6 @@ lemma append_withDualInOther_eq :
| Sum.inr k => | Sum.inr k =>
simp simp
lemma withDualInOther_append_eq : l.withDualInOther (l2 ++ l3) = lemma withDualInOther_append_eq : l.withDualInOther (l2 ++ l3) =
l.withDualInOther l2 ∪ l.withDualInOther l3 := by l.withDualInOther l2 ∪ l.withDualInOther l3 := by
ext i ext i

57
HepLean/SpaceTime/LorentzTensor/IndexNotation/WithUniqueDual.lean
View file

@ -15,13 +15,11 @@ Finite sets of indices with a unique dual.
namespace IndexNotation namespace IndexNotation
namespace IndexList namespace IndexList
variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X] variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
variable (l l2 l3 : IndexList X) variable (l l2 l3 : IndexList X)
/-! /-!
## Unique duals ## Unique duals
@ -37,7 +35,7 @@ def withUniqueDual : Finset (Fin l.length) :=
list. -/ list. -/
def withUniqueDualInOther : Finset (Fin l.length) := def withUniqueDualInOther : Finset (Fin l.length) :=
Finset.filter (fun i => i ∉ l.withDual ∧ i ∈ l.withDualInOther l2 Finset.filter (fun i => i ∉ l.withDual ∧ i ∈ l.withDualInOther l2
∧ (∀ j, l.AreDualInOther l2 i j → j = l.getDualInOther? l2 i)) Finset.univ ∧ (∀ j, l.AreDualInOther l2 i j → j = l.getDualInOther? l2 i)) Finset.univ
/-! /-!
@ -61,8 +59,6 @@ lemma mem_withDual_of_withUniqueDual (i : l.withUniqueDual) :
i.1 ∈ l.withDual := i.1 ∈ l.withDual :=
mem_withDual_of_mem_withUniqueDual l (↑i) i.2 mem_withDual_of_mem_withUniqueDual l (↑i) i.2
/-! /-!
## Basic properties of withUniqueDualInOther ## Basic properties of withUniqueDualInOther
@ -128,7 +124,7 @@ lemma getDual?_get_getDual?_get_of_withUniqueDual (i : Fin l.length) (h : i ∈
(l.getDual? ((l.getDual? i).get (mem_withUniqueDual_isSome l i h))).get (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 (l.getDual?_getDual?_get_isSome i (mem_withUniqueDual_isSome l i h)) = i := by
by_contra hn by_contra hn
have h' : l.AreDualInSelf i ((l.getDual? ((l.getDual? i).get have h' : l.AreDualInSelf i ((l.getDual? ((l.getDual? i).get
(mem_withUniqueDual_isSome l i h))).get ( (mem_withUniqueDual_isSome l i h))).get (
getDual?_getDual?_get_isSome l i (mem_withUniqueDual_isSome l i h))) := by getDual?_getDual?_get_isSome l i (mem_withUniqueDual_isSome l i h))) := by
simp [AreDualInSelf, hn] simp [AreDualInSelf, hn]
@ -168,7 +164,6 @@ lemma getDual?_get_of_mem_withUnique_mem (i : Fin l.length) (h : i ∈ l.withUni
subst h1 subst h1
exact Eq.symm (getDual?_getDual?_get_of_withUniqueDual l i h) exact Eq.symm (getDual?_getDual?_get_of_withUniqueDual l i h)
/-! /-!
## Properties of getDualInOther? and withUniqueDualInOther ## Properties of getDualInOther? and withUniqueDualInOther
@ -188,7 +183,7 @@ lemma some_eq_getDualInOther?_of_withUniqueDualInOther_iff (i : Fin l.length) (j
exact fun h' => l.all_dual_eq_of_withUniqueDualInOther l2 i h j h' exact fun h' => l.all_dual_eq_of_withUniqueDualInOther l2 i h j h'
intro h' intro h'
have hj : j = (l.getDualInOther? l2 i).get (mem_withUniqueDualInOther_isSome l l2 i h) := have hj : j = (l.getDualInOther? l2 i).get (mem_withUniqueDualInOther_isSome l l2 i h) :=
Eq.symm (Option.get_of_mem (mem_withUniqueDualInOther_isSome l l2 i h) (id (Eq.symm h'))) Eq.symm (Option.get_of_mem (mem_withUniqueDualInOther_isSome l l2 i h) (id (Eq.symm h')))
subst hj subst hj
exact getDualInOther?_areDualInOther_get l l2 i (mem_withUniqueDualInOther_isSome l l2 i h) exact getDualInOther?_areDualInOther_get l l2 i (mem_withUniqueDualInOther_isSome l l2 i h)
@ -210,10 +205,10 @@ lemma getDualInOther?_get_getDualInOther?_get_of_withUniqueDualInOther
(l.getDualInOther?_getDualInOther?_get_isSome l2 i (l.getDualInOther?_getDualInOther?_get_isSome l2 i
(mem_withUniqueDualInOther_isSome l l2 i h)) = i := by (mem_withUniqueDualInOther_isSome l l2 i h)) = i := by
by_contra hn by_contra hn
have h' : l.AreDualInSelf i ((l2.getDualInOther? l ((l.getDualInOther? l2 i).get have h' : l.AreDualInSelf i ((l2.getDualInOther? l ((l.getDualInOther? l2 i).get
(mem_withUniqueDualInOther_isSome l l2 i h))).get (mem_withUniqueDualInOther_isSome l l2 i h))).get
(l.getDualInOther?_getDualInOther?_get_isSome l2 i (l.getDualInOther?_getDualInOther?_get_isSome l2 i
(mem_withUniqueDualInOther_isSome l l2 i h))):= by (mem_withUniqueDualInOther_isSome l l2 i h))) := by
simp [AreDualInSelf, hn] simp [AreDualInSelf, hn]
exact fun a => hn (id (Eq.symm a)) exact fun a => hn (id (Eq.symm a))
have h1 := l.not_mem_withDual_of_withUniqueDualInOther l2 ⟨i, h⟩ have h1 := l.not_mem_withDual_of_withUniqueDualInOther l2 ⟨i, h⟩
@ -285,17 +280,12 @@ lemma getDualInOther?_get_of_mem_withUniqueInOther_mem (i : Fin l.length)
rw [Fin.find_eq_none_iff] at h rw [Fin.find_eq_none_iff] at h
simp_all only simp_all only
@[simp] @[simp]
lemma getDualInOther?_self_of_mem_withUniqueInOther (i : Fin l.length) lemma getDualInOther?_self_of_mem_withUniqueInOther (i : Fin l.length)
(h : i ∈ l.withUniqueDualInOther l) : (h : i ∈ l.withUniqueDualInOther l) :
l.getDualInOther? l i = some i := by l.getDualInOther? l i = some i := by
rw [all_dual_eq_of_withUniqueDualInOther l l i h i rfl] rw [all_dual_eq_of_withUniqueDualInOther l l i h i rfl]
/-! /-!
## Properties of getDual?, withUniqueDual and append ## Properties of getDual?, withUniqueDual and append
@ -319,7 +309,6 @@ lemma append_inl_not_mem_withDual_of_withDualInOther (i : Fin l.length)
simp only [getDual?_isSome_append_inl_iff] at ht simp only [getDual?_isSome_append_inl_iff] at ht
simp_all simp_all
lemma append_inr_not_mem_withDual_of_withDualInOther (i : Fin l2.length) lemma append_inr_not_mem_withDual_of_withDualInOther (i : Fin l2.length)
(h : appendEquiv (Sum.inr i) ∈ (l ++ l2).withUniqueDual) : (h : appendEquiv (Sum.inr i) ∈ (l ++ l2).withUniqueDual) :
i ∈ l2.withDual ↔ ¬ i ∈ l2.withDualInOther l := by i ∈ l2.withDual ↔ ¬ i ∈ l2.withDualInOther l := by
@ -337,7 +326,6 @@ lemma append_inr_not_mem_withDual_of_withDualInOther (i : Fin l2.length)
simp only [getDual?_isSome_append_inr_iff] at ht simp only [getDual?_isSome_append_inr_iff] at ht
simp_all simp_all
lemma getDual?_append_symm_of_withUniqueDual_of_inl (i : Fin l.length) (k : Fin l2.length) lemma getDual?_append_symm_of_withUniqueDual_of_inl (i : Fin l.length) (k : Fin l2.length)
(h : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual) : (h : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual) :
(l ++ l2).getDual? (appendEquiv (Sum.inl i)) = some (appendEquiv (Sum.inr k)) (l ++ l2).getDual? (appendEquiv (Sum.inl i)) = some (appendEquiv (Sum.inr k))
@ -394,10 +382,10 @@ lemma mem_withUniqueDual_append_symm (i : Fin l.length) :
implies_true, and_self, mem_withUniqueDual_isSome, eq_getDual?_get_of_withUniqueDual_iff, implies_true, and_self, mem_withUniqueDual_isSome, eq_getDual?_get_of_withUniqueDual_iff,
getDual?_areDualInSelf_get] getDual?_areDualInSelf_get]
| Sum.inr k => | Sum.inr k =>
have hk' := h' (appendEquiv (Sum.inl k)) have hk' := h' (appendEquiv (Sum.inl k))
simp only [AreDualInSelf.append_inl_inl] at hk' simp only [AreDualInSelf.append_inl_inl] at hk'
simp only [AreDualInSelf.append_inr_inr] at hj simp only [AreDualInSelf.append_inr_inr] at hj
refine ((l.getDual?_append_symm_of_withUniqueDual_of_inl' l2 _ _ ?_).mp (hk' hj).symm).symm refine ((l.getDual?_append_symm_of_withUniqueDual_of_inl' l2 _ _ ?_).mp (hk' hj).symm).symm
simp_all only [AreDualInSelf.append_inl_inl, imp_self, withUniqueDual, simp_all only [AreDualInSelf.append_inl_inl, imp_self, withUniqueDual,
mem_withDual_iff_isSome, Finset.mem_filter, Finset.mem_univ, getDual?_isSome_append_inl_iff, mem_withDual_iff_isSome, Finset.mem_filter, Finset.mem_univ, getDual?_isSome_append_inl_iff,
implies_true, and_self, mem_withUniqueDual_isSome, eq_getDual?_get_of_withUniqueDual_iff, implies_true, and_self, mem_withUniqueDual_isSome, eq_getDual?_get_of_withUniqueDual_iff,
@ -415,30 +403,30 @@ lemma mem_withUniqueDual_append_symm (i : Fin l.length) :
implies_true, and_self, mem_withUniqueDual_isSome, eq_getDual?_get_of_withUniqueDual_iff, implies_true, and_self, mem_withUniqueDual_isSome, eq_getDual?_get_of_withUniqueDual_iff,
getDual?_areDualInSelf_get] getDual?_areDualInSelf_get]
| Sum.inr k => | Sum.inr k =>
have hk' := h' (appendEquiv (Sum.inl k)) have hk' := h' (appendEquiv (Sum.inl k))
simp only [AreDualInSelf.append_inr_inl] at hk' simp only [AreDualInSelf.append_inr_inl] at hk'
simp only [AreDualInSelf.append_inl_inr] at hj simp only [AreDualInSelf.append_inl_inr] at hj
refine ((l2.getDual?_append_symm_of_withUniqueDual_of_inr l _ _ ?_).mp (hk' hj).symm).symm refine ((l2.getDual?_append_symm_of_withUniqueDual_of_inr l _ _ ?_).mp (hk' hj).symm).symm
simp_all only [AreDualInSelf.append_inr_inl, imp_self, withUniqueDual, simp_all only [AreDualInSelf.append_inr_inl, imp_self, withUniqueDual,
mem_withDual_iff_isSome, Finset.mem_filter, Finset.mem_univ, getDual?_isSome_append_inr_iff, mem_withDual_iff_isSome, Finset.mem_filter, Finset.mem_univ, getDual?_isSome_append_inr_iff,
implies_true, and_self, mem_withUniqueDual_isSome, eq_getDual?_get_of_withUniqueDual_iff, implies_true, and_self, mem_withUniqueDual_isSome, eq_getDual?_get_of_withUniqueDual_iff,
getDual?_areDualInSelf_get] getDual?_areDualInSelf_get]
@[simp] @[simp]
lemma not_mem_withDualInOther_of_inl_mem_withUniqueDual (i : Fin l.length) lemma not_mem_withDualInOther_of_inl_mem_withUniqueDual (i : Fin l.length)
(h : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual) (hs : i ∈ l.withUniqueDual) : (h : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual) (hs : i ∈ l.withUniqueDual) :
¬ i ∈ l.withUniqueDualInOther l2 := by ¬ i ∈ l.withUniqueDualInOther l2 := by
have hn := l.append_inl_not_mem_withDual_of_withDualInOther l2 i h have hn := l.append_inl_not_mem_withDual_of_withDualInOther l2 i h
simp_all simp_all
by_contra ho by_contra ho
have ho' : (l.getDualInOther? l2 i).isSome := by have ho' : (l.getDualInOther? l2 i).isSome := by
exact mem_withUniqueDualInOther_isSome l l2 i ho exact mem_withUniqueDualInOther_isSome l l2 i ho
simp_all [Option.isSome_none, Bool.false_eq_true] simp_all [Option.isSome_none, Bool.false_eq_true]
@[simp] @[simp]
lemma not_mem_withUniqueDual_of_inl_mem_withUnqieuDual (i : Fin l.length) 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) : (h : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual) (hi : i ∈ l.withUniqueDualInOther l2) :
¬ i ∈ l.withUniqueDual := by ¬ i ∈ l.withUniqueDual := by
by_contra hs by_contra hs
simp_all only [not_mem_withDualInOther_of_inl_mem_withUniqueDual] simp_all only [not_mem_withDualInOther_of_inl_mem_withUniqueDual]
@ -457,7 +445,7 @@ lemma mem_withUniqueDual_of_inl (i : Fin l.length)
simp_all simp_all
@[simp] @[simp]
lemma mem_withUniqueDualInOther_of_inl_withDualInOther (i : Fin l.length) lemma mem_withUniqueDualInOther_of_inl_withDualInOther (i : Fin l.length)
(h : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual) (h : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual)
(hi : (l.getDualInOther? l2 i).isSome) : i ∈ l.withUniqueDualInOther l2 := by (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, simp only [withUniqueDualInOther, mem_withDual_iff_isSome, Bool.not_eq_true, Option.not_isSome,
@ -644,7 +632,7 @@ lemma append_withUniqueDual : (l ++ l2).withUniqueDual =
lemma append_withUniqueDual_disjSum : (l ++ l2).withUniqueDual = lemma append_withUniqueDual_disjSum : (l ++ l2).withUniqueDual =
Equiv.finsetCongr appendEquiv Equiv.finsetCongr appendEquiv
(((l.withUniqueDual ∩ (l.withDualInOther l2)ᶜ) ∪ l.withUniqueDualInOther l2).disjSum (((l.withUniqueDual ∩ (l.withDualInOther l2)ᶜ) ∪ l.withUniqueDualInOther l2).disjSum
((l2.withUniqueDual ∩ (l2.withDualInOther l)ᶜ) ∪ l2.withUniqueDualInOther l)) := by ((l2.withUniqueDual ∩ (l2.withDualInOther l)ᶜ) ∪ l2.withUniqueDualInOther l)) := by
rw [← Equiv.symm_apply_eq] rw [← Equiv.symm_apply_eq]
simp only [Equiv.finsetCongr_symm, append_withUniqueDual, Equiv.finsetCongr_apply] simp only [Equiv.finsetCongr_symm, append_withUniqueDual, Equiv.finsetCongr_apply]
rw [Finset.map_union] rw [Finset.map_union]
@ -660,8 +648,6 @@ lemma append_withUniqueDual_disjSum : (l ++ l2).withUniqueDual =
-/ -/
lemma mem_append_withUniqueDualInOther_symm (i : Fin l.length) : lemma mem_append_withUniqueDualInOther_symm (i : Fin l.length) :
appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDualInOther l3 ↔ appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDualInOther l3 ↔
appendEquiv (Sum.inr i) ∈ (l2 ++ l).withUniqueDualInOther l3 := by appendEquiv (Sum.inr i) ∈ (l2 ++ l).withUniqueDualInOther l3 := by
@ -729,24 +715,23 @@ lemma withUniqueDualInOther_append_isSome_fst_iff_not_isSome_snd (i : Fin l.leng
lemma getDualInOther?_append_symm_of_withUniqueDual_of_inl (i : Fin l.length) lemma getDualInOther?_append_symm_of_withUniqueDual_of_inl (i : Fin l.length)
(k : Fin l2.length) (h : i ∈ l.withUniqueDualInOther (l2 ++ l3)) : (k : Fin l2.length) (h : i ∈ l.withUniqueDualInOther (l2 ++ l3)) :
l.getDualInOther? (l2 ++ l3) i = some (appendEquiv (Sum.inl k)) l.getDualInOther? (l2 ++ l3) i = some (appendEquiv (Sum.inl k))
↔ l.getDualInOther? (l3 ++ l2) i = some (appendEquiv (Sum.inr k)) := by ↔ l.getDualInOther? (l3 ++ l2) i = some (appendEquiv (Sum.inr k)) := by
have h := l.withUniqueDualInOther_append_isSome_fst_iff_not_isSome_snd l2 l3 i h have h := l.withUniqueDualInOther_append_isSome_fst_iff_not_isSome_snd l2 l3 i h
by_cases hs : (l.getDualInOther? l2 i).isSome by_cases hs : (l.getDualInOther? l2 i).isSome
<;> by_cases ho : (l.getDualInOther? l3 i).isSome <;> by_cases ho : (l.getDualInOther? l3 i).isSome
<;> simp_all [hs] <;> simp_all [hs]
lemma getDualInOther?_append_symm_of_withUniqueDual_of_inr (i : Fin l.length) lemma getDualInOther?_append_symm_of_withUniqueDual_of_inr (i : Fin l.length)
(k : Fin l3.length) (h : i ∈ l.withUniqueDualInOther (l2 ++ l3)) : (k : Fin l3.length) (h : i ∈ l.withUniqueDualInOther (l2 ++ l3)) :
l.getDualInOther? (l2 ++ l3) i = some (appendEquiv (Sum.inr k)) l.getDualInOther? (l2 ++ l3) i = some (appendEquiv (Sum.inr k))
↔ l.getDualInOther? (l3 ++ l2) i = some (appendEquiv (Sum.inl k)) := by ↔ l.getDualInOther? (l3 ++ l2) i = some (appendEquiv (Sum.inl k)) := by
have h := l.withUniqueDualInOther_append_isSome_fst_iff_not_isSome_snd l2 l3 i h have h := l.withUniqueDualInOther_append_isSome_fst_iff_not_isSome_snd l2 l3 i h
by_cases hs : (l.getDualInOther? l2 i).isSome by_cases hs : (l.getDualInOther? l2 i).isSome
<;> by_cases ho : (l.getDualInOther? l3 i).isSome <;> by_cases ho : (l.getDualInOther? l3 i).isSome
<;> simp_all [hs] <;> simp_all [hs]
lemma mem_withUniqueDualInOther_symm' (i : Fin l.length) lemma mem_withUniqueDualInOther_symm' (i : Fin l.length)
(h : i ∈ l.withUniqueDualInOther (l2 ++ l3)): (h : i ∈ l.withUniqueDualInOther (l2 ++ l3)) :
i ∈ l.withUniqueDualInOther (l3 ++ l2) := by i ∈ l.withUniqueDualInOther (l3 ++ l2) := by
have h' := h have h' := h
simp only [withUniqueDualInOther, mem_withDual_iff_isSome, Bool.not_eq_true, simp only [withUniqueDualInOther, mem_withDual_iff_isSome, Bool.not_eq_true,
@ -759,7 +744,7 @@ lemma mem_withUniqueDualInOther_symm' (i : Fin l.length)
by_cases h1 : (l.getDualInOther? l2 i).isSome <;> by_cases h1 : (l.getDualInOther? l2 i).isSome <;>
by_cases h2 : (l.getDualInOther? l3 i).isSome by_cases h2 : (l.getDualInOther? l3 i).isSome
· simp only [h1, h2, not_true_eq_false, imp_false] at hc · simp only [h1, h2, not_true_eq_false, imp_false] at hc
rw [← @Option.not_isSome_iff_eq_none] at hc rw [← @Option.not_isSome_iff_eq_none] at hc
simp [h2] at hc simp [h2] at hc
· simp only [h1, or_true, true_and] · simp only [h1, or_true, true_and]
intro j intro j
@ -803,7 +788,6 @@ lemma mem_withUniqueDualInOther_symm (i : Fin l.length) :
i ∈ l.withUniqueDualInOther (l2 ++ l3) ↔ i ∈ l.withUniqueDualInOther (l3 ++ l2) := i ∈ l.withUniqueDualInOther (l2 ++ l3) ↔ i ∈ l.withUniqueDualInOther (l3 ++ l2) :=
Iff.intro (l.mem_withUniqueDualInOther_symm' l2 l3 i) (l.mem_withUniqueDualInOther_symm' l3 l2 i) Iff.intro (l.mem_withUniqueDualInOther_symm' l2 l3 i) (l.mem_withUniqueDualInOther_symm' l3 l2 i)
/-! /-!
## The equivalence defined by getDual? ## The equivalence defined by getDual?
@ -847,7 +831,6 @@ lemma getDualInOtherEquiv_self_refl : l.getDualInOtherEquiv l = Equiv.refl _ :=
intro x intro x
simp [getDualInOtherEquiv] simp [getDualInOtherEquiv]
end IndexList end IndexList
end IndexNotation end IndexNotation

6
HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean
View file

@ -85,11 +85,10 @@ noncomputable def fromIndexStringColor {cn : Fin n → realTensorColor.Color}
(hd : TensorColor.ColorMap.DualMap.boolFin (hd : TensorColor.ColorMap.DualMap.boolFin
(toIndexList' s hs).colorMap (cn ∘ Fin.cast hn.symm)) : (toIndexList' s hs).colorMap (cn ∘ Fin.cast hn.symm)) :
(realLorentzTensor d).TensorIndex := (realLorentzTensor d).TensorIndex :=
TensorStructure.TensorIndex.mkDualMap T ⟨(toIndexList' s hs), hD, TensorStructure.TensorIndex.mkDualMap T ⟨(toIndexList' s hs), hD,
IndexList.ColorCond.iff_bool.mpr hC⟩ hn IndexList.ColorCond.iff_bool.mpr hC⟩ hn
(TensorColor.ColorMap.DualMap.boolFin_DualMap hd) (TensorColor.ColorMap.DualMap.boolFin_DualMap hd)
/-- A tactic used to prove `boolFin` for real Lornetz tensors. -/ /-- A tactic used to prove `boolFin` for real Lornetz tensors. -/
macro "dualMapTactic" : tactic => macro "dualMapTactic" : tactic =>
`(tactic| { `(tactic| {
@ -114,10 +113,9 @@ macro "prodTactic" : tactic =>
/-- The product of Real Lorentz tensors. Conditions on indices are checked automatically. -/ /-- The product of Real Lorentz tensors. Conditions on indices are checked automatically. -/
notation:10 T "⊗ᵀ" S:11 => TensorIndex.prod T S (by prodTactic) notation:10 T "⊗ᵀ" S:11 => TensorIndex.prod T S (by prodTactic)
/-- An example showing the allowed constructions. -/ /-- An example showing the allowed constructions. -/
example (T : (realLorentzTensor d).Tensor ![ColorType.up, ColorType.down]) : True := by example (T : (realLorentzTensor d).Tensor ![ColorType.up, ColorType.down]) : True := by
let _ := T|"ᵤ₁ᵤ₂" ⊗ᵀ T|"ᵘ³ᵤ₄" ⊗ᵀ T|"ᵘ⁴ᵤ₃" let _ := T|"ᵤ₁ᵤ₂" ⊗ᵀ T|"ᵘ³ᵤ₄" ⊗ᵀ T|"ᵘ⁴ᵤ₃"
let _ := T|"ᵤ₁ᵤ₂" ⊗ᵀ T|"ᵘ³ᵤ₄" ⊗ᵀ T|"ᵘ¹ᵘ²" ⊗ᵀ T|"ᵘ⁴ᵤ₃" let _ := T|"ᵤ₁ᵤ₂" ⊗ᵀ T|"ᵘ³ᵤ₄" ⊗ᵀ T|"ᵘ¹ᵘ²" ⊗ᵀ T|"ᵘ⁴ᵤ₃"
exact trivial exact trivial