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

feat: Update contraction for index notation

Browse source
This commit is contained in:
jstoobysmith 2024-10-10 08:57:22 +00:00
parent e90e41751e
commit 3f5eb58db4
10 changed files with 401 additions and 153 deletions
Download patch file Download diff file Expand all files Collapse all files

17
HepLean/SpaceTime/WeylFermion/ColorFun.lean → HepLean/Tensors/ComplexLorentz/ColorFun.lean
View file

@ -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.Tensors.ColorCat.Basic
import HepLean.Tensors.OverColor.Basic
import HepLean.Mathematics.PiTensorProduct
/-!
@ -30,6 +30,21 @@ inductive Color
| up : Color
| down : Color
def τ : Color → Color
| Color.upL => Color.downL
| Color.downL => Color.upL
| Color.upR => Color.downR
| Color.downR => Color.upR
| Color.up => Color.down
| Color.down => Color.up
def evalNo : Color → ℕ
| Color.upL => 2
| Color.downL => 2
| Color.upR => 2
| Color.downR => 2
| Color.up => 4
| Color.down => 4
/-- The corresponding representations associated with a color. -/
def colorToRep (c : Color) : Rep ℂ SL(2, ℂ) :=
match c with

0
HepLean/Tensors/ComplexLorentz/ContrNatTransform.lean Normal file
View file

38
HepLean/Tensors/ComplexLorentz/Examples.lean Normal file
View file

@ -0,0 +1,38 @@
/-
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.Tensors.Tree.Basic
import HepLean.Tensors.ComplexLorentz.TensorStruct
import HepLean.Tensors.Tree.Elab
/-!
## The tensor structure for complex Lorentz tensors
-/
open IndexNotation
open CategoryTheory
open MonoidalCategory
open Matrix
open MatrixGroups
open Complex
open TensorProduct
open IndexNotation
open CategoryTheory
noncomputable section
namespace complexLorentzTensor
def upDown : Fin 2 → complexLorentzTensor.C
| 0 => Fermion.Color.up
| 1 => Fermion.Color.down
variable (T S : complexLorentzTensor.F.obj (OverColor.mk upDown))
#check {T | i i}ᵀ.dot
end complexLorentzTensor
end

36
HepLean/Tensors/ComplexLorentz/TensorStruct.lean Normal file
View file

@ -0,0 +1,36 @@
/-
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.Tensors.Tree.Basic
import HepLean.Tensors.ComplexLorentz.ColorFun
/-!
## The tensor structure for complex Lorentz tensors
-/
open IndexNotation
open CategoryTheory
open MonoidalCategory
open Matrix
open MatrixGroups
open Complex
open TensorProduct
open IndexNotation
open CategoryTheory
noncomputable section
def complexLorentzTensor : TensorStruct where
C := Fermion.Color
G := SL(2, ℂ)
G_group := inferInstance
k := ℂ
k_commRing := inferInstance
F := Fermion.colorFunMon
τ := Fermion.τ
evalNo := Fermion.evalNo
end

151
HepLean/Tensors/ColorCat/Basic.lean → HepLean/Tensors/OverColor/Basic.lean
View file

