feat: def of graphical species

HepLean/SpaceTime/LorentzTensor/Basic.lean

@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.SpaceTime.LorentzTensor.GraphicalSpecies
+import HepLean.SpaceTime.LorentzVector.Basic
+/-!
+
+# Lorentz Tensors
+
+This file is currently a work-in-progress.
+
+The aim is to define Lorentz tensors, and devlop a systematic way to manipulate them.
+
+To manipulate them we will use the theory of modular operads
+(see e.g. [Raynor][raynor2021graphical]).
+
+
+-/
+
+/-- A Lorentz Tensor defined by its coordinate map. -/
+def LorentzTensor (d : ℕ) (X : FintypeCat) : Type :=
+  (X → Fin 1 ⊕ Fin d) → ℝ
+
+/-- An instance of a additive commutative monoid on `LorentzTensor`. -/
+instance (d : ℕ) (X : FintypeCat)  : AddCommMonoid (LorentzTensor d X) := Pi.addCommMonoid
+
+/-- An instance of a module on `LorentzVector`. -/
+noncomputable instance (d : ℕ) (X : FintypeCat)  : Module ℝ (LorentzTensor d X) := Pi.module _ _ _
+
+namespace LorentzTensor
+open BigOperators
+open elGr
+open CategoryTheory
+
+variable {d : ℕ} {X Y : FintypeCat}
+
+/-- The map taking a list of `LorentzVector d` indexed by `X` to a ` LorentzTensor d X`. -/
+def tmul (t : X → LorentzVector d) : LorentzTensor d X :=
+  fun f => ∏ x, (t x) (f x)
+
+/- An equivalence between `X → Fin 1 ⊕ Fin d` and `Y → Fin 1 ⊕ Fin d` given an isomorphism
+  between `X` and `Y`. -/
+def indexEquivOfIndexHom (f : X ≅ Y) : (X → Fin 1 ⊕ Fin d) ≃ (Y → Fin 1 ⊕ Fin d)  :=
+  Equiv.piCongrLeft' _ (FintypeCat.equivEquivIso.symm f)
+
+/-- Given an isomorphism of indexing sets, a linear equivalence on Lorentz tensors. -/
+noncomputable def mapOfIndexHom (f : X ≅ Y) :  LorentzTensor d Y ≃ₗ[ℝ] LorentzTensor d X :=
+  LinearEquiv.piCongrLeft' ℝ _ (indexEquivOfIndexHom f).symm
+
+/-!
+
+## Graphical species and Lorentz tensors
+
+-/
+
+/-- The graphical species defined by Lorentz tensors.
+
+For this simple case, 𝓣 gets mapped to `PUnit`, if one wishes to include fermions etc,
+then `PUnit` will change to account for the colouring of edges. -/
+noncomputable def graphicalSpecies (d : ℕ) : GraphicalSpecies where
+  obj x :=
+    match x with
+    | ⟨𝓣⟩ => PUnit
+    | ⟨as f⟩ => LorentzTensor d f
+  map {x y} f :=
+    match x, y, f with
+    | ⟨𝓣⟩, ⟨𝓣⟩, _ => 𝟙 PUnit
+    | ⟨𝓣⟩, ⟨as x⟩, ⟨f⟩ => Empty.elim f
+    | ⟨as f⟩, ⟨𝓣⟩, _ => fun _ => PUnit.unit
+    | ⟨as f⟩, ⟨as g⟩, ⟨h⟩ => (mapOfIndexHom h).toEquiv.toFun
+  map_id X := by
+    match X with
+    | ⟨𝓣⟩ => rfl
+    | ⟨as f⟩ => rfl
+  map_comp {x y z} f g := by
+    match x, y, z, f, g with
+    | ⟨𝓣⟩, ⟨𝓣⟩, ⟨𝓣⟩, _, _ => rfl
+    | _, ⟨𝓣⟩, ⟨as _⟩, _, ⟨g⟩ => exact Empty.elim g
+    | ⟨𝓣⟩, ⟨as _⟩, _, ⟨f⟩, _ =>  exact Empty.elim f
+    | ⟨as x⟩, ⟨as y⟩, ⟨as z⟩, ⟨f⟩, ⟨g⟩ => rfl
+    | ⟨as x⟩, ⟨𝓣⟩, ⟨𝓣⟩, _, _ => rfl
+    | ⟨as x⟩, ⟨as y⟩, ⟨𝓣⟩, _, _ => rfl
+
+end LorentzTensor

HepLean/SpaceTime/LorentzTensor/GraphicalSpecies.lean

