PhysLean/HepLean/FeynmanDiagrams/Momentum.lean

/-
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.Data.Real.Basic
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.

The number of loops of a Feynman diagram is related to the dimension of the resulting
vector space.

-/

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

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

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

There is a linear map from `F.FullMomentumSpace` to `F.EdgeMomentumSpace`, induced
by the constraints at each edge.

We impose the constraint that we live in the kernal of this linear map.

A similar result is true for the vertex constraints.

-/


end FeynmanDiagram