From 3890095a17b3b0ea2e082daeef919593a1646bd1 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 3 Jul 2024 16:38:56 -0400 Subject: [PATCH] feat: add properties of graphical species --- HepLean/SpaceTime/LorentzTensor/Basic.lean | 1 + .../LorentzTensor/GraphicalSpecies.lean | 156 +++++++++++++++++- 2 files changed, 156 insertions(+), 1 deletion(-) diff --git a/HepLean/SpaceTime/LorentzTensor/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Basic.lean index 42bdcfb..a02edc4 100644 --- a/HepLean/SpaceTime/LorentzTensor/Basic.lean +++ b/HepLean/SpaceTime/LorentzTensor/Basic.lean @@ -83,4 +83,5 @@ noncomputable def graphicalSpecies (d : ℕ) : GraphicalSpecies where | ⟨as x⟩, ⟨𝓣⟩, ⟨𝓣⟩, _, _ => rfl | ⟨as x⟩, ⟨as y⟩, ⟨𝓣⟩, _, _ => rfl + end LorentzTensor diff --git a/HepLean/SpaceTime/LorentzTensor/GraphicalSpecies.lean b/HepLean/SpaceTime/LorentzTensor/GraphicalSpecies.lean index e015707..e756308 100644 --- a/HepLean/SpaceTime/LorentzTensor/GraphicalSpecies.lean +++ b/HepLean/SpaceTime/LorentzTensor/GraphicalSpecies.lean @@ -5,6 +5,12 @@ Authors: Joseph Tooby-Smith -/ import Mathlib.CategoryTheory.FintypeCat import Mathlib.Tactic.FinCases +import Mathlib.Data.PFun +import Mathlib.Data.Fintype.Sum +import Mathlib.CategoryTheory.Limits.FintypeCat +import Mathlib.CategoryTheory.Core +import Mathlib.CategoryTheory.Limits.Shapes.Types +import LeanCopilot /-! # Graphical species @@ -113,7 +119,155 @@ instance : Category elGr where | as d, as c, as b, as a, f, g, h => simp only [Hom.comp, Iso.trans_assoc] +def ch {X : FintypeCat} (x : X) : Hom 𝓣 (as X) := (x, 0) + +def τ : Hom 𝓣 𝓣 := 1 + +@[simp] +lemma τ_comp_self : τ ≫ τ = 𝟙 𝓣 := rfl + +def coreFintypeIncl : Core FintypeCat ⥤ elGr where + obj X := as X + map f := f + +noncomputable def fintypeCoprod (X Y : FintypeCat) : elGr := as (X ⨿ Y) + +noncomputable def fintypeCoprodTerm (X : FintypeCat) : elGr := fintypeCoprod X (⊤_ FintypeCat) + +example : CategoryTheory.Functor.ReflectsIsomorphisms FintypeCat.incl := by + exact reflectsIsomorphisms_of_full_and_faithful FintypeCat.incl + + +def terminalLimitCone : Limits.LimitCone (Functor.empty (FintypeCat)) where + cone := + { pt := FintypeCat.of PUnit + π := (Functor.uniqueFromEmpty _).hom} + isLimit := { + lift := fun _ _ => PUnit.unit + fac := fun _ => by rintro ⟨⟨⟩⟩ + uniq := fun _ _ _ => by + funext + rfl} + +noncomputable def isoToTerm : (⊤_ FintypeCat) ≅ FintypeCat.of PUnit := + CategoryTheory.Limits.limit.isoLimitCone terminalLimitCone + +noncomputable def objTerm : (⊤_ FintypeCat) := isoToTerm.inv PUnit.unit + +noncomputable def starObj (X : FintypeCat) : (X ⨿ (⊤_ FintypeCat) : FintypeCat) := + (@Limits.coprod.inr _ _ X (⊤_ FintypeCat) _) objTerm + +/- TODO: derive this from `CategoryTheory.Limits.coprod.functor`. -/ +noncomputable def coprodCore : Core FintypeCat × Core FintypeCat ⥤ Core FintypeCat where + obj := fun (X, Y) => (X ⨿ Y : FintypeCat) + map f := CategoryTheory.Limits.coprod.mapIso f.1 f.2 + map_id := by + intro X + simp [Limits.coprod.mapIso] + trans + · rfl + · aesop_cat + map_comp := by + intro X Y Z f g + simp_all only [prod_Hom, prod_comp] + obtain ⟨fst, snd⟩ := X + obtain ⟨fst_1, snd_1⟩ := Y + obtain ⟨fst_2, snd_2⟩ := Z + simp_all only + dsimp [Limits.coprod.mapIso] + congr + · simp_all only [Limits.coprod.map_map] + · simp_all only [Limits.coprod.map_map] + apply Eq.refl + + end elGr +open elGr + /-- The category of graphical species. -/ -abbrev GraphicalSpecies := elGrᵒᵖ ⥤ Type +abbrev GraphicalSpecies := elGrᵒᵖ ⥤ Type + +namespace GraphicalSpecies + +variable (S : GraphicalSpecies) + +abbrev colors := S.obj ⟨𝓣⟩ + +def MatchColours (X Y : FintypeCat) : Type := + Subtype fun (R : S.obj ⟨as (X ⨿ (⊤_ FintypeCat))⟩ × S.obj ⟨as (Y ⨿ (⊤_ FintypeCat))⟩) ↦ + S.map (Quiver.Hom.op $ ch (elGr.starObj X)) R.1 = + S.map (Quiver.Hom.op $ τ ≫ ch (elGr.starObj Y)) R.2 + + +/-- Given two finite types `X` and `Y`, the objects + of `S.obj ⟨elGr.as X⟩ × S.obj ⟨elGr.as Y⟩` which on `x ∈ X` and `y ∈ Y` map to dual colors. -/ +def MatchColor {X Y : FintypeCat} (x : X) (y : Y) : Type := + Subtype fun (R : S.obj ⟨elGr.as X⟩ × S.obj ⟨elGr.as Y⟩) ↦ + S.map (Quiver.Hom.op (ch x)) R.1 = S.map (Quiver.Hom.op (τ ≫ ch y)) R.2 + +/-- An element of `S.MatchColor y x ` given an element of `S.MatchColor x y`. -/ +def matchColorSwap {X Y : FintypeCat} {x : X} {y : Y} (R : S.MatchColor x y) : S.MatchColor y x := + ⟨(R.val.2, R.val.1), by + have hS := congrArg (S.map (Quiver.Hom.op τ)) R.2 + rw [← FunctorToTypes.map_comp_apply, ← FunctorToTypes.map_comp_apply] at hS + rw [← op_comp, ← op_comp, ← Category.assoc] at hS + simpa using hS.symm⟩ + +def matchColorCongrLeft {X Y Z : FintypeCat} (f : X ≅ Z) {x : X} {y : Y} (R : S.MatchColor (f.hom x) y) : + S.MatchColor x y := + ⟨(S.map (Quiver.Hom.op $ Hom.as f) R.val.1, R.val.2), by + rw [← R.2, ← FunctorToTypes.map_comp_apply, ← op_comp] + rfl⟩ + +def matchColorCongrRight {X Y Z : FintypeCat} (f : Y ≅ Z) {x : X} {y : Y} (R : S.MatchColor x (f.hom y)) : + S.MatchColor x y := + ⟨(R.val.1, S.map (Quiver.Hom.op $ Hom.as f) R.val.2), by + rw [R.2, ← FunctorToTypes.map_comp_apply, ← op_comp] + rfl⟩ + +def matchColorCongr {X Y Z W : FintypeCat} (f : X ≅ W) (g : Y ≅ Z) {x : X} {y : Y} + (R : S.MatchColor (f.hom x) (g.hom y)) : S.MatchColor x y := + S.matchColorCongrLeft f (S.matchColorCongrRight g R) + +def matchColorIndexCongrLeft {X Y : FintypeCat} {x x' : X} {y : Y} (h : x = x') (R : S.MatchColor x y) : + S.MatchColor x' y := + ⟨(R.val.1, R.val.2), by + subst h + exact R.2⟩ + +def MatchColorFin (X Y : FintypeCat) : Type := + @MatchColor S (FintypeCat.of $ X ⊕ Fin 1) (FintypeCat.of $ Y ⊕ Fin 1) (Sum.inr 0) (Sum.inr 0) + +def matchColorFinCongrLeft {X Y Z : FintypeCat} (f : X ≅ W) (R : S.MatchColorFin X Y) : + S.MatchColorFin W Z := by + + let f' : FintypeCat.of (X ⊕ Fin 1) ≅ FintypeCat.of (W ⊕ Fin 1) := + FintypeCat.equivEquivIso $ Equiv.sumCongr (FintypeCat.equivEquivIso.symm f) + (FintypeCat.equivEquivIso.symm (Iso.refl (Fin 1))) + let x := @matchColorCongrLeft S _ (FintypeCat.of (Y ⊕ Fin 1)) _ f' (Sum.inr 0) (Sum.inr 0) R + +end GraphicalSpecies + +structure MulGraphicalSpecies where + toGraphicalSpecies : GraphicalSpecies + mul : ∀ {X Y : FintypeCat}, + toGraphicalSpecies.MatchColorFin X Y → toGraphicalSpecies.obj + ⟨elGr.as (FintypeCat.of (X ⊕ Y))⟩ + comm : ∀ {X Y : FintypeCat} {x : X} {y : Y} (R : toGraphicalSpecies.MatchColorFin X Y), + mul R = toGraphicalSpecies.map (fintypeCoprodSwap X Y).op + (mul (toGraphicalSpecies.matchColorSwap R)) + equivariance : ∀ {X Y Z W : FintypeCat} (f : X ≃ W) (g : Y ≃ Z) {x : X} {y : Y} + (R : toGraphicalSpecies.MatchColor (f x) (g y)), + toGraphicalSpecies.map (fintypeCoprodMap f g).op (mul R) = + mul (toGraphicalSpecies.matchColorCongr f g R) + +namespace MulGraphicalSpecies + +variable (S : MulGraphicalSpecies) + +def obj := S.toGraphicalSpecies.obj + +def map {X Y : elGrᵒᵖ} (f : X ⟶ Y) : S.obj X ⟶ S.obj Y := S.toGraphicalSpecies.map f + +end MulGraphicalSpecies