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

feat: Add properties of dualization of indices

Browse source
This commit is contained in:
jstoobysmith 2024-10-09 07:42:56 +00:00
parent 0e3f4cb048
commit 175d39a271
2 changed files with 98 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

95
HepLean/Tensors/ColorCat/Basic.lean
View file

@ -230,6 +230,92 @@ 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
def emptyEquiv (X1 X2 Y1 Y2 : Type): (X1 ⊕ X2) ⊕ (Y1 ⊕ Y2) ≃ (X1 ⊕ Y1) ⊕ (X2 ⊕ Y2) := by
exact Equiv.sumSumSumComm X1 X2 Y1 Y2
def tensor : 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
/-!
## 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) := {
@ -246,6 +332,15 @@ def equivToIso {c : X → C} (e : X ≃ Y) : mk c ≅ mk (c ∘ e.symm) := {
simp only [Iso.symm_hom, Iso.inv_hom_id]
rfl}
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

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

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Tensors.ColorCat.Basic
import Mathlib.CategoryTheory.Monoidal.NaturalTransformation
/-!
## Tensor trees
@ -32,6 +33,8 @@ structure TensorStruct where
F : MonoidalFunctor (OverColor C) (Rep k G)
/-- A map from `C` to `C`. An involution. -/
τ : C → C
/-- A monoidal natural isomorphism from OverColor.map τ ⋙ F to F. -/
dual : MonoidalNatIso (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 → ℕ