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.

TODO

• Prove lemmas that make the calculation of the number of loops of a Feynman diagram easier.

Note

This section is non-computable as we depend on the norm on F.HalfEdgeMomenta.

Vector spaces associated with momenta in Feynman diagrams.

We define the vector space associated with momenta carried by half-edges, outflowing momenta of edges, and inflowing momenta of vertices.

We define the direct sum of the edge and vertex momentum spaces.

def FeynmanDiagram.HalfEdgeMomenta {P : PreFeynmanRule} (F : FeynmanDiagram P) : Type

The type which associates to each half-edge a 1-dimensional vector space. Corresponding to that spanned by its momentum.

Equations

• F.HalfEdgeMomenta = (F.𝓱𝓔 → ℝ)

instance FeynmanDiagram.instAddCommGroupHalfEdgeMomenta {P : PreFeynmanRule} (F : FeynmanDiagram P) : AddCommGroup F.HalfEdgeMomenta

The half momenta carries the structure of an additive commutative group.

Equations

• F.instAddCommGroupHalfEdgeMomenta = Pi.addCommGroup

instance FeynmanDiagram.instModuleRealHalfEdgeMomenta {P : PreFeynmanRule} (F : FeynmanDiagram P) : Module ℝ F.HalfEdgeMomenta

The half momenta carries the structure of a module over ℝ. Defined via its target.

Equations

• F.instModuleRealHalfEdgeMomenta = Pi.module F.𝓱𝓔 (fun (a : F.𝓱𝓔) => ℝ) ℝ

def FeynmanDiagram.euclidInnerAux {P : PreFeynmanRule} (F : FeynmanDiagram P) [F.IsFiniteDiagram] (x : F.HalfEdgeMomenta) : F.HalfEdgeMomenta →ₗ[ℝ] ℝ

An auxiliary function used to define the Euclidean inner product on F.HalfEdgeMomenta.

Equations

• F.euclidInnerAux x = { toFun := fun (y : F.HalfEdgeMomenta) => ∑ i : F.𝓱𝓔, x i * y i, map_add' := ⋯, map_smul' := ⋯ }

theorem FeynmanDiagram.euclidInnerAux_symm {P : PreFeynmanRule} (F : FeynmanDiagram P) [F.IsFiniteDiagram] (x y : F.HalfEdgeMomenta) : (F.euclidInnerAux x) y = (F.euclidInnerAux y) x

def FeynmanDiagram.euclidInner {P : PreFeynmanRule} (F : FeynmanDiagram P) [F.IsFiniteDiagram] : F.HalfEdgeMomenta →ₗ[ℝ] F.HalfEdgeMomenta →ₗ[ℝ] ℝ

The Euclidean inner product on F.HalfEdgeMomenta.

Equations

• F.euclidInner = { toFun := fun (x : F.HalfEdgeMomenta) => F.euclidInnerAux x, map_add' := ⋯, map_smul' := ⋯ }

def FeynmanDiagram.EdgeMomenta {P : PreFeynmanRule} (F : FeynmanDiagram P) : Type

The type which associates to each edge a 1-dimensional vector space. Corresponding to that spanned by its total outflowing momentum.

Equations

• F.EdgeMomenta = (F.𝓔 → ℝ)

instance FeynmanDiagram.instAddCommGroupEdgeMomenta {P : PreFeynmanRule} (F : FeynmanDiagram P) : AddCommGroup F.EdgeMomenta

The edge momenta form an additive commutative group.

Equations

• F.instAddCommGroupEdgeMomenta = Pi.addCommGroup

instance FeynmanDiagram.instModuleRealEdgeMomenta {P : PreFeynmanRule} (F : FeynmanDiagram P) : Module ℝ F.EdgeMomenta

The edge momenta form a module over ℝ.

Equations

• F.instModuleRealEdgeMomenta = Pi.module F.𝓔 (fun (a : F.𝓔) => ℝ) ℝ

def FeynmanDiagram.VertexMomenta {P : PreFeynmanRule} (F : FeynmanDiagram P) : Type

The type which associates to each edge a 1-dimensional vector space. Corresponding to that spanned by its total inflowing momentum.

Equations

• F.VertexMomenta = (F.𝓥 → ℝ)

instance FeynmanDiagram.instAddCommGroupVertexMomenta {P : PreFeynmanRule} (F : FeynmanDiagram P) : AddCommGroup F.VertexMomenta

The vertex momenta carries the structure of an additive commutative group.

Equations

• F.instAddCommGroupVertexMomenta = Pi.addCommGroup

instance FeynmanDiagram.instModuleRealVertexMomenta {P : PreFeynmanRule} (F : FeynmanDiagram P) : Module ℝ F.VertexMomenta

The vertex momenta carries the structure of a module over ℝ.

Equations

• F.instModuleRealVertexMomenta = Pi.module F.𝓥 (fun (a : F.𝓥) => ℝ) ℝ

def FeynmanDiagram.EdgeVertexMomentaMap {P : PreFeynmanRule} (F : FeynmanDiagram P) : Fin 2 → Type

The map from Fin 2 to Type landing on EdgeMomenta and VertexMomenta.

Equations

• F.EdgeVertexMomentaMap 0 = F.EdgeMomenta
• F.EdgeVertexMomentaMap 1 = F.VertexMomenta

instance FeynmanDiagram.instAddCommGroupEdgeVertexMomentaMap {P : PreFeynmanRule} (F : FeynmanDiagram P) (i : Fin 2) : AddCommGroup (F.EdgeVertexMomentaMap i)

The target of the map EdgeVertexMomentaMap is either the type of edge momenta or vertex momenta and thus carries the structure of an additive commutative group.

Equations

• F.instAddCommGroupEdgeVertexMomentaMap 0 = F.instAddCommGroupEdgeMomenta
• F.instAddCommGroupEdgeVertexMomentaMap 1 = F.instAddCommGroupVertexMomenta

instance FeynmanDiagram.instModuleRealEdgeVertexMomentaMap {P : PreFeynmanRule} (F : FeynmanDiagram P) (i : Fin 2) : Module ℝ (F.EdgeVertexMomentaMap i)

The target of the map EdgeVertexMomentaMap is either the type of edge momenta or vertex momenta and thus carries the structure of a module over ℝ.

Equations

• F.instModuleRealEdgeVertexMomentaMap 0 = F.instModuleRealEdgeMomenta
• F.instModuleRealEdgeVertexMomentaMap 1 = F.instModuleRealVertexMomenta

def FeynmanDiagram.EdgeVertexMomenta {P : PreFeynmanRule} (F : FeynmanDiagram P) : Type

The direct sum of EdgeMomenta and VertexMomenta.

Equations

• F.EdgeVertexMomenta = DirectSum (Fin 2) F.EdgeVertexMomentaMap

instance FeynmanDiagram.instAddCommGroupEdgeVertexMomenta {P : PreFeynmanRule} (F : FeynmanDiagram P) : AddCommGroup F.EdgeVertexMomenta

The structure of a additive commutative group on EdgeVertexMomenta for a Feynman diagram F.

Equations

• F.instAddCommGroupEdgeVertexMomenta = DirectSum.instAddCommGroup F.EdgeVertexMomentaMap

instance FeynmanDiagram.instModuleRealEdgeVertexMomenta {P : PreFeynmanRule} (F : FeynmanDiagram P) : Module ℝ F.EdgeVertexMomenta

The structure of a module over ℝ on EdgeVertexMomenta for a Feynman diagram F.

Equations

• F.instModuleRealEdgeVertexMomenta = DirectSum.instModule

Linear maps between the vector spaces.

We define various maps into F.HalfEdgeMomenta.

In particular, we define a map from F.EdgeVertexMomenta to F.HalfEdgeMomenta. This map represents the space orthogonal (with respect to the standard Euclidean inner product) to the allowed momenta of half-edges (up-to an offset determined by the external momenta).

The number of loops of a diagram is defined as the number of half-edges minus the rank of this matrix.

def FeynmanDiagram.edgeToHalfEdgeMomenta {P : PreFeynmanRule} (F : FeynmanDiagram P) : F.EdgeMomenta →ₗ[ℝ] F.HalfEdgeMomenta

The linear map from F.EdgeMomenta to F.HalfEdgeMomenta induced by the map F.𝓱𝓔To𝓔.hom.

Equations

• F.edgeToHalfEdgeMomenta = { toFun := fun (x : F.EdgeMomenta) => x ∘ F.𝓱𝓔To𝓔.hom, map_add' := ⋯, map_smul' := ⋯ }

def FeynmanDiagram.vertexToHalfEdgeMomenta {P : PreFeynmanRule} (F : FeynmanDiagram P) : F.VertexMomenta →ₗ[ℝ] F.HalfEdgeMomenta

The linear map from F.VertexMomenta to F.HalfEdgeMomenta induced by the map F.𝓱𝓔To𝓥.hom.

Equations

• F.vertexToHalfEdgeMomenta = { toFun := fun (x : F.VertexMomenta) => x ∘ F.𝓱𝓔To𝓥.hom, map_add' := ⋯, map_smul' := ⋯ }

def FeynmanDiagram.edgeVertexToHalfEdgeMomenta {P : PreFeynmanRule} (F : FeynmanDiagram P) : F.EdgeVertexMomenta →ₗ[ℝ] F.HalfEdgeMomenta

The linear map from F.EdgeVertexMomenta to F.HalfEdgeMomenta induced by F.edgeToHalfEdgeMomenta and F.vertexToHalfEdgeMomenta.

Equations

• F.edgeVertexToHalfEdgeMomenta = DirectSum.toModule ℝ (Fin 2) F.HalfEdgeMomenta fun (i : Fin 2) => match i with | 0 => F.edgeToHalfEdgeMomenta | 1 => F.vertexToHalfEdgeMomenta

Submodules

We define submodules of F.HalfEdgeMomenta which correspond to the orthogonal space to allowed momenta (up-to an offset), and the space of allowed momenta.

def FeynmanDiagram.orthogHalfEdgeMomenta {P : PreFeynmanRule} (F : FeynmanDiagram P) : Submodule ℝ F.HalfEdgeMomenta

The submodule of F.HalfEdgeMomenta corresponding to the range of F.edgeVertexToHalfEdgeMomenta.

Equations

• F.orthogHalfEdgeMomenta = LinearMap.range F.edgeVertexToHalfEdgeMomenta

def FeynmanDiagram.allowedHalfEdgeMomenta {P : PreFeynmanRule} (F : FeynmanDiagram P) [F.IsFiniteDiagram] : Submodule ℝ F.HalfEdgeMomenta

The submodule of F.HalfEdgeMomenta corresponding to the allowed momenta.

Equations

• F.allowedHalfEdgeMomenta = F.orthogHalfEdgeMomenta.orthogonalBilin F.euclidInner

Number of loops

We define the number of loops of a Feynman diagram as the dimension of the allowed space of half-edge momenta.

noncomputable def FeynmanDiagram.numberOfLoops {P : PreFeynmanRule} (F : FeynmanDiagram P) [F.IsFiniteDiagram] : ℕ

The number of loops of a Feynman diagram. Defined as the dimension of the space of allowed Half-loop momenta.

Equations

• F.numberOfLoops = Module.finrank ℝ ↥F.allowedHalfEdgeMomenta

Lemmas regarding numberOfLoops

We now give a series of lemmas which be used to help calculate the number of loops for specific Feynman diagrams.

TODO

• Complete this section.

Category theory

TODO

• Complete this section.