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

feat: Add OverColor const and diag

Browse source
This commit is contained in:
jstoobysmith 2024-10-09 16:57:41 +00:00
parent 1a5bff7254
commit e90e41751e
2 changed files with 34 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -269,7 +269,7 @@ def map {C D : Type} (f : C → D) : MonoidalFunctor (OverColor C) (OverColor D)
| Sum.inr x => rfl
/-- The tensor product on `OverColor C` as a monoidal functor. -/
def tensor : MonoidalFunctor (OverColor C × OverColor C) (OverColor C) where
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
@ -312,6 +312,35 @@ def tensor : MonoidalFunctor (OverColor C × OverColor C) (OverColor C) where
| 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.

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

@ -13,6 +13,7 @@ import Mathlib.CategoryTheory.Monoidal.NaturalTransformation
open IndexNotation
open CategoryTheory
open MonoidalCategory
/-- The sturcture of a type of tensors e.g. Lorentz tensors, Einstien tensors,
complex Lorentz tensors.
@ -33,6 +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