From 4e097b12f8858f76ef013011fba2e5f7284b9ec3 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 3 Dec 2024 07:03:14 +0000
Subject: [PATCH] refactor: Improve WickAlgebra

---
 HepLean/PerturbationTheory/Wick/Algebra.lean | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/HepLean/PerturbationTheory/Wick/Algebra.lean b/HepLean/PerturbationTheory/Wick/Algebra.lean
index 00a0ec8..f2fc4aa 100644
--- a/HepLean/PerturbationTheory/Wick/Algebra.lean
+++ b/HepLean/PerturbationTheory/Wick/Algebra.lean
@@ -21,6 +21,7 @@ We will formally define the operator ring, in terms of the fields present in the
 - Ryan Thorngren (https://physics.stackexchange.com/users/10336/ryan-thorngren), Fermions,
   different species and (anti-)commutation rules, URL (version: 2019-02-20) :
   https://physics.stackexchange.com/q/461929
+- Tong, https://www.damtp.cam.ac.uk/user/tong/qft/qft.pdf
 -/
 
 namespace Wick
@@ -30,9 +31,7 @@ open PreFeynmanRule
 
 informal_definition WickAlgebra where
   math :≈ "
-    Modifications of this may be needed, in particular
-    need to add asympotic states.
-
+    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.
@@ -40,9 +39,14 @@ informal_definition WickAlgebra where
     - A map `ψd : 𝓔 × SpaceTime → A`.
     Subject to the conditions:
     - The sum of `ψc` and `ψd` is `ψ`.
+    - All maps land on homogeneous elements.
     - 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. "
+      center of the algebra.
+    Asympotic states:
+    - `φc : 𝓔 × SpaceTime → A`. The creation asympotic state (incoming).
+    - `φd : 𝓔 × SpaceTime → A`. The destruction asympotic state (outgoing).
+      "
   physics :≈ "This is defined to be an
     abstraction of the notion of an operator algebra."
   ref :≈ "https://physics.stackexchange.com/questions/24157/"