From 79cba76a2f7fa4e27b0684604b174c8469410d77 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 2 Dec 2024 06:00:59 +0000
Subject: [PATCH] docs: Improve some documentation

---
 HepLean/FeynmanDiagrams/Wick/Algebra.lean | 10 ++---
 HepLean/FeynmanDiagrams/Wick/Species.lean |  5 ++-
 HepLean/FeynmanDiagrams/Wick/String.lean  | 46 ++++++++++++-----------
 3 files changed, 33 insertions(+), 28 deletions(-)

diff --git a/HepLean/FeynmanDiagrams/Wick/Algebra.lean b/HepLean/FeynmanDiagrams/Wick/Algebra.lean
index d4a7f076..0460774f 100644
--- a/HepLean/FeynmanDiagrams/Wick/Algebra.lean
+++ b/HepLean/FeynmanDiagrams/Wick/Algebra.lean
@@ -34,10 +34,10 @@ informal_definition WickAlgebra where
     A structure with the following data:
     - A ℤ₂-graded algebra A.
     - A map from `ψ : 𝓔 × SpaceTime → A` where 𝓔 are field colors.
-    - A map `ψ₊ : 𝓔 × SpaceTime → A`.
-    - A map `ψ₋ : 𝓔 × SpaceTime → A`.
+    - A map `ψc : 𝓔 × SpaceTime → A`.
+    - A map `ψd : 𝓔 × SpaceTime → A`.
     Subject to the conditions:
-    - The sum of `ψ0` and `ψ1` is `ψ`.
+    - The sum of `ψc` and `ψd` is `ψ`.
     - Two fields super-commute if there colors are not dual to each other.
     - The super-commutator of two fields is always in the
       center of the algebra. "
@@ -65,8 +65,8 @@ informal_definition timeOrder where
 informal_definition normalOrder where
   math :≈ "A function from WickMonomial to WickAlgebra which takes a monomial and
     returns the element in `WickAlgebra` defined as follows
-    - The ψ₊ fields are move to the right.
-    - The ψ₋ fields are moved to the left.
+    - The ψd fields are move to the right.
+    - The ψc fields are moved to the left.
     - Othewise the order of the fields is preserved."
   ref :≈ "https://www.imperial.ac.uk/media/imperial-college/research-centres-and-groups/theoretical-physics/msc/current/qft/handouts/qftwickstheorem.pdf"
   deps :≈ [``WickAlgebra, ``WickMonomial]
diff --git a/HepLean/FeynmanDiagrams/Wick/Species.lean b/HepLean/FeynmanDiagrams/Wick/Species.lean
index d74ea93f..9f9450c7 100644
--- a/HepLean/FeynmanDiagrams/Wick/Species.lean
+++ b/HepLean/FeynmanDiagrams/Wick/Species.lean
@@ -22,7 +22,8 @@ namespace Wick
 /-- The basic structure needed to write down Wick contractions for a theory and
   calculate the corresponding Feynman diagrams.
 
-  WARNING: This definition is not yet complete. -/
+  WARNING: This definition is not yet complete.
+   -/
 structure Species where
   /-- The color of Field operators which appear in a theory. -/
   𝓕 : Type
@@ -32,7 +33,7 @@ structure Species where
   ξ_involutive : Function.Involutive ξ
   /-- The color of vertices which appear in a theory. -/
   𝓥 : Type
-  /-- The number of edges each vertex corresponds to. -/
+  /-- The edges each vertex corresponds to. -/
   𝓥Fields : 𝓥 → Σ n, Fin n → 𝓕
 
 end Wick
diff --git a/HepLean/FeynmanDiagrams/Wick/String.lean b/HepLean/FeynmanDiagrams/Wick/String.lean
index cc992940..50e96ae6 100644
--- a/HepLean/FeynmanDiagrams/Wick/String.lean
+++ b/HepLean/FeynmanDiagrams/Wick/String.lean
@@ -133,41 +133,45 @@ def size {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔} {no : 
   | endOutgoing w => size w + 1
 
 /-- The number of vertices in a Wick string. This does NOT include external vertices. -/
-def numVertex {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔} {no : ℕ} {o : Fin no → 𝓔}
+def numIntVertex {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔} {no : ℕ} {o : Fin no → 𝓔}
     {f : WickStringLast} : WickString i c o f → ℕ := fun
   | empty => 0
-  | incoming w e => numVertex w
-  | endIncoming w => numVertex w
-  | vertex w v => numVertex w + 1
-  | endVertex w => numVertex w
-  | outgoing w e => numVertex w
-  | endOutgoing w => numVertex w
+  | incoming w e => numIntVertex w
+  | endIncoming w => numIntVertex w
+  | vertex w v => numIntVertex w + 1
+  | endVertex w => numIntVertex w
+  | outgoing w e => numIntVertex w
+  | endOutgoing w => numIntVertex w
 
 /-- The vertices present in a Wick string. This does NOT include external vertices. -/
-def vertices {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔} {no : ℕ} {o : Fin no → 𝓔}
-    {f : WickStringLast} : (w : WickString i c o f) → Fin w.numVertex → 𝓥 := fun
+def intVertex {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔} {no : ℕ} {o : Fin no → 𝓔}
+    {f : WickStringLast} : (w : WickString i c o f) → Fin w.numIntVertex → 𝓥 := fun
   | empty => Fin.elim0
-  | incoming w e => vertices w
-  | endIncoming w => vertices w
-  | vertex w v => Fin.cons v (vertices w)
-  | endVertex w => vertices w
-  | outgoing w e => vertices w
-  | endOutgoing w => vertices w
-
-informal_definition fieldToVertex where
-  math :≈ "A function which takes a field and returns the vertex it is associated with.
-    This is a map from `Fin n` to `Fin w.numVertex`"
+  | incoming w e => intVertex w
+  | endIncoming w => intVertex w
+  | vertex w v => Fin.cons v (intVertex w)
+  | endVertex w => intVertex w
+  | outgoing w e => intVertex w
+  | endOutgoing w => intVertex w
+
+informal_definition intExtVertex where
+  math :≈ "The vertices present in a Wick string, including external vertices."
+  deps :≈ [``WickString]
+
+informal_definition fieldToIntExtVertex where
+  math :≈ "A function which takes a field and returns the internal or
+    external vertex it is associated with."
   deps :≈ [``WickString]
 
 informal_definition exponentialPrefactor where
   math :≈ "The combinatorical prefactor from the expansion of the
     exponential associated with a Wick string."
-  deps :≈ [``vertices, ``WickString]
+  deps :≈ [``intVertex, ``WickString]
 
 informal_definition vertexPrefactor where
   math :≈ "The prefactor arising from the coefficent of vertices in the
     Lagrangian. This should not take account of the exponential prefactor."
-  deps :≈ [``vertices, ``WickString]
+  deps :≈ [``intVertex, ``WickString]
 
 informal_definition minNoLoops where
   math :≈ "The minimum number of loops a Feynman diagram based on a given Wick string can have.