feat: More informal details about Wick contract

HepLean/PerturbationTheory/FeynmanDiagrams/Light.lean

@@ -3,6 +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.PerturbationTheory.Wick.Contract
 import HepLean.PerturbationTheory.Wick.Species
 /-!
 
@@ -21,8 +22,12 @@ informal_definition FeynmanDiagram where
     Let S be a WickSpecies
     A Feynman diagram contains the following data:
     - A type of vertices 𝓥 → S.𝓯 ⊕ S.𝓘.
-    - A type of edges 𝓔 → S.𝓕.
-    - A type of half-edges 𝓱𝓔 → 𝓔 × 𝓥 × S.𝓯.
+    - A type of edges ed : 𝓔 → S.𝓕.
+    - A type of half-edges 𝓱𝓔 with maps `e : 𝓱𝓔 → 𝓔`, `v : 𝓱𝓔 → 𝓥` and `f : 𝓱𝓔 → S.𝓯`
     Subject to the following conditions:
-    ...
-  "
+    - `𝓱𝓔` is a double cover of `𝓔` through `e`. That is,
+      for each edge `x : 𝓔` there exists an isomorphism between `i : Fin 2 → e⁻¹ 𝓱𝓔 {x}`.
+    - These isomorphisms must satisfy `⟦f(i(0))⟧ = ⟦f(i(1))⟧ = ed(e)` and `f(i(0)) = S.ξ (f(i(1)))`.
+    - For each vertex `ver : 𝓥` there exists an isomorphism between the object (roughly)
+      `(𝓘Fields v).2` and the pullback of `v` along `ver`."
+  deps :≈ [``Wick.Species]

HepLean/PerturbationTheory/Wick/Algebra.lean

@@ -124,7 +124,7 @@ informal_lemma timeOrder_pair where
 
 informal_definition WickMap where
   math :≈ "A linear map `vev` from the Wick algebra `A` to the underlying field such that
-    `vev(...ψd(t)) = 0` and `vev(ψc(t)...) = 0`."
+     `vev(...ψd(t)) = 0` and `vev(ψc(t)...) = 0`."
   physics :≈ "An abstraction of the notion of a vacuum expectation value, containing
     the necessary properties for lots of theorems to hold."
   deps :≈ [``WickAlgebra, ``WickMonomial]

HepLean/PerturbationTheory/Wick/Species.lean

@@ -51,12 +51,6 @@ informal_definition 𝓕 where
   physics :≈ "The different types of fields present in a theory."
   deps :≈ [``Species]
 
-informal_definition 𝓕ToOver𝓯 where
-  math :≈ "The map from `S.𝓕` to functions `Fin 2 → S.𝓯` with this function
-    landing on orbits.
-    This may require an order on `S.𝓯`."
-  deps :≈ [``Species]
-
 end Species
 
 end Wick