refactor: Index notation
This commit is contained in:
jstoobysmith
parent
097571453f
commit
cf0cbb78bb
8 changed files with 551 additions and 438 deletions
|
|
@ -12,16 +12,9 @@ import HepLean.SpaceTime.LorentzTensor.Contraction
|
|||
|
||||
# Index lists and color
|
||||
|
||||
In this file we look at the interaction of index lists with color.
|
||||
|
||||
The main definiton of this file is `ColorIndexList`. This type defines the
|
||||
permissible index lists which can be used for a tensor. These are lists of indices for which
|
||||
every index with a dual has a unique dual, and the color of that dual (when it exists) is dual
|
||||
to the color of the index.
|
||||
|
||||
We also define `AppendCond`, which is a condition on two `ColorIndexList`s which allows them to be
|
||||
appended to form a new `ColorIndexList`.
|
||||
In this file we look at the interaction of index lists and color.
|
||||
|
||||
The main definition of this file is `ColorCond`.
|
||||
-/
|
||||
|
||||
namespace IndexNotation
|
||||
|
|
@ -593,430 +586,4 @@ end ColorCond
|
|||
|
||||
end IndexList
|
||||
|
||||
variable (𝓒 : TensorColor)
|
||||
variable [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
|
||||
|
||||
/-- A list of indices with the additional constraint that if a index has a dual,
|
||||
that dual is unique, and the dual of an index has dual color to that index.
|
||||
|
||||
This is the permissible type of indices which can be used for a tensor. For example,
|
||||
the index list `['ᵘ¹', 'ᵤ₁']` can be extended to a `ColorIndexList` but the index list
|
||||
`['ᵘ¹', 'ᵤ₁', 'ᵤ₁']` cannot. -/
|
||||
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
|
||||
an identical `id`. -/
|
||||
unique_duals : toIndexList.withDual = toIndexList.withUniqueDual
|
||||
/-- The condition that for an index with a dual, that dual has dual color to the index. -/
|
||||
dual_color : IndexList.ColorCond toIndexList
|
||||
|
||||
namespace ColorIndexList
|
||||
|
||||
variable {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
|
||||
|
||||
variable (l l2 : ColorIndexList 𝓒)
|
||||
open IndexList TensorColor
|
||||
|
||||
instance : Coe (ColorIndexList 𝓒) (IndexList 𝓒.Color) := ⟨fun l => l.toIndexList⟩
|
||||
|
||||
/-- The colorMap of a `ColorIndexList` as a `𝓒.ColorMap`.
|
||||
This is to be compared with `colorMap` which is a map `Fin l.length → 𝓒.Color`. -/
|
||||
def colorMap' : 𝓒.ColorMap (Fin l.length) :=
|
||||
l.colorMap
|
||||
|
||||
@[ext]
|
||||
lemma ext {l l' : ColorIndexList 𝓒} (h : l.val = l'.val) : l = l' := by
|
||||
cases l
|
||||
cases l'
|
||||
simp_all
|
||||
apply IndexList.ext
|
||||
exact h
|
||||
|
||||
lemma ext' {l l' : ColorIndexList 𝓒} (h : l.toIndexList = l'.toIndexList) : l = l' := by
|
||||
cases l
|
||||
cases l'
|
||||
simp_all
|
||||
|
||||
/-! TODO: `orderEmbOfFin_univ` should be replaced with a mathlib lemma if possible. -/
|
||||
lemma orderEmbOfFin_univ (n m : ℕ) (h : n = m) :
|
||||
Finset.orderEmbOfFin (Finset.univ : Finset (Fin n)) (by simp [h]: Finset.univ.card = m) =
|
||||
(Fin.castOrderIso h.symm).toOrderEmbedding := by
|
||||
symm
|
||||
have h1 : (Fin.castOrderIso h.symm).toFun =
|
||||
(Finset.orderEmbOfFin (Finset.univ : Finset (Fin n))
|
||||
(by simp [h]: Finset.univ.card = m)).toFun := by
|
||||
apply Finset.orderEmbOfFin_unique
|
||||
intro x
|
||||
exact Finset.mem_univ ((Fin.castOrderIso (Eq.symm h)).toFun x)
|
||||
exact fun ⦃a b⦄ a => a
|
||||
exact Eq.symm (Fin.orderEmbedding_eq (congrArg Set.range (id (Eq.symm h1))))
|
||||
|
||||
/-!
|
||||
|
||||
## Cons for `ColorIndexList`
|
||||
|
||||
-/
|
||||
|
||||
/-- The `ColorIndexList` whose underlying list of indices is empty. -/
|
||||
def empty : ColorIndexList 𝓒 where
|
||||
val := []
|
||||
unique_duals := rfl
|
||||
dual_color := rfl
|
||||
|
||||
/-- The `ColorIndexList` obtained by adding an index, subject to some conditions,
|
||||
to the start of `l`. -/
|
||||
def cons (I : Index 𝓒.Color) (hI1 : l.val.countP (fun J => I.id = J.id) ≤ 1)
|
||||
(hI2 : l.val.countP (fun J => I.id = J.id) =
|
||||
l.val.countP (fun J => I.id = J.id ∧ I.toColor = 𝓒.τ J.toColor)) : ColorIndexList 𝓒 where
|
||||
toIndexList := l.toIndexList.cons I
|
||||
unique_duals := by
|
||||
symm
|
||||
rw [withUniqueDual_eq_withDual_cons_iff]
|
||||
· exact hI1
|
||||
· exact l.unique_duals.symm
|
||||
dual_color := by
|
||||
have h1 : (l.toIndexList.cons I).withUniqueDual = (l.toIndexList.cons I).withDual ∧
|
||||
(l.toIndexList.cons I).ColorCond := by
|
||||
rw [ColorCond.cons_iff]
|
||||
exact ⟨l.unique_duals.symm, l.dual_color, hI1, hI2⟩
|
||||
exact h1.2
|
||||
|
||||
/-- The tail of a `ColorIndexList`. In other words, the `ColorIndexList` with the first index
|
||||
removed. -/
|
||||
def tail (l : ColorIndexList 𝓒) : ColorIndexList 𝓒 where
|
||||
toIndexList := l.toIndexList.tail
|
||||
unique_duals := by
|
||||
by_cases hl : l.toIndexList = {val := []}
|
||||
· rw [hl]
|
||||
simp [IndexList.tail]
|
||||
rfl
|
||||
· have hl' := l.head_cons_tail hl
|
||||
have h1 := l.unique_duals
|
||||
rw [hl'] at h1
|
||||
exact (withUniqueDual_eq_withDual_of_cons _ h1.symm).symm
|
||||
dual_color := by
|
||||
by_cases hl : l.toIndexList = {val := []}
|
||||
· rw [hl]
|
||||
simp [IndexList.tail]
|
||||
rfl
|
||||
· have hl' := l.head_cons_tail hl
|
||||
have h1 := l.unique_duals
|
||||
have h2 := l.dual_color
|
||||
rw [hl'] at h1 h2
|
||||
exact (ColorCond.of_cons _ h2 h1.symm)
|
||||
|
||||
@[simp]
|
||||
lemma tail_toIndexList : l.tail.toIndexList = l.toIndexList.tail := by
|
||||
rfl
|
||||
|
||||
/-- The first index in a `ColorIndexList`. -/
|
||||
def head (h : l ≠ empty) : Index 𝓒.Color :=
|
||||
l.toIndexList.head (by
|
||||
cases' l
|
||||
simpa [empty] using h)
|
||||
|
||||
lemma head_uniqueDual (h : l ≠ empty) :
|
||||
l.tail.val.countP (fun J => (l.head h).id = J.id) ≤ 1 := by
|
||||
have h1 := l.unique_duals.symm
|
||||
have hl : l.toIndexList = (l.tail.toIndexList.cons (l.head h)) := by
|
||||
simpa using l.head_cons_tail _
|
||||
rw [hl] at h1
|
||||
rw [withUniqueDual_eq_withDual_cons_iff'] at h1
|
||||
exact h1.2
|
||||
|
||||
lemma head_color_dual (h : l ≠ empty) :
|
||||
l.tail.val.countP (fun J => (l.head h).id = J.id) =
|
||||
l.tail.val.countP (fun J => (l.head h).id = J.id ∧ (l.head h).toColor = 𝓒.τ J.toColor) := by
|
||||
have h1 : l.withUniqueDual = l.withDual ∧ ColorCond l := ⟨l.unique_duals.symm, l.dual_color⟩
|
||||
have hl : l.toIndexList = (l.tail.toIndexList.cons (l.head h)) := by
|
||||
simpa using l.head_cons_tail _
|
||||
rw [hl, ColorCond.cons_iff] at h1
|
||||
exact h1.2.2.2
|
||||
|
||||
lemma head_cons_tail (h : l ≠ empty) :
|
||||
l = (l.tail).cons (l.head h) (l.head_uniqueDual h) (l.head_color_dual h) := by
|
||||
apply ext'
|
||||
exact IndexList.head_cons_tail _ _
|
||||
|
||||
/-!
|
||||
|
||||
## Induction for `ColorIndexList`
|
||||
|
||||
-/
|
||||
|
||||
lemma induction {P : ColorIndexList 𝓒 → Prop } (h_nil : P empty)
|
||||
(h_cons : ∀ (I : Index 𝓒.Color) (l : ColorIndexList 𝓒)
|
||||
(hI1 : l.val.countP (fun J => I.id = J.id) ≤ 1) (hI2 : l.val.countP (fun J => I.id = J.id) =
|
||||
l.val.countP (fun J => I.id = J.id ∧ I.toColor = 𝓒.τ J.toColor)), P l → P (l.cons I hI1 hI2))
|
||||
(l : ColorIndexList 𝓒) : P l := by
|
||||
by_cases h : l = empty
|
||||
· subst l
|
||||
exact h_nil
|
||||
· rw [l.head_cons_tail h]
|
||||
refine h_cons (l.head h) (l.tail) (l.head_uniqueDual h) (l.head_color_dual h) ?_
|
||||
exact induction h_nil h_cons l.tail
|
||||
termination_by l.length
|
||||
decreasing_by {
|
||||
by_cases hn : l = empty
|
||||
· subst hn
|
||||
simp
|
||||
exact False.elim (h rfl)
|
||||
· have h1 : l.tail.length < l.length := by
|
||||
simp [IndexList.tail, length]
|
||||
by_contra hn'
|
||||
simp at hn'
|
||||
have hv : l = empty := ext hn'
|
||||
exact False.elim (hn hv)
|
||||
exact h1
|
||||
}
|
||||
/-!
|
||||
|
||||
## Contracting an `ColorIndexList`
|
||||
|
||||
-/
|
||||
|
||||
/-- The contraction of a `ColorIndexList`, `l`.
|
||||
That is, the `ColorIndexList` obtained by taking only those indices in `l` which do not
|
||||
have a dual. This can be thought of as contracting all of those indices with a dual. -/
|
||||
def contr : ColorIndexList 𝓒 where
|
||||
toIndexList := l.toIndexList.contrIndexList
|
||||
unique_duals := by
|
||||
simp
|
||||
dual_color := by
|
||||
funext i
|
||||
simp [Option.guard]
|
||||
|
||||
@[simp]
|
||||
lemma contr_contr : l.contr.contr = l.contr := by
|
||||
apply ext
|
||||
simp [contr]
|
||||
|
||||
@[simp]
|
||||
lemma contr_contr_idMap (i : Fin l.contr.contr.length) :
|
||||
l.contr.contr.idMap i = l.contr.idMap (Fin.cast (by simp) i) := by
|
||||
simp only [contr, contrIndexList_idMap, Fin.cast_trans]
|
||||
apply congrArg
|
||||
simp only [withoutDualEquiv, RelIso.coe_fn_toEquiv, Finset.coe_orderIsoOfFin_apply,
|
||||
EmbeddingLike.apply_eq_iff_eq]
|
||||
have h1 : l.contrIndexList.withoutDual = Finset.univ := by
|
||||
have hx := l.contrIndexList.withDual_union_withoutDual
|
||||
have hx2 := l.contrIndexList_withDual
|
||||
simp_all
|
||||
simp only [h1]
|
||||
rw [orderEmbOfFin_univ]
|
||||
· rfl
|
||||
· rw [h1]
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
lemma contr_contr_colorMap (i : Fin l.contr.contr.length) :
|
||||
l.contr.contr.colorMap i = l.contr.colorMap (Fin.cast (by simp) i) := by
|
||||
simp only [contr, contrIndexList_colorMap, Fin.cast_trans]
|
||||
apply congrArg
|
||||
simp only [withoutDualEquiv, RelIso.coe_fn_toEquiv, Finset.coe_orderIsoOfFin_apply,
|
||||
EmbeddingLike.apply_eq_iff_eq]
|
||||
have h1 : l.contrIndexList.withoutDual = Finset.univ := by
|
||||
have hx := l.contrIndexList.withDual_union_withoutDual
|
||||
have hx2 := l.contrIndexList_withDual
|
||||
simp_all
|
||||
simp only [h1]
|
||||
rw [orderEmbOfFin_univ]
|
||||
· rfl
|
||||
· rw [h1]
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
lemma contr_of_withDual_empty (h : l.withDual = ∅) :
|
||||
l.contr = l := by
|
||||
simp [contr]
|
||||
apply ext
|
||||
simp [l.contrIndexList_of_withDual_empty h]
|
||||
|
||||
@[simp]
|
||||
lemma contr_getDual?_eq_none (i : Fin l.contr.length) :
|
||||
l.contr.getDual? i = none := by
|
||||
simp only [contr, contrIndexList_getDual?]
|
||||
|
||||
@[simp]
|
||||
lemma contr_areDualInSelf (i j : Fin l.contr.length) :
|
||||
l.contr.AreDualInSelf i j ↔ False := by
|
||||
simp [contr]
|
||||
|
||||
/-!
|
||||
|
||||
## Contract equiv
|
||||
|
||||
-/
|
||||
|
||||
/-- 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`),
|
||||
and those indices without duals.
|
||||
|
||||
This equivalence is used to contract the indices of tensors. -/
|
||||
def contrEquiv : (l.withUniqueDualLT ⊕ l.withUniqueDualLT) ⊕ Fin l.contr.length ≃ Fin l.length :=
|
||||
(Equiv.sumCongr (l.withUniqueLTGTEquiv) (Equiv.refl _)).trans <|
|
||||
(Equiv.sumCongr (Equiv.subtypeEquivRight (by
|
||||
simp only [l.unique_duals, implies_true]))
|
||||
(Fin.castOrderIso l.contrIndexList_length).toEquiv).trans <|
|
||||
l.dualEquiv
|
||||
|
||||
lemma contrEquiv_inl_inl_isSome (i : l.withUniqueDualLT) :
|
||||
(l.getDual? (l.contrEquiv (Sum.inl (Sum.inl i)))).isSome := by
|
||||
change (l.getDual? i).isSome
|
||||
have h1 : i.1 ∈ l.withUniqueDual := by
|
||||
have hi2 := i.2
|
||||
simp only [withUniqueDualLT, Finset.mem_filter] at hi2
|
||||
exact hi2.1
|
||||
exact mem_withUniqueDual_isSome l.toIndexList (↑i) h1
|
||||
|
||||
@[simp]
|
||||
lemma contrEquiv_inl_inr_eq (i : l.withUniqueDualLT) :
|
||||
(l.contrEquiv (Sum.inl (Sum.inr i))) =
|
||||
(l.getDual? i.1).get (l.contrEquiv_inl_inl_isSome i) := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma contrEquiv_inl_inl_eq (i : l.withUniqueDualLT) :
|
||||
(l.contrEquiv (Sum.inl (Sum.inl i))) = i := by
|
||||
rfl
|
||||
|
||||
lemma contrEquiv_colorMapIso :
|
||||
ColorMap.MapIso (Equiv.refl (Fin l.contr.length))
|
||||
(ColorMap.contr l.contrEquiv l.colorMap) l.contr.colorMap := by
|
||||
simp [ColorMap.MapIso, ColorMap.contr]
|
||||
funext i
|
||||
simp [contr]
|
||||
rfl
|
||||
|
||||
lemma contrEquiv_contrCond : ColorMap.ContrCond l.contrEquiv l.colorMap := by
|
||||
simp only [ColorMap.ContrCond]
|
||||
funext i
|
||||
simp only [Function.comp_apply, contrEquiv_inl_inl_eq, contrEquiv_inl_inr_eq]
|
||||
have h1 := l.dual_color
|
||||
rw [ColorCond.iff_on_isSome] at h1
|
||||
exact (h1 i.1 _).symm
|
||||
|
||||
@[simp]
|
||||
lemma contrEquiv_on_withDual_empty (i : Fin l.contr.length) (h : l.withDual = ∅) :
|
||||
l.contrEquiv (Sum.inr i) = Fin.cast (by simp [h]) i := by
|
||||
simp [contrEquiv]
|
||||
change l.dualEquiv (Sum.inr ((Fin.castOrderIso _).toEquiv i)) = _
|
||||
simp [dualEquiv, withoutDualEquiv]
|
||||
have h : l.withoutDual = Finset.univ := by
|
||||
have hx := l.withDual_union_withoutDual
|
||||
simp_all
|
||||
simp [h]
|
||||
rw [orderEmbOfFin_univ]
|
||||
· rfl
|
||||
· rw [h]
|
||||
simp
|
||||
|
||||
/-!
|
||||
|
||||
## Append
|
||||
|
||||
-/
|
||||
|
||||
/-- The condition on the `ColorIndexList`s `l` and `l2` so that on appending they form
|
||||
a `ColorIndexList`.
|
||||
|
||||
Note: `AppendCond` does not form an equivalence relation as it is not reflexive or
|
||||
transitive. -/
|
||||
def AppendCond : Prop :=
|
||||
(l.toIndexList ++ l2.toIndexList).withUniqueDual = (l.toIndexList ++ l2.toIndexList).withDual
|
||||
∧ ColorCond (l.toIndexList ++ l2.toIndexList)
|
||||
|
||||
/-- Given two `ColorIndexList`s satisfying `AppendCond`. The correponding combined
|
||||
`ColorIndexList`. -/
|
||||
def append (h : AppendCond l l2) : ColorIndexList 𝓒 where
|
||||
toIndexList := l.toIndexList ++ l2.toIndexList
|
||||
unique_duals := h.1.symm
|
||||
dual_color := h.2
|
||||
|
||||
/-- The join of two `ColorIndexList` satisfying the condition `AppendCond` that they
|
||||
can be appended to form a `ColorIndexList`. -/
|
||||
scoped[IndexNotation.ColorIndexList] notation l " ++["h"] " l2 => append l l2 h
|
||||
|
||||
@[simp]
|
||||
lemma append_toIndexList (h : AppendCond l l2) :
|
||||
(l ++[h] l2).toIndexList = l.toIndexList ++ l2.toIndexList := by
|
||||
rfl
|
||||
|
||||
namespace AppendCond
|
||||
|
||||
variable {l l2 l3 : ColorIndexList 𝓒}
|
||||
|
||||
@[symm]
|
||||
lemma symm (h : AppendCond l l2) : AppendCond l2 l := by
|
||||
apply And.intro _ (h.2.symm h.1)
|
||||
rw [append_withDual_eq_withUniqueDual_symm]
|
||||
exact h.1
|
||||
|
||||
lemma inr (h : AppendCond l l2) (h' : AppendCond (l ++[h] l2) l3) :
|
||||
AppendCond l2 l3 := by
|
||||
apply And.intro
|
||||
· have h1 := h'.1
|
||||
simp at h1
|
||||
rw [append_assoc] at h1
|
||||
exact l.append_withDual_eq_withUniqueDual_inr (l2.toIndexList ++ l3.toIndexList) h1
|
||||
· have h1 := h'.2
|
||||
simp at h1
|
||||
rw [append_assoc] at h1
|
||||
refine ColorCond.inr ?_ h1
|
||||
rw [← append_assoc]
|
||||
exact h'.1
|
||||
|
||||
lemma assoc (h : AppendCond l l2) (h' : AppendCond (l ++[h] l2) l3) :
|
||||
AppendCond l (l2 ++[h.inr h'] l3) := by
|
||||
apply And.intro
|
||||
· simp
|
||||
rw [← append_assoc]
|
||||
simpa using h'.1
|
||||
· simp
|
||||
rw [← append_assoc]
|
||||
exact h'.2
|
||||
|
||||
lemma swap (h : AppendCond l l2) (h' : AppendCond (l ++[h] l2) l3) :
|
||||
AppendCond (l2 ++[h.symm] l) l3:= by
|
||||
apply And.intro
|
||||
· simp only [append_toIndexList]
|
||||
rw [← append_withDual_eq_withUniqueDual_swap]
|
||||
simpa using h'.1
|
||||
· exact ColorCond.swap h'.1 h'.2
|
||||
|
||||
/-! TODO: Show that `AppendCond l l2` implies `AppendCond l.contr l2.contr`. -/
|
||||
/-! TODO: Show that `(l1.contr ++[h.contr] l2.contr).contr = (l1 ++[h] l2)` -/
|
||||
|
||||
lemma of_eq (h1 : l.withUniqueDual = l.withDual)
|
||||
(h2 : l2.withUniqueDual = l2.withDual)
|
||||
(h3 : l.withUniqueDualInOther l2 = l.withDualInOther l2)
|
||||
(h4 : l2.withUniqueDualInOther l = l2.withDualInOther l)
|
||||
(h5 : ColorCond.bool (l.toIndexList ++ l2.toIndexList)) :
|
||||
AppendCond l l2 := by
|
||||
rw [AppendCond]
|
||||
rw [append_withDual_eq_withUniqueDual_iff']
|
||||
simp_all
|
||||
exact ColorCond.iff_bool.mpr h5
|
||||
|
||||
/-- A boolean which is true for two index lists `l` and `l2` if on appending
|
||||
they can form a `ColorIndexList`. -/
|
||||
def bool (l l2 : IndexList 𝓒.Color) : Bool :=
|
||||
if ¬ (l ++ l2).withUniqueDual = (l ++ l2).withDual then
|
||||
false
|
||||
else
|
||||
ColorCond.bool (l ++ l2)
|
||||
|
||||
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]
|
||||
simp
|
||||
|
||||
end AppendCond
|
||||
|
||||
end ColorIndexList
|
||||
|
||||
end IndexNotation
|
||||
|
|
|
|||
|
|
@ -0,0 +1,133 @@
|
|||
/-
|
||||
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.ColorIndexList.Basic
|
||||
import HepLean.SpaceTime.LorentzTensor.Basic
|
||||
import Init.Data.List.Lemmas
|
||||
/-!
|
||||
|
||||
# Appending two ColorIndexLists
|
||||
|
||||
We define the contraction of ColorIndexLists.
|
||||
|
||||
-/
|
||||
|
||||
namespace IndexNotation
|
||||
namespace ColorIndexList
|
||||
|
||||
variable {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
|
||||
(l l2 : ColorIndexList 𝓒)
|
||||
|
||||
open IndexList TensorColor
|
||||
|
||||
/-!
|
||||
|
||||
## Append
|
||||
|
||||
-/
|
||||
|
||||
/-- The condition on the `ColorIndexList`s `l` and `l2` so that on appending they form
|
||||
a `ColorIndexList`.
|
||||
|
||||
Note: `AppendCond` does not form an equivalence relation as it is not reflexive or
|
||||
transitive. -/
|
||||
def AppendCond : Prop :=
|
||||
(l.toIndexList ++ l2.toIndexList).withUniqueDual = (l.toIndexList ++ l2.toIndexList).withDual
|
||||
∧ ColorCond (l.toIndexList ++ l2.toIndexList)
|
||||
|
||||
/-- Given two `ColorIndexList`s satisfying `AppendCond`. The correponding combined
|
||||
`ColorIndexList`. -/
|
||||
def append (h : AppendCond l l2) : ColorIndexList 𝓒 where
|
||||
toIndexList := l.toIndexList ++ l2.toIndexList
|
||||
unique_duals := h.1.symm
|
||||
dual_color := h.2
|
||||
|
||||
/-- The join of two `ColorIndexList` satisfying the condition `AppendCond` that they
|
||||
can be appended to form a `ColorIndexList`. -/
|
||||
scoped[IndexNotation.ColorIndexList] notation l " ++["h"] " l2 => append l l2 h
|
||||
|
||||
@[simp]
|
||||
lemma append_toIndexList (h : AppendCond l l2) :
|
||||
(l ++[h] l2).toIndexList = l.toIndexList ++ l2.toIndexList := by
|
||||
rfl
|
||||
|
||||
namespace AppendCond
|
||||
|
||||
variable {l l2 l3 : ColorIndexList 𝓒}
|
||||
|
||||
@[symm]
|
||||
lemma symm (h : AppendCond l l2) : AppendCond l2 l := by
|
||||
apply And.intro _ (h.2.symm h.1)
|
||||
rw [append_withDual_eq_withUniqueDual_symm]
|
||||
exact h.1
|
||||
|
||||
lemma inr (h : AppendCond l l2) (h' : AppendCond (l ++[h] l2) l3) :
|
||||
AppendCond l2 l3 := by
|
||||
apply And.intro
|
||||
· have h1 := h'.1
|
||||
simp at h1
|
||||
rw [append_assoc] at h1
|
||||
exact l.append_withDual_eq_withUniqueDual_inr (l2.toIndexList ++ l3.toIndexList) h1
|
||||
· have h1 := h'.2
|
||||
simp at h1
|
||||
rw [append_assoc] at h1
|
||||
refine ColorCond.inr ?_ h1
|
||||
rw [← append_assoc]
|
||||
exact h'.1
|
||||
|
||||
lemma assoc (h : AppendCond l l2) (h' : AppendCond (l ++[h] l2) l3) :
|
||||
AppendCond l (l2 ++[h.inr h'] l3) := by
|
||||
apply And.intro
|
||||
· simp
|
||||
rw [← append_assoc]
|
||||
simpa using h'.1
|
||||
· simp
|
||||
rw [← append_assoc]
|
||||
exact h'.2
|
||||
|
||||
lemma swap (h : AppendCond l l2) (h' : AppendCond (l ++[h] l2) l3) :
|
||||
AppendCond (l2 ++[h.symm] l) l3:= by
|
||||
apply And.intro
|
||||
· simp only [append_toIndexList]
|
||||
rw [← append_withDual_eq_withUniqueDual_swap]
|
||||
simpa using h'.1
|
||||
· exact ColorCond.swap h'.1 h'.2
|
||||
|
||||
/-! TODO: Show that `AppendCond l l2` implies `AppendCond l.contr l2.contr`. -/
|
||||
/-! TODO: Show that `(l1.contr ++[h.contr] l2.contr).contr = (l1 ++[h] l2)` -/
|
||||
|
||||
lemma of_eq (h1 : l.withUniqueDual = l.withDual)
|
||||
(h2 : l2.withUniqueDual = l2.withDual)
|
||||
(h3 : l.withUniqueDualInOther l2 = l.withDualInOther l2)
|
||||
(h4 : l2.withUniqueDualInOther l = l2.withDualInOther l)
|
||||
(h5 : ColorCond.bool (l.toIndexList ++ l2.toIndexList)) :
|
||||
AppendCond l l2 := by
|
||||
rw [AppendCond]
|
||||
rw [append_withDual_eq_withUniqueDual_iff']
|
||||
simp_all
|
||||
exact ColorCond.iff_bool.mpr h5
|
||||
|
||||
/-- A boolean which is true for two index lists `l` and `l2` if on appending
|
||||
they can form a `ColorIndexList`. -/
|
||||
def bool (l l2 : IndexList 𝓒.Color) : Bool :=
|
||||
if ¬ (l ++ l2).withUniqueDual = (l ++ l2).withDual then
|
||||
false
|
||||
else
|
||||
ColorCond.bool (l ++ l2)
|
||||
|
||||
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]
|
||||
simp
|
||||
|
||||
end AppendCond
|
||||
|
||||
end ColorIndexList
|
||||
end IndexNotation
|
||||
|
|
@ -0,0 +1,204 @@
|
|||
/-
|
||||
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.Color
|
||||
import HepLean.SpaceTime.LorentzTensor.IndexNotation.OnlyUniqueDuals
|
||||
import HepLean.SpaceTime.LorentzTensor.Basic
|
||||
import Init.Data.List.Lemmas
|
||||
import HepLean.SpaceTime.LorentzTensor.Contraction
|
||||
/-!
|
||||
|
||||
# Index lists and color
|
||||
|
||||
The main definiton of this file is `ColorIndexList`. This type defines the
|
||||
permissible index lists which can be used for a tensor. These are lists of indices for which
|
||||
every index with a dual has a unique dual, and the color of that dual (when it exists) is dual
|
||||
to the color of the index.
|
||||
|
||||
We also define `AppendCond`, which is a condition on two `ColorIndexList`s which allows them to be
|
||||
appended to form a new `ColorIndexList`.
|
||||
|
||||
-/
|
||||
|
||||
namespace IndexNotation
|
||||
|
||||
variable (𝓒 : TensorColor)
|
||||
variable [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
|
||||
|
||||
/-- A list of indices with the additional constraint that if a index has a dual,
|
||||
that dual is unique, and the dual of an index has dual color to that index.
|
||||
|
||||
This is the permissible type of indices which can be used for a tensor. For example,
|
||||
the index list `['ᵘ¹', 'ᵤ₁']` can be extended to a `ColorIndexList` but the index list
|
||||
`['ᵘ¹', 'ᵤ₁', 'ᵤ₁']` cannot. -/
|
||||
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
|
||||
an identical `id`. -/
|
||||
unique_duals : toIndexList.withDual = toIndexList.withUniqueDual
|
||||
/-- The condition that for an index with a dual, that dual has dual color to the index. -/
|
||||
dual_color : IndexList.ColorCond toIndexList
|
||||
|
||||
namespace ColorIndexList
|
||||
|
||||
variable {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
|
||||
|
||||
variable (l l2 : ColorIndexList 𝓒)
|
||||
open IndexList TensorColor
|
||||
|
||||
instance : Coe (ColorIndexList 𝓒) (IndexList 𝓒.Color) := ⟨fun l => l.toIndexList⟩
|
||||
|
||||
/-- The colorMap of a `ColorIndexList` as a `𝓒.ColorMap`.
|
||||
This is to be compared with `colorMap` which is a map `Fin l.length → 𝓒.Color`. -/
|
||||
def colorMap' : 𝓒.ColorMap (Fin l.length) :=
|
||||
l.colorMap
|
||||
|
||||
@[ext]
|
||||
lemma ext {l l' : ColorIndexList 𝓒} (h : l.val = l'.val) : l = l' := by
|
||||
cases l
|
||||
cases l'
|
||||
simp_all
|
||||
apply IndexList.ext
|
||||
exact h
|
||||
|
||||
lemma ext' {l l' : ColorIndexList 𝓒} (h : l.toIndexList = l'.toIndexList) : l = l' := by
|
||||
cases l
|
||||
cases l'
|
||||
simp_all
|
||||
|
||||
/-! TODO: `orderEmbOfFin_univ` should be replaced with a mathlib lemma if possible. -/
|
||||
lemma orderEmbOfFin_univ (n m : ℕ) (h : n = m) :
|
||||
Finset.orderEmbOfFin (Finset.univ : Finset (Fin n)) (by simp [h]: Finset.univ.card = m) =
|
||||
(Fin.castOrderIso h.symm).toOrderEmbedding := by
|
||||
symm
|
||||
have h1 : (Fin.castOrderIso h.symm).toFun =
|
||||
(Finset.orderEmbOfFin (Finset.univ : Finset (Fin n))
|
||||
(by simp [h]: Finset.univ.card = m)).toFun := by
|
||||
apply Finset.orderEmbOfFin_unique
|
||||
intro x
|
||||
exact Finset.mem_univ ((Fin.castOrderIso (Eq.symm h)).toFun x)
|
||||
exact fun ⦃a b⦄ a => a
|
||||
exact Eq.symm (Fin.orderEmbedding_eq (congrArg Set.range (id (Eq.symm h1))))
|
||||
|
||||
/-!
|
||||
|
||||
## Cons for `ColorIndexList`
|
||||
|
||||
-/
|
||||
|
||||
/-- The `ColorIndexList` whose underlying list of indices is empty. -/
|
||||
def empty : ColorIndexList 𝓒 where
|
||||
val := []
|
||||
unique_duals := rfl
|
||||
dual_color := rfl
|
||||
|
||||
/-- The `ColorIndexList` obtained by adding an index, subject to some conditions,
|
||||
to the start of `l`. -/
|
||||
def cons (I : Index 𝓒.Color) (hI1 : l.val.countP (fun J => I.id = J.id) ≤ 1)
|
||||
(hI2 : l.val.countP (fun J => I.id = J.id) =
|
||||
l.val.countP (fun J => I.id = J.id ∧ I.toColor = 𝓒.τ J.toColor)) : ColorIndexList 𝓒 where
|
||||
toIndexList := l.toIndexList.cons I
|
||||
unique_duals := by
|
||||
symm
|
||||
rw [withUniqueDual_eq_withDual_cons_iff]
|
||||
· exact hI1
|
||||
· exact l.unique_duals.symm
|
||||
dual_color := by
|
||||
have h1 : (l.toIndexList.cons I).withUniqueDual = (l.toIndexList.cons I).withDual ∧
|
||||
(l.toIndexList.cons I).ColorCond := by
|
||||
rw [ColorCond.cons_iff]
|
||||
exact ⟨l.unique_duals.symm, l.dual_color, hI1, hI2⟩
|
||||
exact h1.2
|
||||
|
||||
/-- The tail of a `ColorIndexList`. In other words, the `ColorIndexList` with the first index
|
||||
removed. -/
|
||||
def tail (l : ColorIndexList 𝓒) : ColorIndexList 𝓒 where
|
||||
toIndexList := l.toIndexList.tail
|
||||
unique_duals := by
|
||||
by_cases hl : l.toIndexList = {val := []}
|
||||
· rw [hl]
|
||||
simp [IndexList.tail]
|
||||
rfl
|
||||
· have hl' := l.head_cons_tail hl
|
||||
have h1 := l.unique_duals
|
||||
rw [hl'] at h1
|
||||
exact (withUniqueDual_eq_withDual_of_cons _ h1.symm).symm
|
||||
dual_color := by
|
||||
by_cases hl : l.toIndexList = {val := []}
|
||||
· rw [hl]
|
||||
simp [IndexList.tail]
|
||||
rfl
|
||||
· have hl' := l.head_cons_tail hl
|
||||
have h1 := l.unique_duals
|
||||
have h2 := l.dual_color
|
||||
rw [hl'] at h1 h2
|
||||
exact (ColorCond.of_cons _ h2 h1.symm)
|
||||
|
||||
@[simp]
|
||||
lemma tail_toIndexList : l.tail.toIndexList = l.toIndexList.tail := by
|
||||
rfl
|
||||
|
||||
/-- The first index in a `ColorIndexList`. -/
|
||||
def head (h : l ≠ empty) : Index 𝓒.Color :=
|
||||
l.toIndexList.head (by
|
||||
cases' l
|
||||
simpa [empty] using h)
|
||||
|
||||
lemma head_uniqueDual (h : l ≠ empty) :
|
||||
l.tail.val.countP (fun J => (l.head h).id = J.id) ≤ 1 := by
|
||||
have h1 := l.unique_duals.symm
|
||||
have hl : l.toIndexList = (l.tail.toIndexList.cons (l.head h)) := by
|
||||
simpa using l.head_cons_tail _
|
||||
rw [hl] at h1
|
||||
rw [withUniqueDual_eq_withDual_cons_iff'] at h1
|
||||
exact h1.2
|
||||
|
||||
lemma head_color_dual (h : l ≠ empty) :
|
||||
l.tail.val.countP (fun J => (l.head h).id = J.id) =
|
||||
l.tail.val.countP (fun J => (l.head h).id = J.id ∧ (l.head h).toColor = 𝓒.τ J.toColor) := by
|
||||
have h1 : l.withUniqueDual = l.withDual ∧ ColorCond l := ⟨l.unique_duals.symm, l.dual_color⟩
|
||||
have hl : l.toIndexList = (l.tail.toIndexList.cons (l.head h)) := by
|
||||
simpa using l.head_cons_tail _
|
||||
rw [hl, ColorCond.cons_iff] at h1
|
||||
exact h1.2.2.2
|
||||
|
||||
lemma head_cons_tail (h : l ≠ empty) :
|
||||
l = (l.tail).cons (l.head h) (l.head_uniqueDual h) (l.head_color_dual h) := by
|
||||
apply ext'
|
||||
exact IndexList.head_cons_tail _ _
|
||||
|
||||
/-!
|
||||
|
||||
## Induction for `ColorIndexList`
|
||||
|
||||
-/
|
||||
|
||||
lemma induction {P : ColorIndexList 𝓒 → Prop } (h_nil : P empty)
|
||||
(h_cons : ∀ (I : Index 𝓒.Color) (l : ColorIndexList 𝓒)
|
||||
(hI1 : l.val.countP (fun J => I.id = J.id) ≤ 1) (hI2 : l.val.countP (fun J => I.id = J.id) =
|
||||
l.val.countP (fun J => I.id = J.id ∧ I.toColor = 𝓒.τ J.toColor)), P l → P (l.cons I hI1 hI2))
|
||||
(l : ColorIndexList 𝓒) : P l := by
|
||||
by_cases h : l = empty
|
||||
· subst l
|
||||
exact h_nil
|
||||
· rw [l.head_cons_tail h]
|
||||
refine h_cons (l.head h) (l.tail) (l.head_uniqueDual h) (l.head_color_dual h) ?_
|
||||
exact induction h_nil h_cons l.tail
|
||||
termination_by l.length
|
||||
decreasing_by {
|
||||
by_cases hn : l = empty
|
||||
· subst hn
|
||||
simp
|
||||
exact False.elim (h rfl)
|
||||
· have h1 : l.tail.length < l.length := by
|
||||
simp [IndexList.tail, length]
|
||||
by_contra hn'
|
||||
simp at hn'
|
||||
have hv : l = empty := ext hn'
|
||||
exact False.elim (hn hv)
|
||||
exact h1
|
||||
}
|
||||
|
||||
end ColorIndexList
|
||||
end IndexNotation
|
||||
|
|
@ -0,0 +1,199 @@
|
|||
/-
|
||||
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.ColorIndexList.Basic
|
||||
import HepLean.SpaceTime.LorentzTensor.Basic
|
||||
import Init.Data.List.Lemmas
|
||||
/-!
|
||||
|
||||
# Contraction of ColorIndexLists
|
||||
|
||||
We define the contraction of ColorIndexLists.
|
||||
|
||||
-/
|
||||
|
||||
namespace IndexNotation
|
||||
namespace ColorIndexList
|
||||
|
||||
variable {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
|
||||
(l l2 : ColorIndexList 𝓒)
|
||||
|
||||
open IndexList TensorColor
|
||||
|
||||
/-!
|
||||
|
||||
## Contracting an `ColorIndexList`
|
||||
|
||||
-/
|
||||
|
||||
/-- The contraction of a `ColorIndexList`, `l`.
|
||||
That is, the `ColorIndexList` obtained by taking only those indices in `l` which do not
|
||||
have a dual. This can be thought of as contracting all of those indices with a dual. -/
|
||||
def contr : ColorIndexList 𝓒 where
|
||||
toIndexList := l.toIndexList.contrIndexList
|
||||
unique_duals := by
|
||||
simp
|
||||
dual_color := by
|
||||
funext i
|
||||
simp [Option.guard]
|
||||
|
||||
@[simp]
|
||||
lemma contr_contr : l.contr.contr = l.contr := by
|
||||
apply ext
|
||||
simp [contr]
|
||||
|
||||
@[simp]
|
||||
lemma contr_contr_idMap (i : Fin l.contr.contr.length) :
|
||||
l.contr.contr.idMap i = l.contr.idMap (Fin.cast (by simp) i) := by
|
||||
simp only [contr, contrIndexList_idMap, Fin.cast_trans]
|
||||
apply congrArg
|
||||
simp only [withoutDualEquiv, RelIso.coe_fn_toEquiv, Finset.coe_orderIsoOfFin_apply,
|
||||
EmbeddingLike.apply_eq_iff_eq]
|
||||
have h1 : l.contrIndexList.withoutDual = Finset.univ := by
|
||||
have hx := l.contrIndexList.withDual_union_withoutDual
|
||||
have hx2 := l.contrIndexList_withDual
|
||||
simp_all
|
||||
simp only [h1]
|
||||
rw [orderEmbOfFin_univ]
|
||||
· rfl
|
||||
· rw [h1]
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
lemma contr_contr_colorMap (i : Fin l.contr.contr.length) :
|
||||
l.contr.contr.colorMap i = l.contr.colorMap (Fin.cast (by simp) i) := by
|
||||
simp only [contr, contrIndexList_colorMap, Fin.cast_trans]
|
||||
apply congrArg
|
||||
simp only [withoutDualEquiv, RelIso.coe_fn_toEquiv, Finset.coe_orderIsoOfFin_apply,
|
||||
EmbeddingLike.apply_eq_iff_eq]
|
||||
have h1 : l.contrIndexList.withoutDual = Finset.univ := by
|
||||
have hx := l.contrIndexList.withDual_union_withoutDual
|
||||
have hx2 := l.contrIndexList_withDual
|
||||
simp_all
|
||||
simp only [h1]
|
||||
rw [orderEmbOfFin_univ]
|
||||
· rfl
|
||||
· rw [h1]
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
lemma contr_of_withDual_empty (h : l.withDual = ∅) :
|
||||
l.contr = l := by
|
||||
simp [contr]
|
||||
apply ext
|
||||
simp [l.contrIndexList_of_withDual_empty h]
|
||||
|
||||
@[simp]
|
||||
lemma contr_getDual?_eq_none (i : Fin l.contr.length) :
|
||||
l.contr.getDual? i = none := by
|
||||
simp only [contr, contrIndexList_getDual?]
|
||||
|
||||
@[simp]
|
||||
lemma contr_areDualInSelf (i j : Fin l.contr.length) :
|
||||
l.contr.AreDualInSelf i j ↔ False := by
|
||||
simp [contr]
|
||||
|
||||
lemma contr_countP_eq_zero_of_countP (I : Index 𝓒.Color)
|
||||
(h : l.val.countP (fun J => I.id = J.id) = 0) :
|
||||
l.contr.val.countP (fun J => I.id = J.id) = 0 := by
|
||||
simp [contr]
|
||||
exact countP_contrIndexList_zero_of_countP l.toIndexList I h
|
||||
|
||||
lemma contr_countP (I : Index 𝓒.Color) :
|
||||
l.contr.val.countP (fun J => I.id = J.id) =
|
||||
(l.val.filter (fun J => I.id = J.id)).countP (fun i => l.val.countP (fun j => i.id = j.id) = 1) := by
|
||||
simp [contr, contrIndexList]
|
||||
rw [List.countP_filter, List.countP_filter]
|
||||
congr
|
||||
funext J
|
||||
simp
|
||||
exact
|
||||
Bool.and_comm (decide (I.id = J.id))
|
||||
(decide (List.countP (fun j => decide (J.id = j.id)) l.val = 1))
|
||||
|
||||
lemma contr_cons_dual (I : Index 𝓒.Color) (hI1 : l.val.countP (fun J => I.id = J.id) ≤ 1) :
|
||||
l.contr.val.countP (fun J => I.id = J.id) ≤ 1 := by
|
||||
rw [contr_countP]
|
||||
by_cases hI1 : l.val.countP (fun J => I.id = J.id) = 0
|
||||
· rw [filter_of_countP_zero]
|
||||
· simp
|
||||
· exact hI1
|
||||
· have hI1 : l.val.countP (fun J => I.id = J.id) = 1 := by
|
||||
omega
|
||||
rw [consDual_filter]
|
||||
· simp_all
|
||||
· exact hI1
|
||||
|
||||
/-!
|
||||
|
||||
## Contract equiv
|
||||
|
||||
-/
|
||||
|
||||
/-- 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`),
|
||||
and those indices without duals.
|
||||
|
||||
This equivalence is used to contract the indices of tensors. -/
|
||||
def contrEquiv : (l.withUniqueDualLT ⊕ l.withUniqueDualLT) ⊕ Fin l.contr.length ≃ Fin l.length :=
|
||||
(Equiv.sumCongr (l.withUniqueLTGTEquiv) (Equiv.refl _)).trans <|
|
||||
(Equiv.sumCongr (Equiv.subtypeEquivRight (by
|
||||
simp only [l.unique_duals, implies_true]))
|
||||
(Fin.castOrderIso l.contrIndexList_length).toEquiv).trans <|
|
||||
l.dualEquiv
|
||||
|
||||
lemma contrEquiv_inl_inl_isSome (i : l.withUniqueDualLT) :
|
||||
(l.getDual? (l.contrEquiv (Sum.inl (Sum.inl i)))).isSome := by
|
||||
change (l.getDual? i).isSome
|
||||
have h1 : i.1 ∈ l.withUniqueDual := by
|
||||
have hi2 := i.2
|
||||
simp only [withUniqueDualLT, Finset.mem_filter] at hi2
|
||||
exact hi2.1
|
||||
exact mem_withUniqueDual_isSome l.toIndexList (↑i) h1
|
||||
|
||||
@[simp]
|
||||
lemma contrEquiv_inl_inr_eq (i : l.withUniqueDualLT) :
|
||||
(l.contrEquiv (Sum.inl (Sum.inr i))) =
|
||||
(l.getDual? i.1).get (l.contrEquiv_inl_inl_isSome i) := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma contrEquiv_inl_inl_eq (i : l.withUniqueDualLT) :
|
||||
(l.contrEquiv (Sum.inl (Sum.inl i))) = i := by
|
||||
rfl
|
||||
|
||||
lemma contrEquiv_colorMapIso :
|
||||
ColorMap.MapIso (Equiv.refl (Fin l.contr.length))
|
||||
(ColorMap.contr l.contrEquiv l.colorMap) l.contr.colorMap := by
|
||||
simp [ColorMap.MapIso, ColorMap.contr]
|
||||
funext i
|
||||
simp [contr]
|
||||
rfl
|
||||
|
||||
lemma contrEquiv_contrCond : ColorMap.ContrCond l.contrEquiv l.colorMap := by
|
||||
simp only [ColorMap.ContrCond]
|
||||
funext i
|
||||
simp only [Function.comp_apply, contrEquiv_inl_inl_eq, contrEquiv_inl_inr_eq]
|
||||
have h1 := l.dual_color
|
||||
rw [ColorCond.iff_on_isSome] at h1
|
||||
exact (h1 i.1 _).symm
|
||||
|
||||
@[simp]
|
||||
lemma contrEquiv_on_withDual_empty (i : Fin l.contr.length) (h : l.withDual = ∅) :
|
||||
l.contrEquiv (Sum.inr i) = Fin.cast (by simp [h]) i := by
|
||||
simp [contrEquiv]
|
||||
change l.dualEquiv (Sum.inr ((Fin.castOrderIso _).toEquiv i)) = _
|
||||
simp [dualEquiv, withoutDualEquiv]
|
||||
have h : l.withoutDual = Finset.univ := by
|
||||
have hx := l.withDual_union_withoutDual
|
||||
simp_all
|
||||
simp [h]
|
||||
rw [orderEmbOfFin_univ]
|
||||
· rfl
|
||||
· rw [h]
|
||||
simp
|
||||
|
||||
end ColorIndexList
|
||||
end IndexNotation
|
||||
|
|
@ -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.Color
|
||||
import HepLean.SpaceTime.LorentzTensor.IndexNotation.ColorIndexList.Contraction
|
||||
import HepLean.SpaceTime.LorentzTensor.Basic
|
||||
import Init.Data.List.Lemmas
|
||||
/-!
|
||||
|
|
@ -170,12 +170,18 @@ lemma withUniqueDual_eq_withDual_filter_id_fin (h : l.withUniqueDual = l.withDua
|
|||
omega
|
||||
|
||||
section filterID
|
||||
|
||||
lemma filter_id_of_countP_zero {i : Fin l.length}
|
||||
(h1 : l.val.countP (fun J => (l.val.get i).id = J.id) = 0) :
|
||||
l.val.filter (fun J => (l.val.get i).id = J.id) = [] := by
|
||||
rw [List.countP_eq_length_filter, List.length_eq_zero] at h1
|
||||
exact h1
|
||||
|
||||
lemma filter_of_countP_zero {I : Index X} (h1 : l.val.countP (fun J => I.id = J.id) = 0) :
|
||||
l.val.filter (fun J => I.id = J.id) = [] := by
|
||||
rw [List.countP_eq_length_filter, List.length_eq_zero] at h1
|
||||
exact h1
|
||||
|
||||
lemma filter_id_of_countP_one {i : Fin l.length}
|
||||
(h1 : l.val.countP (fun J => (l.val.get i).id = J.id) = 1) :
|
||||
l.val.filter (fun J => (l.val.get i).id = J.id) = [l.val.get i] := by
|
||||
|
|
|
|||
|
|
@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.SpaceTime.LorentzTensor.IndexNotation.Color
|
||||
import HepLean.SpaceTime.LorentzTensor.IndexNotation.Relations
|
||||
import HepLean.SpaceTime.LorentzTensor.IndexNotation.ColorIndexList.Relations
|
||||
import HepLean.SpaceTime.LorentzTensor.IndexNotation.ColorIndexList.Append
|
||||
import HepLean.SpaceTime.LorentzTensor.Basic
|
||||
import HepLean.SpaceTime.LorentzTensor.RisingLowering
|
||||
import HepLean.SpaceTime.LorentzTensor.Contraction
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue