Feynman diagrams

Feynman diagrams are a graphical representation of the terms in the perturbation expansion of a quantum field theory.

The definition of Pre Feynman rules

We define the notion of a pre-Feynman rule, which specifies the possible half-edges, edges and vertices in a diagram. It does not specify how to turn a diagram into an algebraic expression.

TODO

Prove that the halfEdgeLimit functor lands on limits of functors.

structure PreFeynmanRule : Type 1

A PreFeynmanRule is a set of rules specifying the allowed half-edges, edges and vertices in a diagram. (It does not specify how to turn the diagram into an algebraic expression.)

• HalfEdgeLabel : Type

  The type labelling the different types of half-edges.

• EdgeLabel : Type

  A type labelling the different types of edges.

• VertexLabel : Type

  A type labelling the different types of vertices.

• edgeLabelMap : self.EdgeLabel → CategoryTheory.Over self.HalfEdgeLabel

  A function taking EdgeLabels to the half edges it contains. This will usually land on Fin 2 → _

• vertexLabelMap : self.VertexLabel → CategoryTheory.Over self.HalfEdgeLabel

  A function taking VertexLabels to the half edges it contains. For example, if the vertex is of order-3 it will land on Fin 3 → _.

def PreFeynmanRule.toVertex (P : PreFeynmanRule) {𝓔 𝓥 : Type} : CategoryTheory.Functor (CategoryTheory.Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) (CategoryTheory.Over 𝓥)

The functor from Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel) to Over (P.VertexLabel) induced by projections on products.

Equations

• P.toVertex = CategoryTheory.Over.map (Prod.snd ∘ Prod.snd)

def PreFeynmanRule.toEdge (P : PreFeynmanRule) {𝓔 𝓥 : Type} : CategoryTheory.Functor (CategoryTheory.Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) (CategoryTheory.Over 𝓔)

The functor from Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel) to Over (P.EdgeLabel) induced by projections on products.

Equations

• P.toEdge = CategoryTheory.Over.map (Prod.fst ∘ Prod.snd)

@[simp]

theorem PreFeynmanRule.toEdge_obj_hom (P : PreFeynmanRule) {𝓔 𝓥 : Type} (X : CategoryTheory.Comma (CategoryTheory.Functor.id Type) (CategoryTheory.Functor.fromPUnit (P.HalfEdgeLabel × 𝓔 × 𝓥))) (a✝ : (CategoryTheory.Functor.id Type).obj X.left) : (P.toEdge.obj X).hom a✝ = (X.hom a✝).2.1

@[simp]

theorem PreFeynmanRule.toEdge_map_left (P : PreFeynmanRule) {𝓔 𝓥 : Type} {X✝ Y✝ : CategoryTheory.Comma (CategoryTheory.Functor.id Type) (CategoryTheory.Functor.fromPUnit (P.HalfEdgeLabel × 𝓔 × 𝓥))} (f : X✝ ⟶ Y✝) (a✝ : X✝.left) : (P.toEdge.map f).left a✝ = f.left a✝

@[simp]

theorem PreFeynmanRule.toEdge_map_right (P : PreFeynmanRule) {𝓔 𝓥 : Type} {X✝ Y✝ : CategoryTheory.Comma (CategoryTheory.Functor.id Type) (CategoryTheory.Functor.fromPUnit (P.HalfEdgeLabel × 𝓔 × 𝓥))} (f : X✝ ⟶ Y✝) : (P.toEdge.map f).right = CategoryTheory.CategoryStruct.id X✝.right

@[simp]

theorem PreFeynmanRule.toEdge_obj_left (P : PreFeynmanRule) {𝓔 𝓥 : Type} (X : CategoryTheory.Comma (CategoryTheory.Functor.id Type) (CategoryTheory.Functor.fromPUnit (P.HalfEdgeLabel × 𝓔 × 𝓥))) : (P.toEdge.obj X).left = X.left

def PreFeynmanRule.toHalfEdge (P : PreFeynmanRule) {𝓔 𝓥 : Type} : CategoryTheory.Functor (CategoryTheory.Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) (CategoryTheory.Over P.HalfEdgeLabel)

The functor from Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel) to Over (P.HalfEdgeLabel) induced by projections on products.

Equations

• P.toHalfEdge = CategoryTheory.Over.map Prod.fst

@[simp]

theorem PreFeynmanRule.toHalfEdge_obj_hom (P : PreFeynmanRule) {𝓔 𝓥 : Type} (X : CategoryTheory.Comma (CategoryTheory.Functor.id Type) (CategoryTheory.Functor.fromPUnit (P.HalfEdgeLabel × 𝓔 × 𝓥))) (a✝ : (CategoryTheory.Functor.id Type).obj X.left) : (P.toHalfEdge.obj X).hom a✝ = (X.hom a✝).1

@[simp]

theorem PreFeynmanRule.toHalfEdge_map_right (P : PreFeynmanRule) {𝓔 𝓥 : Type} {X✝ Y✝ : CategoryTheory.Comma (CategoryTheory.Functor.id Type) (CategoryTheory.Functor.fromPUnit (P.HalfEdgeLabel × 𝓔 × 𝓥))} (f : X✝ ⟶ Y✝) : (P.toHalfEdge.map f).right = CategoryTheory.CategoryStruct.id X✝.right

@[simp]

theorem PreFeynmanRule.toHalfEdge_obj_left (P : PreFeynmanRule) {𝓔 𝓥 : Type} (X : CategoryTheory.Comma (CategoryTheory.Functor.id Type) (CategoryTheory.Functor.fromPUnit (P.HalfEdgeLabel × 𝓔 × 𝓥))) : (P.toHalfEdge.obj X).left = X.left

@[simp]

theorem PreFeynmanRule.toHalfEdge_map_left (P : PreFeynmanRule) {𝓔 𝓥 : Type} {X✝ Y✝ : CategoryTheory.Comma (CategoryTheory.Functor.id Type) (CategoryTheory.Functor.fromPUnit (P.HalfEdgeLabel × 𝓔 × 𝓥))} (f : X✝ ⟶ Y✝) (a✝ : X✝.left) : (P.toHalfEdge.map f).left a✝ = f.left a✝

def PreFeynmanRule.preimageType' {𝓥 : Type} (v : 𝓥) : CategoryTheory.Functor (CategoryTheory.Over 𝓥) Type

