From fe50df3fc9201ee0059381425f5aa895a29ac4c7 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 18 Jun 2024 15:34:57 -0400
Subject: [PATCH] feat: Add Momentum

---
 HepLean/FeynmanDiagrams/Basic.lean    | 31 ++++++++++++
 HepLean/FeynmanDiagrams/Momentum.lean | 73 +++++++++++++++++++++++++++
 2 files changed, 104 insertions(+)
 create mode 100644 HepLean/FeynmanDiagrams/Momentum.lean

diff --git a/HepLean/FeynmanDiagrams/Basic.lean b/HepLean/FeynmanDiagrams/Basic.lean
index 4611cca..12714fb 100644
--- a/HepLean/FeynmanDiagrams/Basic.lean
+++ b/HepLean/FeynmanDiagrams/Basic.lean
@@ -16,6 +16,7 @@ import Mathlib.Data.Fintype.Perm
 import Mathlib.Combinatorics.SimpleGraph.Basic
 import Mathlib.Combinatorics.SimpleGraph.Connectivity
 import Mathlib.SetTheory.Cardinal.Basic
+import LeanCopilot
 /-!
 # Feynman diagrams
 
@@ -204,6 +205,36 @@ instance preimageEdgeMapFintype  [IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type}
 
 /-!
 
+## External and internal Vertices
+
+We say a vertex Label is `external` if it has only one half-edge associated with it.
+Otherwise, we say it is `internal`.
+
+We will show that for `IsFinitePreFeynmanRule` the condition of been external is decidable.
+-/
+
+/-- A vertex is external if it has a single half-edge associated to it. -/
+def External {P : PreFeynmanRule} (v : P.VertexLabel) : Prop :=
+  IsIsomorphic (P.vertexLabelMap v).left (Fin 1)
+
+lemma external_iff_exists_bijection {P : PreFeynmanRule}  (v : P.VertexLabel) :
+    External v ↔ ∃ (κ : (P.vertexLabelMap v).left → Fin 1), Function.Bijective κ := by
+  refine Iff.intro (fun h => ?_) (fun h => ?_)
+  obtain ⟨κ, κm1, h1, h2⟩ := h
+  let f : (P.vertexLabelMap v).left ≅ (Fin 1) :=  ⟨κ, κm1, h1, h2⟩
+  exact ⟨f.hom, (isIso_iff_bijective f.hom).mp $ Iso.isIso_hom f⟩
+  obtain ⟨κ, h1⟩ := h
+  let f : (P.vertexLabelMap v).left ⟶ (Fin 1) := κ
+  have ft : IsIso f := (isIso_iff_bijective κ).mpr h1
+  obtain ⟨fm, hf1, hf2⟩ := ft
+  exact ⟨f, fm, hf1, hf2⟩
+
+instance externalDecidable [IsFinitePreFeynmanRule P] (v : P.VertexLabel) :
+    Decidable (External v) :=
+  decidable_of_decidable_of_iff (external_iff_exists_bijection v).symm
+
+/-!
+
 ## Conditions to form a diagram.
 
 -/
diff --git a/HepLean/FeynmanDiagrams/Momentum.lean b/HepLean/FeynmanDiagrams/Momentum.lean
new file mode 100644
index 0000000..e811ab3
--- /dev/null
+++ b/HepLean/FeynmanDiagrams/Momentum.lean
@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.FeynmanDiagrams.Basic
+import Mathlib.Analysis.InnerProductSpace.Adjoint
+import Mathlib.Algebra.Category.ModuleCat.Basic
+/-!
+# Momentum in Feynman diagrams
+
+The aim of this file is to associate with each half-edge of a Feynman diagram a momentum,
+and constrain the momentums based conservation at each vertex and edge.
+
+-/
+
+namespace FeynmanDiagram
+
+open CategoryTheory
+open PreFeynmanRule
+
+variable {P : PreFeynmanRule} (F : FeynmanDiagram P)
+variable (d : ℕ)
+
+/-- The momentum space for a `d`-dimensional field theory for a single particle.
+  TODO: Move this definition, and define it as a four-vector. -/
+def SingleMomentumSpace : Type :=  Fin d → ℝ
+
+instance : AddCommGroup (SingleMomentumSpace d) := Pi.addCommGroup
+
+noncomputable instance : Module ℝ (SingleMomentumSpace d) := Pi.module _ _ _
+
+/-- The type which asociates to each half-edge a `d`-dimensional vector.
+ This is to be interpreted as the momentum associated to that half-edge flowing from the
+ corresponding `edge` to the corresponding `vertex`. So all momentums flow into vertices. -/
+def FullMomentumSpace : Type := F.𝓱𝓔 → Fin d → ℝ
+
+instance : AddCommGroup (F.FullMomentumSpace d) := Pi.addCommGroup
+
+noncomputable instance : Module ℝ (F.FullMomentumSpace d) := Pi.module _ _ _
+
+/-- The linear map taking a half-edge to its momentum.
+ (defined as flowing from the `edge` to the vertex.) -/
+def toHalfEdgeMomentum (i : F.𝓱𝓔) : F.FullMomentumSpace d →ₗ[ℝ] SingleMomentumSpace d where
+  toFun x := x i
+  map_add' x y := by rfl
+  map_smul' c x := by rfl
+
+namespace Hom
+
+variable {F G : FeynmanDiagram P}
+variable (f : F ⟶ G)
+
+/-- The linear map induced by a morphism of Feynman diagrams. -/
+def toLinearMap : G.FullMomentumSpace d →ₗ[ℝ] F.FullMomentumSpace d where
+  toFun x := x ∘ f.𝓱𝓔
+  map_add' x y := by rfl
+  map_smul' c x := by rfl
+
+
+end Hom
+
+/-- The contravariant functor from Feynman diagrams to Modules over `ℝ`.  -/
+noncomputable def funcFullMomentumSpace : FeynmanDiagram P ⥤ (ModuleCat ℝ)ᵒᵖ where
+  obj F := Opposite.op $ ModuleCat.of ℝ (F.FullMomentumSpace d)
+  map f := Opposite.op $ Hom.toLinearMap d f
+
+
+/-!
+## Edge constraints
+
+-/
+end FeynmanDiagram