@@ -0,0 +1,119 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import Mathlib.CategoryTheory.FintypeCat
+import Mathlib.Tactic.FinCases
+/-!
+
+# Graphical species
+
+We define the general notion of a graphical species.
+This will be used to define contractions of Lorentz tensors.
+
+## References
+
+- [Raynor][raynor2021graphical]
+- https://arxiv.org/pdf/1906.01144 (TODO: add to references)
+
+-/
+
+open CategoryTheory
+
+/-- Finite types adjoined with a distinguished object. -/
+inductive elGr where
+  | 𝓣
+  | as (f : FintypeCat)
+
+namespace elGr
+
+/-- The morphism sets between elements of `elGr`. -/
+def Hom (a b : elGr) : Type :=
+  match a, b with
+  | 𝓣, 𝓣 => Fin 2
+  | 𝓣, as f => f × Fin 2
+  | as _, 𝓣 => Empty
+  | as f, as g => f ≅ g
+
+instance : OfNat (Hom 𝓣 𝓣) 0 := ⟨(0 : Fin 2)⟩
+
+instance : OfNat (Hom 𝓣 𝓣) 1 := ⟨(1 : Fin 2)⟩
+
+
+namespace Hom
+
+/-- The identity morphism. -/
+@[simp]
+def id (a : elGr) : Hom a a :=
+  match a with
+  | 𝓣 => 0
+  | as f => Iso.refl f
+
+/-- The composition of two morphisms. -/
+@[simp]
+def comp {a b c : elGr} (f : Hom a b) (g : Hom b c) : Hom a c :=
+  match a, b, c, f, g with
+  | 𝓣, 𝓣, 𝓣, 0, 0 => 0
+  | 𝓣, 𝓣, 𝓣, 0, 1 => 1
+  | 𝓣, 𝓣, 𝓣, 1, 0 => 1
+  | 𝓣, 𝓣, 𝓣, 1, 1 => 0
+  | 𝓣, as _, 𝓣, _, g => Empty.elim g
+  | 𝓣, 𝓣, as _fakeMod, 0, (g, 0) => (g, 0)
+  | 𝓣, 𝓣, as _, 0, (g, 1) => (g, 1)
+  | 𝓣, 𝓣, as _, 1, (g, 0) => (g, 1)
+  | 𝓣, 𝓣, as _, 1, (g, 1) => (g, 0)
+  | 𝓣, as _, as _, (f, 0), g => (g.hom f, 0)
+  | 𝓣, as _, as _, (f, 1), g => (g.hom f, 1)
+  | as _, as _, as _, f, g => f ≪≫ g
+
+instance : Fintype (Hom 𝓣 𝓣) := Fin.fintype 2
+
+end Hom
+
+/-- The category of elementary graphs. -/
+instance : Category elGr where
+  Hom := Hom
+  id := Hom.id
+  comp := Hom.comp
+  id_comp := by
+    intro X Y f
+    match X, Y, f with
+    | 𝓣, 𝓣, (0 : Fin 2) => rfl
+    | 𝓣, 𝓣, (1 : Fin 2) => rfl
+    | 𝓣, as y, (f, (0 : Fin 2)) => rfl
+    | 𝓣, as y, (f, (1 : Fin 2)) => rfl
+    | as x, as y, f => rfl
+  comp_id := by
+    intro X Y f
+    match X, Y, f with
+    | 𝓣, 𝓣, (0 : Fin 2) => rfl
+    | 𝓣, 𝓣, (1 : Fin 2) => rfl
+    | 𝓣, as y, (f, (0 : Fin 2)) => rfl
+    | 𝓣, as y, (f, (1 : Fin 2)) => rfl
+    | as x, as y, f => rfl
+  assoc := by
+    intro X Y Z W f g h
+    match X, Y, Z, W, f, g, h with
+    | _, _, as _, 𝓣, _, _, x => exact Empty.elim x
+    | _, as _, 𝓣,  _, _, x, _ => exact Empty.elim x
+    | as _, 𝓣, _,  _, x, _, _ => exact Empty.elim x
+    | 𝓣, 𝓣, 𝓣, 𝓣, f, g, h =>
+      simp only at g f h
+      fin_cases g <;> fin_cases f <;> fin_cases h <;> rfl
+    | 𝓣, 𝓣, 𝓣, as a, f, g, (h, hx) =>
+      simp only at g f
+      fin_cases g <;> fin_cases f <;> fin_cases hx <;> rfl
+    | 𝓣, 𝓣, as b, as a, f, (g, hg), h =>
+      simp only at g f
+      fin_cases f <;> fin_cases hg <;>  rfl
+    | 𝓣, as c, as b, as a, (f, hf ), g, h =>
+      simp only at g f
+      fin_cases hf  <;>  rfl
+    | as d, as c, as b, as a, f, g, h =>
+      simp only [Hom.comp, Iso.trans_assoc]
+
+end elGr
+
+/-- The category of graphical species. -/
+abbrev  GraphicalSpecies := elGrᵒᵖ ⥤ Type