From 2fcafb17962ccfbfacaf8eba99e7520c81776aee Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 21 Jan 2025 10:23:05 +0000 Subject: [PATCH] Docs: Documentation related to Wick contraction (#287) * refactor: Fix field struct defn. * rename: FieldStruct to FieldSpecification * feat: Add examples of field specifications * docs: Slight improvement of module docs * refactor: Rename CreateAnnihilate * docs: Algebras * Update CrAnStates.lean --- HepLean.lean | 2 +- .../Algebras/StateAlgebra/Basic.lean | 12 ++++-- .../FieldSpecification/CrAnSection.lean | 37 ++++++++----------- ...{CreateAnnihilate.lean => CrAnStates.lean} | 24 +++++++++++- .../FieldStatistics/ExchangeSign.lean | 20 ++++++++-- 5 files changed, 64 insertions(+), 31 deletions(-) rename HepLean/PerturbationTheory/FieldSpecification/{CreateAnnihilate.lean => CrAnStates.lean} (75%) diff --git a/HepLean.lean b/HepLean.lean index 089134f0..e6509a71 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -133,7 +133,7 @@ import HepLean.PerturbationTheory.FeynmanDiagrams.Instances.Phi4 import HepLean.PerturbationTheory.FeynmanDiagrams.Momentum import HepLean.PerturbationTheory.FieldSpecification.Basic import HepLean.PerturbationTheory.FieldSpecification.CrAnSection -import HepLean.PerturbationTheory.FieldSpecification.CreateAnnihilate +import HepLean.PerturbationTheory.FieldSpecification.CrAnStates import HepLean.PerturbationTheory.FieldSpecification.Examples import HepLean.PerturbationTheory.FieldSpecification.Filters import HepLean.PerturbationTheory.FieldSpecification.NormalOrder diff --git a/HepLean/PerturbationTheory/Algebras/StateAlgebra/Basic.lean b/HepLean/PerturbationTheory/Algebras/StateAlgebra/Basic.lean index a65b7cda..c8a3d8a4 100644 --- a/HepLean/PerturbationTheory/Algebras/StateAlgebra/Basic.lean +++ b/HepLean/PerturbationTheory/Algebras/StateAlgebra/Basic.lean @@ -3,13 +3,19 @@ Copyright (c) 2025 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.FieldSpecification.CreateAnnihilate +import HepLean.PerturbationTheory.FieldSpecification.CrAnStates /-! # State algebra -We define the state algebra of a field structure to be the free algebra -generated by the states. +From the states associated with a field specification we can form a free algebra +generated by these states. We call this the state algebra, or the state free-algebra. + +The state free-algebra has minimal assumptions, yet can be used to concretely define time-ordering. + +In +`HepLean.PerturbationTheory.Algebras.CrAnAlgebra.Basic` +we defined a related free-algebra generated by creation and annihilation states. -/ diff --git a/HepLean/PerturbationTheory/FieldSpecification/CrAnSection.lean b/HepLean/PerturbationTheory/FieldSpecification/CrAnSection.lean index dd6502ea..b66ed1a7 100644 --- a/HepLean/PerturbationTheory/FieldSpecification/CrAnSection.lean +++ b/HepLean/PerturbationTheory/FieldSpecification/CrAnSection.lean @@ -3,32 +3,28 @@ Copyright (c) 2025 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.FieldSpecification.CreateAnnihilate +import HepLean.PerturbationTheory.FieldSpecification.CrAnStates /-! # Creation and annihlation sections -This module defines creation and annihilation sections, which represent different ways to associate -fields with creation or annihilation operators. +In the module +`HepLean.PerturbationTheory.FieldSpecification.Basic` +we defined states for a field specification, and in the module +`HepLean.PerturbationTheory.FieldStatistics.CrAnStates` +we defined a refinement of states called `CrAnStates` which distinquishes between the +creation and annihilation components of states. +There exists, in particular, a map from `CrAnStates` to `States` called `crAnStatesToStates`. -## Main definitions +Given a list of `States`, `φs`, in this module we define a section of `φs` to be a list of +`CrAnStates`, `ψs`, such that under the map `crAnStatesToStates`, `ψs` is mapped to `φs`. +That is to say, the states underlying `ψs` are the states in `φs`. +We denote these sections as `CrAnSection φs`. -- `CrAnSection φs` : Represents sections in `𝓕.CrAnStates` over a list of states `φs`. - Given fields `φ₁...φₙ`, this captures all possible ways to assign each field as either a creation - or annihilation operator. +Looking forward the main consequence of this definition is the lemma +`FieldSpecification.CrAnAlgebra.ofStateList_sum`. -- `head`, `tail` : Access the first element and remaining elements of a section - -- `cons` : Constructs a new section by prepending a creation/annihilation state - -- Various equivalences: - * `nilEquiv` : Empty sections - * `singletonEquiv` : Sections over single elements - * `consEquiv` : Separates head and tail - * `appendEquiv` : Splits sections at a given point - -All sections form finite types and support operations like taking/dropping elements and -concatenation while preserving the relationship between states and their operator assignments. +In this module we define various properties of `CrAnSection`. -/ @@ -41,8 +37,7 @@ variable {𝓕 : FieldSpecification} `φ₁⁰φ₂¹...φₙ⁰` `φ₁¹φ₂¹...φₙ⁰` etc. If some fields are exclusively creation or annhilation operators at this point (e.g. ansymptotic states) this is accounted for. -/ def CrAnSection (φs : List 𝓕.States) : Type := - {ψs : List 𝓕.CrAnStates // - List.map 𝓕.crAnStatesToStates ψs = φs} + {ψs : List 𝓕.CrAnStates // ψs.map 𝓕.crAnStatesToStates = φs} -- Π i, 𝓕.statesToCreateAnnihilateType (φs.get i) namespace CrAnSection diff --git a/HepLean/PerturbationTheory/FieldSpecification/CreateAnnihilate.lean b/HepLean/PerturbationTheory/FieldSpecification/CrAnStates.lean similarity index 75% rename from HepLean/PerturbationTheory/FieldSpecification/CreateAnnihilate.lean rename to HepLean/PerturbationTheory/FieldSpecification/CrAnStates.lean index b9939b2a..dae35ee2 100644 --- a/HepLean/PerturbationTheory/FieldSpecification/CreateAnnihilate.lean +++ b/HepLean/PerturbationTheory/FieldSpecification/CrAnStates.lean @@ -7,10 +7,30 @@ import HepLean.PerturbationTheory.FieldSpecification.Basic import HepLean.PerturbationTheory.CreateAnnihilate /-! -# Creation and annihlation parts of fields +# Creation and annihilation states --/ +Called `CrAnStates` for short here. + +Given a field specification, in addition to defining states +(see: `HepLean.PerturbationTheory.FieldSpecification.Basic`), +we can also define creation and annihilation states. +These are similar to states but come with an additional specification of whether they correspond to +creation or annihilation operators. + +In particular we have the following creation and annihilation states for each field: +- Negative asymptotic states - with the implicit specification that it is a creation state. +- Position states with a creation specification. +- Position states with an annihilation specification. +- Positive asymptotic states - with the implicit specification that it is an annihilation state. +In this module in addition to defining `CrAnStates` we also define some maps: +- The map `crAnStatesToStates` takes a `CrAnStates` to its state in `States`. +- The map `crAnStatesToCreateAnnihilate` takes a `CrAnStates` to its corresponding +`CreateAnnihilate` value. +- The map `crAnStatistics` takes a `CrAnStates` to its corresponding `FieldStatistic` +(bosonic or fermionic). + +-/ namespace FieldSpecification variable (𝓕 : FieldSpecification) diff --git a/HepLean/PerturbationTheory/FieldStatistics/ExchangeSign.lean b/HepLean/PerturbationTheory/FieldStatistics/ExchangeSign.lean index 621f784e..dfd91dff 100644 --- a/HepLean/PerturbationTheory/FieldStatistics/ExchangeSign.lean +++ b/HepLean/PerturbationTheory/FieldStatistics/ExchangeSign.lean @@ -8,6 +8,16 @@ import HepLean.PerturbationTheory.FieldStatistics.Basic # Exchange sign for field statistics +Suppose we have two fields `φ` and `ψ`, and the term `φψ`, if we swap them +`ψφ`, we may pick up a sign. This sign is called the exchange sign. +This sign is `-1` if both fields `ψ` and `φ` are fermionic and `1` otherwise. + +In this module we define the exchange sign for general field statistics, +and prove some properties of it. Importantly: +- It is symmetric `exchangeSign_symm`. +- When multiplied with itself it is `1` `exchangeSign_mul_self`. +- It is a cocycle `exchangeSign_cocycle`. + -/ namespace FieldStatistic @@ -47,16 +57,17 @@ def exchangeSign : FieldStatistic →* FieldStatistic →* ℂ where Defined to be `-1` if both field statistics are `fermionic` and `1` otherwise. -/ scoped[FieldStatistic] notation "𝓢(" a "," b ")" => exchangeSign a b +/-- The exchange sign is symmetric. -/ +lemma exchangeSign_symm (a b : FieldStatistic) : 𝓢(a, b) = 𝓢(b, a) := by + fin_cases a <;> fin_cases b <;> rfl + @[simp] lemma exchangeSign_bosonic (a : FieldStatistic) : 𝓢(a, bosonic) = 1 := by fin_cases a <;> rfl @[simp] lemma bosonic_exchangeSign (a : FieldStatistic) : 𝓢(bosonic, a) = 1 := by - fin_cases a <;> rfl - -lemma exchangeSign_symm (a b : FieldStatistic) : 𝓢(a, b) = 𝓢(b, a) := by - fin_cases a <;> fin_cases b <;> rfl + rw [exchangeSign_symm, exchangeSign_bosonic] lemma exchangeSign_eq_if (a b : FieldStatistic) : 𝓢(a, b) = if a = fermionic ∧ b = fermionic then - 1 else 1 := by @@ -75,6 +86,7 @@ lemma exchangeSign_ofList_cons (a : FieldStatistic) 𝓢(a, ofList s (φ :: φs)) = 𝓢(a, s φ) * 𝓢(a, ofList s φs) := by rw [ofList_cons_eq_mul, map_mul] +/-- The exchange sign is a cocycle. -/ lemma exchangeSign_cocycle (a b c : FieldStatistic) : 𝓢(a, b * c) * 𝓢(b, c) = 𝓢(a, b) * 𝓢(a * b, c) := by fin_cases a <;> fin_cases b <;> fin_cases c <;> simp