@ -13,7 +13,7 @@ import HepLean.SpaceTime.WeylFermion.Basic
import HepLean.SpaceTime.LorentzVector.Complex
/-!
## Over category.
## Over color category.
-/
@ -65,6 +65,16 @@ lemma toEquiv_comp_inv_apply (m : f ⟶ g) (i : g.left) :
f.hom ((OverColor.Hom.toEquiv m).symm i) = g.hom i := by
simpa [toEquiv, types_comp] using congrFun m.inv.w i
def toIso (m : f ⟶ g) : f ≅ g := {
hom := m,
inv := m.symm,
hom_inv_id := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
simp only [CategoryStruct.comp, Iso.self_symm_id, Iso.refl_hom, Over.id_left, types_id_apply]
rfl,
inv_hom_id := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
simp only [CategoryStruct.comp, Iso.symm_self_id, Iso.refl_hom, Over.id_left, types_id_apply]
rfl}
end Hom
section monoidal
@ -234,145 +244,6 @@ def mk (f : X → C) : OverColor C := Over.mk f
open MonoidalCategory
/-- The monoidal functor from `OverColor C` to `OverColor D` constructed from a map
`f : C → D`. -/
def map {C D : Type} (f : C → D) : MonoidalFunctor (OverColor C) (OverColor D) where
toFunctor := Core.functorToCore (Core.inclusion (Over C) ⋙ (Over.map f))
ε := Over.isoMk (Iso.refl _) (by
ext x
exact Empty.elim x)
μ X Y := Over.isoMk (Iso.refl _) (by
ext x
match x with
| Sum.inl x => rfl
| Sum.inr x => rfl)
μ_natural_left X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl x => rfl
| Sum.inr x => rfl
μ_natural_right X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl x => rfl
| Sum.inr x => rfl
associativity X Y Z := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl (Sum.inl x) => rfl
| Sum.inl (Sum.inr x) => rfl
| Sum.inr x => rfl
left_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl x => rfl
| Sum.inr x => rfl
right_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl x => rfl
| Sum.inr x => rfl
/-- The tensor product on `OverColor C` as a monoidal functor. -/
def tensor (C : Type) : MonoidalFunctor (OverColor C × OverColor C) (OverColor C) where
toFunctor := MonoidalCategory.tensor (OverColor C)
ε := Over.isoMk (Equiv.sumEmpty Empty Empty).symm.toIso (by
ext x
exact Empty.elim x)
μ X Y := Over.isoMk (Equiv.sumSumSumComm X.1.left X.2.left Y.1.left Y.2.left).toIso (by
ext x
match x with
| Sum.inl (Sum.inl x) => rfl
| Sum.inl (Sum.inr x) => rfl
| Sum.inr (Sum.inl x) => rfl
| Sum.inr (Sum.inr x) => rfl)
μ_natural_left X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl (Sum.inl x) => rfl
| Sum.inl (Sum.inr x) => rfl
| Sum.inr (Sum.inl x) => rfl
| Sum.inr (Sum.inr x) => rfl
μ_natural_right X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl (Sum.inl x) => rfl
| Sum.inl (Sum.inr x) => rfl
| Sum.inr (Sum.inl x) => rfl
| Sum.inr (Sum.inr x) => rfl
associativity X Y Z := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl (Sum.inl (Sum.inl x)) => rfl
| Sum.inl (Sum.inl (Sum.inr x)) => rfl
| Sum.inl (Sum.inr (Sum.inl x)) => rfl
| Sum.inl (Sum.inr (Sum.inr x)) => rfl
| Sum.inr (Sum.inl x) => rfl
| Sum.inr (Sum.inr x) => rfl
left_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl x => exact Empty.elim x
| Sum.inr (Sum.inl x)=> rfl
| Sum.inr (Sum.inr x)=> rfl
right_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl (Sum.inl x) => rfl
| Sum.inl (Sum.inr x) => rfl
| Sum.inr x => exact Empty.elim x
def diag (C : Type) : MonoidalFunctor (OverColor C) (OverColor C × OverColor C) :=
MonoidalFunctor.diag (OverColor C)
def const (C : Type) : MonoidalFunctor (OverColor C) (OverColor C) where
toFunctor := (Functor.const (OverColor C)).obj (𝟙_ (OverColor C))
ε := 𝟙 (𝟙_ (OverColor C))
μ _ _:= (λ_ (𝟙_ (OverColor C))).hom
μ_natural_left _ _ := by
simp only [Functor.const_obj_obj, Functor.const_obj_map, MonoidalCategory.whiskerRight_id,
Category.id_comp, Iso.hom_inv_id, Category.comp_id]
μ_natural_right _ _ := by
simp only [Functor.const_obj_obj, Functor.const_obj_map, MonoidalCategory.whiskerLeft_id,
Category.id_comp, Category.comp_id]
associativity X Y Z := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => by
match i with
| Sum.inl (Sum.inl i) => rfl
| Sum.inl (Sum.inr i) => rfl
| Sum.inr i => rfl
left_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => by
match i with
| Sum.inl i => exact Empty.elim i
| Sum.inr i => exact Empty.elim i
right_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => by
match i with
| Sum.inl i => exact Empty.elim i
| Sum.inr i => exact Empty.elim i
/-!
## Useful equivalences.
-/
/-- The isomorphism between `c : X → C` and `c ∘ e.symm` as objects in `OverColor C` for an
equivalence `e`. -/
def equivToIso {c : X → C} (e : X ≃ Y) : mk c ≅ mk (c ∘ e.symm) := {
hom := Over.isoMk e.toIso ((Iso.eq_inv_comp e.toIso).mp rfl),
inv := (Over.isoMk e.toIso ((Iso.eq_inv_comp e.toIso).mp rfl)).symm,
hom_inv_id := by
apply CategoryTheory.Iso.ext
erw [CategoryTheory.Iso.trans_hom]
simp only [Functor.id_obj, Over.mk_left, Over.mk_hom, Iso.symm_hom, Iso.hom_inv_id]
rfl,
inv_hom_id := by
apply CategoryTheory.Iso.ext
erw [CategoryTheory.Iso.trans_hom]
simp only [Iso.symm_hom, Iso.inv_hom_id]
rfl}
/-- The equivalence between `Fin n.succ` and `Fin 1 ⊕ Fin n` extracting the
`i`th component. -/
def finExtractOne {n : ℕ} (i : Fin n.succ) : Fin n.succ ≃ Fin 1 ⊕ Fin n :=
(finCongr (by omega : n.succ = i + 1 + (n - i))).trans <|
finSumFinEquiv.symm.trans <|
(Equiv.sumCongr (finSumFinEquiv.symm.trans (Equiv.sumComm (Fin i) (Fin 1)))
(Equiv.refl (Fin (n-i)))).trans <|
(Equiv.sumAssoc (Fin 1) (Fin i) (Fin (n - i))).trans <|
Equiv.sumCongr (Equiv.refl (Fin 1)) (finSumFinEquiv.trans (finCongr (by omega)))
end OverColor
end IndexNotation

