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] 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