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

Update CreateAnnihilateSect.lean

Browse source
This commit is contained in:
Pietro Monticone 2025-01-14 00:00:37 +01:00
parent 89baced65e
commit 8bcc691bdf
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
HepLean/PerturbationTheory/FieldStruct/CreateAnnihilateSect.lean
View file

@ -16,9 +16,9 @@ variable {𝓕 : FieldStruct}
/-- The sections in `𝓕.CreateAnnihilateStates` over a list `φs : List 𝓕.States`.
In terms of physics, given some fields `φ₁...φₙ`, the different ways one can associate
each field as a `creation` or an `annilation` operator. E.g. the number of terms
`φ₁⁰φ₂¹...φₙ⁰` `φ₁¹φ₂¹...φₙ⁰` etc. If some fields are exclusively creation or annhilation
operators at this point (e.g. ansymptotic states) this is accounted for. -/
each field as a `creation` or an `annihilation` operator. E.g. the number of terms
`φ₁⁰φ₂¹...φₙ⁰` `φ₁¹φ₂¹...φₙ⁰` etc. If some fields are exclusively creation or annihilation
operators at this point (e.g. asymptotic states) this is accounted for. -/
def CreateAnnihilateSect (φs : List 𝓕.States) : Type :=
{ψs : List 𝓕.CreateAnnihilateStates //
List.map 𝓕.createAnnihilateStatesToStates ψs = φs}
@ -87,7 +87,7 @@ def singletonEquiv {φ : 𝓕.States} : CreateAnnihilateSect [φ] ≃
simp [head]
rfl
/-- An equivalence seperating the head of a creation and annhilation section
/-- An equivalence separating the head of a creation and annihilation section
from the tail. -/
def consEquiv {φ : 𝓕.States} {φs : List 𝓕.States} : CreateAnnihilateSect (φ :: φs) ≃
𝓕.statesToCreateAnnihilateType φ × CreateAnnihilateSect φs where