128
HepLean/Tensors/OverColor/Functors.lean Normal file
View file

@ -0,0 +1,128 @@
/-
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.Tensors.OverColor.Basic
/-!
## Functors related to the OverColor category
-/
namespace IndexNotation
namespace OverColor
open CategoryTheory
open MonoidalCategory
/-- The monoidal functor from `OverColor C` to `OverColor D` constructed from a map
`f : C → D`. -/
def map {C D : Type} (f : C → D) : MonoidalFunctor (OverColor C) (OverColor D) where
toFunctor := Core.functorToCore (Core.inclusion (Over C) ⋙ (Over.map f))
ε := Over.isoMk (Iso.refl _) (by
ext x
exact Empty.elim x)
μ X Y := Over.isoMk (Iso.refl _) (by
ext x
match x with
| Sum.inl x => rfl
| Sum.inr x => rfl)
μ_natural_left X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl x => rfl
| Sum.inr x => rfl
μ_natural_right X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl x => rfl
| Sum.inr x => rfl
associativity X Y Z := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl (Sum.inl x) => rfl
| Sum.inl (Sum.inr x) => rfl
| Sum.inr x => rfl
left_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl x => rfl
| Sum.inr x => rfl
right_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl x => rfl
| Sum.inr x => rfl
/-- The tensor product on `OverColor C` as a monoidal functor. -/
def tensor (C : Type) : MonoidalFunctor (OverColor C × OverColor C) (OverColor C) where
toFunctor := MonoidalCategory.tensor (OverColor C)
ε := Over.isoMk (Equiv.sumEmpty Empty Empty).symm.toIso (by
ext x
exact Empty.elim x)
μ X Y := Over.isoMk (Equiv.sumSumSumComm X.1.left X.2.left Y.1.left Y.2.left).toIso (by
ext x
match x with
| Sum.inl (Sum.inl x) => rfl
| Sum.inl (Sum.inr x) => rfl
| Sum.inr (Sum.inl x) => rfl
| Sum.inr (Sum.inr x) => rfl)
μ_natural_left X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl (Sum.inl x) => rfl
| Sum.inl (Sum.inr x) => rfl
| Sum.inr (Sum.inl x) => rfl
| Sum.inr (Sum.inr x) => rfl
μ_natural_right X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl (Sum.inl x) => rfl
| Sum.inl (Sum.inr x) => rfl
| Sum.inr (Sum.inl x) => rfl
| Sum.inr (Sum.inr x) => rfl
associativity X Y Z := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl (Sum.inl (Sum.inl x)) => rfl
| Sum.inl (Sum.inl (Sum.inr x)) => rfl
| Sum.inl (Sum.inr (Sum.inl x)) => rfl
| Sum.inl (Sum.inr (Sum.inr x)) => rfl
| Sum.inr (Sum.inl x) => rfl
| Sum.inr (Sum.inr x) => rfl
left_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl x => exact Empty.elim x
| Sum.inr (Sum.inl x)=> rfl
| Sum.inr (Sum.inr x)=> rfl
right_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl (Sum.inl x) => rfl
| Sum.inl (Sum.inr x) => rfl
| Sum.inr x => exact Empty.elim x
def diag (C : Type) : MonoidalFunctor (OverColor C) (OverColor C × OverColor C) :=
MonoidalFunctor.diag (OverColor C)
def const (C : Type) : MonoidalFunctor (OverColor C) (OverColor C) where
toFunctor := (Functor.const (OverColor C)).obj (𝟙_ (OverColor C))
ε := 𝟙 (𝟙_ (OverColor C))
μ _ _:= (λ_ (𝟙_ (OverColor C))).hom
μ_natural_left _ _ := by
simp only [Functor.const_obj_obj, Functor.const_obj_map, MonoidalCategory.whiskerRight_id,
Category.id_comp, Iso.hom_inv_id, Category.comp_id]
μ_natural_right _ _ := by
simp only [Functor.const_obj_obj, Functor.const_obj_map, MonoidalCategory.whiskerLeft_id,
Category.id_comp, Category.comp_id]
associativity X Y Z := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => by
match i with
| Sum.inl (Sum.inl i) => rfl
| Sum.inl (Sum.inr i) => rfl
| Sum.inr i => rfl
left_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => by
match i with
| Sum.inl i => exact Empty.elim i
| Sum.inr i => exact Empty.elim i
right_unitality X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => by
match i with
| Sum.inl i => exact Empty.elim i
| Sum.inr i => exact Empty.elim i
def contrPair (C : Type) (τ : C → C) : MonoidalFunctor (OverColor C) (OverColor C) :=
OverColor.diag C
⊗⋙ (MonoidalFunctor.prod (MonoidalFunctor.id (OverColor C)) (OverColor.map τ))
⊗⋙ OverColor.tensor C
end OverColor
end IndexNotation

