From 777a878d856ef1156973c116006b257dc2d9f943 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 2 Dec 2024 16:25:14 +0000
Subject: [PATCH] refactor: Move Feynman diagrams

---
 HepLean.lean                                              | 8 ++++----
 .../{ => PertubationTheory}/FeynmanDiagrams/Basic.lean    | 0
 .../FeynmanDiagrams/Instances/ComplexScalar.lean          | 2 +-
 .../FeynmanDiagrams/Instances/Phi4.lean                   | 2 +-
 .../{ => PertubationTheory}/FeynmanDiagrams/Momentum.lean | 2 +-
 HepLean/PertubationTheory/Wick/PositionSpace.lean         | 2 +-
 HepLean/PertubationTheory/Wick/Species.lean               | 2 +-
 7 files changed, 9 insertions(+), 9 deletions(-)
 rename HepLean/{ => PertubationTheory}/FeynmanDiagrams/Basic.lean (100%)
 rename HepLean/{ => PertubationTheory}/FeynmanDiagrams/Instances/ComplexScalar.lean (97%)
 rename HepLean/{ => PertubationTheory}/FeynmanDiagrams/Instances/Phi4.lean (98%)
 rename HepLean/{ => PertubationTheory}/FeynmanDiagrams/Momentum.lean (99%)

diff --git a/HepLean.lean b/HepLean.lean
index 22e45b1..84d7f06 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -51,10 +51,6 @@ import HepLean.BeyondTheStandardModel.PatiSalam.Basic
 import HepLean.BeyondTheStandardModel.Spin10.Basic
 import HepLean.BeyondTheStandardModel.TwoHDM.Basic
 import HepLean.BeyondTheStandardModel.TwoHDM.GaugeOrbits
-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
@@ -111,6 +107,10 @@ import HepLean.Meta.AllFilePaths
 import HepLean.Meta.Basic
 import HepLean.Meta.Informal
 import HepLean.Meta.TransverseTactics
+import HepLean.PertubationTheory.FeynmanDiagrams.Basic
+import HepLean.PertubationTheory.FeynmanDiagrams.Instances.ComplexScalar
+import HepLean.PertubationTheory.FeynmanDiagrams.Instances.Phi4
+import HepLean.PertubationTheory.FeynmanDiagrams.Momentum
 import HepLean.PertubationTheory.Wick.Algebra
 import HepLean.PertubationTheory.Wick.Contract
 import HepLean.PertubationTheory.Wick.MomentumSpace
diff --git a/HepLean/FeynmanDiagrams/Basic.lean b/HepLean/PertubationTheory/FeynmanDiagrams/Basic.lean
similarity index 100%
rename from HepLean/FeynmanDiagrams/Basic.lean
rename to HepLean/PertubationTheory/FeynmanDiagrams/Basic.lean
diff --git a/HepLean/FeynmanDiagrams/Instances/ComplexScalar.lean b/HepLean/PertubationTheory/FeynmanDiagrams/Instances/ComplexScalar.lean
similarity index 97%
rename from HepLean/FeynmanDiagrams/Instances/ComplexScalar.lean
rename to HepLean/PertubationTheory/FeynmanDiagrams/Instances/ComplexScalar.lean
index 50a3529..1efdf32 100644
--- a/HepLean/FeynmanDiagrams/Instances/ComplexScalar.lean
+++ b/HepLean/PertubationTheory/FeynmanDiagrams/Instances/ComplexScalar.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.FeynmanDiagrams.Basic
+import HepLean.PertubationTheory.FeynmanDiagrams.Basic
 /-!
 # Feynman diagrams in a complex scalar field theory
 
diff --git a/HepLean/FeynmanDiagrams/Instances/Phi4.lean b/HepLean/PertubationTheory/FeynmanDiagrams/Instances/Phi4.lean
similarity index 98%
rename from HepLean/FeynmanDiagrams/Instances/Phi4.lean
rename to HepLean/PertubationTheory/FeynmanDiagrams/Instances/Phi4.lean
index 8f9df3f..6bd0052 100644
--- a/HepLean/FeynmanDiagrams/Instances/Phi4.lean
+++ b/HepLean/PertubationTheory/FeynmanDiagrams/Instances/Phi4.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.FeynmanDiagrams.Basic
+import HepLean.PertubationTheory.FeynmanDiagrams.Basic
 /-!
 # Feynman diagrams in Phi^4 theory
 
diff --git a/HepLean/FeynmanDiagrams/Momentum.lean b/HepLean/PertubationTheory/FeynmanDiagrams/Momentum.lean
similarity index 99%
rename from HepLean/FeynmanDiagrams/Momentum.lean
rename to HepLean/PertubationTheory/FeynmanDiagrams/Momentum.lean
index 705d3fb..c9044bf 100644
--- a/HepLean/FeynmanDiagrams/Momentum.lean
+++ b/HepLean/PertubationTheory/FeynmanDiagrams/Momentum.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.FeynmanDiagrams.Basic
+import HepLean.PertubationTheory.FeynmanDiagrams.Basic
 import Mathlib.Data.Real.Basic
 import Mathlib.Algebra.DirectSum.Module
 import Mathlib.LinearAlgebra.SesquilinearForm
diff --git a/HepLean/PertubationTheory/Wick/PositionSpace.lean b/HepLean/PertubationTheory/Wick/PositionSpace.lean
index e3a5245..57c6821 100644
--- a/HepLean/PertubationTheory/Wick/PositionSpace.lean
+++ b/HepLean/PertubationTheory/Wick/PositionSpace.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.FeynmanDiagrams.Basic
+import HepLean.PertubationTheory.FeynmanDiagrams.Basic
 import HepLean.Meta.Informal
 /-!
 
diff --git a/HepLean/PertubationTheory/Wick/Species.lean b/HepLean/PertubationTheory/Wick/Species.lean
index 9f9450c..da9ba76 100644
--- a/HepLean/PertubationTheory/Wick/Species.lean
+++ b/HepLean/PertubationTheory/Wick/Species.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.FeynmanDiagrams.Basic
+import HepLean.PertubationTheory.FeynmanDiagrams.Basic
 import HepLean.Meta.Informal
 /-!