feat: Informal results for wick algebras

HepLean/FeynmanDiagrams/Wick/Algebra.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.FeynmanDiagrams.Basic
+import HepLean.Meta.Informal
 /-!
 
 # Operator algebra
@@ -28,4 +29,53 @@ open CategoryTheory
 open FeynmanDiagram
 open PreFeynmanRule
 
+informal_definition WickAlgebra where
+  math :≈ "
+    Modifications of this may be needed.
+    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`.
+    Subject to the conditions:
+    - The sum of `ψ0` and `ψ1` 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. "
+  ref :≈ "https://physics.stackexchange.com/questions/24157/"
+
+informal_definition WickMonomial where
+  math :≈ "The type of elements of the Wick algebra which is a product of fields."
+  deps :≈ [``WickAlgebra]
+
+namespace WickMonomial
+
+informal_definition toWickAlgebra where
+  math :≈ "A function from WickMonomial to WickAlgebra which takes a monomial and
+    returns the product of the fields in the monomial."
+  deps :≈ [``WickAlgebra, ``WickMonomial]
+
+informal_definition timeOrdering where
+  math :≈ "A function from WickMonomial to WickAlgebra which takes a monomial and
+    returns the monomial with the fields time ordered, with the correct sign
+    determined by the Koszul sign factor."
+  deps :≈ [``WickAlgebra, ``WickMonomial]
+
+informal_definition normalOrdering 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.
+    - 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]
+
+end WickMonomial
+
+informal_definition contraction where
+  math :≈ "Given two `i j : 𝓔 × SpaceTime`, the element of WickAlgebra
+    defined by subtracting the normal ordering of `ψ i ψ j` from the time-ordering of
+    `ψ i ψ j`."
+  deps :≈ [``WickAlgebra, ``WickMonomial]
+
 end TwoComplexScalar