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

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

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

From 277436c3476ee00dc860c442dbe22c84d55d670c Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 19 Jun 2024 07:45:19 -0400
Subject: [PATCH 2/5] fix: Imports to make computable

---
 HepLean/FeynmanDiagrams/Basic.lean    |  2 +-
 HepLean/FeynmanDiagrams/Momentum.lean | 19 ++++++++++++++++---
 2 files changed, 17 insertions(+), 4 deletions(-)

diff --git a/HepLean/FeynmanDiagrams/Basic.lean b/HepLean/FeynmanDiagrams/Basic.lean
index 12714fb..6267594 100644
--- a/HepLean/FeynmanDiagrams/Basic.lean
+++ b/HepLean/FeynmanDiagrams/Basic.lean
@@ -737,7 +737,7 @@ instance [IsFiniteDiagram F] :
 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. -/
+/-- A Feynman diagram is connected if its simple graph is connected. -/
 def Connected : Prop := F.toSimpleGraph.Connected
 
 instance [IsFiniteDiagram F] : Decidable (Connected F) :=
diff --git a/HepLean/FeynmanDiagrams/Momentum.lean b/HepLean/FeynmanDiagrams/Momentum.lean
index e811ab3..5bcccfd 100644
--- a/HepLean/FeynmanDiagrams/Momentum.lean
+++ b/HepLean/FeynmanDiagrams/Momentum.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.FeynmanDiagrams.Basic
-import Mathlib.Analysis.InnerProductSpace.Adjoint
+import Mathlib.Data.Real.Basic
 import Mathlib.Algebra.Category.ModuleCat.Basic
 /-!
 # Momentum in Feynman diagrams
@@ -12,6 +12,9 @@ import Mathlib.Algebra.Category.ModuleCat.Basic
 The aim of this file is to associate with each half-edge of a Feynman diagram a momentum,
 and constrain the momentums based conservation at each vertex and edge.
 
+The number of loops of a Feynman diagram is related to the dimension of the resulting
+vector space.
+
 -/
 
 namespace FeynmanDiagram
@@ -28,7 +31,8 @@ def SingleMomentumSpace : Type :=  Fin d → ℝ
 
 instance : AddCommGroup (SingleMomentumSpace d) := Pi.addCommGroup
 
-noncomputable instance : Module ℝ (SingleMomentumSpace d) := Pi.module _ _ _
+instance : Module ℝ (SingleMomentumSpace d) := Pi.module _ _ _
+
 
 /-- The type which asociates to each half-edge a `d`-dimensional vector.
  This is to be interpreted as the momentum associated to that half-edge flowing from the
@@ -37,7 +41,7 @@ def FullMomentumSpace : Type := F.𝓱𝓔 → Fin d → ℝ
 
 instance : AddCommGroup (F.FullMomentumSpace d) := Pi.addCommGroup
 
-noncomputable instance : Module ℝ (F.FullMomentumSpace d) := Pi.module _ _ _
+instance : Module ℝ (F.FullMomentumSpace d) := Pi.module _ _ _
 
 /-- The linear map taking a half-edge to its momentum.
  (defined as flowing from the `edge` to the vertex.) -/
@@ -69,5 +73,14 @@ noncomputable def funcFullMomentumSpace : FeynmanDiagram P ⥤ (ModuleCat ℝ)
 /-!
 ## Edge constraints
 
+There is a linear map from `F.FullMomentumSpace` to `F.EdgeMomentumSpace`, induced
+by the constraints at each edge.
+
+We impose the constraint that we live in the kernal of this linear map.
+
+A similar result is true for the vertex constraints.
+
 -/
+
+
 end FeynmanDiagram

From 65cbef4bd21f67e90d2e9c6aaa7507e93fe8b2fd Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 19 Jun 2024 13:02:09 -0400
Subject: [PATCH 3/5] feat: Add definition of Number of Loops

---
 HepLean/FeynmanDiagrams/Basic.lean          |  16 ++
 HepLean/FeynmanDiagrams/Instances/Phi4.lean |  31 ++-
 HepLean/FeynmanDiagrams/Momentum.lean       | 213 +++++++++++++++-----
 3 files changed, 207 insertions(+), 53 deletions(-)

