DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat: Update time ordering

Browse source
This commit is contained in:
jstoobysmith 2024-12-02 07:18:42 +00:00
parent 75d6e3618c
commit 626bc38c61
1 changed files with 10 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

11
HepLean/FeynmanDiagrams/Wick/Algebra.lean
View file

@ -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