163
HepLean/Tensors/OverColor/Iso.lean Normal file
View file

@ -0,0 +1,163 @@
/-
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.Tensors.OverColor.Functors
/-!
## Isomorphisms in the OverColor category
-/
namespace IndexNotation
namespace OverColor
open CategoryTheory
open MonoidalCategory
/-!
## Useful equivalences.
-/
/-- The isomorphism between `c : X → C` and `c ∘ e.symm` as objects in `OverColor C` for an
equivalence `e`. -/
def equivToIso {c : X → C} (e : X ≃ Y) : mk c ≅ mk (c ∘ e.symm) :=
Hom.toIso (Over.isoMk e.toIso ((Iso.eq_inv_comp e.toIso).mp rfl))
def mkSum (c : X ⊕ Y → C) : mk c ≅ mk (c ∘ Sum.inl) ⊗ mk (c ∘ Sum.inr) :=
Hom.toIso (Over.isoMk (Equiv.refl _).toIso (by
ext x
match x with
| Sum.inl x => rfl
| Sum.inr x => rfl))
def mkIso {c1 c2 : X → C} (h : c1 = c2) : mk c1 ≅ mk c2 :=
Hom.toIso (Over.isoMk (Equiv.refl _).toIso (by
subst h
rfl))
/-- The equivalence between `Fin n.succ` and `Fin 1 ⊕ Fin n` extracting the
`i`th component. -/
def finExtractOne {n : ℕ} (i : Fin n.succ) : Fin n.succ ≃ Fin 1 ⊕ Fin n :=
(finCongr (by omega : n.succ = i + 1 + (n - i))).trans <|
finSumFinEquiv.symm.trans <|
(Equiv.sumCongr (finSumFinEquiv.symm.trans (Equiv.sumComm (Fin i) (Fin 1)))
(Equiv.refl (Fin (n-i)))).trans <|
(Equiv.sumAssoc (Fin 1) (Fin i) (Fin (n - i))).trans <|
Equiv.sumCongr (Equiv.refl (Fin 1)) (finSumFinEquiv.trans (finCongr (by omega)))
lemma finExtractOne_symm_inr {n : ℕ} (i : Fin n.succ) :
(finExtractOne i).symm ∘ Sum.inr = i.succAbove := by
ext x
simp only [Nat.succ_eq_add_one, finExtractOne, Function.comp_apply, Equiv.symm_trans_apply,
finCongr_symm, Equiv.symm_symm, Equiv.sumCongr_symm, Equiv.refl_symm, Equiv.sumCongr_apply,
Equiv.coe_refl, Sum.map_inr, finCongr_apply, Fin.coe_cast]
change (finSumFinEquiv (Sum.map (⇑(finSumFinEquiv.symm.trans (Equiv.sumComm (Fin ↑i) (Fin 1))).symm) id
((Equiv.sumAssoc (Fin 1) (Fin ↑i) (Fin (n - i))).symm (Sum.inr (finSumFinEquiv.symm (Fin.cast (finExtractOne.proof_2 i).symm x)))))).val = _
by_cases hi : x.1 < i.1
· have h1 : (finSumFinEquiv.symm (Fin.cast (finExtractOne.proof_2 i).symm x)) =
Sum.inl ⟨x, hi⟩ := by
rw [← finSumFinEquiv_symm_apply_castAdd]
apply congrArg
ext
simp
rw [h1]
simp only [Nat.succ_eq_add_one, Equiv.sumAssoc_symm_apply_inr_inl, Sum.map_inl,
Equiv.symm_trans_apply, Equiv.symm_symm, Equiv.sumComm_symm, Equiv.sumComm_apply,
Sum.swap_inr, finSumFinEquiv_apply_left, Fin.castAdd_mk]
rw [Fin.succAbove]
split
· rfl
rename_i hn
simp_all only [Nat.succ_eq_add_one, not_lt, Fin.le_def, Fin.coe_castSucc, Fin.val_succ,
self_eq_add_right, one_ne_zero]
omega
· have h1 : (finSumFinEquiv.symm (Fin.cast (finExtractOne.proof_2 i).symm x)) =
Sum.inr ⟨x - i, by omega⟩ := by
rw [← finSumFinEquiv_symm_apply_natAdd]
apply congrArg
ext
simp
omega
rw [h1, Fin.succAbove]
split
· rename_i hn
simp_all [Fin.lt_def]
simp only [Nat.succ_eq_add_one, Equiv.sumAssoc_symm_apply_inr_inr, Sum.map_inr, id_eq,
finSumFinEquiv_apply_right, Fin.natAdd_mk, Fin.val_succ]
omega
@[simp]
lemma finExtractOne_symm_inr_apply {n : ℕ} (i : Fin n.succ) (x : Fin n) :
(finExtractOne i).symm (Sum.inr x) = i.succAbove x := calc
_ = ((finExtractOne i).symm ∘ Sum.inr) x := rfl
_ = i.succAbove x := by rw [finExtractOne_symm_inr]
@[simp]
lemma finExtractOne_symm_inl_apply {n : ℕ} (i : Fin n.succ) :
(finExtractOne i).symm (Sum.inl 0) = i := by
simp only [Nat.succ_eq_add_one, finExtractOne, Fin.isValue, Equiv.symm_trans_apply, finCongr_symm,
Equiv.symm_symm, Equiv.sumCongr_symm, Equiv.refl_symm, Equiv.sumCongr_apply, Equiv.coe_refl,
Sum.map_inl, id_eq, Equiv.sumAssoc_symm_apply_inl, Equiv.sumComm_symm, Equiv.sumComm_apply,
Sum.swap_inl, finSumFinEquiv_apply_right, finSumFinEquiv_apply_left, finCongr_apply]
ext
rfl
def finExtractTwo {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
Fin n.succ.succ ≃ (Fin 1 ⊕ Fin 1) ⊕ Fin n :=
(finExtractOne i).trans <|
(Equiv.sumCongr (Equiv.refl (Fin 1)) (finExtractOne j)).trans <|
(Equiv.sumAssoc (Fin 1) (Fin 1) (Fin n)).symm
lemma finExtractTwo_symm_inr {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
(finExtractTwo i j).symm ∘ Sum.inr = i.succAbove ∘ j.succAbove := by
rw [finExtractTwo]
ext1 x
simp
@[simp]
lemma finExtractTwo_symm_inr_apply {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) (x : Fin n) :
(finExtractTwo i j).symm (Sum.inr x) = i.succAbove (j.succAbove x) := by
rw [finExtractTwo]
simp
@[simp]
lemma finExtractTwo_symm_inl_inr_apply {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
(finExtractTwo i j).symm (Sum.inl (Sum.inr 0)) = i.succAbove j := by
rw [finExtractTwo]
simp
@[simp]
lemma finExtractTwo_symm_inl_inl_apply {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
(finExtractTwo i j).symm (Sum.inl (Sum.inl 0)) = i := by
rw [finExtractTwo]
simp
def contrPairFin1Fin1 (τ : C → C) (c : Fin 1 ⊕ Fin 1 → C)
(h : c (Sum.inr 0) = τ (c (Sum.inl 0))) :
OverColor.mk c ≅ (contrPair C τ).obj (OverColor.mk (fun (_ : Fin 1) => c (Sum.inl 0))) :=
Hom.toIso (Over.isoMk (Equiv.refl _).toIso (by
ext x
match x with
| Sum.inl x =>
fin_cases x
rfl
| Sum.inr x =>
fin_cases x
change _ = c (Sum.inr 0)
rw [h]
rfl))
def contrPairEquiv {n : ℕ} (τ : C → C) (c : Fin n.succ.succ → C) (i : Fin n.succ.succ)
(j : Fin n.succ) (h : c (i.succAbove j) = τ (c i)) :
OverColor.mk c ≅ ((contrPair C τ).obj (Over.mk (fun (_ : Fin 1) => c i))) ⊗
(OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)) :=
(equivToIso (finExtractTwo i j)).trans <|
(OverColor.mkSum (c ∘ ⇑(finExtractTwo i j).symm)).trans <|
tensorIso
(contrPairFin1Fin1 τ ((c ∘ ⇑(finExtractTwo i j).symm) ∘ Sum.inl) (by simpa using h)) <|
mkIso (by ext x; simp)
end OverColor
end IndexNotation

15
HepLean/Tensors/Tree/Basic.lean
View file

@ -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.Tensors.ColorCat.Basic
import HepLean.Tensors.OverColor.Iso
import Mathlib.CategoryTheory.Monoidal.NaturalTransformation
/-!
@ -34,12 +34,9 @@ structure TensorStruct where
F : MonoidalFunctor (OverColor C) (Rep k G)
/-- A map from `C` to `C`. An involution. -/
τ : C → C
/-- Contraction natural transformation. -/
ηContr : (OverColor.diag C) ⊗⋙ (MonoidalFunctor.prod (MonoidalFunctor.id (OverColor C)) (OverColor.map τ))
⊗⋙ OverColor.tensor C ⊗⋙ F ⟶ @constMonoFunc (OverColor C) G k
/-- A monoidal natural isomorphism from OverColor.map τ ⊗⋙ F to F.
This will allow us to, for example, rise and lower indices. -/
dual : (OverColor.map τ ⊗⋙ F) ≅ F
/-
μContr : OverColor.contrPair C τ ⊗⋙ F ⟶ OverColor.const C ⊗⋙ F
dual : (OverColor.map τ ⊗⋙ F) ≅ F-/
/-- A specification of the dimension of each color in C. This will be used for explicit
evaluation of tensors. -/
evalNo : C → ℕ
@ -67,7 +64,7 @@ inductive TensorTree (S : TensorStruct) : ∀ {n : ℕ}, (Fin n → S.C) → Typ
(i : Fin n.succ) → (j : Fin m.succ) → TensorTree S c → TensorTree S c1 →
TensorTree S (Sum.elim (c ∘ Fin.succAbove i) (c1 ∘ Fin.succAbove j) ∘ finSumFinEquiv.symm)
| contr {n : ℕ} {c : Fin n.succ.succ → S.C} : (i : Fin n.succ.succ) →
(j : Fin n.succ) → TensorTree S c → TensorTree S (c ∘ Fin.succAbove i ∘ Fin.succAbove j)
(j : Fin n.succ) → (h : c (i.succAbove j) = S.τ (c i)) → TensorTree S c → TensorTree S (c ∘ Fin.succAbove i ∘ Fin.succAbove j)
| jiggle {n : ℕ} {c : Fin n → S.C} : (i : Fin n) → TensorTree S c →
TensorTree S (Function.update c i (S.τ (c i)))
| eval {n : ℕ} {c : Fin n.succ → S.C} :
@ -89,7 +86,7 @@ def size : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → ℕ := fun
| smul _ t => t.size + 1
| prod t1 t2 => t1.size + t2.size + 1
| mult _ _ t1 t2 => t1.size + t2.size + 1
| contr _ _ t => t.size + 1
| contr _ _ _ t => t.size + 1
| jiggle _ t => t.size + 1
| eval _ _ t => t.size + 1

2
HepLean/Tensors/Tree/Dot.lean
View file

@ -53,7 +53,7 @@ def dotString (m : ℕ) (nt : ℕ) : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTr
let jiggleNode := " node" ++ toString m ++ " [label=\"τ\", shape=box];\n"
let edge1 := " node" ++ toString m ++ " -> node" ++ toString (m + 1) ++ ";\n"
jiggleNode ++ dotString (m + 1) nt t1 ++ edge1
| contr i j t1 =>
| contr i j _ t1 =>
let contrNode := " node" ++ toString m ++ " [label=\"contr " ++ toString i ++ " "
++ toString j ++ "\", shape=box];\n"
let edge1 := " node" ++ toString m ++ " -> node" ++ toString (m + 1) ++ ";\n"

4
HepLean/Tensors/Tree/Elab.lean
View file

@ -192,7 +192,7 @@ def withoutContr (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := do
/-- For each element of `l : List (ℕ × ℕ)` applies `TensorTree.contr` to the given term. -/
def contrSyntax (l : List (ℕ × ℕ)) (T : Term) : Term :=
l.foldl (fun T' (x0, x1) => Syntax.mkApp (mkIdent ``TensorTree.contr)
#[Syntax.mkNumLit (toString x1), Syntax.mkNumLit (toString x0), T']) T
#[Syntax.mkNumLit (toString x1), Syntax.mkNumLit (toString x0), mkIdent ``rfl, T']) T
/-- Creates the syntax associated with a tensor node. -/
def syntaxFull (stx : Syntax) : TermElabM Term := do
@ -256,7 +256,7 @@ def withoutContr (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := do
/-- For each element of `l : List (ℕ × ℕ)` applies `TensorTree.contr` to the given term. -/
def contrSyntax (l : List (ℕ × ℕ)) (T : Term) : Term :=
l.foldl (fun T' (x0, x1) => Syntax.mkApp (mkIdent ``TensorTree.contr)
#[Syntax.mkNumLit (toString x1), Syntax.mkNumLit (toString x0), T']) T
#[Syntax.mkNumLit (toString x1), Syntax.mkNumLit (toString x0), mkIdent ``rfl, T']) T
/-- The syntax associated with a product of tensors. -/
def prodSyntax (T1 T2 : Term) : Term :=