Imports
/-
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
-/
module
public import Physlib.QFT.PerturbationTheory.FieldSpecification.CrAnSectionCreation and annihilation free-algebra
This module defines the creation and annihilation algebra for a field structure.
The creation and annihilation algebra extends from the state algebra by adding information about whether a state is a creation or annihilation operator.
The algebra is spanned by lists of creation/annihilation states.
The main structures defined in this module are:
FieldOpFreeAlgebra - The creation and annihilation algebra
ofCrAnOpF - Maps a creation/annihilation state to the algebra
ofCrAnListF - Maps a list of creation/annihilation states to the algebra
ofFieldOpF - Maps a state to a sum of creation and annihilation operators
crPartF - The creation part of a state in the algebra
anPartF - The annihilation part of a state in the algebra
superCommuteF - The super commutator on the algebra
The key lemmas show how these operators interact, particularly focusing on the super commutation relations between creation and annihilation operators.
@[expose] public section
For a field specification 𝓕, the algebra 𝓕.FieldOpFreeAlgebra is
the free algebra generated by 𝓕.CrAnFieldOp.
abbrev FieldOpFreeAlgebra (𝓕 : FieldSpecification) : Type := FreeAlgebra ℂ 𝓕.CrAnFieldOp
For a field specification 𝓕, and a element φ of 𝓕.CrAnFieldOp,
ofCrAnOpF φ is defined as the element of 𝓕.FieldOpFreeAlgebra formed by φ.
def ofCrAnOpF (φ : 𝓕.CrAnFieldOp) : FieldOpFreeAlgebra 𝓕 :=
FreeAlgebra.ι ℂ φ
The algebra 𝓕.FieldOpFreeAlgebra satisfies the universal property that for any other algebra
A (e.g. the operator algebra of the theory) with a map f : 𝓕.CrAnFieldOp → A (e.g.
the inclusion of the creation and annihilation parts of field operators into the
operator algebra) there is a unique algebra map g : 𝓕.FieldOpFreeAlgebra → A
such that g ∘ ofCrAnOpF = f.
The unique g is given by FreeAlgebra.lift ℂ f.
lemma universality {A : Type} [Semiring A] [Algebra ℂ A] (f : 𝓕.CrAnFieldOp → A) :
∃! g : FieldOpFreeAlgebra 𝓕 →ₐ[ℂ] A, g ∘ ofCrAnOpF = f := 𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → A⊢ ∃! g, ⇑g ∘ ofCrAnOpF = f
𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → A⊢ (fun g => ⇑g ∘ ofCrAnOpF = f) ((FreeAlgebra.lift ℂ) f) ∧
∀ (y : 𝓕.FieldOpFreeAlgebra →ₐ[ℂ] A), (fun g => ⇑g ∘ ofCrAnOpF = f) y → y = (FreeAlgebra.lift ℂ) f
𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → A⊢ (fun g => ⇑g ∘ ofCrAnOpF = f) ((FreeAlgebra.lift ℂ) f)𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → A⊢ ∀ (y : 𝓕.FieldOpFreeAlgebra →ₐ[ℂ] A), (fun g => ⇑g ∘ ofCrAnOpF = f) y → y = (FreeAlgebra.lift ℂ) f
𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → A⊢ (fun g => ⇑g ∘ ofCrAnOpF = f) ((FreeAlgebra.lift ℂ) f) 𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ax:𝓕.CrAnFieldOp⊢ (⇑((FreeAlgebra.lift ℂ) f) ∘ ofCrAnOpF) x = f x
All goals completed! 🐙
𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → A⊢ ∀ (y : 𝓕.FieldOpFreeAlgebra →ₐ[ℂ] A), (fun g => ⇑g ∘ ofCrAnOpF = f) y → y = (FreeAlgebra.lift ℂ) f 𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ag:𝓕.FieldOpFreeAlgebra →ₐ[ℂ] Ahg:⇑g ∘ ofCrAnOpF = f⊢ g = (FreeAlgebra.lift ℂ) f
𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ag:𝓕.FieldOpFreeAlgebra →ₐ[ℂ] Ahg:⇑g ∘ ofCrAnOpF = fx:𝓕.CrAnFieldOp⊢ (⇑g ∘ FreeAlgebra.ι ℂ) x = (⇑((FreeAlgebra.lift ℂ) f) ∘ FreeAlgebra.ι ℂ) x
𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ag:𝓕.FieldOpFreeAlgebra →ₐ[ℂ] Ahg:⇑g ∘ ofCrAnOpF = fx:𝓕.CrAnFieldOph1:(⇑g ∘ ofCrAnOpF) x = f x⊢ (⇑g ∘ FreeAlgebra.ι ℂ) x = (⇑((FreeAlgebra.lift ℂ) f) ∘ FreeAlgebra.ι ℂ) x
𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ag:𝓕.FieldOpFreeAlgebra →ₐ[ℂ] Ahg:⇑g ∘ ofCrAnOpF = fx:𝓕.CrAnFieldOph1:g (ofCrAnOpF x) = f x⊢ g (FreeAlgebra.ι ℂ x) = f x
All goals completed! 🐙
For a field specification 𝓕, and a list φs of 𝓕.CrAnFieldOp,
ofCrAnListF φs is defined as the element of 𝓕.FieldOpFreeAlgebra
obtained by the product of ofCrAnListF φ for each φ in φs.
For example ofCrAnListF [φ₁, φ₂, φ₃] = ofCrAnOpF φ₁ * ofCrAnOpF φ₂ * ofCrAnOpF φ₃.
The set of all ofCrAnListF φs forms a basis of FieldOpFreeAlgebra 𝓕.
def ofCrAnListF (φs : List 𝓕.CrAnFieldOp) : FieldOpFreeAlgebra 𝓕 := (List.map ofCrAnOpF φs).prod@[simp]
lemma ofCrAnListF_nil : ofCrAnListF ([] : List 𝓕.CrAnFieldOp) = 1 := rfllemma ofCrAnListF_cons (φ : 𝓕.CrAnFieldOp) (φs : List 𝓕.CrAnFieldOp) :
ofCrAnListF (φ :: φs) = ofCrAnOpF φ * ofCrAnListF φs := rfllemma ofCrAnListF_append (φs φs' : List 𝓕.CrAnFieldOp) :
ofCrAnListF (φs ++ φs') = ofCrAnListF φs * ofCrAnListF φs' := 𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp⊢ ofCrAnListF (φs ++ φs') = ofCrAnListF φs * ofCrAnListF φs'
All goals completed! 🐙lemma ofCrAnListF_singleton (φ : 𝓕.CrAnFieldOp) :
ofCrAnListF [φ] = ofCrAnOpF φ := 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOp⊢ ofCrAnListF [φ] = ofCrAnOpF φ All goals completed! 🐙
For a field specification 𝓕, and an element φ of 𝓕.FieldOp,
ofFieldOpF φ is the element of 𝓕.FieldOpFreeAlgebra formed by summing over
ofCrAnOpF of the
creation and annihilation parts of φ.
For example, for φ an incoming asymptotic field operator we get
ofCrAnOpF ⟨φ, ()⟩, and for φ a
position field operator we get ofCrAnOpF ⟨φ, .create⟩ + ofCrAnOpF ⟨φ, .annihilate⟩.
def ofFieldOpF (φ : 𝓕.FieldOp) : FieldOpFreeAlgebra 𝓕 :=
∑ (i : 𝓕.fieldOpToCrAnType φ), ofCrAnOpF ⟨φ, i⟩
For a field specification 𝓕, and a list φs of 𝓕.FieldOp,
𝓕.ofFieldOpListF φs is defined as the element of 𝓕.FieldOpFreeAlgebra
obtained by the product of ofFieldOpF φ for each φ in φs.
For example ofFieldOpListF [φ₁, φ₂, φ₃] = ofFieldOpF φ₁ * ofFieldOpF φ₂ * ofFieldOpF φ₃.
def ofFieldOpListF (φs : List 𝓕.FieldOp) : FieldOpFreeAlgebra 𝓕 := (List.map ofFieldOpF φs).prod
Coercion from List 𝓕.FieldOp to FieldOpFreeAlgebra 𝓕 through ofFieldOpListF.
instance : Coe (List 𝓕.FieldOp) (FieldOpFreeAlgebra 𝓕) := ⟨ofFieldOpListF⟩@[simp]
lemma ofFieldOpListF_nil : ofFieldOpListF ([] : List 𝓕.FieldOp) = 1 := rfllemma ofFieldOpListF_cons (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) :
ofFieldOpListF (φ :: φs) = ofFieldOpF φ * ofFieldOpListF φs := rfllemma ofFieldOpListF_singleton (φ : 𝓕.FieldOp) :
ofFieldOpListF [φ] = ofFieldOpF φ := 𝓕:FieldSpecificationφ:𝓕.FieldOp⊢ ofFieldOpListF [φ] = ofFieldOpF φ All goals completed! 🐙All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:ofFieldOpListF φs = ∑ s, ofCrAnListF ↑s⊢ ofFieldOpF φ * ofFieldOpListF φs = (∑ i, ofCrAnOpF ⟨φ, i⟩) * ofFieldOpListF φs
All goals completed! 🐙Creation and annihilation parts of a state
The algebra map taking an element of the free-state algebra to the part of it in the creation and annihilation free algebra spanned by creation operators.
def crPartF : 𝓕.FieldOp → 𝓕.FieldOpFreeAlgebra := fun φ =>
match φ with
| FieldOp.inAsymp φ => ofCrAnOpF ⟨FieldOp.inAsymp φ, ()⟩
| FieldOp.position φ => ofCrAnOpF ⟨FieldOp.position φ, CreateAnnihilate.create⟩
| FieldOp.outAsymp _ => 0@[simp]
lemma crPartF_negAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × Momentum) :
crPartF (FieldOp.inAsymp φ) = ofCrAnOpF ⟨FieldOp.inAsymp φ, ()⟩ := 𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ crPartF (FieldOp.inAsymp φ) = ofCrAnOpF ⟨FieldOp.inAsymp φ, ()⟩
All goals completed! 🐙@[simp]
lemma crPartF_position (φ : (Σ f, 𝓕.PositionLabel f) × SpaceTime) :
crPartF (FieldOp.position φ) =
ofCrAnOpF ⟨FieldOp.position φ, CreateAnnihilate.create⟩ := 𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ crPartF (FieldOp.position φ) = ofCrAnOpF ⟨FieldOp.position φ, CreateAnnihilate.create⟩
All goals completed! 🐙@[simp]
lemma crPartF_posAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × Momentum) :
crPartF (FieldOp.outAsymp φ) = 0 := 𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ crPartF (FieldOp.outAsymp φ) = 0
All goals completed! 🐙The algebra map taking an element of the free-state algebra to the part of it in the creation and annihilation free algebra spanned by annihilation operators.
def anPartF : 𝓕.FieldOp → 𝓕.FieldOpFreeAlgebra := fun φ =>
match φ with
| FieldOp.inAsymp _ => 0
| FieldOp.position φ => ofCrAnOpF ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩
| FieldOp.outAsymp φ => ofCrAnOpF ⟨FieldOp.outAsymp φ, ()⟩@[simp]
lemma anPartF_negAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × Momentum) :
anPartF (FieldOp.inAsymp φ) = 0 := 𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ anPartF (FieldOp.inAsymp φ) = 0
All goals completed! 🐙@[simp]
lemma anPartF_position (φ : (Σ f, 𝓕.PositionLabel f) × SpaceTime) :
anPartF (FieldOp.position φ) =
ofCrAnOpF ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩ := 𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ anPartF (FieldOp.position φ) = ofCrAnOpF ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩
All goals completed! 🐙@[simp]
lemma anPartF_posAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × Momentum) :
anPartF (FieldOp.outAsymp φ) = ofCrAnOpF ⟨FieldOp.outAsymp φ, ()⟩ := 𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ anPartF (FieldOp.outAsymp φ) = ofCrAnOpF ⟨FieldOp.outAsymp φ, ()⟩
All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOp⊢ ∑ i, ofCrAnOpF ⟨φ, i⟩ = crPartF φ + anPartF φ
cases φ with
𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ ∑ i, ofCrAnOpF ⟨FieldOp.inAsymp φ, i⟩ = crPartF (FieldOp.inAsymp φ) + anPartF (FieldOp.inAsymp φ) All goals completed! 🐙
𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ ∑ i, ofCrAnOpF ⟨FieldOp.position φ, i⟩ = crPartF (FieldOp.position φ) + anPartF (FieldOp.position φ) 𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ ∑ x, ofCrAnOpF ⟨FieldOp.position φ, x⟩ =
ofCrAnOpF ⟨FieldOp.position φ, CreateAnnihilate.create⟩ + ofCrAnOpF ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩; erw [𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ ofCrAnOpF ⟨FieldOp.position φ, CreateAnnihilate.create⟩ + ofCrAnOpF ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩ =
ofCrAnOpF ⟨FieldOp.position φ, CreateAnnihilate.create⟩ + ofCrAnOpF ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩All goals completed! 🐙
𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ ∑ i, ofCrAnOpF ⟨FieldOp.outAsymp φ, i⟩ = crPartF (FieldOp.outAsymp φ) + anPartF (FieldOp.outAsymp φ) All goals completed! 🐙The basis of the creation and annihilation free-algebra.
𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpkey:∀ (ψs : List 𝓕.CrAnFieldOp),
FreeAlgebra.equivMonoidAlgebraFreeMonoid (ofCrAnListF ψs) = MonoidAlgebra.single (FreeMonoid.ofList ψs) 1⊢ ofCrAnListFBasis.repr (ofCrAnListF φs) = Finsupp.single φs 1
𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpkey:∀ (ψs : List 𝓕.CrAnFieldOp),
FreeAlgebra.equivMonoidAlgebraFreeMonoid (ofCrAnListF ψs) = MonoidAlgebra.single (FreeMonoid.ofList ψs) 1⊢ (MonoidAlgebra.coeffLinearEquiv ℂ) (MonoidAlgebra.single (FreeMonoid.ofList φs) 1) = Finsupp.single φs 1
All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOph:ofCrAnListFBasis φs = ofCrAnListFBasis φs'⊢ φs = φs'
All goals completed! 🐙Some useful multi-linear maps.
lemma mulLinearMap_apply (a b : FieldOpFreeAlgebra 𝓕) :
mulLinearMap a b = a * b := rfl