The functor from Over P.VertexLabel to Type induced by pull-back along insertion of v : P.VertexLabel.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PreFeynmanRule.preimageType'_obj {𝓥 : Type} (v : 𝓥) (f : CategoryTheory.Over 𝓥) : (preimageType' v).obj f = ↑(f.hom ⁻¹' {v})

@[simp]

theorem PreFeynmanRule.preimageType'_map_coe {𝓥 : Type} (v : 𝓥) {f g : CategoryTheory.Over 𝓥} (F : f ⟶ g) (x : ↑(f.hom ⁻¹' {v})) : ↑((preimageType' v).map F x) = F.left ↑x

def PreFeynmanRule.preimageVertex (P : PreFeynmanRule) {𝓔 𝓥 : Type} (v : 𝓥) : CategoryTheory.Functor (CategoryTheory.Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) (CategoryTheory.Over P.HalfEdgeLabel)

The functor from Over (P.HalfEdgeLabel × 𝓔 × 𝓥) to Over P.HalfEdgeLabel induced by pull-back along insertion of v : P.VertexLabel. For a given vertex, it returns all half edges corresponding to that vertex.

Equations

• One or more equations did not get rendered due to their size.

def PreFeynmanRule.preimageEdge (P : PreFeynmanRule) {𝓔 𝓥 : Type} (v : 𝓔) : CategoryTheory.Functor (CategoryTheory.Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) (CategoryTheory.Over P.HalfEdgeLabel)

The functor from Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel) to Over P.HalfEdgeLabel induced by pull-back along insertion of v : P.EdgeLabel. For a given edge, it returns all half edges corresponding to that edge.

Equations

• One or more equations did not get rendered due to their size.

Finiteness of pre-Feynman rules

We define a class of PreFeynmanRule which have nice properties with regard to decidability and finiteness.

In practice, every pre-Feynman rule considered in the physics literature satisfies these properties.

class PreFeynmanRule.IsFinitePreFeynmanRule (P : PreFeynmanRule) : Type

A set of conditions on PreFeynmanRule for it to be considered finite.

• edgeLabelDecidable : DecidableEq P.EdgeLabel

  The type of edge labels is decidable.

• vertexLabelDecidable : DecidableEq P.VertexLabel

  The type of vertex labels is decidable.

• halfEdgeLabelDecidable : DecidableEq P.HalfEdgeLabel

  The type of half-edge labels is decidable.

• vertexMapFintype (v : P.VertexLabel) : Fintype (P.vertexLabelMap v).left

  The type of half-edges associated with a vertex is finite.

• vertexMapDecidable (v : P.VertexLabel) : DecidableEq (P.vertexLabelMap v).left

  The type of half-edges associated with a vertex is decidable.

• edgeMapFintype (v : P.EdgeLabel) : Fintype (P.edgeLabelMap v).left

  The type of half-edges associated with an edge is finite.

• edgeMapDecidable (v : P.EdgeLabel) : DecidableEq (P.edgeLabelMap v).left

  The type of half-edges associated with an edge is decidable.

instance PreFeynmanRule.preFeynmanRuleDecEq𝓔 (P : PreFeynmanRule) [P.IsFinitePreFeynmanRule] : DecidableEq P.EdgeLabel

If P is a finite pre feynman rule, then equality of edge labels of P is decidable.

Equations

• P.preFeynmanRuleDecEq𝓔 = PreFeynmanRule.IsFinitePreFeynmanRule.edgeLabelDecidable

instance PreFeynmanRule.preFeynmanRuleDecEq𝓥 (P : PreFeynmanRule) [P.IsFinitePreFeynmanRule] : DecidableEq P.VertexLabel

If P is a finite pre feynman rule, then equality of vertex labels of P is decidable.

Equations

• P.preFeynmanRuleDecEq𝓥 = PreFeynmanRule.IsFinitePreFeynmanRule.vertexLabelDecidable

instance PreFeynmanRule.preFeynmanRuleDecEq𝓱𝓔 (P : PreFeynmanRule) [P.IsFinitePreFeynmanRule] : DecidableEq P.HalfEdgeLabel

If P is a finite pre feynman rule, then equality of half-edge labels of P is decidable.

Equations

• P.preFeynmanRuleDecEq𝓱𝓔 = PreFeynmanRule.IsFinitePreFeynmanRule.halfEdgeLabelDecidable

instance PreFeynmanRule.instFintypeLeftDiscretePUnitVertexLabelMapOfIsFinitePreFeynmanRule (P : PreFeynmanRule) [P.IsFinitePreFeynmanRule] (v : P.VertexLabel) : Fintype (P.vertexLabelMap v).left

If P is a finite pre-feynman rule, then every vertex has a finite number of half-edges associated to it.

Equations

• P.instFintypeLeftDiscretePUnitVertexLabelMapOfIsFinitePreFeynmanRule v = PreFeynmanRule.IsFinitePreFeynmanRule.vertexMapFintype v

instance PreFeynmanRule.instDecidableEqLeftDiscretePUnitVertexLabelMapOfIsFinitePreFeynmanRule (P : PreFeynmanRule) [P.IsFinitePreFeynmanRule] (v : P.VertexLabel) : DecidableEq (P.vertexLabelMap v).left

If P is a finite pre-feynman rule, then the indexing set of half-edges associated to a vertex is decidable.

Equations

• P.instDecidableEqLeftDiscretePUnitVertexLabelMapOfIsFinitePreFeynmanRule v = PreFeynmanRule.IsFinitePreFeynmanRule.vertexMapDecidable v

instance PreFeynmanRule.instFintypeLeftDiscretePUnitEdgeLabelMapOfIsFinitePreFeynmanRule (P : PreFeynmanRule) [P.IsFinitePreFeynmanRule] (v : P.EdgeLabel) : Fintype (P.edgeLabelMap v).left

If P is a finite pre-feynman rule, then every edge has a finite number of half-edges associated to it.

Equations

• P.instFintypeLeftDiscretePUnitEdgeLabelMapOfIsFinitePreFeynmanRule v = PreFeynmanRule.IsFinitePreFeynmanRule.edgeMapFintype v

instance PreFeynmanRule.instDecidableEqLeftDiscretePUnitEdgeLabelMapOfIsFinitePreFeynmanRule (P : PreFeynmanRule) [P.IsFinitePreFeynmanRule] (v : P.EdgeLabel) : DecidableEq (P.edgeLabelMap v).left

If P is a finite pre-feynman rule, then the indexing set of half-edges associated to an edge is decidable.

Equations

• P.instDecidableEqLeftDiscretePUnitEdgeLabelMapOfIsFinitePreFeynmanRule v = PreFeynmanRule.IsFinitePreFeynmanRule.edgeMapDecidable v

instance PreFeynmanRule.preimageVertexDecidablePred (P : PreFeynmanRule) {𝓔 𝓥 : Type} [DecidableEq 𝓥] (v : 𝓥) (F : CategoryTheory.Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) : DecidablePred fun (x : (CategoryTheory.Functor.id Type).obj (P.toVertex.obj F).left) => x ∈ (P.toVertex.obj F).hom ⁻¹' {v}

It is decidable to check whether a half edge of a diagram (an object in Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) corresponds to a given vertex.

Equations

• P.preimageVertexDecidablePred v F y = match decEq ((P.toVertex.obj F).hom y) v with | isTrue h => isTrue h | isFalse h => isFalse h

instance PreFeynmanRule.preimageEdgeDecidablePred (P : PreFeynmanRule) {𝓔 𝓥 : Type} [DecidableEq 𝓔] (v : 𝓔) (F : CategoryTheory.Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) : DecidablePred fun (x : (CategoryTheory.Functor.id Type).obj (P.toEdge.obj F).left) => x ∈ (P.toEdge.obj F).hom ⁻¹' {v}

It is decidable to check whether a half edge of a diagram (an object in Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) corresponds to a given edge.

Equations

• P.preimageEdgeDecidablePred v F y = match decEq ((P.toEdge.obj F).hom y) v with | isTrue h => isTrue h | isFalse h => isFalse h

instance PreFeynmanRule.preimageVertexDecidable (P : PreFeynmanRule) {𝓔 𝓥 : Type} (v : 𝓥) (F : CategoryTheory.Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [DecidableEq F.left] : DecidableEq ((P.preimageVertex v).obj F).left

If F is an object in Over (P.HalfEdgeLabel × 𝓔 × 𝓥), with a decidable source, then the object in Over P.HalfEdgeLabel formed by following the functor preimageVertex has a decidable source (since it is the same source).

Equations

• P.preimageVertexDecidable v F = Subtype.instDecidableEq

instance PreFeynmanRule.preimageEdgeDecidable (P : PreFeynmanRule) {𝓔 𝓥 : Type} (v : 𝓔) (F : CategoryTheory.Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [DecidableEq F.left] : DecidableEq ((P.preimageEdge v).obj F).left

The half edges corresponding to a given edge has an indexing set which is decidable.

Equations

• P.preimageEdgeDecidable v F = Subtype.instDecidableEq

instance PreFeynmanRule.preimageVertexFintype (P : PreFeynmanRule) {𝓔 𝓥 : Type} [DecidableEq 𝓥] (v : 𝓥) (F : CategoryTheory.Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [h : Fintype F.left] : Fintype ((P.preimageVertex v).obj F).left

The half edges corresponding to a given vertex has an indexing set which is decidable.

Equations

• P.preimageVertexFintype v F = Subtype.fintype (Membership.mem ((P.toVertex.obj F).hom ⁻¹' {v}))

instance PreFeynmanRule.preimageEdgeFintype (P : PreFeynmanRule) {𝓔 𝓥 : Type} [DecidableEq 𝓔] (v : 𝓔) (F : CategoryTheory.Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [h : Fintype F.left] : Fintype ((P.preimageEdge v).obj F).left

The half edges corresponding to a given edge has an indexing set which is finite.

Equations

• P.preimageEdgeFintype v F = Subtype.fintype (Membership.mem ((P.toEdge.obj F).hom ⁻¹' {v}))

instance PreFeynmanRule.preimageVertexMapFintype (P : PreFeynmanRule) [P.IsFinitePreFeynmanRule] {𝓔 𝓥 : Type} [DecidableEq 𝓥] (v : 𝓥) (f : 𝓥 ⟶ P.VertexLabel) (F : CategoryTheory.Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [Fintype F.left] : Fintype ((P.vertexLabelMap (f v)).left → ((P.preimageVertex v).obj F).left)

The half edges corresponding to a given vertex has an indexing set which is finite.

Equations

• P.preimageVertexMapFintype v f F = Pi.instFintype

instance PreFeynmanRule.preimageEdgeMapFintype (P : PreFeynmanRule) [P.IsFinitePreFeynmanRule] {𝓔 𝓥 : Type} [DecidableEq 𝓔] (v : 𝓔) (f : 𝓔 ⟶ P.EdgeLabel) (F : CategoryTheory.Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [Fintype F.left] : Fintype ((P.edgeLabelMap (f v)).left → ((P.preimageEdge v).obj F).left)

Given an edge, there is a finite number of maps between the indexing set of the expected half-edges corresponding to that edges label, and the actual indexing set of half-edges corresponding to that edge. Given various finiteness conditions.

Equations

• P.preimageEdgeMapFintype v f F = Pi.instFintype

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.

def PreFeynmanRule.External {P : PreFeynmanRule} (v : P.VertexLabel) : Prop

A vertex is external if it has a single half-edge associated to it.

Equations

• PreFeynmanRule.External v = CategoryTheory.IsIsomorphic (P.vertexLabelMap v).left (Fin 1)

theorem PreFeynmanRule.external_iff_exists_bijection {P : PreFeynmanRule} (v : P.VertexLabel) : External v ↔ ∃ (κ : (P.vertexLabelMap v).left → Fin 1), Function.Bijective κ

instance PreFeynmanRule.externalDecidable (P : PreFeynmanRule) [P.IsFinitePreFeynmanRule] (v : P.VertexLabel) : Decidable (External v)

Whether or not a vertex is external is decidable.

Equations

• P.externalDecidable v = decidable_of_decidable_of_iff ⋯

Conditions to form a diagram.

def PreFeynmanRule.DiagramVertexProp (P : PreFeynmanRule) {𝓔 𝓥 : Type} (F : CategoryTheory.Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) (f : 𝓥 ⟶ P.VertexLabel) : Prop

The proposition on vertices which must be satisfied by an object F : Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel) for it to be a Feynman diagram. This condition corresponds to the vertices of F having the correct half-edges associated with them.

Equations

• P.DiagramVertexProp F f = ∀ (v : 𝓥), CategoryTheory.IsIsomorphic (P.vertexLabelMap (f v)) ((P.preimageVertex v).obj F)

def PreFeynmanRule.DiagramEdgeProp (P : PreFeynmanRule) {𝓔 𝓥 : Type} (F : CategoryTheory.Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) (f : 𝓔 ⟶ P.EdgeLabel) : Prop

The proposition on edges which must be satisfied by an object F : Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel) for it to be a Feynman diagram. This condition corresponds to the edges of F having the correct half-edges associated with them.

Equations

• P.DiagramEdgeProp F f = ∀ (v : 𝓔), CategoryTheory.IsIsomorphic (P.edgeLabelMap (f v)) ((P.preimageEdge v).obj F)

theorem PreFeynmanRule.diagramVertexProp_iff (P : PreFeynmanRule) {𝓔 𝓥 : Type} (F : CategoryTheory.Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) (f : 𝓥 ⟶ P.VertexLabel) : P.DiagramVertexProp F f ↔ ∀ (v : 𝓥), ∃ (κ : (P.vertexLabelMap (f v)).left → ((P.preimageVertex v).obj F).left), Function.Bijective κ ∧ ((P.preimageVertex v).obj F).hom ∘ κ = (P.vertexLabelMap (f v)).hom

theorem PreFeynmanRule.diagramEdgeProp_iff (P : PreFeynmanRule) {𝓔 𝓥 : Type} (F : CategoryTheory.Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) (f : 𝓔 ⟶ P.EdgeLabel) : P.DiagramEdgeProp F f ↔ ∀ (v : 𝓔), ∃ (κ : (P.edgeLabelMap (f v)).left → ((P.preimageEdge v).obj F).left), Function.Bijective κ ∧ ((P.preimageEdge v).obj F).hom ∘ κ = (P.edgeLabelMap (f v)).hom

instance PreFeynmanRule.diagramVertexPropDecidable (P : PreFeynmanRule) [P.IsFinitePreFeynmanRule] {𝓔 𝓥 : Type} [Fintype 𝓥] [DecidableEq 𝓥] (F : CategoryTheory.Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [DecidableEq F.left] [Fintype F.left] (f : 𝓥 ⟶ P.VertexLabel) : Decidable (P.DiagramVertexProp F f)

The proposition DiagramVertexProp is decidable given various decidability and finite conditions.

Equations

• P.diagramVertexPropDecidable F f = decidable_of_decidable_of_iff ⋯

instance PreFeynmanRule.diagramEdgePropDecidable (P : PreFeynmanRule) [P.IsFinitePreFeynmanRule] {𝓔 𝓥 : Type} [Fintype 𝓔] [DecidableEq 𝓔] (F : CategoryTheory.Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [DecidableEq F.left] [Fintype F.left] (f : 𝓔 ⟶ P.EdgeLabel) : Decidable (P.DiagramEdgeProp F f)

The proposition DiagramEdgeProp is decidable given various decidability and finite conditions.

Equations

• P.diagramEdgePropDecidable F f = decidable_of_decidable_of_iff ⋯

The definition of Feynman diagrams

We now define the type of Feynman diagrams for a given pre-Feynman rule.

structure FeynmanDiagram (P : PreFeynmanRule) : Type 1

The type of Feynman diagrams given a PreFeynmanRule.

• 𝓔𝓞 : CategoryTheory.Over P.EdgeLabel

  The type of edges in the Feynman diagram, labelled by their type.

• 𝓥𝓞 : CategoryTheory.Over P.VertexLabel

  The type of vertices in the Feynman diagram, labelled by their type.

• 𝓱𝓔To𝓔𝓥 : CategoryTheory.Over (P.HalfEdgeLabel × self.𝓔𝓞.left × self.𝓥𝓞.left)

  The type of half-edges in the Feynman diagram, labelled by their type, the edge it belongs to, and the vertex they belong to.

• 𝓔Cond : P.DiagramEdgeProp self.𝓱𝓔To𝓔𝓥 self.𝓔𝓞.hom

  Each edge has the correct type of half edges.

• 𝓥Cond : P.DiagramVertexProp self.𝓱𝓔To𝓔𝓥 self.𝓥𝓞.hom

  Each vertex has the correct sort of half edges.

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

The type of edges.

Equations

• F.𝓔 = F.𝓔𝓞.left

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

The type of vertices.

Equations

• F.𝓥 = F.𝓥𝓞.left

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

The type of half-edges.

Equations

• F.𝓱𝓔 = F.𝓱𝓔To𝓔𝓥.left

def FeynmanDiagram.𝓱𝓔𝓞 {P : PreFeynmanRule} (F : FeynmanDiagram P) : CategoryTheory.Over P.HalfEdgeLabel

The object in Over P.HalfEdgeLabel generated by a Feynman diagram.

Equations

• F.𝓱𝓔𝓞 = P.toHalfEdge.obj F.𝓱𝓔To𝓔𝓥

def FeynmanDiagram.𝓱𝓔To𝓔 {P : PreFeynmanRule} (F : FeynmanDiagram P) : CategoryTheory.Over F.𝓔

The map F.𝓱𝓔 → F.𝓔 as an object in Over F.𝓔 .

Equations

• F.𝓱𝓔To𝓔 = P.toEdge.obj F.𝓱𝓔To𝓔𝓥

def FeynmanDiagram.𝓱𝓔To𝓥 {P : PreFeynmanRule} (F : FeynmanDiagram P) : CategoryTheory.Over F.𝓥

The map F.𝓱𝓔 → F.𝓥 as an object in Over F.𝓥 .

Equations

• F.𝓱𝓔To𝓥 = P.toVertex.obj F.𝓱𝓔To𝓔𝓥

Making a Feynman diagram

def FeynmanDiagram.Cond {P : PreFeynmanRule} {𝓔 𝓥 𝓱𝓔 : Type} (𝓔𝓞 : 𝓔 → P.EdgeLabel) (𝓥𝓞 : 𝓥 → P.VertexLabel) (𝓱𝓔To𝓔𝓥 : 𝓱𝓔 → P.HalfEdgeLabel × 𝓔 × 𝓥) : Prop

The condition which must be satisfied by maps to form a Feynman diagram.

Equations

• FeynmanDiagram.Cond 𝓔𝓞 𝓥𝓞 𝓱𝓔To𝓔𝓥 = (P.DiagramEdgeProp (CategoryTheory.Over.mk 𝓱𝓔To𝓔𝓥) 𝓔𝓞 ∧ P.DiagramVertexProp (CategoryTheory.Over.mk 𝓱𝓔To𝓔𝓥) 𝓥𝓞)

theorem FeynmanDiagram.cond_self {P : PreFeynmanRule} (F : FeynmanDiagram P) : Cond F.𝓔𝓞.hom F.𝓥𝓞.hom F.𝓱𝓔To𝓔𝓥.hom

instance FeynmanDiagram.CondDecidable {P : PreFeynmanRule} [P.IsFinitePreFeynmanRule] {𝓔 𝓥 𝓱𝓔 : Type} (𝓔𝓞 : 𝓔 → P.EdgeLabel) (𝓥𝓞 : 𝓥 → P.VertexLabel) (𝓱𝓔To𝓔𝓥 : 𝓱𝓔 → P.HalfEdgeLabel × 𝓔 × 𝓥) [Fintype 𝓥] [DecidableEq 𝓥] [Fintype 𝓔] [DecidableEq 𝓔] [h : Fintype 𝓱𝓔] [DecidableEq 𝓱𝓔] : Decidable (Cond 𝓔𝓞 𝓥𝓞 𝓱𝓔To𝓔𝓥)

Cond is decidable.

Equations

• FeynmanDiagram.CondDecidable 𝓔𝓞 𝓥𝓞 𝓱𝓔To𝓔𝓥 = instDecidableAnd

def FeynmanDiagram.mk' {P : PreFeynmanRule} {𝓔 𝓥 𝓱𝓔 : Type} (𝓔𝓞 : 𝓔 → P.EdgeLabel) (𝓥𝓞 : 𝓥 → P.VertexLabel) (𝓱𝓔To𝓔𝓥 : 𝓱𝓔 → P.HalfEdgeLabel × 𝓔 × 𝓥) (C : Cond 𝓔𝓞 𝓥𝓞 𝓱𝓔To𝓔𝓥) : FeynmanDiagram P

Making a Feynman diagram from maps of edges, vertices and half-edges.

Equations

• FeynmanDiagram.mk' 𝓔𝓞 𝓥𝓞 𝓱𝓔To𝓔𝓥 C = { 𝓔𝓞 := CategoryTheory.Over.mk 𝓔𝓞, 𝓥𝓞 := CategoryTheory.Over.mk 𝓥𝓞, 𝓱𝓔To𝓔𝓥 := CategoryTheory.Over.mk 𝓱𝓔To𝓔𝓥, 𝓔Cond := ⋯, 𝓥Cond := ⋯ }

theorem FeynmanDiagram.mk'_self {P : PreFeynmanRule} (F : FeynmanDiagram P) : mk' F.𝓔𝓞.hom F.𝓥𝓞.hom F.𝓱𝓔To𝓔𝓥.hom ⋯ = F

Finiteness of Feynman diagrams

As defined above our Feynman diagrams can have non-finite Types of half-edges etc. We define the class of those Feynman diagrams which are finite in the appropriate sense. In practice, every Feynman diagram considered in the physics literature is finite.

This finiteness condition will be used to prove certain Types are Fintype, and prove that certain propositions are decidable.

class FeynmanDiagram.IsFiniteDiagram {P : PreFeynmanRule} (F : FeynmanDiagram P) : Type

A set of conditions on a Feynman diagram for it to be considered finite.

• 𝓔Fintype : Fintype F.𝓔

  The type of edges is finite.

• 𝓔DecidableEq : DecidableEq F.𝓔

  The type of edges is decidable.

• 𝓥Fintype : Fintype F.𝓥

  The type of vertices is finite.

• 𝓥DecidableEq : DecidableEq F.𝓥

  The type of vertices is decidable.

• 𝓱𝓔Fintype : Fintype F.𝓱𝓔

  The type of half-edges is finite.

• 𝓱𝓔DecidableEq : DecidableEq F.𝓱𝓔

  The type of half-edges is decidable.

instance FeynmanDiagram.instIsFiniteDiagramMk'OfFintypeOfDecidableEq {P : PreFeynmanRule} {𝓔 𝓥 𝓱𝓔 : Type} [h1 : Fintype 𝓔] [h2 : DecidableEq 𝓔] [h3 : Fintype 𝓥] [h4 : DecidableEq 𝓥] [h5 : Fintype 𝓱𝓔] [h6 : DecidableEq 𝓱𝓔] (𝓔𝓞 : 𝓔 → P.EdgeLabel) (𝓥𝓞 : 𝓥 → P.VertexLabel) (𝓱𝓔To𝓔𝓥 : 𝓱𝓔 → P.HalfEdgeLabel × 𝓔 × 𝓥) (C : Cond 𝓔𝓞 𝓥𝓞 𝓱𝓔To𝓔𝓥) : (mk' 𝓔𝓞 𝓥𝓞 𝓱𝓔To𝓔𝓥 C).IsFiniteDiagram

The instance of a finite diagram given explicit finiteness and decidable conditions on the various maps making it up.

Equations

• FeynmanDiagram.instIsFiniteDiagramMk'OfFintypeOfDecidableEq 𝓔𝓞 𝓥𝓞 𝓱𝓔To𝓔𝓥 C = { 𝓔Fintype := h1, 𝓔DecidableEq := h2, 𝓥Fintype := h3, 𝓥DecidableEq := h4, 𝓱𝓔Fintype := h5, 𝓱𝓔DecidableEq := h6 }

instance FeynmanDiagram.instFintype𝓔OfIsFiniteDiagram {P : PreFeynmanRule} {F : FeynmanDiagram P} [F.IsFiniteDiagram] : Fintype F.𝓔

If F is a finite Feynman diagram, then its edges are finite.

Equations

• FeynmanDiagram.instFintype𝓔OfIsFiniteDiagram = FeynmanDiagram.IsFiniteDiagram.𝓔Fintype

instance FeynmanDiagram.instDecidableEq𝓔OfIsFiniteDiagram {P : PreFeynmanRule} {F : FeynmanDiagram P} [F.IsFiniteDiagram] : DecidableEq F.𝓔

If F is a finite Feynman diagram, then its edges are decidable.

Equations

• FeynmanDiagram.instDecidableEq𝓔OfIsFiniteDiagram = FeynmanDiagram.IsFiniteDiagram.𝓔DecidableEq

instance FeynmanDiagram.instFintype𝓥OfIsFiniteDiagram {P : PreFeynmanRule} {F : FeynmanDiagram P} [F.IsFiniteDiagram] : Fintype F.𝓥

If F is a finite Feynman diagram, then its vertices are finite.

Equations

• FeynmanDiagram.instFintype𝓥OfIsFiniteDiagram = FeynmanDiagram.IsFiniteDiagram.𝓥Fintype

instance FeynmanDiagram.instDecidableEq𝓥OfIsFiniteDiagram {P : PreFeynmanRule} {F : FeynmanDiagram P} [F.IsFiniteDiagram] : DecidableEq F.𝓥

If F is a finite Feynman diagram, then its vertices are decidable.

Equations

• FeynmanDiagram.instDecidableEq𝓥OfIsFiniteDiagram = FeynmanDiagram.IsFiniteDiagram.𝓥DecidableEq

instance FeynmanDiagram.instFintype𝓱𝓔OfIsFiniteDiagram {P : PreFeynmanRule} {F : FeynmanDiagram P} [F.IsFiniteDiagram] : Fintype F.𝓱𝓔

If F is a finite Feynman diagram, then its half-edges are finite.

Equations

• FeynmanDiagram.instFintype𝓱𝓔OfIsFiniteDiagram = FeynmanDiagram.IsFiniteDiagram.𝓱𝓔Fintype

instance FeynmanDiagram.instDecidableEq𝓱𝓔OfIsFiniteDiagram {P : PreFeynmanRule} {F : FeynmanDiagram P} [F.IsFiniteDiagram] : DecidableEq F.𝓱𝓔

If F is a finite Feynman diagram, then its half-edges are decidable.

Equations

• FeynmanDiagram.instDecidableEq𝓱𝓔OfIsFiniteDiagram = FeynmanDiagram.IsFiniteDiagram.𝓱𝓔DecidableEq

instance FeynmanDiagram.instDecidableEqObjDiscretePUnitFromPUnit𝓔Right𝓱𝓔To𝓔HomOfIsFiniteDiagram {P : PreFeynmanRule} {F : FeynmanDiagram P} [F.IsFiniteDiagram] (i : F.𝓱𝓔) (j : F.𝓔) : Decidable (F.𝓱𝓔To𝓔.hom i = j)

The proposition of whether the given an half-edge and an edge, the edge corresponding to the half edges is the given edge is decidable.

Equations

• FeynmanDiagram.instDecidableEqObjDiscretePUnitFromPUnit𝓔Right𝓱𝓔To𝓔HomOfIsFiniteDiagram i j = FeynmanDiagram.IsFiniteDiagram.𝓔DecidableEq (F.𝓱𝓔To𝓔.hom i) j

instance FeynmanDiagram.fintypeProdHalfEdgeLabel𝓔𝓥 {P : PreFeynmanRule} {F : FeynmanDiagram P} [P.IsFinitePreFeynmanRule] [F.IsFiniteDiagram] : DecidableEq (P.HalfEdgeLabel × F.𝓔 × F.𝓥)

For a finite feynman diagram, the type of half edge labels, edges and vertices is decidable.

Equations

• FeynmanDiagram.fintypeProdHalfEdgeLabel𝓔𝓥 = instDecidableEqProd

Morphisms of Feynman diagrams

We define a morphism between Feynman diagrams, and properties thereof. This will be used to define the category of Feynman diagrams.

def FeynmanDiagram.edgeVertexMap {P : PreFeynmanRule} {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ⟶ G.𝓔) (𝓥 : F.𝓥 ⟶ G.𝓥) : P.HalfEdgeLabel × F.𝓔 × F.𝓥 → P.HalfEdgeLabel × G.𝓔 × G.𝓥

Given two maps F.𝓔 ⟶ G.𝓔 and F.𝓥 ⟶ G.𝓥 the corresponding map P.HalfEdgeLabel × F.𝓔 × F.𝓥 → P.HalfEdgeLabel × G.𝓔 × G.𝓥.

Equations

• FeynmanDiagram.edgeVertexMap 𝓔 𝓥 x = (x.1, 𝓔 x.2.1, 𝓥 x.2.2)

@[simp]

theorem FeynmanDiagram.edgeVertexMap_snd {P : PreFeynmanRule} {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ⟶ G.𝓔) (𝓥 : F.𝓥 ⟶ G.𝓥) (a✝ : P.HalfEdgeLabel × F.𝓔 × F.𝓥) : (edgeVertexMap 𝓔 𝓥 a✝).2 = (𝓔 a✝.2.1, 𝓥 a✝.2.2)

@[simp]

theorem FeynmanDiagram.edgeVertexMap_fst {P : PreFeynmanRule} {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ⟶ G.𝓔) (𝓥 : F.𝓥 ⟶ G.𝓥) (a✝ : P.HalfEdgeLabel × F.𝓔 × F.𝓥) : (edgeVertexMap 𝓔 𝓥 a✝).1 = a✝.1

def FeynmanDiagram.edgeVertexEquiv {P : PreFeynmanRule} {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ≃ G.𝓔) (𝓥 : F.𝓥 ≃ G.𝓥) : P.HalfEdgeLabel × F.𝓔 × F.𝓥 ≃ P.HalfEdgeLabel × G.𝓔 × G.𝓥

Given equivalences F.𝓔 ≃ G.𝓔 and F.𝓥 ≃ G.𝓥, the induced equivalence between P.HalfEdgeLabel × F.𝓔 × F.𝓥 and P.HalfEdgeLabel × G.𝓔 × G.𝓥

Equations

• FeynmanDiagram.edgeVertexEquiv 𝓔 𝓥 = { toFun := FeynmanDiagram.edgeVertexMap 𝓔.toFun 𝓥.toFun, invFun := FeynmanDiagram.edgeVertexMap 𝓔.invFun 𝓥.invFun, left_inv := ⋯, right_inv := ⋯ }

def FeynmanDiagram.edgeVertexFunc {P : PreFeynmanRule} {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ⟶ G.𝓔) (𝓥 : F.𝓥 ⟶ G.𝓥) : CategoryTheory.Functor (CategoryTheory.Over (P.HalfEdgeLabel × F.𝓔 × F.𝓥)) (CategoryTheory.Over (P.HalfEdgeLabel × G.𝓔 × G.𝓥))

The functor of over-categories generated by edgeVertexMap.

Equations

• FeynmanDiagram.edgeVertexFunc 𝓔 𝓥 = CategoryTheory.Over.map (FeynmanDiagram.edgeVertexMap 𝓔 𝓥)

@[simp]

theorem FeynmanDiagram.edgeVertexFunc_obj_left {P : PreFeynmanRule} {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ⟶ G.𝓔) (𝓥 : F.𝓥 ⟶ G.𝓥) (X : CategoryTheory.Comma (CategoryTheory.Functor.id Type) (CategoryTheory.Functor.fromPUnit (P.HalfEdgeLabel × F.𝓔 × F.𝓥))) : ((edgeVertexFunc 𝓔 𝓥).obj X).left = X.left

@[simp]

theorem FeynmanDiagram.edgeVertexFunc_map_left {P : PreFeynmanRule} {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ⟶ G.𝓔) (𝓥 : F.𝓥 ⟶ G.𝓥) {X✝ Y✝ : CategoryTheory.Comma (CategoryTheory.Functor.id Type) (CategoryTheory.Functor.fromPUnit (P.HalfEdgeLabel × F.𝓔 × F.𝓥))} (f : X✝ ⟶ Y✝) (a✝ : X✝.left) : ((edgeVertexFunc 𝓔 𝓥).map f).left a✝ = f.left a✝

@[simp]

theorem FeynmanDiagram.edgeVertexFunc_map_right {P : PreFeynmanRule} {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ⟶ G.𝓔) (𝓥 : F.𝓥 ⟶ G.𝓥) {X✝ Y✝ : CategoryTheory.Comma (CategoryTheory.Functor.id Type) (CategoryTheory.Functor.fromPUnit (P.HalfEdgeLabel × F.𝓔 × F.𝓥))} (f : X✝ ⟶ Y✝) : ((edgeVertexFunc 𝓔 𝓥).map f).right = CategoryTheory.CategoryStruct.id X✝.right

@[simp]

theorem FeynmanDiagram.edgeVertexFunc_obj_hom {P : PreFeynmanRule} {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ⟶ G.𝓔) (𝓥 : F.𝓥 ⟶ G.𝓥) (X : CategoryTheory.Comma (CategoryTheory.Functor.id Type) (CategoryTheory.Functor.fromPUnit (P.HalfEdgeLabel × F.𝓔 × F.𝓥))) (a✝ : (CategoryTheory.Functor.id Type).obj X.left) : ((edgeVertexFunc 𝓔 𝓥).obj X).hom a✝ = edgeVertexMap 𝓔 𝓥 (X.hom a✝)

structure FeynmanDiagram.Hom {P : PreFeynmanRule} (F G : FeynmanDiagram P) : Type

A morphism of Feynman diagrams.

• 𝓔𝓞 : F.𝓔𝓞 ⟶ G.𝓔𝓞

  The morphism of edge objects.

• 𝓥𝓞 : F.𝓥𝓞 ⟶ G.𝓥𝓞

  The morphism of vertex objects.

• 𝓱𝓔To𝓔𝓥 : (edgeVertexFunc self.𝓔𝓞.left self.𝓥𝓞.left).obj F.𝓱𝓔To𝓔𝓥 ⟶ G.𝓱𝓔To𝓔𝓥

  The morphism of half-edge objects.

def FeynmanDiagram.Hom.𝓔 {P : PreFeynmanRule} {F G : FeynmanDiagram P} (f : F.Hom G) : F.𝓔 → G.𝓔

The map F.𝓔 → G.𝓔 induced by a homomorphism of Feynman diagrams.

Equations

• f.𝓔 = f.𝓔𝓞.left

def FeynmanDiagram.Hom.𝓥 {P : PreFeynmanRule} {F G : FeynmanDiagram P} (f : F.Hom G) : F.𝓥 → G.𝓥

The map F.𝓥 → G.𝓥 induced by a homomorphism of Feynman diagrams.

Equations

• f.𝓥 = f.𝓥𝓞.left

def FeynmanDiagram.Hom.𝓱𝓔 {P : PreFeynmanRule} {F G : FeynmanDiagram P} (f : F.Hom G) : F.𝓱𝓔 → G.𝓱𝓔

The map F.𝓱𝓔 → G.𝓱𝓔 induced by a homomorphism of Feynman diagrams.

Equations

• f.𝓱𝓔 = f.𝓱𝓔To𝓔𝓥.left

def FeynmanDiagram.Hom.𝓱𝓔𝓞 {P : PreFeynmanRule} {F G : FeynmanDiagram P} (f : F.Hom G) : F.𝓱𝓔𝓞 ⟶ G.𝓱𝓔𝓞

The morphism F.𝓱𝓔𝓞 ⟶ G.𝓱𝓔𝓞 induced by a homomorphism of Feynman diagrams.

Equations

• f.𝓱𝓔𝓞 = P.toHalfEdge.map f.𝓱𝓔To𝓔𝓥

def FeynmanDiagram.Hom.id {P : PreFeynmanRule} (F : FeynmanDiagram P) : F.Hom F

The identity morphism for a Feynman diagram.

Equations

• FeynmanDiagram.Hom.id F = { 𝓔𝓞 := CategoryTheory.CategoryStruct.id F.𝓔𝓞, 𝓥𝓞 := CategoryTheory.CategoryStruct.id F.𝓥𝓞, 𝓱𝓔To𝓔𝓥 := CategoryTheory.CategoryStruct.id F.𝓱𝓔To𝓔𝓥 }

def FeynmanDiagram.Hom.comp {P : PreFeynmanRule} {F G H : FeynmanDiagram P} (f : F.Hom G) (g : G.Hom H) : F.Hom H

The composition of two morphisms of Feynman diagrams.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FeynmanDiagram.Hom.comp_𝓔𝓞_left {P : PreFeynmanRule} {F G H : FeynmanDiagram P} (f : F.Hom G) (g : G.Hom H) (a✝ : F.𝓔𝓞.left) : (f.comp g).𝓔𝓞.left a✝ = g.𝓔𝓞.left (f.𝓔𝓞.left a✝)

@[simp]

theorem FeynmanDiagram.Hom.comp_𝓱𝓔To𝓔𝓥_left {P : PreFeynmanRule} {F G H : FeynmanDiagram P} (f : F.Hom G) (g : G.Hom H) (a✝ : ((edgeVertexFunc (CategoryTheory.CategoryStruct.comp f.𝓔𝓞 g.𝓔𝓞).left (CategoryTheory.CategoryStruct.comp f.𝓥𝓞 g.𝓥𝓞).left).obj F.𝓱𝓔To𝓔𝓥).left) : (f.comp g).𝓱𝓔To𝓔𝓥.left a✝ = g.𝓱𝓔To𝓔𝓥.left (f.𝓱𝓔To𝓔𝓥.left a✝)

@[simp]

theorem FeynmanDiagram.Hom.comp_𝓥𝓞_left {P : PreFeynmanRule} {F G H : FeynmanDiagram P} (f : F.Hom G) (g : G.Hom H) (a✝ : F.𝓥𝓞.left) : (f.comp g).𝓥𝓞.left a✝ = g.𝓥𝓞.left (f.𝓥𝓞.left a✝)

theorem FeynmanDiagram.Hom.ext' {P : PreFeynmanRule} {F G : FeynmanDiagram P} {f g : F.Hom G} (h𝓔 : f.𝓔𝓞 = g.𝓔𝓞) (h𝓥 : f.𝓥𝓞 = g.𝓥𝓞) (h𝓱𝓔 : f.𝓱𝓔 = g.𝓱𝓔) : f = g

theorem FeynmanDiagram.Hom.ext {P : PreFeynmanRule} {F G : FeynmanDiagram P} {f g : F.Hom G} (h𝓔 : f.𝓔 = g.𝓔) (h𝓥 : f.𝓥 = g.𝓥) (h𝓱𝓔 : f.𝓱𝓔 = g.𝓱𝓔) : f = g

def FeynmanDiagram.Hom.Cond {P : PreFeynmanRule} {F G : FeynmanDiagram P} (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔) : Prop

The condition on maps of edges, vertices and half-edges for it to be lifted to a morphism of Feynman diagrams.

Equations

• One or more equations did not get rendered due to their size.

theorem FeynmanDiagram.Hom.cond_satisfied {P : PreFeynmanRule} {F G : FeynmanDiagram P} (f : F.Hom G) : Cond f.𝓔 f.𝓥 f.𝓱𝓔

theorem FeynmanDiagram.Hom.cond_symm {P : PreFeynmanRule} {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ≃ G.𝓔) (𝓥 : F.𝓥 ≃ G.𝓥) (𝓱𝓔 : F.𝓱𝓔 ≃ G.𝓱𝓔) (h : Cond ⇑𝓔 ⇑𝓥 ⇑𝓱𝓔) : Cond ⇑𝓔.symm ⇑𝓥.symm ⇑𝓱𝓔.symm

instance FeynmanDiagram.Hom.instDecidableForallEqObjDiscretePUnitFromPUnitEdgeLabelRight𝓔𝓞HomOfIsFiniteDiagramOfIsFinitePreFeynmanRule {P : PreFeynmanRule} {F G : FeynmanDiagram P} [F.IsFiniteDiagram] [P.IsFinitePreFeynmanRule] (𝓔 : F.𝓔 → G.𝓔) : Decidable (∀ (x : F.𝓔), G.𝓔𝓞.hom (𝓔 x) = F.𝓔𝓞.hom x)

If 𝓔 is a map between the edges of one finite Feynman diagram and another Feynman diagram, then deciding whether 𝓔 from a morphism in Over P.EdgeLabel between the edge maps is decidable.

Equations

• FeynmanDiagram.Hom.instDecidableForallEqObjDiscretePUnitFromPUnitEdgeLabelRight𝓔𝓞HomOfIsFiniteDiagramOfIsFinitePreFeynmanRule 𝓔 = Fintype.decidableForallFintype

instance FeynmanDiagram.Hom.instDecidableForallEqObjDiscretePUnitFromPUnitVertexLabelRight𝓥𝓞HomOfIsFiniteDiagramOfIsFinitePreFeynmanRule {P : PreFeynmanRule} {F G : FeynmanDiagram P} [F.IsFiniteDiagram] [P.IsFinitePreFeynmanRule] (𝓥 : F.𝓥 → G.𝓥) : Decidable (∀ (x : F.𝓥), G.𝓥𝓞.hom (𝓥 x) = F.𝓥𝓞.hom x)

If 𝓥 is a map between the vertices of one finite Feynman diagram and another Feynman diagram, then deciding whether 𝓥 from a morphism in Over P.VertexLabel between the vertex maps is decidable.

Equations

• FeynmanDiagram.Hom.instDecidableForallEqObjDiscretePUnitFromPUnitVertexLabelRight𝓥𝓞HomOfIsFiniteDiagramOfIsFinitePreFeynmanRule 𝓥 = Fintype.decidableForallFintype

instance FeynmanDiagram.Hom.instDecidableForallEqObjDiscretePUnitFromPUnitProdHalfEdgeLabelLeft𝓔𝓞𝓥𝓞Right𝓱𝓔To𝓔𝓥HomEdgeVertexMapOfIsFiniteDiagramOfIsFinitePreFeynmanRule {P : PreFeynmanRule} {F G : FeynmanDiagram P} [F.IsFiniteDiagram] [G.IsFiniteDiagram] [P.IsFinitePreFeynmanRule] (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔) : Decidable (∀ (x : F.𝓱𝓔), G.𝓱𝓔To𝓔𝓥.hom (𝓱𝓔 x) = edgeVertexMap 𝓔 𝓥 (F.𝓱𝓔To𝓔𝓥.hom x))

Given maps between parts of two Feynman diagrams, it is decidable to determine whether on mapping half-edges, the corresponding half-edge labels, edges and vertices are consistent.

Equations

• One or more equations did not get rendered due to their size.

instance FeynmanDiagram.Hom.instDecidableCondOfIsFiniteDiagramOfIsFinitePreFeynmanRule {P : PreFeynmanRule} {F G : FeynmanDiagram P} [F.IsFiniteDiagram] [G.IsFiniteDiagram] [P.IsFinitePreFeynmanRule] (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔) : Decidable (Cond 𝓔 𝓥 𝓱𝓔)

The condition on whether a map of maps of edges, vertices and half-edges can be lifted to a morphism of Feynman diagrams is decidable.

Equations

• FeynmanDiagram.Hom.instDecidableCondOfIsFiniteDiagramOfIsFinitePreFeynmanRule 𝓔 𝓥 𝓱𝓔 = instDecidableAnd

def FeynmanDiagram.Hom.mk' {P : PreFeynmanRule} {F G : FeynmanDiagram P} (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔) (C : Cond 𝓔 𝓥 𝓱𝓔) : F.Hom G

Making a Feynman diagram from maps of edges, vertices and half-edges.

Equations

• FeynmanDiagram.Hom.mk' 𝓔 𝓥 𝓱𝓔 C = { 𝓔𝓞 := CategoryTheory.Over.homMk 𝓔 ⋯, 𝓥𝓞 := CategoryTheory.Over.homMk 𝓥 ⋯, 𝓱𝓔To𝓔𝓥 := CategoryTheory.Over.homMk 𝓱𝓔 ⋯ }

@[simp]

theorem FeynmanDiagram.Hom.mk'_𝓔𝓞_left {P : PreFeynmanRule} {F G : FeynmanDiagram P} (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔) (C : Cond 𝓔 𝓥 𝓱𝓔) (a✝ : F.𝓔) : (mk' 𝓔 𝓥 𝓱𝓔 C).𝓔𝓞.left a✝ = 𝓔 a✝

@[simp]

theorem FeynmanDiagram.Hom.mk'_𝓱𝓔To𝓔𝓥_left {P : PreFeynmanRule} {F G : FeynmanDiagram P} (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔) (C : Cond 𝓔 𝓥 𝓱𝓔) (a✝ : F.𝓱𝓔) : (mk' 𝓔 𝓥 𝓱𝓔 C).𝓱𝓔To𝓔𝓥.left a✝ = 𝓱𝓔 a✝

@[simp]

theorem FeynmanDiagram.Hom.mk'_𝓥𝓞_left {P : PreFeynmanRule} {F G : FeynmanDiagram P} (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔) (C : Cond 𝓔 𝓥 𝓱𝓔) (a✝ : F.𝓥) : (mk' 𝓔 𝓥 𝓱𝓔 C).𝓥𝓞.left a✝ = 𝓥 a✝

theorem FeynmanDiagram.Hom.mk'_self {P : PreFeynmanRule} {F G : FeynmanDiagram P} (f : F.Hom G) : mk' f.𝓔 f.𝓥 f.𝓱𝓔 ⋯ = f

The Category of Feynman diagrams

Feynman diagrams, as defined above, form a category. We will be able to use this category to define the symmetry factor of a Feynman diagram, and the condition on whether a diagram is connected.

instance FeynmanDiagram.instCategory {P : PreFeynmanRule} : CategoryTheory.Category.{0, 1} (FeynmanDiagram P)

Feynman diagrams form a category.

Equations

• FeynmanDiagram.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[simp]

theorem FeynmanDiagram.instCategory_id_𝓱𝓔To𝓔𝓥_left {P : PreFeynmanRule} (F : FeynmanDiagram P) (a✝ : F.𝓱𝓔To𝓔𝓥.left) : (CategoryTheory.CategoryStruct.id F).𝓱𝓔To𝓔𝓥.left a✝ = a✝

@[simp]

theorem FeynmanDiagram.instCategory_id_𝓔𝓞_left {P : PreFeynmanRule} (F : FeynmanDiagram P) (a✝ : F.𝓔𝓞.left) : (CategoryTheory.CategoryStruct.id F).𝓔𝓞.left a✝ = a✝

@[simp]

theorem FeynmanDiagram.instCategory_comp_𝓔𝓞_left {P : PreFeynmanRule} {X✝ Y✝ Z✝ : FeynmanDiagram P} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) (a✝ : X✝.𝓔𝓞.left) : (CategoryTheory.CategoryStruct.comp f g).𝓔𝓞.left a✝ = g.𝓔𝓞.left (f.𝓔𝓞.left a✝)

@[simp]

theorem FeynmanDiagram.instCategory_comp_𝓱𝓔To𝓔𝓥_left {P : PreFeynmanRule} {X✝ Y✝ Z✝ : FeynmanDiagram P} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) (a✝ : ((edgeVertexFunc (CategoryTheory.CategoryStruct.comp f.𝓔𝓞 g.𝓔𝓞).left (CategoryTheory.CategoryStruct.comp f.𝓥𝓞 g.𝓥𝓞).left).obj X✝.𝓱𝓔To𝓔𝓥).left) : (CategoryTheory.CategoryStruct.comp f g).𝓱𝓔To𝓔𝓥.left a✝ = g.𝓱𝓔To𝓔𝓥.left (f.𝓱𝓔To𝓔𝓥.left a✝)

@[simp]

theorem FeynmanDiagram.instCategory_comp_𝓥𝓞_left {P : PreFeynmanRule} {X✝ Y✝ Z✝ : FeynmanDiagram P} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) (a✝ : X✝.𝓥𝓞.left) : (CategoryTheory.CategoryStruct.comp f g).𝓥𝓞.left a✝ = g.𝓥𝓞.left (f.𝓥𝓞.left a✝)

@[simp]

theorem FeynmanDiagram.instCategory_id_𝓥𝓞_left {P : PreFeynmanRule} (F : FeynmanDiagram P) (a✝ : F.𝓥𝓞.left) : (CategoryTheory.CategoryStruct.id F).𝓥𝓞.left a✝ = a✝

def FeynmanDiagram.mkIso {P : PreFeynmanRule} {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ≃ G.𝓔) (𝓥 : F.𝓥 ≃ G.𝓥) (𝓱𝓔 : F.𝓱𝓔 ≃ G.𝓱𝓔) (C : Hom.Cond ⇑𝓔 ⇑𝓥 ⇑𝓱𝓔) : F ≅ G

An isomorphism of Feynman diagrams from isomorphisms of edges, vertices and half-edges.

Equations

• FeynmanDiagram.mkIso 𝓔 𝓥 𝓱𝓔 C = { hom := FeynmanDiagram.Hom.mk' (⇑𝓔) (⇑𝓥) (⇑𝓱𝓔) C, inv := FeynmanDiagram.Hom.mk' ⇑𝓔.symm ⇑𝓥.symm ⇑𝓱𝓔.symm ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }

def FeynmanDiagram.func𝓔𝓞 {P : PreFeynmanRule} : CategoryTheory.Functor (FeynmanDiagram P) (CategoryTheory.Over P.EdgeLabel)

The functor from Feynman diagrams to category over edge labels.

Equations

• FeynmanDiagram.func𝓔𝓞 = { obj := fun (F : FeynmanDiagram P) => F.𝓔𝓞, map := fun {X Y : FeynmanDiagram P} (f : X ⟶ Y) => f.𝓔𝓞, map_id := ⋯, map_comp := ⋯ }

def FeynmanDiagram.func𝓥𝓞 {P : PreFeynmanRule} : CategoryTheory.Functor (FeynmanDiagram P) (CategoryTheory.Over P.VertexLabel)

The functor from Feynman diagrams to category over vertex labels.

Equations

• FeynmanDiagram.func𝓥𝓞 = { obj := fun (F : FeynmanDiagram P) => F.𝓥𝓞, map := fun {X Y : FeynmanDiagram P} (f : X ⟶ Y) => f.𝓥𝓞, map_id := ⋯, map_comp := ⋯ }

def FeynmanDiagram.func𝓱𝓔𝓞 {P : PreFeynmanRule} : CategoryTheory.Functor (FeynmanDiagram P) (CategoryTheory.Over P.HalfEdgeLabel)

The functor from Feynman diagrams to category over half-edge labels.

Equations

• FeynmanDiagram.func𝓱𝓔𝓞 = { obj := fun (F : FeynmanDiagram P) => F.𝓱𝓔𝓞, map := fun {X Y : FeynmanDiagram P} (f : X ⟶ Y) => FeynmanDiagram.Hom.𝓱𝓔𝓞 f, map_id := ⋯, map_comp := ⋯ }

def FeynmanDiagram.func𝓔 {P : PreFeynmanRule} : CategoryTheory.Functor (FeynmanDiagram P) Type

The functor from Feynman diagrams to Type landing on edges.

Equations

• FeynmanDiagram.func𝓔 = { obj := fun (F : FeynmanDiagram P) => F.𝓔, map := fun {X Y : FeynmanDiagram P} (f : X ⟶ Y) => FeynmanDiagram.Hom.𝓔 f, map_id := ⋯, map_comp := ⋯ }

def FeynmanDiagram.func𝓥 {P : PreFeynmanRule} : CategoryTheory.Functor (FeynmanDiagram P) Type

The functor from Feynman diagrams to Type landing on vertices.

Equations

• FeynmanDiagram.func𝓥 = { obj := fun (F : FeynmanDiagram P) => F.𝓥, map := fun {X Y : FeynmanDiagram P} (f : X ⟶ Y) => FeynmanDiagram.Hom.𝓥 f, map_id := ⋯, map_comp := ⋯ }

def FeynmanDiagram.func𝓱𝓔 {P : PreFeynmanRule} : CategoryTheory.Functor (FeynmanDiagram P) Type

The functor from Feynman diagrams to Type landing on half-edges.

Equations

• FeynmanDiagram.func𝓱𝓔 = { obj := fun (F : FeynmanDiagram P) => F.𝓱𝓔, map := fun {X Y : FeynmanDiagram P} (f : X ⟶ Y) => FeynmanDiagram.Hom.𝓱𝓔 f, map_id := ⋯, map_comp := ⋯ }

Symmetry factors

The symmetry factor of a Feynman diagram is the cardinality of the group of automorphisms of that diagram.

We show that the symmetry factor for a finite Feynman diagram is finite.

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

The type of isomorphisms of a Feynman diagram.

Equations

• F.SymmetryType = (F ≅ F)

def FeynmanDiagram.symmetryTypeEquiv {P : PreFeynmanRule} (F : FeynmanDiagram P) : F.SymmetryType ≃ { S : Equiv.Perm F.𝓔 × Equiv.Perm F.𝓥 × Equiv.Perm F.𝓱𝓔 // Hom.Cond ⇑S.1 ⇑S.2.1 ⇑S.2.2 }

An equivalence between SymmetryType and permutation of edges, vertices and half-edges satisfying Hom.Cond.

Equations

• One or more equations did not get rendered due to their size.

instance FeynmanDiagram.instFintypeSymmetryTypeOfIsFinitePreFeynmanRuleOfIsFiniteDiagram {P : PreFeynmanRule} (F : FeynmanDiagram P) [P.IsFinitePreFeynmanRule] [F.IsFiniteDiagram] : Fintype F.SymmetryType

For a finite Feynman diagram, the type of automorphisms of that Feynman diagram is finite.

Equations

• One or more equations did not get rendered due to their size.

def FeynmanDiagram.cardSymmetryFactor {P : PreFeynmanRule} (F : FeynmanDiagram P) : Cardinal.{0}

The symmetry factor can be defined as the cardinal of the symmetry type. In general this is not a finite number.

Equations

• F.cardSymmetryFactor = Cardinal.mk F.SymmetryType

def FeynmanDiagram.symmetryFactor {P : PreFeynmanRule} (F : FeynmanDiagram P) [P.IsFinitePreFeynmanRule] [F.IsFiniteDiagram] : ℕ

The symmetry factor of a Finite Feynman diagram, as a natural number.

Equations

• F.symmetryFactor = Fintype.card F.SymmetryType

@[simp]

theorem FeynmanDiagram.symmetryFactor_eq_cardSymmetryFactor {P : PreFeynmanRule} (F : FeynmanDiagram P) [P.IsFinitePreFeynmanRule] [F.IsFiniteDiagram] : ↑F.symmetryFactor = F.cardSymmetryFactor

Connectedness

Given a Feynman diagram we can create a simple graph based on the obvious adjacency relation. A feynman diagram is connected if its simple graph is connected.

TODO

• Complete this section.

def FeynmanDiagram.AdjRelation {P : PreFeynmanRule} (F : FeynmanDiagram P) : F.𝓥 → F.𝓥 → Prop

A relation on the vertices of Feynman diagrams. The proposition is true if the two vertices are not equal and are connected by a single edge. This is the adjacency relation.

Equations

• F.AdjRelation x y = (x ≠ y ∧ ∃ (a : F.𝓱𝓔) (b : F.𝓱𝓔), (F.𝓱𝓔To𝓔𝓥.hom a).2.1 = (F.𝓱𝓔To𝓔𝓥.hom b).2.1 ∧ (F.𝓱𝓔To𝓔𝓥.hom a).2.2 = x ∧ (F.𝓱𝓔To𝓔𝓥.hom b).2.2 = y)

instance FeynmanDiagram.instDecidableRel𝓥AdjRelationOfIsFiniteDiagram {P : PreFeynmanRule} (F : FeynmanDiagram P) [F.IsFiniteDiagram] : DecidableRel F.AdjRelation

The condition on whether two vertices are adjacent is decidable.

Equations

• F.instDecidableRel𝓥AdjRelationOfIsFiniteDiagram x✝¹ x✝ = instDecidableAnd

def FeynmanDiagram.toSimpleGraph {P : PreFeynmanRule} (F : FeynmanDiagram P) : SimpleGraph F.𝓥

From a Feynman diagram the simple graph showing those vertices which are connected.

Equations

• F.toSimpleGraph = { Adj := F.AdjRelation, symm := ⋯, loopless := ⋯ }

instance FeynmanDiagram.instDecidableRel𝓥AdjToSimpleGraphOfIsFiniteDiagram {P : PreFeynmanRule} (F : FeynmanDiagram P) [F.IsFiniteDiagram] : DecidableRel F.toSimpleGraph.Adj

The adjacency relation for a simple graph created by a finite Feynman diagram is a decidable relation.

Equations

• F.instDecidableRel𝓥AdjToSimpleGraphOfIsFiniteDiagram = F.instDecidableRel𝓥AdjRelationOfIsFiniteDiagram

instance FeynmanDiagram.instDecidableAndPreconnected𝓥ToSimpleGraphNonemptyOfIsFiniteDiagram {P : PreFeynmanRule} (F : FeynmanDiagram P) [F.IsFiniteDiagram] : Decidable (F.toSimpleGraph.Preconnected ∧ Nonempty F.𝓥)

For a finite feynman diagram it is decidable whether it is preconnected and has the Feynman diagram has a non-empty type of vertices.

Equations

• F.instDecidableAndPreconnected𝓥ToSimpleGraphNonemptyOfIsFiniteDiagram = instDecidableAnd

instance FeynmanDiagram.instDecidableConnected𝓥ToSimpleGraphOfIsFiniteDiagram {P : PreFeynmanRule} (F : FeynmanDiagram P) [F.IsFiniteDiagram] : Decidable F.toSimpleGraph.Connected

For a finite Feynman diagram it is decidable whether the simple graph corresponding to it is connected.

Equations

• F.instDecidableConnected𝓥ToSimpleGraphOfIsFiniteDiagram = decidable_of_iff (F.toSimpleGraph.Preconnected ∧ Nonempty F.𝓥) ⋯

def FeynmanDiagram.Connected {P : PreFeynmanRule} (F : FeynmanDiagram P) : Prop

A Feynman diagram is connected if its simple graph is connected.

Equations

• F.Connected = F.toSimpleGraph.Connected

instance FeynmanDiagram.instDecidableConnectedOfIsFiniteDiagram {P : PreFeynmanRule} (F : FeynmanDiagram P) [F.IsFiniteDiagram] : Decidable F.Connected

For a finite Feynman diagram it is decidable whether or not it is connected.

Equations

• F.instDecidableConnectedOfIsFiniteDiagram = F.instDecidableConnected𝓥ToSimpleGraphOfIsFiniteDiagram