From 626bc38c614f07a5911e021024f3d05271be924f Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 2 Dec 2024 07:18:42 +0000
Subject: [PATCH] feat: Update time ordering

---
 HepLean/FeynmanDiagrams/Wick/Algebra.lean | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/HepLean/FeynmanDiagrams/Wick/Algebra.lean b/HepLean/FeynmanDiagrams/Wick/Algebra.lean
index 0460774..581cc7b 100644
--- a/HepLean/FeynmanDiagrams/Wick/Algebra.lean
+++ b/HepLean/FeynmanDiagrams/Wick/Algebra.lean
@@ -59,7 +59,16 @@ informal_definition toWickAlgebra where
 informal_definition timeOrder 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."
+    determined by the Koszul sign factor.
+
+    If two fields have the same time, then their order is preserved e.g.
+    T(ψ₁(t)ψ₂(t)) = ψ₁(t)ψ₂(t)
+    and
+    T(ψ₂(t)ψ₁(t)) = ψ₂(t)ψ₁(t).
+    This allows us to make sense of the construction in e.g.
+    https://www.physics.purdue.edu/~clarkt/Courses/Physics662/ps/qftch32.pdf
+    which permits normal-ordering within time-ordering.
+    "
   deps :≈ [``WickAlgebra, ``WickMonomial]
 
 informal_definition normalOrder where