diff --git a/HepLean/FeynmanDiagrams/Basic.lean b/HepLean/FeynmanDiagrams/Basic.lean
index 6267594..dc69ac2 100644
--- a/HepLean/FeynmanDiagrams/Basic.lean
+++ b/HepLean/FeynmanDiagrams/Basic.lean
@@ -348,6 +348,12 @@ 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𝓔𝓥
 
+/-- The map `F.𝓱𝓔 → F.𝓔` as an object in `Over F.𝓔 `. -/
+def 𝓱𝓔To𝓔 : Over F.𝓔 := P.toEdge.obj F.𝓱𝓔To𝓔𝓥
+
+/-- The map `F.𝓱𝓔 → F.𝓥` as an object in `Over F.𝓥 `. -/
+def 𝓱𝓔To𝓥 : Over F.𝓥 := P.toVertex.obj F.𝓱𝓔To𝓔𝓥
+
 /-!
 
 ## Making a Feynman diagram
@@ -414,6 +420,13 @@ class IsFiniteDiagram (F : FeynmanDiagram P) where
   /-- The type of half-edges is decidable. -/
   𝓱𝓔DecidableEq : DecidableEq F.𝓱𝓔
 
+instance {𝓔 𝓥 𝓱𝓔 : Type} [h1 : Fintype 𝓔] [h2 : DecidableEq 𝓔]
+    [h3 : Fintype 𝓥] [h4 : DecidableEq 𝓥] [h5 : Fintype 𝓱𝓔] [h6 : DecidableEq 𝓱𝓔]
+    (𝓔𝓞 : 𝓔 → P.EdgeLabel) (𝓥𝓞 : 𝓥 → P.VertexLabel)
+    (𝓱𝓔To𝓔𝓥 : 𝓱𝓔 → P.HalfEdgeLabel × 𝓔 × 𝓥) (C : Cond 𝓔𝓞 𝓥𝓞 𝓱𝓔To𝓔𝓥) :
+    IsFiniteDiagram (mk' 𝓔𝓞 𝓥𝓞 𝓱𝓔To𝓔𝓥 C) :=
+  ⟨h1, h2, h3, h4, h5, h6⟩
+
 instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : Fintype F.𝓔 :=
   IsFiniteDiagram.𝓔Fintype
 
@@ -432,6 +445,9 @@ instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : Fintype F.𝓱𝓔 :=
 instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : DecidableEq F.𝓱𝓔 :=
   IsFiniteDiagram.𝓱𝓔DecidableEq
 
+instance {F : FeynmanDiagram P} [IsFiniteDiagram F] (i : F.𝓱𝓔) (j : F.𝓔) :
+    Decidable (F.𝓱𝓔To𝓔.hom i = j) :=  IsFiniteDiagram.𝓔DecidableEq (F.𝓱𝓔To𝓔.hom i) j
+
 instance fintypeProdHalfEdgeLabel𝓔𝓥 {F : FeynmanDiagram P} [IsFinitePreFeynmanRule P]
     [IsFiniteDiagram F] : DecidableEq (P.HalfEdgeLabel × F.𝓔 × F.𝓥) :=
   instDecidableEqProd
diff --git a/HepLean/FeynmanDiagrams/Instances/Phi4.lean b/HepLean/FeynmanDiagrams/Instances/Phi4.lean
index 86404ea..9ecb20e 100644
--- a/HepLean/FeynmanDiagrams/Instances/Phi4.lean
+++ b/HepLean/FeynmanDiagrams/Instances/Phi4.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.FeynmanDiagrams.Basic
+import HepLean.FeynmanDiagrams.Momentum
 /-!
 # Feynman diagrams in Phi^4 theory
 
@@ -65,6 +65,35 @@ instance : IsFinitePreFeynmanRule phi4PreFeynmanRules where
     match v with
     | 0 => instDecidableEqFin _
 
+/-!
+
+## The figure eight diagram
+
+This section provides an example of the use of Feynman diagrams in HepLean.
+
+-/
+section Example
+
+/-- The figure eight Feynman diagram. -/
+abbrev figureEight : FeynmanDiagram phi4PreFeynmanRules :=
+  mk'
+    ![0, 0] -- edges
+    ![1] -- one internal vertex
+    ![⟨0, 0, 0⟩, ⟨0, 0, 0⟩, ⟨0, 1, 0⟩, ⟨0, 1, 0⟩] -- four half-edges
+    (by decide) -- the condition to form a Feynman diagram.
+
+/-- `figureEight` is connected. We can get this from
+  `#eval Connected figureEight`. -/
+lemma figureEight_connected : Connected figureEight := by decide
+
+/-- The symmetry factor of `figureEight` is 8. We can get this from
+  `#eval symmetryFactor figureEight`. -/
+lemma figureEight_symmetryFactor : symmetryFactor figureEight = 8 := by decide
+
+lemma figureEight_halfEdgeToEdgeIntMatrix :
+  figureEight.halfEdgeToEdgeIntMatrix  = !![1, 0; 1, 0 ; 0, 1; 0, 1] := by decide
+
+end Example
 
 
 end PhiFour
diff --git a/HepLean/FeynmanDiagrams/Momentum.lean b/HepLean/FeynmanDiagrams/Momentum.lean
index 5bcccfd..2152a68 100644
--- a/HepLean/FeynmanDiagrams/Momentum.lean
+++ b/HepLean/FeynmanDiagrams/Momentum.lean
@@ -6,6 +6,11 @@ Authors: Joseph Tooby-Smith
 import HepLean.FeynmanDiagrams.Basic
 import Mathlib.Data.Real.Basic
 import Mathlib.Algebra.Category.ModuleCat.Basic
+import Mathlib.LinearAlgebra.StdBasis
+import Mathlib.LinearAlgebra.Matrix.ToLin
+import Mathlib.Data.Matrix.Rank
+import Mathlib.Algebra.DirectSum.Module
+import Mathlib.LinearAlgebra.SesquilinearForm
 /-!
 # Momentum in Feynman diagrams
 
@@ -15,72 +20,176 @@ and constrain the momentums based conservation at each vertex and edge.
 The number of loops of a Feynman diagram is related to the dimension of the resulting
 vector space.
 
+## TODO
+
+- Prove lemmas that make the calcuation of the number of loops of a Feynman diagram easier.
+
+## Note
+
+This section is non-computable as we depend on the norm on `F.HalfEdgeMomenta`.
 -/
 
+
 namespace FeynmanDiagram
 
 open CategoryTheory
 open PreFeynmanRule
 
-variable {P : PreFeynmanRule} (F : FeynmanDiagram P)
-variable (d : ℕ)
-
-/-- The momentum space for a `d`-dimensional field theory for a single particle.
-  TODO: Move this definition, and define it as a four-vector. -/
-def SingleMomentumSpace : Type :=  Fin d → ℝ
-
-instance : AddCommGroup (SingleMomentumSpace d) := Pi.addCommGroup
-
-instance : Module ℝ (SingleMomentumSpace d) := Pi.module _ _ _
-
-
-/-- The type which asociates to each half-edge a `d`-dimensional vector.
- This is to be interpreted as the momentum associated to that half-edge flowing from the
- corresponding `edge` to the corresponding `vertex`. So all momentums flow into vertices. -/
-def FullMomentumSpace : Type := F.𝓱𝓔 → Fin d → ℝ
-
-instance : AddCommGroup (F.FullMomentumSpace d) := Pi.addCommGroup
-
-instance : Module ℝ (F.FullMomentumSpace d) := Pi.module _ _ _
-
-/-- The linear map taking a half-edge to its momentum.
- (defined as flowing from the `edge` to the vertex.) -/
-def toHalfEdgeMomentum (i : F.𝓱𝓔) : F.FullMomentumSpace d →ₗ[ℝ] SingleMomentumSpace d where
-  toFun x := x i
-  map_add' x y := by rfl
-  map_smul' c x := by rfl
-
-namespace Hom
-
-variable {F G : FeynmanDiagram P}
-variable (f : F ⟶ G)
-
-/-- The linear map induced by a morphism of Feynman diagrams. -/
-def toLinearMap : G.FullMomentumSpace d →ₗ[ℝ] F.FullMomentumSpace d where
-  toFun x := x ∘ f.𝓱𝓔
-  map_add' x y := by rfl
-  map_smul' c x := by rfl
-
-
-end Hom
-
-/-- The contravariant functor from Feynman diagrams to Modules over `ℝ`.  -/
-noncomputable def funcFullMomentumSpace : FeynmanDiagram P ⥤ (ModuleCat ℝ)ᵒᵖ where
-  obj F := Opposite.op $ ModuleCat.of ℝ (F.FullMomentumSpace d)
-  map f := Opposite.op $ Hom.toLinearMap d f
-
+variable {P : PreFeynmanRule} (F : FeynmanDiagram P) [IsFiniteDiagram F]
 
 /-!
-## Edge constraints
 
-There is a linear map from `F.FullMomentumSpace` to `F.EdgeMomentumSpace`, induced
-by the constraints at each edge.
+## Vector spaces associated with momenta in Feynman diagrams.
 
-We impose the constraint that we live in the kernal of this linear map.
+We define the vector space associated with momenta carried by half-edges,
+outflowing momenta of edges, and inflowing momenta of vertices.
 
-A similar result is true for the vertex constraints.
+We define the direct sum of the edge and vertex momentum spaces.
 
 -/
 
+/-- The type which assocaites to each half-edge a `1`-dimensional vector space.
+ Corresponding to that spanned by its momentum.  -/
+def HalfEdgeMomenta : Type :=  F.𝓱𝓔 → ℝ
+
+instance : AddCommGroup F.HalfEdgeMomenta := Pi.addCommGroup
+
+instance : Module ℝ F.HalfEdgeMomenta := Pi.module _ _ _
+
+/-- An auxillary function used to define the Euclidean inner product on `F.HalfEdgeMomenta`. -/
+def euclidInnerAux (x : F.HalfEdgeMomenta) : F.HalfEdgeMomenta →ₗ[ℝ] ℝ where
+  toFun y := ∑ i,  (x i) * (y i)
+  map_add' z y :=
+    show (∑ i, (x i) * (z i + y i)) = (∑ i, x i * z i) + ∑ i, x i * (y i) by
+      simp only [mul_add, Finset.sum_add_distrib]
+  map_smul' c y :=
+    show (∑ i, x i * (c * y i)) = c * ∑ i, x i * y i by
+      rw [Finset.mul_sum]
+      refine Finset.sum_congr rfl (fun _ _  => by ring)
+
+lemma euclidInnerAux_symm (x y : F.HalfEdgeMomenta) :
+    F.euclidInnerAux x y = F.euclidInnerAux y x := Finset.sum_congr rfl (fun _ _ => by ring)
+
+/-- The Euclidean inner product on `F.HalfEdgeMomenta`. -/
+def euclidInner : F.HalfEdgeMomenta →ₗ[ℝ] F.HalfEdgeMomenta →ₗ[ℝ] ℝ where
+  toFun x := F.euclidInnerAux x
+  map_add' x y := by
+    refine LinearMap.ext (fun z  => ?_)
+    simp only [euclidInnerAux_symm, map_add, LinearMap.add_apply]
+  map_smul' c x := by
+    refine LinearMap.ext (fun z  => ?_)
+    simp only [euclidInnerAux_symm, LinearMapClass.map_smul, smul_eq_mul, RingHom.id_apply,
+      LinearMap.smul_apply]
+
+
+/-- The type which assocaites to each ege a `1`-dimensional vector space.
+ Corresponding to that spanned by its total outflowing momentum.  -/
+def EdgeMomenta : Type := F.𝓔 → ℝ
+
+instance : AddCommGroup F.EdgeMomenta := Pi.addCommGroup
+
+instance : Module ℝ F.EdgeMomenta := Pi.module _ _ _
+
+
+/-- The type which assocaites to each ege a `1`-dimensional vector space.
+ Corresponding to that spanned by its total inflowing momentum.  -/
+def VertexMomenta : Type := F.𝓥 → ℝ
+
+instance : AddCommGroup F.VertexMomenta := Pi.addCommGroup
+
+instance : Module ℝ F.VertexMomenta := Pi.module _ _ _
+
+/-- The map from `Fin 2` to `Type` landing on `EdgeMomenta` and `VertexMomenta`. -/
+def EdgeVertexMomentaMap : Fin 2 → Type := fun i =>
+  match i with
+  | 0 =>  F.EdgeMomenta
+  | 1 =>  F.VertexMomenta
+
+instance (i : Fin 2) : AddCommGroup (EdgeVertexMomentaMap F i) :=
+  match i with
+  | 0 => instAddCommGroupEdgeMomenta F
+  | 1 => instAddCommGroupVertexMomenta F
+
+instance (i : Fin 2) : Module ℝ (EdgeVertexMomentaMap F i) :=
+  match i with
+  | 0 => instModuleRealEdgeMomenta F
+  | 1 => instModuleRealVertexMomenta F
+
+/-- The direct sum of `EdgeMomenta` and `VertexMomenta`.-/
+def EdgeVertexMomenta : Type := DirectSum (Fin 2) (EdgeVertexMomentaMap F)
+
+instance : AddCommGroup F.EdgeVertexMomenta := DirectSum.instAddCommGroup _
+
+instance : Module ℝ F.EdgeVertexMomenta := DirectSum.instModule
+
+
+/-!
+
+## Linear maps between the vector spaces.
+
+We define various maps into `F.HalfEdgeMomenta`.
+
+In particular, we define a map from `F.EdgeVertexMomenta` to `F.HalfEdgeMomenta`. This
+map represents the space orthogonal (with respect to the standard Euclidean inner product)
+to the allowed momenta of half-edges (up-to an offset determined by the
+ external momenta).
+
+The number of loops of a diagram is defined as the number of half-edges minus
+the rank of this matrix.
+
+-/
+
+/-- The linear map from `F.EdgeMomenta` to `F.HalfEdgeMomenta` induced by
+  the map `F.𝓱𝓔To𝓔.hom`. -/
+def edgeToHalfEdgeMomenta : F.EdgeMomenta →ₗ[ℝ] F.HalfEdgeMomenta where
+  toFun x := x ∘ F.𝓱𝓔To𝓔.hom
+  map_add' _ _ := by rfl
+  map_smul' _ _ := by rfl
+
+/-- The linear map from `F.VertexMomenta` to `F.HalfEdgeMomenta` induced by
+  the map `F.𝓱𝓔To𝓥.hom`. -/
+def vertexToHalfEdgeMomenta : F.VertexMomenta →ₗ[ℝ] F.HalfEdgeMomenta where
+  toFun x := x ∘ F.𝓱𝓔To𝓥.hom
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
+
+/-- The linear map from `F.EdgeVertexMomenta` to `F.HalfEdgeMomenta` induced by
+   `F.edgeToHalfEdgeMomenta` and `F.vertexToHalfEdgeMomenta`. -/
+def edgeVertexToHalfEdgeMomenta : F.EdgeVertexMomenta →ₗ[ℝ] F.HalfEdgeMomenta :=
+  DirectSum.toModule ℝ (Fin 2) F.HalfEdgeMomenta
+    (fun i => match i with | 0 => F.edgeToHalfEdgeMomenta | 1 => F.vertexToHalfEdgeMomenta)
+
+/-!
+
+## Submodules
+
+We define submodules of `F.HalfEdgeMomenta` which correspond to
+the orthogonal space to allowed momenta (up-to an offset), and the space of
+allowed momenta.
+
+-/
+
+/-- The submodule of `F.HalfEdgeMomenta` corresponding to the range of
+ `F.edgeVertexToHalfEdgeMomenta`. -/
+def orthogHalfEdgeMomenta : Submodule ℝ F.HalfEdgeMomenta :=
+  LinearMap.range F.edgeVertexToHalfEdgeMomenta
+
+/-- The submodule of `F.HalfEdgeMomenta` corresponding to the allowed momenta. -/
+def allowedHalfEdgeMomenta : Submodule ℝ F.HalfEdgeMomenta :=
+  Submodule.orthogonalBilin F.orthogHalfEdgeMomenta F.euclidInner
+
+/-!
+
+## Number of loops
+
+We define the number of loops of a Feynman diagram as the dimension of the
+allowed space of half-edge momenta.
+
+-/
+
+/-- The number of loops of a Feynman diagram. Defined as the dimension
+  of the space of allowed Half-loop momenta. -/
+noncomputable def numberOfLoops : ℕ := FiniteDimensional.finrank ℝ F.allowedHalfEdgeMomenta
+
 
 end FeynmanDiagram

From 0228cd4cf1cd45da131881872dfa928b7f2dc0cd Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 19 Jun 2024 13:07:37 -0400
Subject: [PATCH 4/5] refactor: Lint

---
 HepLean.lean                                | 1 +
 HepLean/FeynmanDiagrams/Basic.lean          | 1 -
 HepLean/FeynmanDiagrams/Instances/Phi4.lean | 3 ---
 3 files changed, 1 insertion(+), 4 deletions(-)

diff --git a/HepLean.lean b/HepLean.lean
index 18386db..ee22052 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -51,6 +51,7 @@ import HepLean.BeyondTheStandardModel.TwoHDM.Basic
 import HepLean.FeynmanDiagrams.Basic
 import HepLean.FeynmanDiagrams.Instances.ComplexScalar
 import HepLean.FeynmanDiagrams.Instances.Phi4
+import HepLean.FeynmanDiagrams.Momentum
 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 dc69ac2..d63e93a 100644
--- a/HepLean/FeynmanDiagrams/Basic.lean
+++ b/HepLean/FeynmanDiagrams/Basic.lean
@@ -16,7 +16,6 @@ import Mathlib.Data.Fintype.Perm
 import Mathlib.Combinatorics.SimpleGraph.Basic
 import Mathlib.Combinatorics.SimpleGraph.Connectivity
 import Mathlib.SetTheory.Cardinal.Basic
-import LeanCopilot
 /-!
 # Feynman diagrams
 
diff --git a/HepLean/FeynmanDiagrams/Instances/Phi4.lean b/HepLean/FeynmanDiagrams/Instances/Phi4.lean
index 9ecb20e..513abff 100644
--- a/HepLean/FeynmanDiagrams/Instances/Phi4.lean
+++ b/HepLean/FeynmanDiagrams/Instances/Phi4.lean
@@ -90,9 +90,6 @@ lemma figureEight_connected : Connected figureEight := by decide
   `#eval symmetryFactor figureEight`. -/
 lemma figureEight_symmetryFactor : symmetryFactor figureEight = 8 := by decide
 
-lemma figureEight_halfEdgeToEdgeIntMatrix :
-  figureEight.halfEdgeToEdgeIntMatrix  = !![1, 0; 1, 0 ; 0, 1; 0, 1] := by decide
-
 end Example
 
 

From 2fb2c6db81f26ee3b0a4969cec54f1648fd537ad Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 19 Jun 2024 13:17:23 -0400
Subject: [PATCH 5/5] docs: Add docs for sections to be done.

---
 HepLean/FeynmanDiagrams/Momentum.lean | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/HepLean/FeynmanDiagrams/Momentum.lean b/HepLean/FeynmanDiagrams/Momentum.lean
index 2152a68..bf68321 100644
--- a/HepLean/FeynmanDiagrams/Momentum.lean
+++ b/HepLean/FeynmanDiagrams/Momentum.lean
@@ -191,5 +191,29 @@ allowed space of half-edge momenta.
   of the space of allowed Half-loop momenta. -/
 noncomputable def numberOfLoops : ℕ := FiniteDimensional.finrank ℝ F.allowedHalfEdgeMomenta
 
+/-!
+
+## Lemmas regarding `numberOfLoops`
+
+We now give a series of lemmas which be used to help calculate the number of loops
+for specific Feynman diagrams.
+
+### TODO
+
+- Complete this section.
+
+
+-/
+
+/-!
+
+## Category theory
+
+### TODO
+
+- Complete this section.
+
+
+-/
 
 end FeynmanDiagram