From a5e9d04941c29cf57476c89f90ccef223a9c106b Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 17 Jun 2024 14:05:45 -0400
Subject: [PATCH 1/3] feat: Add general definition of Feynman diagrams

---
 HepLean/FeynmanDiagrams/Basic.lean | 249 +++++++++++++++++++++++++++++
 1 file changed, 249 insertions(+)
 create mode 100644 HepLean/FeynmanDiagrams/Basic.lean

diff --git a/HepLean/FeynmanDiagrams/Basic.lean b/HepLean/FeynmanDiagrams/Basic.lean
new file mode 100644
index 0000000..97afc3f
--- /dev/null
+++ b/HepLean/FeynmanDiagrams/Basic.lean
@@ -0,0 +1,249 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import Mathlib.Logic.Equiv.Fin
+import Mathlib.Tactic.FinCases
+import Mathlib.Data.Finset.Card
+import Mathlib.CategoryTheory.IsomorphismClasses
+import Mathlib.CategoryTheory.Functor.Category
+import Mathlib.CategoryTheory.Comma.Over
+import Mathlib.Data.Fintype.Pi
+import Mathlib.CategoryTheory.Limits.Shapes.Terminal
+import Mathlib.Data.Fintype.Prod
+import Mathlib.Data.Fintype.Perm
+import Mathlib.Combinatorics.SimpleGraph.Basic
+import Mathlib.Combinatorics.SimpleGraph.Connectivity
+import Mathlib.SetTheory.Cardinal.Basic
+/-!
+# Feynman diagrams
+
+Feynman diagrams are a graphical representation of the terms in the perturbation expansion of
+a quantum field theory.
+
+
+-/
+
+open CategoryTheory
+/-!
+
+## 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.
+
+-/
+
+/-- 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.) -/
+structure PreFeynmanRule where
+  /-- The type labelling the different half-edges. -/
+  HalfEdgeLabel : Type
+  /-- A type labelling the different types of edges. -/
+  EdgeLabel : Type
+  /-- A type labelling the different types of vertices. -/
+  VertexLabel : Type
+  /-- A function taking `EdgeLabels` to the half edges it contains. -/
+  edgeLabelMap : EdgeLabel → CategoryTheory.Over HalfEdgeLabel
+  /-- A function taking `VertexLabels` to the half edges it contains. -/
+  vertexLabelMap : VertexLabel → CategoryTheory.Over HalfEdgeLabel
+
+namespace PreFeynmanRule
+
+variable (P : PreFeynmanRule)
+
+/-- The functor from `Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel)`
+  to `Over (P.VertexLabel)` induced by projections on products. -/
+@[simps!]
+def toVertex {𝓔 𝓥 : Type} : Over (P.HalfEdgeLabel × 𝓔 × 𝓥) ⥤ Over 𝓥 :=
+  Over.map <| Prod.snd ∘ Prod.snd
+
+/-- The functor from `Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel)`
+  to `Over (P.EdgeLabel)` induced by projections on products. -/
+@[simps!]
+def toEdge {𝓔 𝓥 : Type} : Over (P.HalfEdgeLabel × 𝓔 × 𝓥) ⥤ Over 𝓔 :=
+  Over.map <| Prod.fst ∘ Prod.snd
+
+/-- The functor from `Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel)`
+  to `Over (P.HalfEdgeLabel)` induced by projections on products. -/
+@[simps!]
+def toHalfEdge {𝓔 𝓥 : Type}  : Over (P.HalfEdgeLabel × 𝓔 × 𝓥) ⥤ Over P.HalfEdgeLabel :=
+  Over.map Prod.fst
+
+/-- The functor from `Over P.VertexLabel` to `Type` induced by pull-back along insertion of
+  `v : P.VertexLabel`. -/
+@[simps!]
+def preimageType' {𝓥 : Type} (v : 𝓥) : Over 𝓥 ⥤ Type where
+  obj := fun f =>  f.hom ⁻¹' {v}
+  map {f g} F := fun x =>
+    ⟨F.left x.1, by
+      have h := congrFun F.w x
+      simp only [Functor.const_obj_obj, Functor.id_obj, Functor.id_map, types_comp_apply,
+        CostructuredArrow.right_eq_id, Functor.const_obj_map, types_id_apply] at h
+      simpa [h] using x.2⟩
+
+/-- The functor from `Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel)` to
+  `Over P.HalfEdgeLabel` induced by pull-back along insertion of `v : P.VertexLabel`.  -/
+def preimageVertex  {𝓔 𝓥 : Type} (v : 𝓥) :
+    Over (P.HalfEdgeLabel × 𝓔 × 𝓥) ⥤ Over P.HalfEdgeLabel where
+  obj f := Over.mk (fun x =>  Prod.fst (f.hom x.1) :
+     (P.toVertex ⋙ preimageType' v).obj f ⟶ P.HalfEdgeLabel)
+  map {f g} F := Over.homMk ((P.toVertex ⋙ preimageType' v).map F)
+    (funext <| fun x => congrArg Prod.fst <| congrFun F.w x.1)
+
+/-- The functor from `Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel)` to
+  `Over P.HalfEdgeLabel` induced by pull-back along insertion of `v : P.EdgeLabel`.  -/
+def preimageEdge {𝓔 𝓥 : Type} (v : 𝓔) :
+    Over (P.HalfEdgeLabel ×  𝓔 × 𝓥) ⥤ Over P.HalfEdgeLabel where
+  obj f := Over.mk (fun x =>  Prod.fst (f.hom x.1) :
+     (P.toEdge ⋙ preimageType' v).obj f ⟶ P.HalfEdgeLabel)
+  map {f g} F := Over.homMk ((P.toEdge ⋙ preimageType' v).map F)
+    (funext <| fun x => congrArg Prod.fst <| congrFun F.w x.1)
+
+/-- 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. -/
+def diagramVertexProp {𝓔 𝓥 : Type} (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥))
+    (f : 𝓥 ⟶ P.VertexLabel) :=
+  ∀ v, IsIsomorphic (P.vertexLabelMap (f v)) ((P.preimageVertex v).obj F)
+
+
+/-- 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. -/
+def diagramEdgeProp {𝓔 𝓥 : Type} (F : Over (P.HalfEdgeLabel  × 𝓔 × 𝓥))
+    (f : 𝓔 ⟶ P.EdgeLabel) :=
+  ∀ v, IsIsomorphic (P.edgeLabelMap (f v)) ((P.preimageEdge v).obj F)
+
+/-- The proposition which must be satisfied by an object
+  `F : Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel)` for it to be a Feynman diagram. cs-/
+def diagramProp {𝓔 𝓥 : Type} (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥))
+  (f𝓔 : 𝓔 ⟶ P.EdgeLabel) (f𝓥 :  𝓥 ⟶ P.VertexLabel) :=
+  diagramVertexProp P F f𝓥 ∧ diagramEdgeProp P F f𝓔
+
+end PreFeynmanRule
+
+/-!
+
+## The definition of Feynman diagrams
+
+We now define the type of Feynman diagrams for a given pre-Feynman rule.
+
+-/
+
+open PreFeynmanRule
+
+/-- The type of Feynman diagrams given a `PreFeynmanRule`. -/
+structure FeynmanDiagram (P : PreFeynmanRule) where
+  /-- The type of edges in the Feynman diagram, labelled by their type. -/
+  𝓔𝓞 : Over P.EdgeLabel
+  /-- The type of vertices in the Feynman diagram, labelled by their type. -/
+  𝓥𝓞 : Over P.VertexLabel
+  /-- The type of half-edges in the Feynman diagram, labelled by their type, the edge it
+  belongs to, and the vertex they belong to. -/
+  𝓱𝓔To𝓔𝓥 : Over (P.HalfEdgeLabel × 𝓔𝓞.left × 𝓥𝓞.left)
+  /-- Each edge has the correct type of half edges. -/
+  𝓔Cond : P.diagramEdgeProp 𝓱𝓔 𝓔𝓞.hom
+  /-- Each vertex has the correct sort of half edges. -/
+  𝓥Cond : P.diagramVertexProp 𝓱𝓔 𝓥𝓞.hom
+
+namespace FeynmanDiagram
+
+variable {P : PreFeynmanRule} (F : FeynmanDiagram P)
+
+/-- The type of edges. -/
+def 𝓔 : Type := F.𝓔𝓞.left
+
+/-- The type of vertices. -/
+def 𝓥 : Type := F.𝓥𝓞.left
+
+/-- The type of half-edges. -/
+def 𝓱𝓔 : Type := F.𝓱𝓔To𝓔𝓥.left
+
+/-- The object in Over P.HalfEdgeLabel generated by a Feynman diagram. -/
+def 𝓱𝓔𝓞 : Over P.HalfEdgeLabel := P.toHalfEdge.obj F.𝓱𝓔To𝓔𝓥
+
+/-- Given two maps `F.𝓔𝓞 ⟶ G.𝓔𝓞` and `F.𝓥𝓞 ⟶ G.𝓥𝓞` the corresponding map
+  `P.HalfEdgeLabel × F.𝓔𝓞.left × F.𝓥𝓞.left →  P.HalfEdgeLabel × G.𝓔𝓞.left × G.𝓥𝓞.left`.  -/
+def edgeVertexMap {F G : FeynmanDiagram P} (𝓔 : F.𝓔𝓞 ⟶ G.𝓔𝓞) (𝓥 : F.𝓥𝓞 ⟶ G.𝓥𝓞) :
+    P.HalfEdgeLabel × F.𝓔𝓞.left × F.𝓥𝓞.left →  P.HalfEdgeLabel × G.𝓔𝓞.left × G.𝓥𝓞.left :=
+  fun x => ⟨x.1, 𝓔.left x.2.1, 𝓥.left x.2.2⟩
+
+/-- The functor of over-categories generated by `edgeVertexMap`. -/
+def edgeVertexFunc {F G : FeynmanDiagram P} (𝓔 : F.𝓔𝓞 ⟶ G.𝓔𝓞) (𝓥 : F.𝓥𝓞 ⟶ G.𝓥𝓞) :
+   Over (P.HalfEdgeLabel × F.𝓔𝓞.left × F.𝓥𝓞.left)
+   ⥤ Over (P.HalfEdgeLabel × G.𝓔𝓞.left × G.𝓥𝓞.left) :=
+  Over.map <| edgeVertexMap 𝓔 𝓥
+
+/-- A morphism of Feynman diagrams. -/
+structure Hom (F G : FeynmanDiagram P) where
+  /-- The morphism of edge objects. -/
+  𝓔 : F.𝓔𝓞 ⟶ G.𝓔𝓞
+  /-- The morphism of vertex objects. -/
+  𝓥 : F.𝓥𝓞 ⟶ G.𝓥𝓞
+  /-- The morphism of half-edge objects. -/
+  𝓱𝓔 : (edgeVertexFunc 𝓔 𝓥).obj F.𝓱𝓔To𝓔𝓥 ⟶ G.𝓱𝓔To𝓔𝓥
+
+namespace Hom
+
+/-- The identity morphism for a Feynman diagram. -/
+def id (F : FeynmanDiagram P) : Hom F F where
+  𝓔 := 𝟙 F.𝓔𝓞
+  𝓥 := 𝟙 F.𝓥𝓞
+  𝓱𝓔 := 𝟙 F.𝓱𝓔To𝓔𝓥
+
+/-- The composition of two morphisms of Feynman diagrams. -/
+def comp {F G H : FeynmanDiagram P} (f : Hom F G) (g : Hom G H) : Hom F H where
+  𝓔 := f.𝓔 ≫ g.𝓔
+  𝓥 := f.𝓥 ≫ g.𝓥
+  𝓱𝓔 := (edgeVertexFunc g.𝓔 g.𝓥).map f.𝓱𝓔 ≫ g.𝓱𝓔
+
+lemma ext {F G : FeynmanDiagram P} {f g : Hom F G} (h𝓔 : f.𝓔 = g.𝓔)
+    (h𝓥 : f.𝓥 = g.𝓥) (h𝓱𝓔 : f.𝓱𝓔.left = g.𝓱𝓔.left) : f = g := by
+  cases f
+  cases g
+  subst h𝓔 h𝓥
+  simp_all only [mk.injEq, heq_eq_eq, true_and]
+  ext a : 2
+  simp_all only
+
+end Hom
+
+/-- Feynman diagrams form a category. -/
+instance : Category (FeynmanDiagram P) where
+  Hom := Hom
+  id := Hom.id
+  comp := Hom.comp
+
+/-- The functor from Feynman diagrams to category over edge labels. -/
+def toOverEdgeLabel : FeynmanDiagram P ⥤ Over P.EdgeLabel where
+  obj F := F.𝓔𝓞
+  map f := f.𝓔
+
+/-- The functor from Feynman diagrams to category over vertex labels. -/
+def toOverVertexLabel : FeynmanDiagram P ⥤ Over P.VertexLabel where
+  obj F := F.𝓥𝓞
+  map f := f.𝓥
+
+/-- The functor from Feynman diagrams to category over half-edge labels. -/
+def toOverHalfEdgeLabel : FeynmanDiagram P ⥤ Over P.HalfEdgeLabel where
+  obj F := F.𝓱𝓔𝓞
+  map f := P.toHalfEdge.map f.𝓱𝓔
+
+/-- The type of isomorphisms of a Feynman diagram. -/
+def symmetryType : Type := F ≅ F
+
+/-- The symmetry factor can be defined as the cardinal of the symmetry type.
+ In general this is not a finite number. -/
+def symmetryFactor : Cardinal := Cardinal.mk (F.symmetryType)
+
+
+end FeynmanDiagram

From 0a90f67a46dbe0e0dbe94df349ef560d75ac5bc0 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 18 Jun 2024 11:40:36 -0400
Subject: [PATCH 2/3] feat: Generalise Feynman diagrams

---
 HepLean/FeynmanDiagrams/Basic.lean            | 522 ++++++++++++++--
 .../Instances/ComplexScalar.lean              | 100 +++
 HepLean/FeynmanDiagrams/Instances/Phi4.lean   |  83 +++
 HepLean/FeynmanDiagrams/PhiFour/Basic.lean    | 583 ------------------
 4 files changed, 669 insertions(+), 619 deletions(-)
 create mode 100644 HepLean/FeynmanDiagrams/Instances/ComplexScalar.lean
 create mode 100644 HepLean/FeynmanDiagrams/Instances/Phi4.lean
 delete mode 100644 HepLean/FeynmanDiagrams/PhiFour/Basic.lean

diff --git a/HepLean/FeynmanDiagrams/Basic.lean b/HepLean/FeynmanDiagrams/Basic.lean
index 97afc3f..0230d38 100644
--- a/HepLean/FeynmanDiagrams/Basic.lean
+++ b/HepLean/FeynmanDiagrams/Basic.lean
@@ -106,6 +106,100 @@ def preimageEdge {𝓔 𝓥 : Type} (v : 𝓔) :
   map {f g} F := Over.homMk ((P.toEdge ⋙ preimageType' v).map F)
     (funext <| fun x => congrArg Prod.fst <| congrFun F.w x.1)
 
+
+/-!
+
+## Finitness of pre-Feynman rules
+
+We define a class of `PreFeynmanRule` which have nice properties with regard to
+decidablity and finitness.
+
+In practice, every pre-Feynman rule considered in the physics literature satisfies these
+properties.
+
+-/
+
+class IsFinitePreFeynmanRule (P : PreFeynmanRule) where
+  edgeLabelDecidable : DecidableEq P.EdgeLabel
+  vertexLabelDecidable : DecidableEq P.VertexLabel
+  halfEdgeLabelDecidable : DecidableEq P.HalfEdgeLabel
+  vertexMapFintype : ∀ v : P.VertexLabel, Fintype (P.vertexLabelMap v).left
+  vertexMapDecidable : ∀ v : P.VertexLabel, DecidableEq (P.vertexLabelMap v).left
+  edgeMapFintype : ∀ v : P.EdgeLabel, Fintype (P.edgeLabelMap v).left
+  edgeMapDecidable : ∀ v : P.EdgeLabel, DecidableEq (P.edgeLabelMap v).left
+
+instance preFeynmanRuleDecEq𝓔 (P : PreFeynmanRule) [IsFinitePreFeynmanRule P] :
+    DecidableEq P.EdgeLabel :=
+  IsFinitePreFeynmanRule.edgeLabelDecidable
+
+instance preFeynmanRuleDecEq𝓥 (P : PreFeynmanRule) [IsFinitePreFeynmanRule P] :
+    DecidableEq P.VertexLabel :=
+  IsFinitePreFeynmanRule.vertexLabelDecidable
+
+instance preFeynmanRuleDecEq𝓱𝓔 (P : PreFeynmanRule) [IsFinitePreFeynmanRule P] :
+    DecidableEq P.HalfEdgeLabel :=
+  IsFinitePreFeynmanRule.halfEdgeLabelDecidable
+
+instance [IsFinitePreFeynmanRule P] (v : P.VertexLabel) : Fintype (P.vertexLabelMap v).left :=
+  IsFinitePreFeynmanRule.vertexMapFintype v
+
+instance [IsFinitePreFeynmanRule P] (v : P.VertexLabel) : DecidableEq (P.vertexLabelMap v).left :=
+  IsFinitePreFeynmanRule.vertexMapDecidable v
+
+instance [IsFinitePreFeynmanRule P] (v : P.EdgeLabel) : Fintype (P.edgeLabelMap v).left :=
+  IsFinitePreFeynmanRule.edgeMapFintype v
+
+instance [IsFinitePreFeynmanRule P] (v : P.EdgeLabel) : DecidableEq (P.edgeLabelMap v).left :=
+  IsFinitePreFeynmanRule.edgeMapDecidable v
+
+instance preimageVertexDecidablePred {𝓔 𝓥 : Type} [DecidableEq 𝓥] (v : 𝓥)
+    (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) :
+    DecidablePred fun x => x ∈ (P.toVertex.obj F).hom ⁻¹' {v} := fun y =>
+  match decEq ((P.toVertex.obj F).hom y) v with
+  | isTrue h => isTrue h
+  | isFalse h => isFalse h
+
+instance preimageEdgeDecidablePred {𝓔 𝓥 : Type} [DecidableEq 𝓔] (v : 𝓔)
+    (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) :
+    DecidablePred fun x => x ∈ (P.toEdge.obj F).hom ⁻¹' {v} := fun y =>
+  match decEq ((P.toEdge.obj F).hom y) v with
+  | isTrue h => isTrue h
+  | isFalse h => isFalse h
+
+instance preimageVertexDecidable [IsFinitePreFeynmanRule P]  {𝓔 𝓥 : Type} (v : 𝓥)
+   (F : Over (P.HalfEdgeLabel  × 𝓔 × 𝓥)) [DecidableEq F.left] :
+    DecidableEq ((P.preimageVertex v).obj F).left := Subtype.instDecidableEq
+
+instance preimageEdgeDecidable [IsFinitePreFeynmanRule P]  {𝓔 𝓥 : Type} (v : 𝓔)
+   (F : Over (P.HalfEdgeLabel  × 𝓔 × 𝓥)) [DecidableEq F.left] :
+    DecidableEq ((P.preimageEdge v).obj F).left := Subtype.instDecidableEq
+
+instance preimageVertexFintype [IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type} [DecidableEq 𝓥] [Fintype 𝓥]
+    (v : 𝓥) (F : Over (P.HalfEdgeLabel  × 𝓔 × 𝓥)) [DecidableEq F.left] [h : Fintype F.left] :
+    Fintype ((P.preimageVertex v).obj F).left :=  @Subtype.fintype _ _ _ h
+
+instance preimageEdgeFintype [IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type} [DecidableEq 𝓔] [Fintype 𝓔]
+    (v : 𝓔) (F : Over (P.HalfEdgeLabel  × 𝓔 × 𝓥)) [DecidableEq F.left] [h : Fintype F.left] :
+    Fintype ((P.preimageEdge v).obj F).left :=  @Subtype.fintype _ _ _ h
+
+instance preimageVertexMapFintype  [IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type} [Fintype 𝓥]
+    [DecidableEq 𝓥]  (v : 𝓥) (f : 𝓥 ⟶ P.VertexLabel) (F : Over (P.HalfEdgeLabel  × 𝓔 × 𝓥))
+    [DecidableEq F.left] [Fintype F.left]:
+    Fintype  ((P.vertexLabelMap (f v)).left → ((P.preimageVertex v).obj F).left) :=
+  Pi.fintype
+
+instance preimageEdgeMapFintype  [IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type} [Fintype 𝓔]
+    [DecidableEq 𝓔] (v : 𝓔) (f : 𝓔 ⟶ P.EdgeLabel) (F : Over (P.HalfEdgeLabel  × 𝓔 × 𝓥))
+    [DecidableEq F.left] [Fintype F.left]:
+    Fintype  ((P.edgeLabelMap (f v)).left → ((P.preimageEdge v).obj F).left) :=
+  Pi.fintype
+
+/-!
+
+## Conditions to form a diagram.
+
+-/
+
 /-- 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
@@ -114,7 +208,6 @@ def diagramVertexProp {𝓔 𝓥 : Type} (F : Over (P.HalfEdgeLabel × 𝓔 × 
     (f : 𝓥 ⟶ P.VertexLabel) :=
   ∀ v, IsIsomorphic (P.vertexLabelMap (f v)) ((P.preimageVertex v).obj F)
 
-
 /-- 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
@@ -123,11 +216,56 @@ def diagramEdgeProp {𝓔 𝓥 : Type} (F : Over (P.HalfEdgeLabel  × 𝓔 × 
     (f : 𝓔 ⟶ P.EdgeLabel) :=
   ∀ v, IsIsomorphic (P.edgeLabelMap (f v)) ((P.preimageEdge v).obj F)
 
-/-- The proposition which must be satisfied by an object
-  `F : Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel)` for it to be a Feynman diagram. cs-/
-def diagramProp {𝓔 𝓥 : Type} (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥))
-  (f𝓔 : 𝓔 ⟶ P.EdgeLabel) (f𝓥 :  𝓥 ⟶ P.VertexLabel) :=
-  diagramVertexProp P F f𝓥 ∧ diagramEdgeProp P F f𝓔
+lemma diagramVertexProp_iff {𝓔 𝓥 : Type} (F : 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 := by
+  refine Iff.intro (fun h v => ?_) (fun h v => ?_)
+  obtain ⟨κ, κm1, h1, h2⟩ := h v
+  let f := (Over.forget P.HalfEdgeLabel).mapIso ⟨κ, κm1, h1, h2⟩
+  refine ⟨f.hom, (isIso_iff_bijective f.hom).mp $ Iso.isIso_hom f, κ.w⟩
+  obtain ⟨κ, h1, h2⟩ := h v
+  let f : (P.vertexLabelMap (f v)) ⟶ ((P.preimageVertex v).obj F) := Over.homMk κ h2
+  have ft : IsIso ((Over.forget P.HalfEdgeLabel).map f) := (isIso_iff_bijective κ).mpr h1
+  obtain ⟨fm, hf1, hf2⟩ := (isIso_of_reflects_iso _ (Over.forget P.HalfEdgeLabel) : IsIso f)
+  exact ⟨f, fm, hf1, hf2⟩
+
+lemma diagramEdgeProp_iff {𝓔 𝓥 : Type} (F : 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 := by
+  refine Iff.intro (fun h v => ?_) (fun h v => ?_)
+  obtain ⟨κ, κm1, h1, h2⟩ := h v
+  let f  := (Over.forget P.HalfEdgeLabel).mapIso ⟨κ, κm1, h1, h2⟩
+  refine ⟨f.hom, (isIso_iff_bijective f.hom).mp $ Iso.isIso_hom f, κ.w⟩
+  obtain ⟨κ, h1, h2⟩ := h v
+  let f : (P.edgeLabelMap (f v)) ⟶ ((P.preimageEdge v).obj F) := Over.homMk κ h2
+  have ft : IsIso ((Over.forget P.HalfEdgeLabel).map f) := (isIso_iff_bijective κ).mpr h1
+  obtain ⟨fm, hf1, hf2⟩ := (isIso_of_reflects_iso _ (Over.forget P.HalfEdgeLabel) : IsIso f)
+  exact ⟨f, fm, hf1, hf2⟩
+
+instance diagramVertexPropDecidable
+    [IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type} [Fintype 𝓥] [DecidableEq 𝓥]
+    (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [DecidableEq F.left] [Fintype F.left]
+    (f : 𝓥 ⟶ P.VertexLabel) : Decidable (P.diagramVertexProp F f) :=
+  @decidable_of_decidable_of_iff _ _
+    (@Fintype.decidableForallFintype _ _ (fun _ => @Fintype.decidableExistsFintype _ _
+    (fun _ => @And.decidable _ _ _ (@Fintype.decidablePiFintype _ _
+    (fun _ =>  P.preFeynmanRuleDecEq𝓱𝓔) _ _ _)) _ ) _)
+    (P.diagramVertexProp_iff F f).symm
+
+instance diagramEdgePropDecidable
+    [IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type} [Fintype 𝓔]  [DecidableEq 𝓔]
+    (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [DecidableEq F.left] [Fintype F.left]
+    (f : 𝓔 ⟶ P.EdgeLabel) : Decidable (P.diagramEdgeProp F f) :=
+  @decidable_of_decidable_of_iff _ _
+    (@Fintype.decidableForallFintype _ _ (fun _ => @Fintype.decidableExistsFintype _ _
+    (fun _ => @And.decidable _ _ _ (@Fintype.decidablePiFintype _ _
+    (fun _ =>  P.preFeynmanRuleDecEq𝓱𝓔) _ _ _)) _ ) _)
+    (P.diagramEdgeProp_iff F f).symm
+
 
 end PreFeynmanRule
 
@@ -151,9 +289,9 @@ structure FeynmanDiagram (P : PreFeynmanRule) where
   belongs to, and the vertex they belong to. -/
   𝓱𝓔To𝓔𝓥 : Over (P.HalfEdgeLabel × 𝓔𝓞.left × 𝓥𝓞.left)
   /-- Each edge has the correct type of half edges. -/
-  𝓔Cond : P.diagramEdgeProp 𝓱𝓔 𝓔𝓞.hom
+  𝓔Cond : P.diagramEdgeProp 𝓱𝓔To𝓔𝓥 𝓔𝓞.hom
   /-- Each vertex has the correct sort of half edges. -/
-  𝓥Cond : P.diagramVertexProp 𝓱𝓔 𝓥𝓞.hom
+  𝓥Cond : P.diagramVertexProp 𝓱𝓔To𝓔𝓥 𝓥𝓞.hom
 
 namespace FeynmanDiagram
 
@@ -171,79 +309,391 @@ def 𝓱𝓔 : Type := F.𝓱𝓔To𝓔𝓥.left
 /-- The object in Over P.HalfEdgeLabel generated by a Feynman diagram. -/
 def 𝓱𝓔𝓞 : Over P.HalfEdgeLabel := P.toHalfEdge.obj F.𝓱𝓔To𝓔𝓥
 
-/-- Given two maps `F.𝓔𝓞 ⟶ G.𝓔𝓞` and `F.𝓥𝓞 ⟶ G.𝓥𝓞` the corresponding map
-  `P.HalfEdgeLabel × F.𝓔𝓞.left × F.𝓥𝓞.left →  P.HalfEdgeLabel × G.𝓔𝓞.left × G.𝓥𝓞.left`.  -/
-def edgeVertexMap {F G : FeynmanDiagram P} (𝓔 : F.𝓔𝓞 ⟶ G.𝓔𝓞) (𝓥 : F.𝓥𝓞 ⟶ G.𝓥𝓞) :
-    P.HalfEdgeLabel × F.𝓔𝓞.left × F.𝓥𝓞.left →  P.HalfEdgeLabel × G.𝓔𝓞.left × G.𝓥𝓞.left :=
-  fun x => ⟨x.1, 𝓔.left x.2.1, 𝓥.left x.2.2⟩
+/-!
+
+## Making a Feynman diagram
+
+-/
+
+/-- The condition which must be satisfied by maps to form a Feynman diagram. -/
+def Cond {𝓔 𝓥 𝓱𝓔 : Type} (𝓔𝓞 : 𝓔 → P.EdgeLabel) (𝓥𝓞 : 𝓥 → P.VertexLabel)
+    (𝓱𝓔To𝓔𝓥 : 𝓱𝓔 → P.HalfEdgeLabel × 𝓔 × 𝓥)  : Prop :=
+  P.diagramEdgeProp (Over.mk 𝓱𝓔To𝓔𝓥) 𝓔𝓞  ∧
+  P.diagramVertexProp (Over.mk 𝓱𝓔To𝓔𝓥) 𝓥𝓞
+
+lemma cond_self : Cond F.𝓔𝓞.hom F.𝓥𝓞.hom F.𝓱𝓔To𝓔𝓥.hom :=
+  ⟨F.𝓔Cond, F.𝓥Cond⟩
+
+/-- `Cond` is decidable. -/
+instance CondDecidable [IsFinitePreFeynmanRule P] {𝓔 𝓥 𝓱𝓔 : Type} (𝓔𝓞 : 𝓔 → P.EdgeLabel)
+    (𝓥𝓞 : 𝓥 → P.VertexLabel)
+    (𝓱𝓔To𝓔𝓥 : 𝓱𝓔 → P.HalfEdgeLabel × 𝓔 × 𝓥)
+    [Fintype 𝓥] [DecidableEq 𝓥] [Fintype 𝓔] [DecidableEq 𝓔] [h : Fintype 𝓱𝓔] [DecidableEq 𝓱𝓔] :
+    Decidable (Cond 𝓔𝓞 𝓥𝓞 𝓱𝓔To𝓔𝓥) :=
+  @And.decidable _ _
+    (@diagramEdgePropDecidable P _ _ _ _ _ (Over.mk 𝓱𝓔To𝓔𝓥) _ h 𝓔𝓞)
+    (@diagramVertexPropDecidable P _ _ _ _ _ (Over.mk 𝓱𝓔To𝓔𝓥) _ h 𝓥𝓞)
+
+
+/-- Making a Feynman diagram from maps of edges, vertices and half-edges. -/
+def mk' {𝓔 𝓥 𝓱𝓔 : Type} (𝓔𝓞 : 𝓔 → P.EdgeLabel) (𝓥𝓞 : 𝓥 → P.VertexLabel)
+    (𝓱𝓔To𝓔𝓥 : 𝓱𝓔 → P.HalfEdgeLabel × 𝓔 × 𝓥)
+    (C : Cond 𝓔𝓞 𝓥𝓞 𝓱𝓔To𝓔𝓥): FeynmanDiagram P where
+  𝓔𝓞 := Over.mk 𝓔𝓞
+  𝓥𝓞 := Over.mk 𝓥𝓞
+  𝓱𝓔To𝓔𝓥 := Over.mk 𝓱𝓔To𝓔𝓥
+  𝓔Cond := C.1
+  𝓥Cond := C.2
+
+lemma mk'_self : mk' F.𝓔𝓞.hom F.𝓥𝓞.hom F.𝓱𝓔To𝓔𝓥.hom F.cond_self = F := rfl
+
+/-!
+
+## Finitness 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 IsFiniteDiagram (F : FeynmanDiagram P) where
+  𝓔Fintype : Fintype F.𝓔
+  𝓔DecidableEq : DecidableEq F.𝓔
+  𝓥Fintype : Fintype F.𝓥
+  𝓥DecidableEq : DecidableEq F.𝓥
+  𝓱𝓔Fintype : Fintype F.𝓱𝓔
+  𝓱𝓔DecidableEq : DecidableEq F.𝓱𝓔
+
+instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : Fintype F.𝓔 :=
+  IsFiniteDiagram.𝓔Fintype
+
+instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : DecidableEq F.𝓔 :=
+  IsFiniteDiagram.𝓔DecidableEq
+
+instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : Fintype F.𝓥 :=
+  IsFiniteDiagram.𝓥Fintype
+
+instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : DecidableEq F.𝓥 :=
+  IsFiniteDiagram.𝓥DecidableEq
+
+instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : Fintype F.𝓱𝓔 :=
+  IsFiniteDiagram.𝓱𝓔Fintype
+
+instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : DecidableEq F.𝓱𝓔 :=
+  IsFiniteDiagram.𝓱𝓔DecidableEq
+
+instance fintypeProdHalfEdgeLabel𝓔𝓥 {F : FeynmanDiagram P} [IsFinitePreFeynmanRule P]
+    [IsFiniteDiagram F] : DecidableEq (P.HalfEdgeLabel × F.𝓔 × F.𝓥) :=
+  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.
+
+-/
+
+/-- Given two maps `F.𝓔 ⟶ G.𝓔` and `F.𝓥 ⟶ G.𝓥` the corresponding map
+  `P.HalfEdgeLabel × F.𝓔 × F.𝓥 →  P.HalfEdgeLabel × G.𝓔 × G.𝓥`.  -/
+@[simps!]
+def edgeVertexMap {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ⟶ G.𝓔) (𝓥 : F.𝓥 ⟶ G.𝓥) :
+    P.HalfEdgeLabel × F.𝓔 × F.𝓥 →  P.HalfEdgeLabel × G.𝓔 × G.𝓥 :=
+  fun x => ⟨x.1, 𝓔 x.2.1, 𝓥 x.2.2⟩
+
+/-- Given equivalences `F.𝓔 ≃ G.𝓔` and `F.𝓥 ≃ G.𝓥`, the induced equivalence between
+  `P.HalfEdgeLabel × F.𝓔 × F.𝓥` and `P.HalfEdgeLabel × G.𝓔 × G.𝓥 ` -/
+def edgeVertexEquiv {F G : FeynmanDiagram P}  (𝓔 : F.𝓔 ≃ G.𝓔) (𝓥 : F.𝓥 ≃ G.𝓥) :
+    P.HalfEdgeLabel × F.𝓔 × F.𝓥 ≃ P.HalfEdgeLabel × G.𝓔 × G.𝓥 where
+  toFun := edgeVertexMap 𝓔.toFun 𝓥.toFun
+  invFun := edgeVertexMap 𝓔.invFun 𝓥.invFun
+  left_inv := by aesop_cat
+  right_inv := by aesop_cat
 
 /-- The functor of over-categories generated by `edgeVertexMap`. -/
-def edgeVertexFunc {F G : FeynmanDiagram P} (𝓔 : F.𝓔𝓞 ⟶ G.𝓔𝓞) (𝓥 : F.𝓥𝓞 ⟶ G.𝓥𝓞) :
-   Over (P.HalfEdgeLabel × F.𝓔𝓞.left × F.𝓥𝓞.left)
-   ⥤ Over (P.HalfEdgeLabel × G.𝓔𝓞.left × G.𝓥𝓞.left) :=
+@[simps!]
+def edgeVertexFunc {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ⟶ G.𝓔) (𝓥 : F.𝓥 ⟶ G.𝓥) :
+   Over (P.HalfEdgeLabel × F.𝓔 × F.𝓥) ⥤ Over (P.HalfEdgeLabel × G.𝓔 × G.𝓥) :=
   Over.map <| edgeVertexMap 𝓔 𝓥
 
 /-- A morphism of Feynman diagrams. -/
 structure Hom (F G : FeynmanDiagram P) where
   /-- The morphism of edge objects. -/
-  𝓔 : F.𝓔𝓞 ⟶ G.𝓔𝓞
+  𝓔𝓞 : F.𝓔𝓞 ⟶ G.𝓔𝓞
   /-- The morphism of vertex objects. -/
-  𝓥 : F.𝓥𝓞 ⟶ G.𝓥𝓞
+  𝓥𝓞 : F.𝓥𝓞 ⟶ G.𝓥𝓞
   /-- The morphism of half-edge objects. -/
-  𝓱𝓔 : (edgeVertexFunc 𝓔 𝓥).obj F.𝓱𝓔To𝓔𝓥 ⟶ G.𝓱𝓔To𝓔𝓥
+  𝓱𝓔To𝓔𝓥 : (edgeVertexFunc 𝓔𝓞.left 𝓥𝓞.left).obj F.𝓱𝓔To𝓔𝓥 ⟶ G.𝓱𝓔To𝓔𝓥
+
 
 namespace Hom
+variable {F G : FeynmanDiagram P}
+variable (f : Hom F G)
+
+/-- The map `F.𝓔 → G.𝓔` induced by a homomorphism of Feynman diagrams. -/
+@[simp]
+def 𝓔 : F.𝓔 → G.𝓔 := f.𝓔𝓞.left
+
+/-- The map `F.𝓥 → G.𝓥` induced by a homomorphism of Feynman diagrams. -/
+@[simp]
+def 𝓥 : F.𝓥 → G.𝓥 := f.𝓥𝓞.left
+
+/-- The map `F.𝓱𝓔 → G.𝓱𝓔` induced by a homomorphism of Feynman diagrams. -/
+@[simp]
+def 𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔 := f.𝓱𝓔To𝓔𝓥.left
+
+
+/-- The morphism `F.𝓱𝓔𝓞 ⟶ G.𝓱𝓔𝓞` induced by a homomorphism of Feynman diagrams. -/
+@[simp]
+def 𝓱𝓔𝓞 : F.𝓱𝓔𝓞 ⟶ G.𝓱𝓔𝓞 := P.toHalfEdge.map f.𝓱𝓔To𝓔𝓥
+
 
 /-- The identity morphism for a Feynman diagram. -/
 def id (F : FeynmanDiagram P) : Hom F F where
-  𝓔 := 𝟙 F.𝓔𝓞
-  𝓥 := 𝟙 F.𝓥𝓞
-  𝓱𝓔 := 𝟙 F.𝓱𝓔To𝓔𝓥
+  𝓔𝓞 := 𝟙 F.𝓔𝓞
+  𝓥𝓞 := 𝟙 F.𝓥𝓞
+  𝓱𝓔To𝓔𝓥 := 𝟙 F.𝓱𝓔To𝓔𝓥
 
 /-- The composition of two morphisms of Feynman diagrams. -/
+@[simps!]
 def comp {F G H : FeynmanDiagram P} (f : Hom F G) (g : Hom G H) : Hom F H where
-  𝓔 := f.𝓔 ≫ g.𝓔
-  𝓥 := f.𝓥 ≫ g.𝓥
-  𝓱𝓔 := (edgeVertexFunc g.𝓔 g.𝓥).map f.𝓱𝓔 ≫ g.𝓱𝓔
+  𝓔𝓞 := f.𝓔𝓞 ≫ g.𝓔𝓞
+  𝓥𝓞 := f.𝓥𝓞 ≫ g.𝓥𝓞
+  𝓱𝓔To𝓔𝓥 := (edgeVertexFunc g.𝓔 g.𝓥).map f.𝓱𝓔To𝓔𝓥 ≫ g.𝓱𝓔To𝓔𝓥
 
-lemma ext {F G : FeynmanDiagram P} {f g : Hom F G} (h𝓔 : f.𝓔 = g.𝓔)
-    (h𝓥 : f.𝓥 = g.𝓥) (h𝓱𝓔 : f.𝓱𝓔.left = g.𝓱𝓔.left) : f = g := by
+lemma ext' {F G : FeynmanDiagram P} {f g : Hom F G} (h𝓔 : f.𝓔𝓞 = g.𝓔𝓞)
+    (h𝓥 : f.𝓥𝓞 = g.𝓥𝓞) (h𝓱𝓔 : f.𝓱𝓔 = g.𝓱𝓔) : f = g := by
   cases f
   cases g
   subst h𝓔 h𝓥
   simp_all only [mk.injEq, heq_eq_eq, true_and]
   ext a : 2
-  simp_all only
+  simp only [𝓱𝓔] at h𝓱𝓔
+  exact congrFun h𝓱𝓔 a
+
+lemma ext {F G : FeynmanDiagram P} {f g : Hom F G} (h𝓔 : f.𝓔 = g.𝓔)
+    (h𝓥 : f.𝓥 = g.𝓥) (h𝓱𝓔 : f.𝓱𝓔 = g.𝓱𝓔) : f = g :=
+  ext' (Over.OverMorphism.ext h𝓔) (Over.OverMorphism.ext h𝓥) h𝓱𝓔
+
+def Cond {F G : FeynmanDiagram P} (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔) : Prop :=
+  (∀ x, G.𝓔𝓞.hom (𝓔 x) = F.𝓔𝓞.hom x) ∧
+  (∀ x, G.𝓥𝓞.hom (𝓥 x) = F.𝓥𝓞.hom x) ∧
+  (∀ x, G.𝓱𝓔To𝓔𝓥.hom (𝓱𝓔 x) =  edgeVertexMap 𝓔 𝓥 (F.𝓱𝓔To𝓔𝓥.hom x))
+
+lemma cond_satisfied {F G : FeynmanDiagram P} (f : Hom F G) :
+    Cond f.𝓔 f.𝓥 f.𝓱𝓔 :=
+  ⟨fun x => congrFun f.𝓔𝓞.w x, fun x => congrFun f.𝓥𝓞.w x, fun x => congrFun f.𝓱𝓔To𝓔𝓥.w x ⟩
+
+lemma cond_symm {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ≃ G.𝓔) (𝓥 : F.𝓥 ≃ G.𝓥) (𝓱𝓔 : F.𝓱𝓔 ≃ G.𝓱𝓔)
+    (h : Cond 𝓔 𝓥 𝓱𝓔) : Cond 𝓔.symm 𝓥.symm 𝓱𝓔.symm := by
+  refine ⟨?_, ?_, ?_⟩
+  simpa using fun x => (h.1 (𝓔.symm x)).symm
+  simpa using fun x => (h.2.1 (𝓥.symm x)).symm
+  intro x
+  have h1 := h.2.2 (𝓱𝓔.symm x)
+  simp at h1
+  exact (edgeVertexEquiv 𝓔 𝓥).apply_eq_iff_eq_symm_apply.mp (h1).symm
+
+instance {F G : FeynmanDiagram P} [IsFiniteDiagram F] [IsFinitePreFeynmanRule P]
+    (𝓔 : F.𝓔 → G.𝓔) : Decidable (∀ x, G.𝓔𝓞.hom (𝓔 x) = F.𝓔𝓞.hom x) :=
+  @Fintype.decidableForallFintype _ _ (fun _ => preFeynmanRuleDecEq𝓔 P _ _) _
+
+instance {F G : FeynmanDiagram P} [IsFiniteDiagram F] [IsFinitePreFeynmanRule P]
+    (𝓥 : F.𝓥 → G.𝓥) : Decidable (∀ x, G.𝓥𝓞.hom (𝓥 x) = F.𝓥𝓞.hom x) :=
+  @Fintype.decidableForallFintype _ _ (fun _ => preFeynmanRuleDecEq𝓥 P _ _) _
+
+instance {F G : FeynmanDiagram P} [IsFiniteDiagram F] [IsFiniteDiagram G] [IsFinitePreFeynmanRule P]
+    (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔)  :
+    Decidable (∀ x, G.𝓱𝓔To𝓔𝓥.hom (𝓱𝓔 x) =  edgeVertexMap 𝓔 𝓥 (F.𝓱𝓔To𝓔𝓥.hom x)) :=
+  @Fintype.decidableForallFintype _ _ (fun _ => fintypeProdHalfEdgeLabel𝓔𝓥  _ _) _
+
+instance {F G : FeynmanDiagram P} [IsFiniteDiagram F] [IsFiniteDiagram G] [IsFinitePreFeynmanRule P]
+    (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔) : Decidable (Cond 𝓔 𝓥 𝓱𝓔) :=
+  And.decidable
+
+
+/-- Making a Feynman diagram from maps of edges, vertices and half-edges. -/
+@[simps!]
+def mk' {F G : FeynmanDiagram P} (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔)
+    (C : Cond 𝓔 𝓥 𝓱𝓔) : Hom F G where
+  𝓔𝓞 := Over.homMk 𝓔 $ funext C.1
+  𝓥𝓞 := Over.homMk 𝓥 $ funext C.2.1
+  𝓱𝓔To𝓔𝓥 := Over.homMk 𝓱𝓔 $ funext C.2.2
+
+lemma mk'_self {F G : FeynmanDiagram P} (f : Hom F G) :
+    mk' f.𝓔 f.𝓥 f.𝓱𝓔 f.cond_satisfied = f := rfl
 
 end Hom
 
+/-!
+
+## 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.
+-/
+
 /-- Feynman diagrams form a category. -/
+@[simps!]
 instance : Category (FeynmanDiagram P) where
   Hom := Hom
   id := Hom.id
   comp := Hom.comp
 
+/-- An isomorphism of Feynman diagrams from isomorphisms of edges, vertices and half-edges. -/
+def mkIso {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ≃ G.𝓔) (𝓥 : F.𝓥 ≃ G.𝓥) (𝓱𝓔 : F.𝓱𝓔 ≃ G.𝓱𝓔)
+    (C : Hom.Cond 𝓔 𝓥 𝓱𝓔) : F ≅ G where
+  hom := Hom.mk' 𝓔 𝓥 𝓱𝓔 C
+  inv := Hom.mk' 𝓔.symm 𝓥.symm 𝓱𝓔.symm (Hom.cond_symm 𝓔 𝓥 𝓱𝓔 C)
+  hom_inv_id := by
+    apply Hom.ext
+    all_goals
+      aesop_cat
+  inv_hom_id := by
+    apply Hom.ext
+    all_goals
+      aesop_cat
+
 /-- The functor from Feynman diagrams to category over edge labels. -/
-def toOverEdgeLabel : FeynmanDiagram P ⥤ Over P.EdgeLabel where
+def func𝓔𝓞 : FeynmanDiagram P ⥤ Over P.EdgeLabel where
   obj F := F.𝓔𝓞
-  map f := f.𝓔
+  map f := f.𝓔𝓞
 
 /-- The functor from Feynman diagrams to category over vertex labels. -/
-def toOverVertexLabel : FeynmanDiagram P ⥤ Over P.VertexLabel where
+def func𝓥𝓞 : FeynmanDiagram P ⥤ Over P.VertexLabel where
   obj F := F.𝓥𝓞
-  map f := f.𝓥
+  map f := f.𝓥𝓞
 
 /-- The functor from Feynman diagrams to category over half-edge labels. -/
-def toOverHalfEdgeLabel : FeynmanDiagram P ⥤ Over P.HalfEdgeLabel where
+def func𝓱𝓔𝓞 : FeynmanDiagram P ⥤ Over P.HalfEdgeLabel where
   obj F := F.𝓱𝓔𝓞
-  map f := P.toHalfEdge.map f.𝓱𝓔
+  map f := f.𝓱𝓔𝓞
+
+/-- The functor from Feynman diagrams to `Type` landing on edges. -/
+def func𝓔 : FeynmanDiagram P ⥤ Type where
+  obj F := F.𝓔
+  map f := f.𝓔
+
+/-- The functor from Feynman diagrams to `Type` landing on vertices. -/
+def func𝓥 : FeynmanDiagram P ⥤ Type where
+  obj F := F.𝓥
+  map f := f.𝓥
+
+/-- The functor from Feynman diagrams to `Type` landing on half-edges. -/
+def func𝓱𝓔 : FeynmanDiagram P ⥤ Type where
+  obj F := F.𝓱𝓔
+  map f := f.𝓱𝓔
+
+section symmetryFactor
+/-!
+## 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.
+
+-/
 
 /-- The type of isomorphisms of a Feynman diagram. -/
-def symmetryType : Type := F ≅ F
+def SymmetryType : Type := F ≅ F
+
+
+/-- An equivalence between `SymmetryType` and permutation of edges, vertices and half-edges
+  satisfying `Hom.Cond`. -/
+def symmetryTypeEquiv :
+    F.SymmetryType ≃ {S : Equiv.Perm F.𝓔 × Equiv.Perm F.𝓥 × Equiv.Perm F.𝓱𝓔 //
+      Hom.Cond S.1 S.2.1 S.2.2} where
+  toFun f := ⟨⟨(func𝓔.mapIso f).toEquiv, (func𝓥.mapIso f).toEquiv,
+    (func𝓱𝓔.mapIso f).toEquiv⟩, f.1.cond_satisfied⟩
+  invFun S := mkIso S.1.1 S.1.2.1 S.1.2.2 S.2
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+instance [IsFinitePreFeynmanRule P] [IsFiniteDiagram F] : Fintype F.SymmetryType :=
+  Fintype.ofEquiv _ F.symmetryTypeEquiv.symm
 
 /-- The symmetry factor can be defined as the cardinal of the symmetry type.
  In general this is not a finite number. -/
-def symmetryFactor : Cardinal := Cardinal.mk (F.symmetryType)
+@[simp]
+def cardSymmetryFactor : Cardinal := Cardinal.mk (F.SymmetryType)
 
+@[simp]
+def symmetryFactor [IsFinitePreFeynmanRule P] [IsFiniteDiagram F] : ℕ :=
+  (Fintype.card F.SymmetryType)
+
+@[simp]
+lemma symmetryFactor_eq_cardSymmetryFactor [IsFinitePreFeynmanRule P] [IsFiniteDiagram F] :
+    F.symmetryFactor = F.cardSymmetryFactor := by
+  simp only [symmetryFactor, cardSymmetryFactor, Cardinal.mk_fintype]
+
+end symmetryFactor
+
+section connectedness
+/-!
+
+## 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.
+
+-/
+
+/-- 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. -/
+@[simp]
+def adjRelation : F.𝓥 → F.𝓥 → Prop := fun x y =>
+  x ≠ y ∧
+  ∃ (a 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 [IsFinitePreFeynmanRule P] [IsFiniteDiagram F] : DecidableRel F.adjRelation := fun _ _ =>
+  @And.decidable _ _ _ $
+  @Fintype.decidableExistsFintype _ _ (fun _ => @Fintype.decidableExistsFintype _ _  (
+  fun _ => @And.decidable _ _ (instDecidableEq𝓔OfIsFiniteDiagram _ _) $
+    @And.decidable _ _ (instDecidableEq𝓥OfIsFiniteDiagram _ _)
+    (instDecidableEq𝓥OfIsFiniteDiagram _ _)) _ ) _
+
+
+/-- From a Feynman diagram the simple graph showing those vertices which are connected. -/
+def toSimpleGraph : SimpleGraph F.𝓥 where
+  Adj := adjRelation F
+  symm := by
+    intro x y h
+    apply And.intro (Ne.symm h.1)
+    obtain ⟨a, b, hab⟩ := h.2
+    use b, a
+    simp_all only [adjRelation, ne_eq, and_self]
+  loopless := by
+    intro x h
+    simp at h
+
+instance  [IsFinitePreFeynmanRule P] [IsFiniteDiagram F] : DecidableRel F.toSimpleGraph.Adj :=
+  instDecidableRel𝓥AdjRelationOfIsFinitePreFeynmanRuleOfIsFiniteDiagram F
+
+instance [IsFinitePreFeynmanRule P] [IsFiniteDiagram F]  :
+  Decidable (F.toSimpleGraph.Preconnected ∧ Nonempty F.𝓥) :=
+  @And.decidable _ _ _ $ decidable_of_iff _ Finset.univ_nonempty_iff
+
+instance [IsFinitePreFeynmanRule P] [IsFiniteDiagram F] : Decidable F.toSimpleGraph.Connected :=
+  decidable_of_iff _ (SimpleGraph.connected_iff F.toSimpleGraph).symm
+
+/-- We say a Feynman diagram is connected if its simple graph is connected. -/
+def Connected : Prop := F.toSimpleGraph.Connected
+
+instance [IsFinitePreFeynmanRule P] [IsFiniteDiagram F] : Decidable (Connected F) :=
+  instDecidableConnected𝓥ToSimpleGraphOfIsFinitePreFeynmanRuleOfIsFiniteDiagram F
+
+end connectedness
 
 end FeynmanDiagram
diff --git a/HepLean/FeynmanDiagrams/Instances/ComplexScalar.lean b/HepLean/FeynmanDiagrams/Instances/ComplexScalar.lean
new file mode 100644
index 0000000..22801c8
--- /dev/null
+++ b/HepLean/FeynmanDiagrams/Instances/ComplexScalar.lean
@@ -0,0 +1,100 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.FeynmanDiagrams.Basic
+/-!
+# Feynman diagrams in a complex scalar field theory
+
+
+
+-/
+
+
+namespace PhiFour
+open CategoryTheory
+open FeynmanDiagram
+open PreFeynmanRule
+
+@[simps!]
+def complexScalarFeynmanRules : PreFeynmanRule where
+  /- There is 2 types of `half-edge`. -/
+  HalfEdgeLabel := Fin 2
+  /- There is only 1 type of `edge`. -/
+  EdgeLabel := Fin 1
+  /- There are two types of `vertex`, two external `0` and internal `1`. -/
+  VertexLabel := Fin 3
+  edgeLabelMap x :=
+    match x with
+    | 0 => Over.mk ![0, 1]
+  vertexLabelMap x :=
+    match x with
+    | 0 => Over.mk ![0]
+    | 1 => Over.mk ![1]
+    | 2 => Over.mk ![0, 0, 1, 1]
+
+instance (a : ℕ) : OfNat complexScalarFeynmanRules.EdgeLabel a where
+  ofNat := (a : Fin _)
+
+instance (a : ℕ) : OfNat complexScalarFeynmanRules.HalfEdgeLabel a where
+  ofNat := (a : Fin _)
+
+instance (a : ℕ) : OfNat complexScalarFeynmanRules.VertexLabel a where
+  ofNat := (a : Fin _)
+
+
+instance : IsFinitePreFeynmanRule complexScalarFeynmanRules where
+  edgeLabelDecidable :=  instDecidableEqFin _
+  vertexLabelDecidable := instDecidableEqFin _
+  halfEdgeLabelDecidable := instDecidableEqFin _
+  vertexMapFintype := fun v =>
+    match v with
+    | 0 => Fin.fintype _
+    | 1  => Fin.fintype _
+    | 2  => Fin.fintype _
+  edgeMapFintype := fun v =>
+    match v with
+    | 0 => Fin.fintype _
+  vertexMapDecidable := fun v =>
+    match v with
+    | 0 => instDecidableEqFin _
+    | 1  => instDecidableEqFin _
+    | 2  => instDecidableEqFin _
+  edgeMapDecidable := fun v =>
+    match v with
+    | 0 => instDecidableEqFin _
+
+
+
+
+
+set_option maxRecDepth 1000 in
+def loopProp : FeynmanDiagram complexScalarFeynmanRules :=
+  mk' ![0, 0, 0] ![0, 2, 1] ![⟨0, 0, 0⟩, ⟨1, 0, 1⟩,
+    ⟨0, 1, 1⟩, ⟨1, 1, 1⟩, ⟨0, 2, 1⟩, ⟨1, 2, 2⟩] (by decide)
+
+instance : IsFiniteDiagram loopProp where
+  𝓔Fintype := Fin.fintype _
+  𝓔DecidableEq := instDecidableEqFin _
+  𝓥Fintype := Fin.fintype _
+  𝓥DecidableEq := instDecidableEqFin _
+  𝓱𝓔Fintype := Fin.fintype _
+  𝓱𝓔DecidableEq := instDecidableEqFin _
+
+def prop : FeynmanDiagram complexScalarFeynmanRules :=
+  mk' ![0] ![0, 1] ![⟨0, 0, 0⟩, ⟨1, 0, 1⟩] (by decide)
+
+instance : IsFiniteDiagram prop where
+  𝓔Fintype := Fin.fintype _
+  𝓔DecidableEq := instDecidableEqFin _
+  𝓥Fintype := Fin.fintype _
+  𝓥DecidableEq := instDecidableEqFin _
+  𝓱𝓔Fintype := Fin.fintype _
+  𝓱𝓔DecidableEq := instDecidableEqFin _
+
+lemma prop_symmetryFactor_eq_one : symmetryFactor prop = 1 := by decide
+
+
+
+end PhiFour
diff --git a/HepLean/FeynmanDiagrams/Instances/Phi4.lean b/HepLean/FeynmanDiagrams/Instances/Phi4.lean
new file mode 100644
index 0000000..ef1d5e6
--- /dev/null
+++ b/HepLean/FeynmanDiagrams/Instances/Phi4.lean
@@ -0,0 +1,83 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.FeynmanDiagrams.Basic
+/-!
+# Feynman diagrams in Phi^4 theory
+
+The aim of this file is to start building up the theory of Feynman diagrams in the context of
+Phi^4 theory.
+
+
+-/
+
+
+namespace PhiFour
+open CategoryTheory
+open FeynmanDiagram
+open PreFeynmanRule
+
+@[simps!]
+def phi4PreFeynmanRules : PreFeynmanRule where
+  /- There is only 1 type of `half-edge`. -/
+  HalfEdgeLabel := Fin 1
+  /- There is only 1 type of `edge`. -/
+  EdgeLabel := Fin 1
+  /- There are two types of `vertex`, external `0` and internal `1`. -/
+  VertexLabel := Fin 2
+  edgeLabelMap x :=
+    match x with
+    | 0 => Over.mk ![0, 0]
+  vertexLabelMap x :=
+    match x with
+    | 0 => Over.mk ![0]
+    | 1 => Over.mk ![0, 0, 0, 0]
+
+instance (a : ℕ) : OfNat phi4PreFeynmanRules.EdgeLabel a where
+  ofNat := (a : Fin _)
+
+instance (a : ℕ) : OfNat phi4PreFeynmanRules.HalfEdgeLabel a where
+  ofNat := (a : Fin _)
+
+instance (a : ℕ) : OfNat phi4PreFeynmanRules.VertexLabel a where
+  ofNat := (a : Fin _)
+
+
+instance : IsFinitePreFeynmanRule phi4PreFeynmanRules where
+  edgeLabelDecidable :=  instDecidableEqFin _
+  vertexLabelDecidable := instDecidableEqFin _
+  halfEdgeLabelDecidable := instDecidableEqFin _
+  vertexMapFintype := fun v =>
+    match v with
+    | 0 => Fin.fintype _
+    | 1  => Fin.fintype _
+  edgeMapFintype := fun v =>
+    match v with
+    | 0 => Fin.fintype _
+  vertexMapDecidable := fun v =>
+    match v with
+    | 0 => instDecidableEqFin _
+    | 1  => instDecidableEqFin _
+  edgeMapDecidable := fun v =>
+    match v with
+    | 0 => instDecidableEqFin _
+
+
+def figureEight : FeynmanDiagram phi4PreFeynmanRules :=
+  mk' ![0, 0] ![1] ![⟨0, 0, 0⟩, ⟨0, 0, 0⟩, ⟨0, 1, 0⟩, ⟨0, 1, 0⟩] (by decide)
+
+instance : IsFiniteDiagram figureEight where
+  𝓔Fintype := Fin.fintype _
+  𝓔DecidableEq := instDecidableEqFin _
+  𝓥Fintype := Fin.fintype _
+  𝓥DecidableEq := instDecidableEqFin _
+  𝓱𝓔Fintype := Fin.fintype _
+  𝓱𝓔DecidableEq := instDecidableEqFin _
+
+#eval symmetryFactor figureEight
+
+#eval Connected figureEight
+
+end PhiFour
diff --git a/HepLean/FeynmanDiagrams/PhiFour/Basic.lean b/HepLean/FeynmanDiagrams/PhiFour/Basic.lean
deleted file mode 100644
index 6291b2c..0000000
--- a/HepLean/FeynmanDiagrams/PhiFour/Basic.lean
+++ /dev/null
@@ -1,583 +0,0 @@
-/-
-Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
-Released under Apache 2.0 license.
-Authors: Joseph Tooby-Smith
--/
-import Mathlib.Logic.Equiv.Fin
-import Mathlib.Tactic.FinCases
-import Mathlib.Data.Finset.Card
-import Mathlib.CategoryTheory.IsomorphismClasses
-import Mathlib.Data.Fintype.Pi
-import Mathlib.CategoryTheory.Limits.Shapes.Terminal
-import Mathlib.Data.Fintype.Prod
-import Mathlib.Data.Fintype.Perm
-import Mathlib.Combinatorics.SimpleGraph.Basic
-import Mathlib.Combinatorics.SimpleGraph.Connectivity
-/-!
-# Feynman diagrams in Phi^4 theory
-
-The aim of this file is to start building up the theory of Feynman diagrams in the context of
-Phi^4 theory.
-
-## References
-
-- The approach taking to defining Feynman diagrams is based on:
-
-Theo Johnson-Freyd (https://mathoverflow.net/users/78/theo-johnson-freyd), How to count symmetry
-factors of Feynman diagrams? , URL (version: 2010-06-03): https://mathoverflow.net/q/26938
-
-## TODO
-
-- Develop a way to display Feynman diagrams.
-- Define a connected diagram.
-- Define the Feynman rules, and perform an example calculation.
-- Determine an efficent way to calculate symmetry factors. Currently there is a method, but
-it will not work for large diagrams as it scales factorially with the number of half-edges.
-
--/
-
-namespace PhiFour
-open CategoryTheory
-
-/-- Edges in Φ^4  internal `0`.
-  Here `Type` is the category in which half-edges live. In general `Type` will be e.g.
-  `Type × Type` with more fields. -/
-def edgeType : Fin 1 → Type
-  | 0 => Fin 2
-
-/-- Vertices in Φ^4, can either be `external` corresponding to `0`, or a `phi^4` interaction
-corresponding to `1`. -/
-def vertexType : Fin 2 → Type
-  | 0 => Fin 1
-  | 1 => Fin 4
-
-/-- The type of vacuum Feynman diagrams for Phi-4 theory. -/
-structure FeynmanDiagram where
-  /-- The type of half edges in the Feynman diagram. Sometimes also called `flags`. -/
-  𝓱𝓔 : Type
-  /-- The type of edges in the Feynman diagram. -/
-  𝓔 : Type
-  /-- Maps each edge to a label. Labels `0` if it is an external edge,
-    and labels `1` if an internal edge. -/
-  𝓔Label : 𝓔 → Fin 1
-  /-- Maps half-edges to edges. -/
-  𝓱𝓔To𝓔 : 𝓱𝓔 → 𝓔
-  /-- Requires that the fiber of the map `𝓱𝓔To𝓔` at `x ∈ 𝓔` agrees with the corresponding
-  `edgeType`. -/
-  𝓔Fiber : ∀ x,  CategoryTheory.IsIsomorphic (𝓱𝓔To𝓔 ⁻¹' {x} : Type) $ (edgeType ∘ 𝓔Label) x
-  /-- The type of vertices in the Feynman diagram. -/
-  𝓥 : Type
-  /-- Maps each vertex to a label. In this case this map contains no information since
-  there is only one type of vertex.. -/
-  𝓥Label : 𝓥 → Fin 2
-  /-- Maps half-edges to vertices. -/
-  𝓱𝓔To𝓥 : 𝓱𝓔 → 𝓥
-  /-- Requires that the fiber of the map `𝓱𝓔To𝓥` at `x ∈ 𝓥` agrees with the corresponding
-    `vertexType`. -/
-  𝓥Fiber : ∀ x,  CategoryTheory.IsIsomorphic (𝓱𝓔To𝓥 ⁻¹' {x} : Type) $ (vertexType ∘ 𝓥Label) x
-
-namespace FeynmanDiagram
-
-variable (F : FeynmanDiagram)
-
-section Decidability
-/-!
-
-## Decidability
-
-The aim of this section is to make it easy to prove the `𝓔Fiber` and `𝓥Fiber` conditions by
-showing that they are decidable in cases when everything is finite and nice
-(which in practice is always).
-
---/
-
-lemma fiber_cond_edge_iff_exists {𝓱𝓔 𝓔 : Type} (𝓱𝓔To𝓔 : 𝓱𝓔 → 𝓔) (𝓔Label : 𝓔 → Fin 1) (x : 𝓔) :
-    (CategoryTheory.IsIsomorphic (𝓱𝓔To𝓔 ⁻¹' {x} : Type) $ (edgeType ∘ 𝓔Label) x)
-    ↔ ∃ (f : 𝓱𝓔To𝓔 ⁻¹' {x} → (edgeType ∘ 𝓔Label) x), Function.Bijective f :=
-  Iff.intro
-    (fun h ↦ match h with
-            | ⟨f1, f2, h1, h2⟩ => ⟨f1, (isIso_iff_bijective f1).mp ⟨f2, h1, h2⟩⟩)
-    (fun ⟨f1, hb⟩ ↦ match (isIso_iff_bijective f1).mpr hb with
-                   | ⟨f2, h1, h2⟩ => ⟨f1, f2, h1, h2⟩)
-
-lemma fiber_cond_vertex_iff_exists {𝓱𝓥 𝓥 : Type} (𝓱𝓥To𝓥 : 𝓱𝓥 → 𝓥) (𝓥Label : 𝓥 → Fin 2) (x : 𝓥) :
-    (CategoryTheory.IsIsomorphic (𝓱𝓥To𝓥 ⁻¹' {x} : Type) $ (vertexType ∘ 𝓥Label) x)
-    ↔ ∃ (f : 𝓱𝓥To𝓥 ⁻¹' {x} → (vertexType ∘ 𝓥Label) x), Function.Bijective f :=
-  Iff.intro
-    (fun h ↦ match h with
-            | ⟨f1, f2, h1, h2⟩ => ⟨f1, (isIso_iff_bijective f1).mp ⟨f2, h1, h2⟩⟩)
-    (fun ⟨f1, hb⟩ ↦ match (isIso_iff_bijective f1).mpr hb with
-                   | ⟨f2, h1, h2⟩ => ⟨f1, f2, h1, h2⟩)
-
-instance {𝓱𝓔 𝓔 : Type} [DecidableEq 𝓔] (𝓱𝓔To𝓔 : 𝓱𝓔 → 𝓔) (x : 𝓔):
-    DecidablePred (fun y => y ∈  𝓱𝓔To𝓔 ⁻¹' {x}) := fun y =>
-  match decEq (𝓱𝓔To𝓔 y) x with
-  | isTrue h => isTrue h
-  | isFalse h => isFalse h
-
-
-instance {𝓱𝓔 𝓔 : Type} [DecidableEq 𝓱𝓔]  (𝓱𝓔To𝓔 : 𝓱𝓔 → 𝓔) (x : 𝓔) :
-    DecidableEq $ (𝓱𝓔To𝓔 ⁻¹' {x}) := Subtype.instDecidableEq
-
-instance edgeTypeFintype (x : Fin 1) : Fintype (edgeType x) :=
-  match x with
-  | 0 => Fin.fintype 2
-
-instance edgeTypeDecidableEq (x : Fin 1) : DecidableEq (edgeType x) :=
-  match x with
-  | 0 => instDecidableEqFin 2
-
-instance vertexTypeFintype (x : Fin 2) : Fintype (vertexType x) :=
-  match x with
-  | 0 => Fin.fintype 1
-  | 1 => Fin.fintype 4
-
-instance vertexTypeDecidableEq (x : Fin 2) : DecidableEq (vertexType x) :=
-  match x with
-  | 0 => instDecidableEqFin 1
-  | 1 => instDecidableEqFin 4
-
-instance {𝓔 : Type} (𝓔Label : 𝓔 → Fin 1) (x : 𝓔) :
-    DecidableEq ((edgeType ∘ 𝓔Label) x) := edgeTypeDecidableEq (𝓔Label x)
-
-instance {𝓔 : Type} (𝓔Label : 𝓔 → Fin 1) (x : 𝓔) :
-    Fintype ((edgeType ∘ 𝓔Label) x) := edgeTypeFintype (𝓔Label x)
-
-instance {𝓥 : Type} (𝓥Label : 𝓥 → Fin 2) (x : 𝓥) :
-    DecidableEq ((vertexType ∘ 𝓥Label) x) := vertexTypeDecidableEq (𝓥Label x)
-
-instance {𝓥 : Type} (𝓥Label : 𝓥 → Fin 2) (x : 𝓥) :
-    Fintype ((vertexType ∘ 𝓥Label) x) := vertexTypeFintype (𝓥Label x)
-
-
-instance {𝓱𝓔 𝓔 : Type}  [Fintype 𝓱𝓔] [DecidableEq 𝓱𝓔] [DecidableEq 𝓔]
-    (𝓱𝓔To𝓔 : 𝓱𝓔 → 𝓔) (𝓔Label : 𝓔 → Fin 1) (x : 𝓔) :
-    Decidable (CategoryTheory.IsIsomorphic (𝓱𝓔To𝓔 ⁻¹' {x} : Type) $ (edgeType ∘ 𝓔Label) x) :=
-  decidable_of_decidable_of_iff (fiber_cond_edge_iff_exists 𝓱𝓔To𝓔 𝓔Label x).symm
-
-instance {𝓱𝓥 𝓥 : Type}  [Fintype 𝓱𝓥] [DecidableEq 𝓱𝓥] [DecidableEq 𝓥]
-    (𝓱𝓥To𝓥 : 𝓱𝓥 → 𝓥) (𝓥Label : 𝓥 → Fin 2) (x : 𝓥) :
-    Decidable (CategoryTheory.IsIsomorphic (𝓱𝓥To𝓥 ⁻¹' {x} : Type) $ (vertexType ∘ 𝓥Label) x) :=
-  decidable_of_decidable_of_iff (fiber_cond_vertex_iff_exists 𝓱𝓥To𝓥 𝓥Label x).symm
-
-end Decidability
-
-section Finiteness
-/-!
-## Finiteness
-
-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`.
-
--/
-
-/-- A Feynman diagram is said to be finite if its type of half-edges, edges and vertices
-are  finite and decidable. -/
-class IsFiniteDiagram (F : FeynmanDiagram) where
-  /-- The type `𝓔` is finite. -/
-  𝓔Fintype : Fintype F.𝓔
-  /-- The type `𝓔` is decidable. -/
-  𝓔DecidableEq : DecidableEq F.𝓔
-  /-- The type `𝓥` is finite. -/
-  𝓥Fintype : Fintype F.𝓥
-  /-- The type `𝓥` is decidable. -/
-  𝓥DecidableEq : DecidableEq F.𝓥
-  /-- The type `𝓱𝓔` is finite. -/
-  𝓱𝓔Fintype : Fintype F.𝓱𝓔
-  /-- The type `𝓱𝓔` is decidable. -/
-  𝓱𝓔DecidableEq : DecidableEq F.𝓱𝓔
-
-instance {F : FeynmanDiagram} [IsFiniteDiagram F] : Fintype F.𝓔 :=
-  IsFiniteDiagram.𝓔Fintype
-
-instance {F : FeynmanDiagram} [IsFiniteDiagram F] : DecidableEq F.𝓔 :=
-  IsFiniteDiagram.𝓔DecidableEq
-
-instance {F : FeynmanDiagram} [IsFiniteDiagram F] : Fintype F.𝓥 :=
-  IsFiniteDiagram.𝓥Fintype
-
-instance {F : FeynmanDiagram} [IsFiniteDiagram F] : DecidableEq F.𝓥 :=
-  IsFiniteDiagram.𝓥DecidableEq
-
-instance {F : FeynmanDiagram} [IsFiniteDiagram F] : Fintype F.𝓱𝓔 :=
-  IsFiniteDiagram.𝓱𝓔Fintype
-
-instance {F : FeynmanDiagram} [IsFiniteDiagram F] : DecidableEq F.𝓱𝓔 :=
-  IsFiniteDiagram.𝓱𝓔DecidableEq
-
-instance {F : FeynmanDiagram} [IsFiniteDiagram F] : Decidable (Nonempty F.𝓥) :=
-  decidable_of_iff _ Finset.univ_nonempty_iff
-
-end Finiteness
-
-section categoryOfFeynmanDiagrams
-/-!
-
-## 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.
-
--/
-/-- A morphism between two `FeynmanDiagram`.  -/
-structure Hom (F1 F2 : FeynmanDiagram) where
-  /-- A morphism between half-edges. -/
-  𝓱𝓔 : F1.𝓱𝓔 ⟶ F2.𝓱𝓔
-  /-- A morphism between edges. -/
-  𝓔 : F1.𝓔 ⟶ F2.𝓔
-  /-- A morphism between vertices. -/
-  𝓥 : F1.𝓥 ⟶ F2.𝓥
-  /-- The morphism between edges must respect the labels. -/
-  𝓔Label : F1.𝓔Label = F2.𝓔Label ∘ 𝓔
-  /-- The morphism between vertices must respect the labels. -/
-  𝓥Label : F1.𝓥Label = F2.𝓥Label ∘ 𝓥
-  /-- The morphism between edges and half-edges must commute with `𝓱𝓔To𝓔`. -/
-  𝓱𝓔To𝓔 : 𝓔 ∘ F1.𝓱𝓔To𝓔 = F2.𝓱𝓔To𝓔 ∘ 𝓱𝓔
-  /-- The morphism between vertices and half-edges must commute with `𝓱𝓔To𝓥`. -/
-  𝓱𝓔To𝓥 : 𝓥 ∘ F1.𝓱𝓔To𝓥 = F2.𝓱𝓔To𝓥 ∘ 𝓱𝓔
-
-namespace Hom
-
-lemma ext {F1 F2 : FeynmanDiagram} {f g : Hom F1 F2} (h1 : f.𝓱𝓔 = g.𝓱𝓔)
-    (h2 : f.𝓔 = g.𝓔) (h3 : f.𝓥 = g.𝓥) : f = g := by
-  cases f; cases g
-  simp_all only
-
-/-- The identity morphism from a Feynman diagram to itself. -/
-@[simps!]
-def id (F : FeynmanDiagram) : Hom F F where
-  𝓱𝓔 := 𝟙 F.𝓱𝓔
-  𝓔 := 𝟙 F.𝓔
-  𝓥 := 𝟙 F.𝓥
-  𝓔Label := rfl
-  𝓥Label := rfl
-  𝓱𝓔To𝓔 := rfl
-  𝓱𝓔To𝓥 := rfl
-
-/-- Composition of morphisms between Feynman diagrams. -/
-@[simps!]
-def comp {F1 F2 F3 : FeynmanDiagram} (f : Hom F1 F2)  (g : Hom F2 F3) : Hom F1 F3 where
-  𝓱𝓔 :=  f.𝓱𝓔 ≫ g.𝓱𝓔
-  𝓔 := f.𝓔 ≫ g.𝓔
-  𝓥 := f.𝓥 ≫ g.𝓥
-  𝓔Label := by
-    ext
-    simp [f.𝓔Label, g.𝓔Label]
-  𝓥Label := by
-    ext x
-    simp [f.𝓥Label, g.𝓥Label]
-  𝓱𝓔To𝓔 := by
-    rw [types_comp, types_comp, Function.comp.assoc]
-    rw [f.𝓱𝓔To𝓔, ← Function.comp.assoc, g.𝓱𝓔To𝓔]
-    rfl
-  𝓱𝓔To𝓥 := by
-    rw [types_comp, types_comp, Function.comp.assoc]
-    rw [f.𝓱𝓔To𝓥, ← Function.comp.assoc, g.𝓱𝓔To𝓥]
-    rfl
-
-/-- The condition on a triplet of maps for them to form a morphism of Feynman diagrams. -/
-def Cond {F1 F2 : FeynmanDiagram} (f𝓱𝓔 : F1.𝓱𝓔 → F2.𝓱𝓔) (f𝓔 : F1.𝓔 → F2.𝓔)
-    (f𝓥 :  F1.𝓥 → F2.𝓥) : Prop :=
-  F1.𝓔Label = F2.𝓔Label ∘ f𝓔 ∧  F1.𝓥Label = F2.𝓥Label ∘ f𝓥 ∧
-   f𝓔 ∘ F1.𝓱𝓔To𝓔 = F2.𝓱𝓔To𝓔 ∘ f𝓱𝓔 ∧  f𝓥 ∘ F1.𝓱𝓔To𝓥 = F2.𝓱𝓔To𝓥 ∘ f𝓱𝓔
-
-instance {F1 F2 : FeynmanDiagram} [IsFiniteDiagram F1] [IsFiniteDiagram F2]
-    (f𝓱𝓔 : F1.𝓱𝓔 → F2.𝓱𝓔) (f𝓔 : F1.𝓔 → F2.𝓔) (f𝓥 :  F1.𝓥 → F2.𝓥) :
-    Decidable (Cond f𝓱𝓔 f𝓔 f𝓥) :=
-  @And.decidable _ _ _ $
-  @And.decidable _ _ _ $
-  @And.decidable _ _ _ _
-
-end Hom
-
-@[simps!]
-instance : Category FeynmanDiagram where
-  Hom := Hom
-  id := Hom.id
-  comp := Hom.comp
-
-
-/-- The functor from the category of Feynman diagrams to `Type` taking a feynman diagram
-  to its set of half-edges. -/
-def toHalfEdges : FeynmanDiagram ⥤ Type where
-  obj F := F.𝓱𝓔
-  map f := f.𝓱𝓔
-
-/-- The functor from the category of Feynman diagrams to `Type` taking a feynman diagram
-  to its set of edges. -/
-def toEdges : FeynmanDiagram ⥤ Type where
-  obj F := F.𝓔
-  map f := f.𝓔
-
-/-- The functor from the category of Feynman diagrams to `Type` taking a feynman diagram
-  to its set of vertices. -/
-def toVertices : FeynmanDiagram ⥤ Type where
-  obj F := F.𝓥
-  map f := f.𝓥
-
-lemma 𝓱𝓔_bijective_of_isIso {F1 F2 : FeynmanDiagram} (f : F1 ⟶ F2) [IsIso f] :
-    f.𝓱𝓔.Bijective :=
-  (isIso_iff_bijective f.𝓱𝓔).mp $ Functor.map_isIso toHalfEdges f
-
-lemma 𝓔_bijective_of_isIso {F1 F2 : FeynmanDiagram} (f : F1 ⟶ F2) [IsIso f] :
-    f.𝓔.Bijective :=
-  (isIso_iff_bijective f.𝓔).mp $ Functor.map_isIso toEdges f
-
-lemma 𝓥_bijective_of_isIso {F1 F2 : FeynmanDiagram} (f : F1 ⟶ F2) [IsIso f] :
-    f.𝓥.Bijective :=
-  (isIso_iff_bijective f.𝓥).mp $ Functor.map_isIso toVertices f
-
-/-- An isomorphism formed from an equivalence between the types of half-edges, edges and vertices
-  satisfying the appropriate conditions. -/
-def mkIso {F1 F2 : FeynmanDiagram} (f𝓱𝓔 : F1.𝓱𝓔 ≃ F2.𝓱𝓔)
-    (f𝓔 : F1.𝓔 ≃ F2.𝓔) (f𝓥 : F1.𝓥 ≃ F2.𝓥)
-    (h𝓔Label : F1.𝓔Label = F2.𝓔Label ∘ f𝓔)
-    (h𝓥Label : F1.𝓥Label = F2.𝓥Label ∘ f𝓥)
-    (h𝓱𝓔To𝓔 : f𝓔 ∘ F1.𝓱𝓔To𝓔 = F2.𝓱𝓔To𝓔 ∘ f𝓱𝓔)
-    (h𝓱𝓔To𝓥 : f𝓥 ∘ F1.𝓱𝓔To𝓥 = F2.𝓱𝓔To𝓥 ∘ f𝓱𝓔) : F1 ≅ F2 where
-  hom := Hom.mk f𝓱𝓔 f𝓔 f𝓥 h𝓔Label h𝓥Label h𝓱𝓔To𝓔 h𝓱𝓔To𝓥
-  inv := Hom.mk f𝓱𝓔.symm f𝓔.symm f𝓥.symm
-    (((Iso.eq_inv_comp f𝓔.toIso).mpr h𝓔Label.symm).trans (types_comp _ _))
-    (((Iso.eq_inv_comp f𝓥.toIso).mpr h𝓥Label.symm).trans (types_comp _ _))
-    ((Iso.comp_inv_eq f𝓔.toIso).mpr $ (Iso.eq_inv_comp f𝓱𝓔.toIso).mpr $
-       (types_comp _ _).symm.trans (Eq.trans h𝓱𝓔To𝓔.symm (types_comp _ _)))
-    ((Iso.comp_inv_eq f𝓥.toIso).mpr $ (Iso.eq_inv_comp f𝓱𝓔.toIso).mpr $
-       (types_comp _ _).symm.trans (Eq.trans h𝓱𝓔To𝓥.symm (types_comp _ _)))
-  hom_inv_id := by
-    apply Hom.ext
-    ext a
-    simp only [instCategory_comp_𝓱𝓔, Equiv.symm_apply_apply, instCategory_id_𝓱𝓔]
-    ext a
-    simp only [instCategory_comp_𝓔, Equiv.symm_apply_apply, instCategory_id_𝓔]
-    ext a
-    simp only [instCategory_comp_𝓥, Equiv.symm_apply_apply, instCategory_id_𝓥]
-  inv_hom_id := by
-    apply Hom.ext
-    ext a
-    simp only [instCategory_comp_𝓱𝓔, Equiv.apply_symm_apply, instCategory_id_𝓱𝓔]
-    ext a
-    simp only [instCategory_comp_𝓔, Equiv.apply_symm_apply, instCategory_id_𝓔]
-    ext a
-    simp only [instCategory_comp_𝓥, Equiv.apply_symm_apply, instCategory_id_𝓥]
-
-lemma isIso_of_bijections {F1 F2 : FeynmanDiagram} (f : F1 ⟶ F2)
-    (h𝓱𝓔 : f.𝓱𝓔.Bijective) (h𝓔 : f.𝓔.Bijective) (h𝓥 : f.𝓥.Bijective) :
-    IsIso f :=
-  Iso.isIso_hom $ mkIso (Equiv.ofBijective f.𝓱𝓔 h𝓱𝓔) (Equiv.ofBijective f.𝓔 h𝓔)
-    (Equiv.ofBijective f.𝓥 h𝓥) f.𝓔Label f.𝓥Label f.𝓱𝓔To𝓔 f.𝓱𝓔To𝓥
-
-
-lemma isIso_iff_all_bijective {F1 F2 : FeynmanDiagram} (f : F1 ⟶ F2) :
-    IsIso f ↔ f.𝓱𝓔.Bijective ∧ f.𝓔.Bijective ∧ f.𝓥.Bijective :=
-  Iff.intro
-    (fun _ ↦ ⟨𝓱𝓔_bijective_of_isIso f, 𝓔_bijective_of_isIso f, 𝓥_bijective_of_isIso f⟩)
-    (fun ⟨h𝓱𝓔, h𝓔, h𝓥⟩ ↦ isIso_of_bijections f h𝓱𝓔 h𝓔 h𝓥)
-
-/-- An equivalence between the isomorphism class of a Feynman diagram an
-  permutations of the half-edges, edges and vertices satisfying the `Hom.cond`. -/
-def isoEquivBijec {F : FeynmanDiagram} :
-    (F ≅ F) ≃ {S : Equiv.Perm F.𝓱𝓔 × Equiv.Perm F.𝓔 × Equiv.Perm F.𝓥 //
-      Hom.Cond S.1 S.2.1 S.2.2} where
-  toFun f := ⟨⟨(toHalfEdges.mapIso f).toEquiv,
-    (toEdges.mapIso f).toEquiv , (toVertices.mapIso f).toEquiv⟩,
-    f.hom.𝓔Label, f.hom.𝓥Label, f.hom.𝓱𝓔To𝓔, f.hom.𝓱𝓔To𝓥⟩
-  invFun S := mkIso S.1.1 S.1.2.1 S.1.2.2 S.2.1 S.2.2.1 S.2.2.2.1 S.2.2.2.2
-  left_inv _ := rfl
-  right_inv _ := rfl
-
-instance {F : FeynmanDiagram} [IsFiniteDiagram F]  :
-    Fintype (F ≅ F)  :=
-  Fintype.ofEquiv _ isoEquivBijec.symm
-
-end categoryOfFeynmanDiagrams
-
-section symmetryFactors
-/-!
-## Symmetry factors
-
-The symmetry factor of a Feynman diagram is the cardinality of the group of automorphisms of that
-diagram. In this section we define symmetry factors for Feynman diagrams which are
-finite.
-
--/
-
-/-- The symmetry factor is the cardinality of the set of isomorphisms of the Feynman diagram. -/
-def symmetryFactor (F : FeynmanDiagram) [IsFiniteDiagram F] : ℕ :=
-  Fintype.card (F ≅ F)
-
-end symmetryFactors
-
-section connectedness
-/-!
-
-## 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.
-
--/
-
-/-- 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. -/
-@[simp]
-def adjRelation (F : FeynmanDiagram) : F.𝓥 → F.𝓥 → Prop := fun x y =>
-  x ≠ y ∧
-  ∃ (a b : F.𝓱𝓔), F.𝓱𝓔To𝓔 a = F.𝓱𝓔To𝓔 b ∧ F.𝓱𝓔To𝓥 a = x ∧ F.𝓱𝓔To𝓥 b = y
-
-/-- From a Feynman diagram the simple graph showing those vertices which are connected. -/
-def toSimpleGraph (F : FeynmanDiagram) : SimpleGraph F.𝓥 where
-  Adj := adjRelation F
-  symm := by
-    intro x y h
-    apply And.intro (Ne.symm h.1)
-    obtain ⟨a, b, hab⟩ := h.2
-    exact ⟨b, a, ⟨hab.1.symm, hab.2.2, hab.2.1⟩⟩
-  loopless := by
-    intro x h
-    simp at h
-
-instance {F : FeynmanDiagram} [IsFiniteDiagram F] : DecidableRel F.toSimpleGraph.Adj := fun _ _ =>
-   And.decidable
-
-instance {F : FeynmanDiagram} [IsFiniteDiagram F]  :
-  Decidable (F.toSimpleGraph.Preconnected ∧ Nonempty F.𝓥) :=
-  @And.decidable _ _ _ _
-
-instance {F : FeynmanDiagram} [IsFiniteDiagram F] : Decidable F.toSimpleGraph.Connected :=
-  decidable_of_iff _ (SimpleGraph.connected_iff F.toSimpleGraph).symm
-
-/-- We say a Feynman diagram is connected if its simple graph is connected. -/
-def Connected (F : FeynmanDiagram) : Prop := F.toSimpleGraph.Connected
-
-instance {F : FeynmanDiagram} [IsFiniteDiagram F] : Decidable (Connected F) :=
-  PhiFour.FeynmanDiagram.instDecidableConnected𝓥ToSimpleGraphOfIsFiniteDiagram
-
-end connectedness
-
-section examples
-/-!
-
-## Examples
-
-In this section we give examples of Feynman diagrams in Phi^4 theory.
-
-Symmetry factors can be compared with e.g. those in
-- https://arxiv.org/abs/0907.0859
-
--/
-
-/-- The propagator
-  - - - - - -
-
- -/
-def propagator : FeynmanDiagram where
-  𝓱𝓔 := Fin 2
-  𝓔 := Fin 1
-  𝓔Label  := ![0]
-  𝓱𝓔To𝓔 := ![0, 0]
-  𝓔Fiber := by decide
-  𝓥 := Fin 2
-  𝓥Label := ![0, 0]
-  𝓱𝓔To𝓥 := ![0, 1]
-  𝓥Fiber := by decide
-
-instance : IsFiniteDiagram propagator where
-  𝓔Fintype := Fin.fintype 1
-  𝓔DecidableEq := instDecidableEqFin 1
-  𝓥Fintype := Fin.fintype 2
-  𝓥DecidableEq := instDecidableEqFin 2
-  𝓱𝓔Fintype := Fin.fintype 2
-  𝓱𝓔DecidableEq := instDecidableEqFin 2
-
-lemma propagator_symmetryFactor : symmetryFactor propagator = 2 := by
-  decide
-
-/-- The figure 8 Feynman diagram
-     _
-   /    \
-  /      \
-  \      /
-   \    /
-    \  /
-    /  \
-   /    \
-  \      /
-   \ __ /  -/
-@[simps!]
-def figureEight : FeynmanDiagram where
-  𝓱𝓔 := Fin 4
-  𝓔 := Fin 2
-  𝓔Label  := ![0, 0]
-  𝓱𝓔To𝓔 := ![0, 0, 1, 1]
-  𝓔Fiber := by decide
-  𝓥 := Fin 1
-  𝓥Label := ![1]
-  𝓱𝓔To𝓥 := ![0, 0, 0, 0]
-  𝓥Fiber := by decide
-
-instance : IsFiniteDiagram figureEight where
-  𝓔Fintype := Fin.fintype 2
-  𝓔DecidableEq := instDecidableEqFin 2
-  𝓥Fintype := Fin.fintype 1
-  𝓥DecidableEq := instDecidableEqFin 1
-  𝓱𝓔Fintype := Fin.fintype 4
-  𝓱𝓔DecidableEq := instDecidableEqFin 4
-
-
-lemma figureEight_connected : Connected figureEight := by
-  decide
-
-lemma figureEight_symmetryFactor : symmetryFactor figureEight = 8 := by
-  decide
-
-/-- The feynman diagram
-        _ _ _ _ _
-     /           \
-    /             \
- - - - - - - - - - - - -
-    \             /
-     \ _ _ _ _ _/
--/
-def diagram1 : FeynmanDiagram where
-  𝓱𝓔 := Fin 10
-  𝓔 := Fin 5
-  𝓔Label  := ![0, 0, 0, 0, 0]
-  𝓱𝓔To𝓔 := ![0, 0, 1, 1, 2, 2, 3, 3, 4, 4]
-  𝓔Fiber := by decide
-  𝓥 := Fin 4
-  𝓥Label := ![0, 1, 1, 0]
-  𝓱𝓔To𝓥 := ![0, 1, 1, 2, 1, 2, 1, 2, 2, 3]
-  𝓥Fiber := by decide
-
-/-- An example of a disconnected Feynman diagram. -/
-def diagram2 : FeynmanDiagram where
-  𝓱𝓔 := Fin 14
-  𝓔 := Fin 7
-  𝓔Label := ![0, 0, 0, 0, 0, 0, 0]
-  𝓱𝓔To𝓔 := ![0, 0, 1, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, 6]
-  𝓔Fiber := by decide
-  𝓥 := Fin 5
-  𝓥Label := ![0, 0, 1, 1, 1]
-  𝓱𝓔To𝓥 := ![0, 1, 2, 2, 2, 2, 3, 3, 3, 3, 4, 4, 4, 4]
-  𝓥Fiber := by decide
-
-instance : IsFiniteDiagram diagram2 where
-  𝓔Fintype := Fin.fintype _
-  𝓔DecidableEq := instDecidableEqFin _
-  𝓥Fintype := Fin.fintype _
-  𝓥DecidableEq := instDecidableEqFin _
-  𝓱𝓔Fintype := Fin.fintype _
-  𝓱𝓔DecidableEq := instDecidableEqFin _
-
-lemma diagram2_not_connected : ¬ Connected diagram2 := by
-  decide
-
-
-
-end examples
-
-end FeynmanDiagram
-
-end PhiFour

From 4632b66854f0cb5abb2d714329d5fa37860c092b Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 18 Jun 2024 13:07:49 -0400
Subject: [PATCH 3/3] refactor: Lint

---
 HepLean.lean                                  |  4 +-
 HepLean/FeynmanDiagrams/Basic.lean            | 60 ++++++++++++-------
 .../Instances/ComplexScalar.lean              | 31 +---------
 HepLean/FeynmanDiagrams/Instances/Phi4.lean   | 15 +----
 4 files changed, 44 insertions(+), 66 deletions(-)

diff --git a/HepLean.lean b/HepLean.lean
index 42cdf18..18386db 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -48,7 +48,9 @@ import HepLean.AnomalyCancellation.SMNu.PlusU1.PlaneNonSols
 import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSol
 import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSolToSol
 import HepLean.BeyondTheStandardModel.TwoHDM.Basic
-import HepLean.FeynmanDiagrams.PhiFour.Basic
+import HepLean.FeynmanDiagrams.Basic
+import HepLean.FeynmanDiagrams.Instances.ComplexScalar
+import HepLean.FeynmanDiagrams.Instances.Phi4
 import HepLean.FlavorPhysics.CKMMatrix.Basic
 import HepLean.FlavorPhysics.CKMMatrix.Invariants
 import HepLean.FlavorPhysics.CKMMatrix.PhaseFreedom
diff --git a/HepLean/FeynmanDiagrams/Basic.lean b/HepLean/FeynmanDiagrams/Basic.lean
index 0230d38..4611cca 100644
--- a/HepLean/FeynmanDiagrams/Basic.lean
+++ b/HepLean/FeynmanDiagrams/Basic.lean
@@ -119,13 +119,21 @@ properties.
 
 -/
 
+/-- A set of conditions on  `PreFeynmanRule` for it to be considered finite. -/
 class IsFinitePreFeynmanRule (P : PreFeynmanRule) where
+  /-- The type of edge labels is decidable. -/
   edgeLabelDecidable : DecidableEq P.EdgeLabel
+  /-- The type of vertex labels is decidable. -/
   vertexLabelDecidable : DecidableEq P.VertexLabel
+  /-- The type of half-edge labels is decidable. -/
   halfEdgeLabelDecidable : DecidableEq P.HalfEdgeLabel
+  /-- The type of half-edges associated with a vertex is finite. -/
   vertexMapFintype : ∀ v : P.VertexLabel, Fintype (P.vertexLabelMap v).left
+  /-- The type of half-edges associated with a vertex is decidable. -/
   vertexMapDecidable : ∀ v : P.VertexLabel, DecidableEq (P.vertexLabelMap v).left
+  /-- The type of half-edges associated with an edge is finite. -/
   edgeMapFintype : ∀ v : P.EdgeLabel, Fintype (P.edgeLabelMap v).left
+  /-- The type of half-edges associated with an edge is decidable. -/
   edgeMapDecidable : ∀ v : P.EdgeLabel, DecidableEq (P.edgeLabelMap v).left
 
 instance preFeynmanRuleDecEq𝓔 (P : PreFeynmanRule) [IsFinitePreFeynmanRule P] :
@@ -166,31 +174,31 @@ instance preimageEdgeDecidablePred {𝓔 𝓥 : Type} [DecidableEq 𝓔] (v : 
   | isTrue h => isTrue h
   | isFalse h => isFalse h
 
-instance preimageVertexDecidable [IsFinitePreFeynmanRule P]  {𝓔 𝓥 : Type} (v : 𝓥)
+instance preimageVertexDecidable {𝓔 𝓥 : Type} (v : 𝓥)
    (F : Over (P.HalfEdgeLabel  × 𝓔 × 𝓥)) [DecidableEq F.left] :
     DecidableEq ((P.preimageVertex v).obj F).left := Subtype.instDecidableEq
 
-instance preimageEdgeDecidable [IsFinitePreFeynmanRule P]  {𝓔 𝓥 : Type} (v : 𝓔)
+instance preimageEdgeDecidable {𝓔 𝓥 : Type} (v : 𝓔)
    (F : Over (P.HalfEdgeLabel  × 𝓔 × 𝓥)) [DecidableEq F.left] :
     DecidableEq ((P.preimageEdge v).obj F).left := Subtype.instDecidableEq
 
-instance preimageVertexFintype [IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type} [DecidableEq 𝓥] [Fintype 𝓥]
-    (v : 𝓥) (F : Over (P.HalfEdgeLabel  × 𝓔 × 𝓥)) [DecidableEq F.left] [h : Fintype F.left] :
+instance preimageVertexFintype  {𝓔 𝓥 : Type} [DecidableEq 𝓥]
+    (v : 𝓥) (F : Over (P.HalfEdgeLabel  × 𝓔 × 𝓥)) [h : Fintype F.left] :
     Fintype ((P.preimageVertex v).obj F).left :=  @Subtype.fintype _ _ _ h
 
-instance preimageEdgeFintype [IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type} [DecidableEq 𝓔] [Fintype 𝓔]
-    (v : 𝓔) (F : Over (P.HalfEdgeLabel  × 𝓔 × 𝓥)) [DecidableEq F.left] [h : Fintype F.left] :
+instance preimageEdgeFintype {𝓔 𝓥 : Type} [DecidableEq 𝓔]
+    (v : 𝓔) (F : Over (P.HalfEdgeLabel  × 𝓔 × 𝓥)) [h : Fintype F.left] :
     Fintype ((P.preimageEdge v).obj F).left :=  @Subtype.fintype _ _ _ h
 
-instance preimageVertexMapFintype  [IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type} [Fintype 𝓥]
+instance preimageVertexMapFintype  [IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type}
     [DecidableEq 𝓥]  (v : 𝓥) (f : 𝓥 ⟶ P.VertexLabel) (F : Over (P.HalfEdgeLabel  × 𝓔 × 𝓥))
-    [DecidableEq F.left] [Fintype F.left]:
+    [Fintype F.left] :
     Fintype  ((P.vertexLabelMap (f v)).left → ((P.preimageVertex v).obj F).left) :=
   Pi.fintype
 
-instance preimageEdgeMapFintype  [IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type} [Fintype 𝓔]
+instance preimageEdgeMapFintype  [IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type}
     [DecidableEq 𝓔] (v : 𝓔) (f : 𝓔 ⟶ P.EdgeLabel) (F : Over (P.HalfEdgeLabel  × 𝓔 × 𝓥))
-    [DecidableEq F.left] [Fintype F.left]:
+    [Fintype F.left] :
     Fintype  ((P.edgeLabelMap (f v)).left → ((P.preimageEdge v).obj F).left) :=
   Pi.fintype
 
@@ -360,12 +368,19 @@ that certain propositions are decidable.
 
 -/
 
+/-- A set of conditions on a Feynman diagram for it to be considered finite. -/
 class IsFiniteDiagram (F : FeynmanDiagram P) where
+  /-- The type of edges is finite. -/
   𝓔Fintype : Fintype F.𝓔
+  /-- The type of edges is decidable. -/
   𝓔DecidableEq : DecidableEq F.𝓔
+  /-- The type of vertices is finite. -/
   𝓥Fintype : Fintype F.𝓥
+  /-- The type of vertices is decidable. -/
   𝓥DecidableEq : DecidableEq F.𝓥
+  /-- The type of half-edges is finite. -/
   𝓱𝓔Fintype : Fintype F.𝓱𝓔
+  /-- The type of half-edges is decidable. -/
   𝓱𝓔DecidableEq : DecidableEq F.𝓱𝓔
 
 instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : Fintype F.𝓔 :=
@@ -418,7 +433,7 @@ def edgeVertexEquiv {F G : FeynmanDiagram P}  (𝓔 : F.𝓔 ≃ G.𝓔) (𝓥 :
 /-- The functor of over-categories generated by `edgeVertexMap`. -/
 @[simps!]
 def edgeVertexFunc {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ⟶ G.𝓔) (𝓥 : F.𝓥 ⟶ G.𝓥) :
-   Over (P.HalfEdgeLabel × F.𝓔 × F.𝓥) ⥤ Over (P.HalfEdgeLabel × G.𝓔 × G.𝓥) :=
+    Over (P.HalfEdgeLabel × F.𝓔 × F.𝓥) ⥤ Over (P.HalfEdgeLabel × G.𝓔 × G.𝓥) :=
   Over.map <| edgeVertexMap 𝓔 𝓥
 
 /-- A morphism of Feynman diagrams. -/
@@ -460,7 +475,7 @@ def id (F : FeynmanDiagram P) : Hom F F where
   𝓱𝓔To𝓔𝓥 := 𝟙 F.𝓱𝓔To𝓔𝓥
 
 /-- The composition of two morphisms of Feynman diagrams. -/
-@[simps!]
+@[simps! 𝓔𝓞_left 𝓥𝓞_left 𝓱𝓔To𝓔𝓥_left]
 def comp {F G H : FeynmanDiagram P} (f : Hom F G) (g : Hom G H) : Hom F H where
   𝓔𝓞 := f.𝓔𝓞 ≫ g.𝓔𝓞
   𝓥𝓞 := f.𝓥𝓞 ≫ g.𝓥𝓞
@@ -480,6 +495,8 @@ lemma ext {F G : FeynmanDiagram P} {f g : Hom F G} (h𝓔 : f.𝓔 = g.𝓔)
     (h𝓥 : f.𝓥 = g.𝓥) (h𝓱𝓔 : f.𝓱𝓔 = g.𝓱𝓔) : f = g :=
   ext' (Over.OverMorphism.ext h𝓔) (Over.OverMorphism.ext h𝓥) h𝓱𝓔
 
+/-- The condition on maps of edges, vertices and half-edges for it to be lifted to a
+  morphism of Feynman diagrams. -/
 def Cond {F G : FeynmanDiagram P} (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔) : Prop :=
   (∀ x, G.𝓔𝓞.hom (𝓔 x) = F.𝓔𝓞.hom x) ∧
   (∀ x, G.𝓥𝓞.hom (𝓥 x) = F.𝓥𝓞.hom x) ∧
@@ -518,7 +535,7 @@ instance {F G : FeynmanDiagram P} [IsFiniteDiagram F] [IsFiniteDiagram G] [IsFin
 
 
 /-- Making a Feynman diagram from maps of edges, vertices and half-edges. -/
-@[simps!]
+@[simps! 𝓔𝓞_left 𝓥𝓞_left 𝓱𝓔To𝓔𝓥_left]
 def mk' {F G : FeynmanDiagram P} (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔)
     (C : Cond 𝓔 𝓥 𝓱𝓔) : Hom F G where
   𝓔𝓞 := Over.homMk 𝓔 $ funext C.1
@@ -540,7 +557,7 @@ and the condition on whether a diagram is connected.
 -/
 
 /-- Feynman diagrams form a category. -/
-@[simps!]
+@[simps! id_𝓔𝓞_left id_𝓥𝓞_left id_𝓱𝓔To𝓔𝓥_left comp_𝓔𝓞_left comp_𝓥𝓞_left comp_𝓱𝓔To𝓔𝓥_left]
 instance : Category (FeynmanDiagram P) where
   Hom := Hom
   id := Hom.id
@@ -624,6 +641,7 @@ instance [IsFinitePreFeynmanRule P] [IsFiniteDiagram F] : Fintype F.SymmetryType
 @[simp]
 def cardSymmetryFactor : Cardinal := Cardinal.mk (F.SymmetryType)
 
+/-- The symmetry factor of a Finite Feynman diagram, as a natural number.  -/
 @[simp]
 def symmetryFactor [IsFinitePreFeynmanRule P] [IsFiniteDiagram F] : ℕ :=
   (Fintype.card F.SymmetryType)
@@ -657,7 +675,7 @@ def adjRelation : F.𝓥 → F.𝓥 → Prop := fun x y =>
   ∃ (a 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 [IsFinitePreFeynmanRule P] [IsFiniteDiagram F] : DecidableRel F.adjRelation := fun _ _ =>
+instance [IsFiniteDiagram F] : DecidableRel F.adjRelation := fun _ _ =>
   @And.decidable _ _ _ $
   @Fintype.decidableExistsFintype _ _ (fun _ => @Fintype.decidableExistsFintype _ _  (
   fun _ => @And.decidable _ _ (instDecidableEq𝓔OfIsFiniteDiagram _ _) $
@@ -678,21 +696,21 @@ def toSimpleGraph : SimpleGraph F.𝓥 where
     intro x h
     simp at h
 
-instance  [IsFinitePreFeynmanRule P] [IsFiniteDiagram F] : DecidableRel F.toSimpleGraph.Adj :=
-  instDecidableRel𝓥AdjRelationOfIsFinitePreFeynmanRuleOfIsFiniteDiagram F
+instance [IsFiniteDiagram F] : DecidableRel F.toSimpleGraph.Adj :=
+  instDecidableRel𝓥AdjRelationOfIsFiniteDiagram F
 
-instance [IsFinitePreFeynmanRule P] [IsFiniteDiagram F]  :
+instance [IsFiniteDiagram F] :
   Decidable (F.toSimpleGraph.Preconnected ∧ Nonempty F.𝓥) :=
   @And.decidable _ _ _ $ decidable_of_iff _ Finset.univ_nonempty_iff
 
-instance [IsFinitePreFeynmanRule P] [IsFiniteDiagram F] : Decidable F.toSimpleGraph.Connected :=
+instance [IsFiniteDiagram F] : Decidable F.toSimpleGraph.Connected :=
   decidable_of_iff _ (SimpleGraph.connected_iff F.toSimpleGraph).symm
 
 /-- We say a Feynman diagram is connected if its simple graph is connected. -/
 def Connected : Prop := F.toSimpleGraph.Connected
 
-instance [IsFinitePreFeynmanRule P] [IsFiniteDiagram F] : Decidable (Connected F) :=
-  instDecidableConnected𝓥ToSimpleGraphOfIsFinitePreFeynmanRuleOfIsFiniteDiagram F
+instance [IsFiniteDiagram F] : Decidable (Connected F) :=
+  instDecidableConnected𝓥ToSimpleGraphOfIsFiniteDiagram F
 
 end connectedness
 
diff --git a/HepLean/FeynmanDiagrams/Instances/ComplexScalar.lean b/HepLean/FeynmanDiagrams/Instances/ComplexScalar.lean
index 22801c8..6b77219 100644
--- a/HepLean/FeynmanDiagrams/Instances/ComplexScalar.lean
+++ b/HepLean/FeynmanDiagrams/Instances/ComplexScalar.lean
@@ -17,6 +17,7 @@ open CategoryTheory
 open FeynmanDiagram
 open PreFeynmanRule
 
+/-- The pre-Feynman rules for a complex scalar theory. -/
 @[simps!]
 def complexScalarFeynmanRules : PreFeynmanRule where
   /- There is 2 types of `half-edge`. -/
@@ -43,7 +44,6 @@ instance (a : ℕ) : OfNat complexScalarFeynmanRules.HalfEdgeLabel a where
 instance (a : ℕ) : OfNat complexScalarFeynmanRules.VertexLabel a where
   ofNat := (a : Fin _)
 
-
 instance : IsFinitePreFeynmanRule complexScalarFeynmanRules where
   edgeLabelDecidable :=  instDecidableEqFin _
   vertexLabelDecidable := instDecidableEqFin _
@@ -68,33 +68,4 @@ instance : IsFinitePreFeynmanRule complexScalarFeynmanRules where
 
 
 
-
-set_option maxRecDepth 1000 in
-def loopProp : FeynmanDiagram complexScalarFeynmanRules :=
-  mk' ![0, 0, 0] ![0, 2, 1] ![⟨0, 0, 0⟩, ⟨1, 0, 1⟩,
-    ⟨0, 1, 1⟩, ⟨1, 1, 1⟩, ⟨0, 2, 1⟩, ⟨1, 2, 2⟩] (by decide)
-
-instance : IsFiniteDiagram loopProp where
-  𝓔Fintype := Fin.fintype _
-  𝓔DecidableEq := instDecidableEqFin _
-  𝓥Fintype := Fin.fintype _
-  𝓥DecidableEq := instDecidableEqFin _
-  𝓱𝓔Fintype := Fin.fintype _
-  𝓱𝓔DecidableEq := instDecidableEqFin _
-
-def prop : FeynmanDiagram complexScalarFeynmanRules :=
-  mk' ![0] ![0, 1] ![⟨0, 0, 0⟩, ⟨1, 0, 1⟩] (by decide)
-
-instance : IsFiniteDiagram prop where
-  𝓔Fintype := Fin.fintype _
-  𝓔DecidableEq := instDecidableEqFin _
-  𝓥Fintype := Fin.fintype _
-  𝓥DecidableEq := instDecidableEqFin _
-  𝓱𝓔Fintype := Fin.fintype _
-  𝓱𝓔DecidableEq := instDecidableEqFin _
-
-lemma prop_symmetryFactor_eq_one : symmetryFactor prop = 1 := by decide
-
-
-
 end PhiFour
diff --git a/HepLean/FeynmanDiagrams/Instances/Phi4.lean b/HepLean/FeynmanDiagrams/Instances/Phi4.lean
index ef1d5e6..86404ea 100644
--- a/HepLean/FeynmanDiagrams/Instances/Phi4.lean
+++ b/HepLean/FeynmanDiagrams/Instances/Phi4.lean
@@ -19,6 +19,7 @@ open CategoryTheory
 open FeynmanDiagram
 open PreFeynmanRule
 
+/-- The pre-Feynman rules for `Phi^4` theory. -/
 @[simps!]
 def phi4PreFeynmanRules : PreFeynmanRule where
   /- There is only 1 type of `half-edge`. -/
@@ -65,19 +66,5 @@ instance : IsFinitePreFeynmanRule phi4PreFeynmanRules where
     | 0 => instDecidableEqFin _
 
 
-def figureEight : FeynmanDiagram phi4PreFeynmanRules :=
-  mk' ![0, 0] ![1] ![⟨0, 0, 0⟩, ⟨0, 0, 0⟩, ⟨0, 1, 0⟩, ⟨0, 1, 0⟩] (by decide)
-
-instance : IsFiniteDiagram figureEight where
-  𝓔Fintype := Fin.fintype _
-  𝓔DecidableEq := instDecidableEqFin _
-  𝓥Fintype := Fin.fintype _
-  𝓥DecidableEq := instDecidableEqFin _
-  𝓱𝓔Fintype := Fin.fintype _
-  𝓱𝓔DecidableEq := instDecidableEqFin _
-
-#eval symmetryFactor figureEight
-
-#eval Connected figureEight
 
 end PhiFour