Merge pull request #111 from HEPLean/Index-notation
feat: Index notation results
This commit is contained in:
Joseph Tooby-Smith
GitHub
commit
e472107375
12 changed files with 429 additions and 35 deletions
|
|
@ -79,6 +79,7 @@ import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexString
|
|||
import HepLean.SpaceTime.LorentzTensor.IndexNotation.TensorIndex
|
||||
import HepLean.SpaceTime.LorentzTensor.MulActionTensor
|
||||
import HepLean.SpaceTime.LorentzTensor.Real.Basic
|
||||
import HepLean.SpaceTime.LorentzTensor.Real.IndexNotation
|
||||
import HepLean.SpaceTime.LorentzTensor.RisingLowering
|
||||
import HepLean.SpaceTime.LorentzVector.AsSelfAdjointMatrix
|
||||
import HepLean.SpaceTime.LorentzVector.Basic
|
||||
|
|
|
|||
|
|
@ -44,13 +44,16 @@ structure TensorColor where
|
|||
|
||||
namespace TensorColor
|
||||
|
||||
variable (𝓒 : TensorColor)
|
||||
variable (𝓒 : TensorColor) [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
|
||||
variable {d : ℕ} {X Y Y' Z W : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
|
||||
[Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z] [Fintype W] [DecidableEq W]
|
||||
|
||||
/-- A relation on colors which is true if the two colors are equal or are duals. -/
|
||||
def colorRel (μ ν : 𝓒.Color) : Prop := μ = ν ∨ μ = 𝓒.τ ν
|
||||
|
||||
instance : Decidable (colorRel 𝓒 μ ν) :=
|
||||
Or.decidable
|
||||
|
||||
/-- An equivalence relation on colors which is true if the two colors are equal or are duals. -/
|
||||
lemma colorRel_equivalence : Equivalence 𝓒.colorRel where
|
||||
refl := by
|
||||
|
|
@ -87,6 +90,11 @@ instance colorSetoid : Setoid 𝓒.Color := ⟨𝓒.colorRel, 𝓒.colorRel_equi
|
|||
def colorQuot (μ : 𝓒.Color) : Quotient 𝓒.colorSetoid :=
|
||||
Quotient.mk 𝓒.colorSetoid μ
|
||||
|
||||
instance (μ ν : 𝓒.Color) : Decidable (μ ≈ ν) :=
|
||||
Or.decidable
|
||||
|
||||
instance : DecidableEq (Quotient 𝓒.colorSetoid) :=
|
||||
instDecidableEqQuotientOfDecidableEquiv
|
||||
end TensorColor
|
||||
|
||||
noncomputable section
|
||||
|
|
|
|||
|
|
@ -107,6 +107,8 @@ instance : Decidable (listCharIndex X l) :=
|
|||
e.g. `ᵘ¹²` or `ᵤ₄₃` etc. -/
|
||||
def Index : Type := {s : String // listCharIndex X s.toList ∧ s.toList ≠ []}
|
||||
|
||||
instance : DecidableEq (Index X) := Subtype.instDecidableEq
|
||||
|
||||
namespace Index
|
||||
|
||||
variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
|
||||
|
|
@ -295,19 +297,19 @@ instance : DecidableEq l.contrSubtype :=
|
|||
|
||||
/-- Given a `i : l.contrSubtype` the proposition on a `j` in `Fin s.length` for
|
||||
it to be an index of `s` contracting with `i`. -/
|
||||
def getDualProp (i : l.contrSubtype) (j : Fin l.length) : Prop :=
|
||||
i.1 ≠ j ∧ l.idMap i.1 = l.idMap j
|
||||
def getDualProp (i j : Fin l.length) : Prop :=
|
||||
i ≠ j ∧ l.idMap i = l.idMap j
|
||||
|
||||
instance (i : l.contrSubtype) (j : Fin l.length) :
|
||||
instance (i j : Fin l.length) :
|
||||
Decidable (l.getDualProp i j) :=
|
||||
instDecidableAnd
|
||||
|
||||
/-- Given a `i : l.contrSubtype` the index of `s` contracting with `i`. -/
|
||||
def getDualFin (i : l.contrSubtype) : Fin l.length :=
|
||||
(Fin.find (l.getDualProp i)).get (by simpa [NoContr, Fin.isSome_find_iff] using i.prop)
|
||||
(Fin.find (l.getDualProp i.1)).get (by simpa [NoContr, Fin.isSome_find_iff] using i.prop)
|
||||
|
||||
lemma some_getDualFin_eq_find (i : l.contrSubtype) :
|
||||
Fin.find (l.getDualProp i) = some (l.getDualFin i) := by
|
||||
Fin.find (l.getDualProp i.1) = some (l.getDualFin i) := by
|
||||
simp [getDualFin]
|
||||
|
||||
lemma getDualFin_not_NoContr (i : l.contrSubtype) : ¬ l.NoContr (l.getDualFin i) := by
|
||||
|
|
@ -333,6 +335,13 @@ lemma getDual_neq_self (i : l.contrSubtype) : i ≠ l.getDual i := by
|
|||
rw [Fin.find_eq_some_iff] at h1
|
||||
exact ne_of_apply_ne Subtype.val h1.1.1
|
||||
|
||||
lemma getDual_getDualProp (i : l.contrSubtype) : l.getDualProp i.1 (l.getDual i).1 := by
|
||||
simp [getDual]
|
||||
have h1 := l.some_getDualFin_eq_find i
|
||||
rw [Fin.find_eq_some_iff] at h1
|
||||
simp only [getDualProp, ne_eq, and_imp] at h1
|
||||
exact h1.1
|
||||
|
||||
/-!
|
||||
|
||||
## Index lists with no contracting indices
|
||||
|
|
@ -444,6 +453,11 @@ lemma getDual_not_lt_self_mem_contrPairSet {i : l.contrSubtype}
|
|||
simp only
|
||||
exact l.getDual_id i
|
||||
|
||||
/-- The list of elements of `l` which contract together. -/
|
||||
def contrPairList : List (Fin l.length × Fin l.length) :=
|
||||
(List.product (Fin.list l.length) (Fin.list l.length)).filterMap fun (i, j) => if
|
||||
l.getDualProp i j then some (i, j) else none
|
||||
|
||||
end IndexList
|
||||
|
||||
end IndexNotation
|
||||
|
|
|
|||
|
|
@ -5,6 +5,7 @@ Authors: Joseph Tooby-Smith
|
|||
-/
|
||||
import HepLean.SpaceTime.LorentzTensor.IndexNotation.Basic
|
||||
import HepLean.SpaceTime.LorentzTensor.Basic
|
||||
import Init.Data.List.Lemmas
|
||||
/-!
|
||||
|
||||
# Index lists with color conditions
|
||||
|
|
@ -25,9 +26,11 @@ variable [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color
|
|||
/-- An index list is allowed if every contracting index has exactly one dual,
|
||||
and the color of the dual is dual to the color of the index. -/
|
||||
def IndexListColorProp (l : IndexList 𝓒.Color) : Prop :=
|
||||
(∀ (i j : l.contrSubtype), l.getDualProp i j.1 → j = l.getDual i) ∧
|
||||
(∀ (i j : l.contrSubtype), l.getDualProp i.1 j.1 → j = l.getDual i) ∧
|
||||
(∀ (i : l.contrSubtype), l.colorMap i.1 = 𝓒.τ (l.colorMap (l.getDual i).1))
|
||||
|
||||
instance : DecidablePred (IndexListColorProp 𝓒) := fun _ => And.decidable
|
||||
|
||||
/-- The type of index lists which satisfy `IndexListColorProp`. -/
|
||||
def IndexListColor : Type := {s : IndexList 𝓒.Color // IndexListColorProp 𝓒 s}
|
||||
|
||||
|
|
@ -48,6 +51,64 @@ lemma indexListColorProp_of_hasNoContr {s : IndexList 𝓒.Color} (h : s.HasNoCo
|
|||
|
||||
/-!
|
||||
|
||||
## Conditions related to IndexListColorProp
|
||||
|
||||
-/
|
||||
|
||||
/-- The bool which is true if ever index appears at most once in the first element of entries of
|
||||
`l.contrPairList`. I.e. If every element contracts with at most one other element. -/
|
||||
def colorPropFstBool (l : IndexList 𝓒.Color) : Bool :=
|
||||
let l' := List.product l.contrPairList l.contrPairList
|
||||
let l'' := l'.filterMap fun (i, j) => if i.1 = j.1 ∧ i.2 ≠ j.2 then some i else none
|
||||
List.isEmpty l''
|
||||
|
||||
lemma colorPropFstBool_indexListColorProp_fst (l : IndexList 𝓒.Color) (hl : colorPropFstBool l) :
|
||||
∀ (i j : l.contrSubtype), l.getDualProp i.1 j.1 → j = l.getDual i := by
|
||||
simp [colorPropFstBool] at hl
|
||||
rw [List.filterMap_eq_nil] at hl
|
||||
simp at hl
|
||||
intro i j hij
|
||||
have hl' := hl i.1 j.1 i.1 (l.getDual i).1
|
||||
simp [contrPairList] at hl'
|
||||
have h1 {n : ℕ} (m : Fin n) : m ∈ Fin.list n := by
|
||||
have h1' : (Fin.list n)[m] = m := by
|
||||
erw [Fin.getElem_list]
|
||||
rfl
|
||||
rw [← h1']
|
||||
apply List.getElem_mem
|
||||
apply Subtype.ext (hl' (h1 _) (h1 _) hij (h1 _) (h1 _) (l.getDual_getDualProp i))
|
||||
|
||||
/-- The bool which is true if the pairs in `l.contrPairList` have dual colors. -/
|
||||
def colorPropSndBool (l : IndexList 𝓒.Color) : Bool :=
|
||||
List.all l.contrPairList (fun (i, j) => l.colorMap i = 𝓒.τ (l.colorMap j))
|
||||
|
||||
lemma colorPropSndBool_indexListColorProp_snd (l : IndexList 𝓒.Color)
|
||||
(hl2 : colorPropSndBool l) :
|
||||
∀ (i : l.contrSubtype), l.colorMap i.1 = 𝓒.τ (l.colorMap (l.getDual i).1) := by
|
||||
simp [colorPropSndBool] at hl2
|
||||
intro i
|
||||
have h2 := hl2 i.1 (l.getDual i).1
|
||||
simp [contrPairList] at h2
|
||||
have h1 {n : ℕ} (m : Fin n) : m ∈ Fin.list n := by
|
||||
have h1' : (Fin.list n)[m] = m := by
|
||||
erw [Fin.getElem_list]
|
||||
rfl
|
||||
rw [← h1']
|
||||
apply List.getElem_mem
|
||||
exact h2 (h1 _) (h1 _) (l.getDual_getDualProp i)
|
||||
|
||||
/-- The bool which is true if both `colorPropFstBool` and `colorPropSndBool` are true. -/
|
||||
def colorPropBool (l : IndexList 𝓒.Color) : Bool :=
|
||||
colorPropFstBool l && colorPropSndBool l
|
||||
|
||||
lemma colorPropBool_indexListColorProp {l : IndexList 𝓒.Color} (hl : colorPropBool l) :
|
||||
IndexListColorProp 𝓒 l := by
|
||||
simp [colorPropBool] at hl
|
||||
exact And.intro (colorPropFstBool_indexListColorProp_fst l hl.1)
|
||||
(colorPropSndBool_indexListColorProp_snd l hl.2)
|
||||
|
||||
/-!
|
||||
|
||||
## Contraction pairs for IndexListColor
|
||||
|
||||
-/
|
||||
|
|
@ -176,17 +237,19 @@ def PermContr (s1 s2 : IndexListColor 𝓒) : Prop :=
|
|||
s1.contr.1.idMap i = s2.contr.1.idMap j →
|
||||
s1.contr.1.colorMap i = s2.contr.1.colorMap j
|
||||
|
||||
lemma PermContr.refl : Reflexive (@PermContr 𝓒 _) := by
|
||||
namespace PermContr
|
||||
|
||||
lemma refl : Reflexive (@PermContr 𝓒 _) := by
|
||||
intro l
|
||||
simp only [PermContr, List.Perm.refl, true_and]
|
||||
have h1 : l.contr.1.HasNoContr := l.1.contrIndexList_hasNoContr
|
||||
exact fun i j a => hasNoContr_color_eq_of_id_eq (↑l.contr) h1 i j a
|
||||
|
||||
lemma PermContr.symm : Symmetric (@PermContr 𝓒 _) :=
|
||||
lemma symm : Symmetric (@PermContr 𝓒 _) :=
|
||||
fun _ _ h => And.intro (List.Perm.symm h.1) fun i j hij => (h.2 j i hij.symm).symm
|
||||
|
||||
/-- Given an index in `s1` the index in `s2` related by `PermContr` with the same id. -/
|
||||
def PermContr.get {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) (i : Fin s1.contr.1.length) :
|
||||
def get {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) (i : Fin s1.contr.1.length) :
|
||||
Fin s2.contr.1.length :=
|
||||
(Fin.find (fun j => s1.contr.1.idMap i = s2.contr.1.idMap j)).get (by
|
||||
rw [Fin.isSome_find_iff]
|
||||
|
|
@ -207,19 +270,19 @@ def PermContr.get {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) (i : Fin s
|
|||
change _ = (s2.contr.1.get j').id
|
||||
rw [hj'])
|
||||
|
||||
lemma PermContr.some_get_eq_find {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
|
||||
lemma some_get_eq_find {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
|
||||
(i : Fin s1.contr.1.length) :
|
||||
Fin.find (fun j => s1.contr.1.idMap i = s2.contr.1.idMap j) = some (h.get i) := by
|
||||
simp [PermContr.get]
|
||||
|
||||
lemma PermContr.get_id {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
|
||||
lemma get_id {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
|
||||
(i : Fin s1.contr.1.length) :
|
||||
s2.contr.1.idMap (h.get i) = s1.contr.1.idMap i := by
|
||||
have h1 := h.some_get_eq_find i
|
||||
rw [Fin.find_eq_some_iff] at h1
|
||||
exact h1.1.symm
|
||||
|
||||
lemma PermContr.get_unique {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
|
||||
lemma get_unique {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
|
||||
{i : Fin s1.contr.1.length} {j : Fin s2.contr.1.length}
|
||||
(hij : s1.contr.1.idMap i = s2.contr.1.idMap j) :
|
||||
j = h.get i := by
|
||||
|
|
@ -230,17 +293,39 @@ lemma PermContr.get_unique {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
|
|||
apply And.intro hn
|
||||
rw [← hij, PermContr.get_id]
|
||||
|
||||
lemma get_color {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
|
||||
(i : Fin s1.contr.1.length) :
|
||||
s1.contr.1.colorMap i = s2.contr.1.colorMap (h.get i) :=
|
||||
h.2 i (h.get i) (h.get_id i).symm
|
||||
|
||||
@[simp]
|
||||
lemma PermContr.get_symm_apply_get_apply {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
|
||||
lemma get_symm_apply_get_apply {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
|
||||
(i : Fin s1.contr.1.length) : h.symm.get (h.get i) = i :=
|
||||
(h.symm.get_unique (h.get_id i)).symm
|
||||
|
||||
lemma PermContr.get_apply_get_symm_apply {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
|
||||
lemma get_apply_get_symm_apply {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
|
||||
(i : Fin s2.contr.1.length) : h.get (h.symm.get i) = i :=
|
||||
(h.get_unique (h.symm.get_id i)).symm
|
||||
|
||||
lemma trans {s1 s2 s3 : IndexListColor 𝓒} (h1 : PermContr s1 s2) (h2 : PermContr s2 s3) :
|
||||
PermContr s1 s3 := by
|
||||
apply And.intro (h1.1.trans h2.1)
|
||||
intro i j hij
|
||||
rw [h1.get_color i]
|
||||
have hj : j = h2.get (h1.get i) := by
|
||||
apply h2.get_unique
|
||||
rw [get_id]
|
||||
exact hij
|
||||
rw [hj, h2.get_color]
|
||||
|
||||
lemma get_trans {s1 s2 s3 : IndexListColor 𝓒} (h1 : PermContr s1 s2) (h2 : PermContr s2 s3)
|
||||
(i : Fin s1.contr.1.length) :
|
||||
(h1.trans h2).get i = h2.get (h1.get i) := by
|
||||
apply h2.get_unique
|
||||
rw [get_id, get_id]
|
||||
|
||||
/-- Equivalence of indexing types for two `IndexListColor` related by `PermContr`. -/
|
||||
def PermContr.toEquiv {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) :
|
||||
def toEquiv {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) :
|
||||
Fin s1.contr.1.length ≃ Fin s2.contr.1.length where
|
||||
toFun := h.get
|
||||
invFun := h.symm.get
|
||||
|
|
@ -249,16 +334,46 @@ def PermContr.toEquiv {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) :
|
|||
right_inv x := by
|
||||
simp
|
||||
|
||||
lemma PermContr.toEquiv_symm {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) :
|
||||
lemma toEquiv_refl' {s : IndexListColor 𝓒} (h : PermContr s s) :
|
||||
h.toEquiv = Equiv.refl _ := by
|
||||
apply Equiv.ext
|
||||
intro x
|
||||
simp [toEquiv, get]
|
||||
have h1 : Fin.find fun j => s.contr.1.idMap x = s.contr.1.idMap j = some x := by
|
||||
rw [Fin.find_eq_some_iff]
|
||||
have h2 := s.1.contrIndexList_hasNoContr x
|
||||
simp only [true_and]
|
||||
intro j hj
|
||||
by_cases hjx : j = x
|
||||
subst hjx
|
||||
rfl
|
||||
exact False.elim (h2 j (fun a => hjx a.symm) hj)
|
||||
simp only [h1, Option.get_some]
|
||||
|
||||
@[simp]
|
||||
lemma toEquiv_refl {s : IndexListColor 𝓒} :
|
||||
PermContr.toEquiv (PermContr.refl s) = Equiv.refl _ := by
|
||||
exact PermContr.toEquiv_refl' _
|
||||
|
||||
lemma toEquiv_symm {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) :
|
||||
h.toEquiv.symm = h.symm.toEquiv := by
|
||||
rfl
|
||||
|
||||
lemma PermContr.toEquiv_colorMap {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) :
|
||||
lemma toEquiv_colorMap {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) :
|
||||
s2.contr.1.colorMap = s1.contr.1.colorMap ∘ h.toEquiv.symm := by
|
||||
funext x
|
||||
refine (h.2 _ _ ?_).symm
|
||||
simp [← h.get_id, toEquiv]
|
||||
|
||||
lemma toEquiv_trans {s1 s2 s3 : IndexListColor 𝓒} (h1 : PermContr s1 s2) (h2 : PermContr s2 s3) :
|
||||
(h1.trans h2).toEquiv = h1.toEquiv.trans h2.toEquiv := by
|
||||
apply Equiv.ext
|
||||
intro x
|
||||
simp [toEquiv]
|
||||
rw [← get_trans]
|
||||
|
||||
end PermContr
|
||||
|
||||
/-! TODO: Show that `rel` is indeed an equivalence relation. -/
|
||||
|
||||
/-!
|
||||
|
|
|
|||
|
|
@ -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.Basic
|
||||
import HepLean.SpaceTime.LorentzTensor.IndexNotation.TensorIndex
|
||||
/-!
|
||||
|
||||
# Strings of indices
|
||||
|
|
@ -242,3 +242,33 @@ def toIndexList (s : IndexString X) : IndexList X :=
|
|||
end IndexString
|
||||
|
||||
end IndexNotation
|
||||
namespace TensorStructure
|
||||
|
||||
/-!
|
||||
|
||||
## Making a tensor index from an index string
|
||||
|
||||
-/
|
||||
|
||||
namespace TensorIndex
|
||||
variable {R : Type} [CommSemiring R] (𝓣 : TensorStructure R)
|
||||
variable {𝓣 : TensorStructure R} [IndexNotation 𝓣.Color] [Fintype 𝓣.Color] [DecidableEq 𝓣.Color]
|
||||
variable {n m : ℕ} {cn : Fin n → 𝓣.Color} {cm : Fin m → 𝓣.Color}
|
||||
|
||||
open IndexNotation IndexListColor
|
||||
|
||||
/-- The construction of a tensor index from a tensor and a string satisfing conditions which are
|
||||
easy to check automatically. -/
|
||||
noncomputable def fromIndexString (T : 𝓣.Tensor cn) (s : String)
|
||||
(hs : listCharIndexStringBool 𝓣.toTensorColor.Color s.toList = true)
|
||||
(hn : n = (IndexString.toIndexList (⟨s, hs⟩ : IndexString 𝓣.Color)).length)
|
||||
(hc : IndexListColorProp 𝓣.toTensorColor (
|
||||
IndexString.toIndexList (⟨s, hs⟩ : IndexString 𝓣.Color)))
|
||||
(hd : TensorColor.DualMap (IndexString.toIndexList (⟨s, hs⟩ : IndexString 𝓣.Color)).colorMap
|
||||
(cn ∘ Fin.cast hn.symm)) : 𝓣.TensorIndex :=
|
||||
TensorStructure.TensorIndex.mkDualMap T
|
||||
⟨(IndexString.toIndexList (⟨s, hs⟩ : IndexString 𝓣.Color)), hc⟩ hn hd
|
||||
|
||||
end TensorIndex
|
||||
|
||||
end TensorStructure
|
||||
|
|
|
|||
|
|
@ -36,7 +36,7 @@ structure TensorIndex where
|
|||
tensor : 𝓣.Tensor index.1.colorMap
|
||||
|
||||
namespace TensorIndex
|
||||
open TensorColor
|
||||
open TensorColor IndexListColor
|
||||
variable {𝓣 : TensorStructure R} [IndexNotation 𝓣.Color] [Fintype 𝓣.Color] [DecidableEq 𝓣.Color]
|
||||
variable {n m : ℕ} {cn : Fin n → 𝓣.Color} {cm : Fin m → 𝓣.Color}
|
||||
|
||||
|
|
@ -69,6 +69,12 @@ def mkDualMap (T : 𝓣.Tensor cn) (l : IndexListColor 𝓣.toTensorColor) (hn :
|
|||
𝓣.dualize (DualMap.split l.1.colorMap (cn ∘ Fin.cast hn.symm)) <|
|
||||
(𝓣.mapIso (Fin.castOrderIso hn).toEquiv rfl T : 𝓣.Tensor (cn ∘ Fin.cast hn.symm))
|
||||
|
||||
/-!
|
||||
|
||||
## The contraction of indices
|
||||
|
||||
-/
|
||||
|
||||
/-- The contraction of indices in a `TensorIndex`. -/
|
||||
def contr (T : 𝓣.TensorIndex) : 𝓣.TensorIndex where
|
||||
index := T.index.contr
|
||||
|
|
@ -77,6 +83,14 @@ def contr (T : 𝓣.TensorIndex) : 𝓣.TensorIndex where
|
|||
T.index.contr_colorMap <|
|
||||
𝓣.contr (T.index.splitContr).symm T.index.splitContr_map T.tensor
|
||||
|
||||
/-! TODO: Show that contracting twice is the same as contracting once. -/
|
||||
|
||||
/-!
|
||||
|
||||
## Product of `TensorIndex` allowed
|
||||
|
||||
-/
|
||||
|
||||
/-- The tensor product of two `TensorIndex`. -/
|
||||
def prod (T₁ T₂ : 𝓣.TensorIndex)
|
||||
(h : IndexListColorProp 𝓣.toTensorColor (T₁.index.1 ++ T₂.index.1)) : 𝓣.TensorIndex where
|
||||
|
|
@ -87,11 +101,28 @@ def prod (T₁ T₂ : 𝓣.TensorIndex)
|
|||
(IndexListColor.prod_colorMap h) <|
|
||||
𝓣.tensoratorEquiv _ _ (T₁.tensor ⊗ₜ[R] T₂.tensor)
|
||||
|
||||
@[simp]
|
||||
lemma prod_index (T₁ T₂ : 𝓣.TensorIndex)
|
||||
(h : IndexListColorProp 𝓣.toTensorColor (T₁.index.1 ++ T₂.index.1)) :
|
||||
(prod T₁ T₂ h).index = T₁.index.prod T₂.index h := rfl
|
||||
|
||||
/-!
|
||||
|
||||
## Scalar multiplication of
|
||||
|
||||
-/
|
||||
|
||||
/-- The scalar multiplication of a `TensorIndex` by an element of `R`. -/
|
||||
def smul (r : R) (T : 𝓣.TensorIndex) : 𝓣.TensorIndex where
|
||||
index := T.index
|
||||
tensor := r • T.tensor
|
||||
|
||||
/-!
|
||||
|
||||
## Addition of allowed `TensorIndex`
|
||||
|
||||
-/
|
||||
|
||||
/-- The addition of two `TensorIndex` given the condition that, after contraction,
|
||||
their index lists are the same. -/
|
||||
def add (T₁ T₂ : 𝓣.TensorIndex) (h : IndexListColor.PermContr T₁.index T₂.index) :
|
||||
|
|
@ -103,12 +134,70 @@ def add (T₁ T₂ : 𝓣.TensorIndex) (h : IndexListColor.PermContr T₁.index
|
|||
𝓣.mapIso h.toEquiv.symm h.toEquiv_colorMap T₂.contr.tensor
|
||||
T1 + T2
|
||||
|
||||
/-- An (equivalence) relation on two `TensorIndex` given that after contraction,
|
||||
the two underlying tensors are the equal. -/
|
||||
/-!
|
||||
|
||||
## Equivalence relation on `TensorIndex`
|
||||
|
||||
-/
|
||||
|
||||
/-- An (equivalence) relation on two `TensorIndex`.
|
||||
The point in this equivalence relation is that certain things (like the
|
||||
permutation of indices, the contraction of indices, or rising or lowering indices) can be placed
|
||||
in the indices or moved to the tensor itself. These two descriptions are equivalent. -/
|
||||
def Rel (T₁ T₂ : 𝓣.TensorIndex) : Prop :=
|
||||
T₁.index.PermContr T₂.index ∧ ∀ (h : T₁.index.PermContr T₂.index),
|
||||
T₁.contr.tensor = 𝓣.mapIso h.toEquiv.symm h.toEquiv_colorMap T₂.contr.tensor
|
||||
|
||||
namespace Rel
|
||||
|
||||
/-- Rel is reflexive. -/
|
||||
lemma refl (T : 𝓣.TensorIndex) : Rel T T := by
|
||||
apply And.intro
|
||||
exact IndexListColor.PermContr.refl T.index
|
||||
intro h
|
||||
simp [PermContr.toEquiv_refl']
|
||||
|
||||
/-- Rel is symmetric. -/
|
||||
lemma symm {T₁ T₂ : 𝓣.TensorIndex} (h : Rel T₁ T₂) : Rel T₂ T₁ := by
|
||||
apply And.intro h.1.symm
|
||||
intro h'
|
||||
rw [← mapIso_symm]
|
||||
symm
|
||||
erw [LinearEquiv.symm_apply_eq]
|
||||
rw [h.2]
|
||||
apply congrFun
|
||||
congr
|
||||
exact h'.symm
|
||||
|
||||
/-- Rel is transitive. -/
|
||||
lemma trans {T₁ T₂ T₃ : 𝓣.TensorIndex} (h1 : Rel T₁ T₂) (h2 : Rel T₂ T₃) : Rel T₁ T₃ := by
|
||||
apply And.intro (h1.1.trans h2.1)
|
||||
intro h
|
||||
change _ = (𝓣.mapIso (h1.1.trans h2.1).toEquiv.symm _) T₃.contr.tensor
|
||||
trans (𝓣.mapIso ((h1.1).toEquiv.trans (h2.1).toEquiv).symm (by
|
||||
rw [← PermContr.toEquiv_trans]
|
||||
exact proof_2 T₁ T₃ h)) T₃.contr.tensor
|
||||
swap
|
||||
congr
|
||||
rw [← PermContr.toEquiv_trans]
|
||||
erw [← mapIso_trans]
|
||||
simp only [LinearEquiv.trans_apply]
|
||||
apply (h1.2 h1.1).trans
|
||||
apply congrArg
|
||||
exact h2.2 h2.1
|
||||
|
||||
/-- Rel forms an equivalence relation. -/
|
||||
lemma equivalence : Equivalence (@Rel _ _ 𝓣 _) where
|
||||
refl := Rel.refl
|
||||
symm := Rel.symm
|
||||
trans := Rel.trans
|
||||
|
||||
/-- The equality of tensors corresponding to related tensor indices. -/
|
||||
lemma to_eq {T₁ T₂ : 𝓣.TensorIndex} (h : Rel T₁ T₂) :
|
||||
T₁.contr.tensor = 𝓣.mapIso h.1.toEquiv.symm h.1.toEquiv_colorMap T₂.contr.tensor := h.2 h.1
|
||||
|
||||
end Rel
|
||||
|
||||
end TensorIndex
|
||||
end
|
||||
end TensorStructure
|
||||
|
|
|
|||
119
HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean
Normal file
119
HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean
Normal file
|
|
@ -0,0 +1,119 @@
|
|||
/-
|
||||
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.TensorIndex
|
||||
import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexString
|
||||
import HepLean.SpaceTime.LorentzTensor.Real.Basic
|
||||
/-!
|
||||
|
||||
# Index notation for real Lorentz tensors
|
||||
|
||||
This uses the general concepts of index notation in `HepLean.SpaceTime.LorentzTensor.IndexNotation`
|
||||
to define the index notation for real Lorentz tensors.
|
||||
|
||||
-/
|
||||
|
||||
|
||||
instance : IndexNotation realTensorColor.Color where
|
||||
charList := {'ᵘ', 'ᵤ'}
|
||||
notaEquiv :=
|
||||
⟨fun c =>
|
||||
match c with
|
||||
| realTensorColor.ColorType.up => ⟨'ᵘ', Finset.mem_insert_self 'ᵘ' {'ᵤ'}⟩
|
||||
| realTensorColor.ColorType.down => ⟨'ᵤ', Finset.insert_eq_self.mp (by rfl)⟩,
|
||||
fun c =>
|
||||
if c = 'ᵘ' then realTensorColor.ColorType.up
|
||||
else realTensorColor.ColorType.down,
|
||||
by
|
||||
intro c
|
||||
match c with
|
||||
| realTensorColor.ColorType.up => rfl
|
||||
| realTensorColor.ColorType.down => rfl,
|
||||
by
|
||||
intro c
|
||||
by_cases hc : c = 'ᵘ'
|
||||
simp [hc]
|
||||
exact SetCoe.ext (id (Eq.symm hc))
|
||||
have hc' : c = 'ᵤ' := by
|
||||
have hc2 := c.2
|
||||
simp at hc2
|
||||
simp_all
|
||||
simp [hc']
|
||||
exact SetCoe.ext (id (Eq.symm hc'))⟩
|
||||
|
||||
namespace realLorentzTensor
|
||||
|
||||
open realTensorColor
|
||||
|
||||
variable {d : ℕ}
|
||||
|
||||
instance : IndexNotation (realLorentzTensor d).Color := instIndexNotationColorRealTensorColor
|
||||
instance : DecidableEq (realLorentzTensor d).Color := instDecidableEqColorRealTensorColor
|
||||
|
||||
@[simp]
|
||||
lemma indexNotation_eq_color : @realLorentzTensor.instIndexNotationColor d =
|
||||
instIndexNotationColorRealTensorColor := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma realLorentzTensor_color : (realLorentzTensor d).Color = realTensorColor.Color := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma toTensorColor_eq : (realLorentzTensor d).toTensorColor = realTensorColor := by
|
||||
rfl
|
||||
|
||||
open IndexNotation IndexString
|
||||
|
||||
open TensorStructure TensorIndex
|
||||
|
||||
/-- The construction of a tensor index from a tensor and a string satisfying conditions
|
||||
which can be automatically checked. This is a modified version of
|
||||
`TensorStructure.TensorIndex.mkDualMap` specific to real Lorentz tensors. -/
|
||||
noncomputable def fromIndexStringColor {cn : Fin n → realTensorColor.Color}
|
||||
(T : (realLorentzTensor d).Tensor cn) (s : String)
|
||||
(hs : listCharIndexStringBool realTensorColor.Color s.toList = true)
|
||||
(hn : n = (IndexString.toIndexList (⟨s, hs⟩ : IndexString realTensorColor.Color)).length)
|
||||
(hc : IndexListColor.colorPropBool (IndexString.toIndexList ⟨s, hs⟩))
|
||||
(hd : TensorColor.DualMap.boolFin
|
||||
(IndexString.toIndexList ⟨s, hs⟩).colorMap (cn ∘ Fin.cast hn.symm)) :
|
||||
(realLorentzTensor d).TensorIndex :=
|
||||
TensorStructure.TensorIndex.mkDualMap T
|
||||
⟨(IndexString.toIndexList (⟨s, hs⟩ : IndexString realTensorColor.Color)),
|
||||
IndexListColor.colorPropBool_indexListColorProp hc⟩ hn
|
||||
(TensorColor.DualMap.boolFin_DualMap hd)
|
||||
|
||||
/-- A tactics used to prove `colorPropBool` for real Lorentz tensors. -/
|
||||
macro "prodTactic" : tactic =>
|
||||
`(tactic| {
|
||||
change @IndexListColor.colorPropBool realTensorColor _ _ _
|
||||
simp only [toTensorColor_eq, indexNotation_eq_color, fromIndexStringColor, mkDualMap,
|
||||
String.toList, ↓Char.isValue, Equiv.coe_refl, Function.comp_apply, id_eq, ne_eq,
|
||||
Function.comp_id, RelIso.coe_fn_toEquiv, prod_index, IndexListColor.prod]
|
||||
rfl})
|
||||
|
||||
/-- A tactic used to prove `boolFin` for real Lornetz tensors. -/
|
||||
macro "dualMapTactic" : tactic =>
|
||||
`(tactic| {
|
||||
simp only [String.toList, ↓Char.isValue, toTensorColor_eq]
|
||||
rfl})
|
||||
|
||||
/-- Notation for the construction of a tensor index from a tensor and a string.
|
||||
Conditions are checked automatically. -/
|
||||
notation:20 T "|" S:21 => fromIndexStringColor T S (by rfl) (by rfl) (by rfl) (by dualMapTactic)
|
||||
|
||||
/-- Notation for the product of two tensor indices. Conditions are checked automatically. -/
|
||||
notation:10 T "⊗ᵀ" S:11 => TensorIndex.prod T S (IndexListColor.colorPropBool_indexListColorProp
|
||||
(by prodTactic))
|
||||
|
||||
/-- An example showing the allowed constructions. -/
|
||||
example (T : (realLorentzTensor d).Tensor ![ColorType.up, ColorType.down]) : True := by
|
||||
let _ := T|"ᵤ₁ᵤ₂"
|
||||
let _ := T|"ᵘ³ᵤ₄"
|
||||
let _ := T|"ᵤ₁ᵤ₂" ⊗ᵀ T|"ᵘ³ᵤ₄"
|
||||
let _ := T|"ᵤ₁ᵤ₂" ⊗ᵀ T|"ᵘ³ᵤ₄" ⊗ᵀ T|"ᵘ¹ᵘ²" ⊗ᵀ T|"ᵘ⁴ᵤ₃"
|
||||
exact trivial
|
||||
|
||||
end realLorentzTensor
|
||||
|
|
@ -253,6 +253,24 @@ def DualMap (c₁ : X → 𝓒.Color) (c₂ : X → 𝓒.Color) : Prop :=
|
|||
namespace DualMap
|
||||
|
||||
variable {c₁ c₂ c₃ : X → 𝓒.Color}
|
||||
variable {n : ℕ}
|
||||
|
||||
/-- The bool which if `𝓒.colorQuot (c₁ i) = 𝓒.colorQuot (c₂ i)` is true for all `i`. -/
|
||||
def boolFin (c₁ c₂ : Fin n → 𝓒.Color) : Bool :=
|
||||
(Fin.list n).all fun i => if 𝓒.colorQuot (c₁ i) = 𝓒.colorQuot (c₂ i) then true else false
|
||||
|
||||
lemma boolFin_DualMap {c₁ c₂ : Fin n → 𝓒.Color} (h : boolFin c₁ c₂ = true) :
|
||||
DualMap c₁ c₂ := by
|
||||
simp [boolFin] at h
|
||||
simp [DualMap]
|
||||
funext x
|
||||
have h2 {n : ℕ} (m : Fin n) : m ∈ Fin.list n := by
|
||||
have h1' : (Fin.list n)[m] = m := by
|
||||
erw [Fin.getElem_list]
|
||||
rfl
|
||||
rw [← h1']
|
||||
apply List.getElem_mem
|
||||
exact h x (h2 _)
|
||||
|
||||
lemma refl : DualMap c₁ c₁ := by
|
||||
simp [DualMap]
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@
|
|||
[](https://github.com/HEPLean/HepLean/pulls)
|
||||
[](https://leanprover.zulipchat.com)
|
||||
[](https://heplean.github.io/HepLean/TODOList)
|
||||
[](https://github.com/leanprover/lean4/releases/tag/v4.10.0)
|
||||
[](https://github.com/leanprover/lean4/releases/tag/v4.11.0-rc1)
|
||||
|
||||
A project to digitalize high energy physics.
|
||||
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@
|
|||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "leanprover-community",
|
||||
"rev": "0f3e143dffdc3a591662f3401ce1d7a3405227c0",
|
||||
"rev": "dc167d260ff7ee9849b436037add06bed15104be",
|
||||
"name": "batteries",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "main",
|
||||
|
|
@ -25,7 +25,7 @@
|
|||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "leanprover-community",
|
||||
"rev": "209712c78b16c795453b6da7f7adbda4589a8f21",
|
||||
"rev": "ae6ea60e9d8bc2d4b37ff02115854da2e1b710d0",
|
||||
"name": "aesop",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "master",
|
||||
|
|
@ -35,10 +35,10 @@
|
|||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "leanprover-community",
|
||||
"rev": "c87908619cccadda23f71262e6898b9893bffa36",
|
||||
"rev": "a96aee5245720f588876021b6a0aa73efee49c76",
|
||||
"name": "proofwidgets",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "v0.0.40",
|
||||
"inputRev": "v0.0.41",
|
||||
"inherited": true,
|
||||
"configFile": "lakefile.lean"},
|
||||
{"url": "https://github.com/leanprover/lean4-cli",
|
||||
|
|
@ -55,7 +55,7 @@
|
|||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "leanprover-community",
|
||||
"rev": "543725b3bfed792097fc134adca628406f6145f5",
|
||||
"rev": "68cd8ae0f5b996176d1243d94c56e17de570e3bf",
|
||||
"name": "importGraph",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "main",
|
||||
|
|
@ -65,10 +65,10 @@
|
|||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "",
|
||||
"rev": "a719ba5c3115d47b68bf0497a9dd1bcbb21ea663",
|
||||
"rev": "5025874dc5f9f8dd1598190e60ef20dda7b42566",
|
||||
"name": "mathlib",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "v4.10.0",
|
||||
"inputRev": "v4.11.0-rc1",
|
||||
"inherited": false,
|
||||
"configFile": "lakefile.lean"},
|
||||
{"url": "https://github.com/acmepjz/md4lean",
|
||||
|
|
@ -105,10 +105,10 @@
|
|||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "",
|
||||
"rev": "593ac5bd2ca98c5294675b5cccf3d89b300a76eb",
|
||||
"rev": "6d8e3118ab526f8dfcabcbdf9f05dc34e5c423a8",
|
||||
"name": "«doc-gen4»",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "v4.10.0",
|
||||
"inputRev": "v4.11.0-rc1",
|
||||
"inherited": false,
|
||||
"configFile": "lakefile.lean"}],
|
||||
"name": "hep_lean",
|
||||
|
|
|
|||
|
|
@ -6,12 +6,12 @@ defaultTargets = ["HepLean"]
|
|||
[[require]]
|
||||
name = "mathlib"
|
||||
git = "https://github.com/leanprover-community/mathlib4.git"
|
||||
rev = "v4.10.0"
|
||||
rev = "v4.11.0-rc1"
|
||||
|
||||
[[require]]
|
||||
name = "«doc-gen4»"
|
||||
git = "https://github.com/leanprover/doc-gen4"
|
||||
rev = "v4.10.0"
|
||||
rev = "v4.11.0-rc1"
|
||||
|
||||
[[lean_lib]]
|
||||
name = "HepLean"
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
leanprover/lean4:v4.10.0
|
||||
leanprover/lean4:v4.11.0-rc1
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue