The Wick Algebra

This is the algebra with the minimal assumptions necessary to prove Wick's theorem. It satisfies the appropriate universality conditions with respect to the operator algebra.

def FieldSpecification.fieldOpIdealSet (𝓕 : FieldSpecification) : Set 𝓕.FieldOpFreeAlgebra

The set contains the super-commutators equal to zero in the operator algebra. This contains e.g. the super-commutator of two creation operators.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev FieldSpecification.WickAlgebra (𝓕 : FieldSpecification) : Type

For a field specification 𝓕, the algebra 𝓕.WickAlgebra is defined as the quotient of the free algebra 𝓕.FieldOpFreeAlgebra by the ideal generated by

• [ofCrAnOpF φc, ofCrAnOpF φc']ₛF for φc and φc' field creation operators. This corresponds to the condition that two creation operators always super-commute.
• [ofCrAnOpF φa, ofCrAnOpF φa']ₛF for φa and φa' field annihilation operators. This corresponds to the condition that two annihilation operators always super-commute.
• [ofCrAnOpF φ, ofCrAnOpF φ']ₛF for φ and φ' operators with different statistics. This corresponds to the condition that two operators with different statistics always super-commute. In other words, fermions and bosons always super-commute.
• [ofCrAnOpF φ1, [ofCrAnOpF φ2, ofCrAnOpF φ3]ₛF]ₛF. This corresponds to the condition, when combined with the conditions above, that the super-commutator is in the center of the algebra.

Equations

• 𝓕.WickAlgebra = (TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCon.Quotient

instance FieldSpecification.WickAlgebra.instSetoidFieldOpFreeAlgebra {𝓕 : FieldSpecification} : Setoid 𝓕.FieldOpFreeAlgebra

The instance of a setoid on FieldOpFreeAlgebra from the ideal TwoSidedIdeal.

Equations

• FieldSpecification.WickAlgebra.instSetoidFieldOpFreeAlgebra = (TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCon.toSetoid

theorem FieldSpecification.WickAlgebra.equiv_iff_sub_mem_ideal {𝓕 : FieldSpecification} (x y : 𝓕.FieldOpFreeAlgebra) : x ≈ y ↔ x - y ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet

theorem FieldSpecification.WickAlgebra.equiv_iff_exists_add {𝓕 : FieldSpecification} (x y : 𝓕.FieldOpFreeAlgebra) : x ≈ y ↔ ∃ (a : 𝓕.FieldOpFreeAlgebra), x = y + a ∧ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet

def FieldSpecification.WickAlgebra.ι {𝓕 : FieldSpecification} : 𝓕.FieldOpFreeAlgebra →ₐ[ℂ] 𝓕.WickAlgebra

For a field specification 𝓕, ι is defined as the projection

𝓕.FieldOpFreeAlgebra →ₐ[ℂ] 𝓕.WickAlgebra

taking each element of 𝓕.FieldOpFreeAlgebra to its equivalence class in WickAlgebra 𝓕.

Equations

• FieldSpecification.WickAlgebra.ι = { toFun := ⇑(TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCon.mk', map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

theorem FieldSpecification.WickAlgebra.ι_surjective {𝓕 : FieldSpecification} : Function.Surjective ⇑ι

theorem FieldSpecification.WickAlgebra.ι_apply {𝓕 : FieldSpecification} (x : 𝓕.FieldOpFreeAlgebra) : ι x = ⟦x⟧

theorem FieldSpecification.WickAlgebra.ι_of_mem_fieldOpIdealSet {𝓕 : FieldSpecification} (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ 𝓕.fieldOpIdealSet) : ι x = 0

theorem FieldSpecification.WickAlgebra.ι_superCommuteF_of_create_create {𝓕 : FieldSpecification} (φc φc' : 𝓕.CrAnFieldOp) (hφc : 𝓕.crAnFieldOpToCreateAnnihilate φc = CreateAnnihilate.create) (hφc' : 𝓕.crAnFieldOpToCreateAnnihilate φc' = CreateAnnihilate.create) : ι ((FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φc)) (FieldOpFreeAlgebra.ofCrAnOpF φc')) = 0

theorem FieldSpecification.WickAlgebra.ι_superCommuteF_of_annihilate_annihilate {𝓕 : FieldSpecification} (φa φa' : 𝓕.CrAnFieldOp) (hφa : 𝓕.crAnFieldOpToCreateAnnihilate φa = CreateAnnihilate.annihilate) (hφa' : 𝓕.crAnFieldOpToCreateAnnihilate φa' = CreateAnnihilate.annihilate) : ι ((FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φa)) (FieldOpFreeAlgebra.ofCrAnOpF φa')) = 0

theorem FieldSpecification.WickAlgebra.ι_superCommuteF_of_diff_statistic {𝓕 : FieldSpecification} {φ ψ : 𝓕.CrAnFieldOp} (h : 𝓕.crAnStatistics φ ≠ 𝓕.crAnStatistics ψ) : ι ((FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φ)) (FieldOpFreeAlgebra.ofCrAnOpF ψ)) = 0

theorem FieldSpecification.WickAlgebra.ι_superCommuteF_zero_of_fermionic {𝓕 : FieldSpecification} (φ ψ : 𝓕.CrAnFieldOp) (h : (FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φ)) (FieldOpFreeAlgebra.ofCrAnOpF ψ) ∈ FieldOpFreeAlgebra.statisticSubmodule FieldStatistic.fermionic) : ι ((FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φ)) (FieldOpFreeAlgebra.ofCrAnOpF ψ)) = 0

theorem FieldSpecification.WickAlgebra.ι_superCommuteF_ofCrAnOpF_ofCrAnOpF_bosonic_or_zero {𝓕 : FieldSpecification} (φ ψ : 𝓕.CrAnFieldOp) : (FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φ)) (FieldOpFreeAlgebra.ofCrAnOpF ψ) ∈ FieldOpFreeAlgebra.statisticSubmodule FieldStatistic.bosonic ∨ ι ((FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φ)) (FieldOpFreeAlgebra.ofCrAnOpF ψ)) = 0

Super-commutes are in the center

@[simp]

theorem FieldSpecification.WickAlgebra.ι_superCommuteF_ofCrAnOpF_superCommuteF_ofCrAnOpF_ofCrAnOpF {𝓕 : FieldSpecification} (φ1 φ2 φ3 : 𝓕.CrAnFieldOp) : ι ((FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φ1)) ((FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φ2)) (FieldOpFreeAlgebra.ofCrAnOpF φ3))) = 0

theorem FieldSpecification.WickAlgebra.ι_superCommuteF_superCommuteF_ofCrAnOpF_ofCrAnOpF_ofCrAnOpF {𝓕 : FieldSpecification} (φ1 φ2 φ3 : 𝓕.CrAnFieldOp) : ι ((FieldOpFreeAlgebra.superCommuteF ((FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φ1)) (FieldOpFreeAlgebra.ofCrAnOpF φ2))) (FieldOpFreeAlgebra.ofCrAnOpF φ3)) = 0

theorem FieldSpecification.WickAlgebra.ι_superCommuteF_superCommuteF_ofCrAnOpF_ofCrAnOpF_ofCrAnListF {𝓕 : FieldSpecification} (φ1 φ2 : 𝓕.CrAnFieldOp) (φs : List 𝓕.CrAnFieldOp) : ι ((FieldOpFreeAlgebra.superCommuteF ((FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φ1)) (FieldOpFreeAlgebra.ofCrAnOpF φ2))) (FieldOpFreeAlgebra.ofCrAnListF φs)) = 0

@[simp]

theorem FieldSpecification.WickAlgebra.ι_superCommuteF_superCommuteF_ofCrAnOpF_ofCrAnOpF_fieldOpFreeAlgebra {𝓕 : FieldSpecification} (φ1 φ2 : 𝓕.CrAnFieldOp) (a : 𝓕.FieldOpFreeAlgebra) : ι ((FieldOpFreeAlgebra.superCommuteF ((FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φ1)) (FieldOpFreeAlgebra.ofCrAnOpF φ2))) a) = 0

theorem FieldSpecification.WickAlgebra.ι_commute_fieldOpFreeAlgebra_superCommuteF_ofCrAnOpF_ofCrAnOpF {𝓕 : FieldSpecification} (φ1 φ2 : 𝓕.CrAnFieldOp) (a : 𝓕.FieldOpFreeAlgebra) : ι a * ι ((FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φ1)) (FieldOpFreeAlgebra.ofCrAnOpF φ2)) - ι ((FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φ1)) (FieldOpFreeAlgebra.ofCrAnOpF φ2)) * ι a = 0

theorem FieldSpecification.WickAlgebra.ι_superCommuteF_ofCrAnOpF_ofCrAnOpF_mem_center {𝓕 : FieldSpecification} (φ ψ : 𝓕.CrAnFieldOp) : ι ((FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φ)) (FieldOpFreeAlgebra.ofCrAnOpF ψ)) ∈ Subalgebra.center ℂ 𝓕.WickAlgebra

The kernel of ι

theorem FieldSpecification.WickAlgebra.ι_eq_zero_iff_mem_ideal {𝓕 : FieldSpecification} (x : 𝓕.FieldOpFreeAlgebra) : ι x = 0 ↔ x ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet

theorem FieldSpecification.WickAlgebra.bosonicProjF_mem_fieldOpIdealSet_or_zero {𝓕 : FieldSpecification} (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ 𝓕.fieldOpIdealSet) : ↑(FieldOpFreeAlgebra.bosonicProjF x) ∈ 𝓕.fieldOpIdealSet ∨ FieldOpFreeAlgebra.bosonicProjF x = 0

theorem FieldSpecification.WickAlgebra.fermionicProjF_mem_fieldOpIdealSet_or_zero {𝓕 : FieldSpecification} (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ 𝓕.fieldOpIdealSet) : ↑(FieldOpFreeAlgebra.fermionicProjF x) ∈ 𝓕.fieldOpIdealSet ∨ FieldOpFreeAlgebra.fermionicProjF x = 0

theorem FieldSpecification.WickAlgebra.bosonicProjF_mem_ideal {𝓕 : FieldSpecification} (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet) : ↑(FieldOpFreeAlgebra.bosonicProjF x) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet

theorem FieldSpecification.WickAlgebra.fermionicProjF_mem_ideal {𝓕 : FieldSpecification} (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet) : ↑(FieldOpFreeAlgebra.fermionicProjF x) ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet

theorem FieldSpecification.WickAlgebra.ι_eq_zero_iff_ι_bosonicProjF_fermonicProj_zero {𝓕 : FieldSpecification} (x : 𝓕.FieldOpFreeAlgebra) : ι x = 0 ↔ ι ↑(FieldOpFreeAlgebra.bosonicProjF x) = 0 ∧ ι ↑(FieldOpFreeAlgebra.fermionicProjF x) = 0

Constructors

def FieldSpecification.WickAlgebra.ofFieldOp {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) : 𝓕.WickAlgebra

For a field specification 𝓕 and an element φ of 𝓕.FieldOp, ofFieldOp φ is defined as the element of 𝓕.WickAlgebra given by ι (ofFieldOpF φ).

Equations

• FieldSpecification.WickAlgebra.ofFieldOp φ = FieldSpecification.WickAlgebra.ι (FieldSpecification.FieldOpFreeAlgebra.ofFieldOpF φ)

theorem FieldSpecification.WickAlgebra.ofFieldOp_eq_ι_ofFieldOpF {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) : ofFieldOp φ = ι (FieldOpFreeAlgebra.ofFieldOpF φ)

def FieldSpecification.WickAlgebra.ofFieldOpList {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) : 𝓕.WickAlgebra

For a field specification 𝓕 and a list φs of 𝓕.FieldOp, ofFieldOpList φs is defined as the element of 𝓕.WickAlgebra given by ι (ofFieldOpListF φ).

Equations

• FieldSpecification.WickAlgebra.ofFieldOpList φs = FieldSpecification.WickAlgebra.ι (FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF φs)

theorem FieldSpecification.WickAlgebra.ofFieldOpList_eq_ι_ofFieldOpListF {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) : ofFieldOpList φs = ι (FieldOpFreeAlgebra.ofFieldOpListF φs)

theorem FieldSpecification.WickAlgebra.ofFieldOpList_append {𝓕 : FieldSpecification} (φs ψs : List 𝓕.FieldOp) : ofFieldOpList (φs ++ ψs) = ofFieldOpList φs * ofFieldOpList ψs

theorem FieldSpecification.WickAlgebra.ofFieldOpList_cons {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : ofFieldOpList (φ :: φs) = ofFieldOp φ * ofFieldOpList φs

theorem FieldSpecification.WickAlgebra.ofFieldOpList_singleton {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) : ofFieldOpList [φ] = ofFieldOp φ

def FieldSpecification.WickAlgebra.ofCrAnOp {𝓕 : FieldSpecification} (φ : 𝓕.CrAnFieldOp) : 𝓕.WickAlgebra

For a field specification 𝓕 and an element φ of 𝓕.CrAnFieldOp, ofCrAnOp φ is defined as the element of 𝓕.WickAlgebra given by ι (ofCrAnOpF φ).

Equations

• FieldSpecification.WickAlgebra.ofCrAnOp φ = FieldSpecification.WickAlgebra.ι (FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF φ)

theorem FieldSpecification.WickAlgebra.ofCrAnOp_eq_ι_ofCrAnOpF {𝓕 : FieldSpecification} (φ : 𝓕.CrAnFieldOp) : ofCrAnOp φ = ι (FieldOpFreeAlgebra.ofCrAnOpF φ)

theorem FieldSpecification.WickAlgebra.ofFieldOp_eq_sum {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) : ofFieldOp φ = ∑ i : 𝓕.fieldOpToCrAnType φ, ofCrAnOp ⟨φ, i⟩

def FieldSpecification.WickAlgebra.ofCrAnList {𝓕 : FieldSpecification} (φs : List 𝓕.CrAnFieldOp) : 𝓕.WickAlgebra

For a field specification 𝓕 and a list φs of 𝓕.CrAnFieldOp, ofCrAnList φs is defined as the element of 𝓕.WickAlgebra given by ι (ofCrAnListF φ).

Equations

• FieldSpecification.WickAlgebra.ofCrAnList φs = FieldSpecification.WickAlgebra.ι (FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF φs)

theorem FieldSpecification.WickAlgebra.ofCrAnList_eq_ι_ofCrAnListF {𝓕 : FieldSpecification} (φs : List 𝓕.CrAnFieldOp) : ofCrAnList φs = ι (FieldOpFreeAlgebra.ofCrAnListF φs)

theorem FieldSpecification.WickAlgebra.ofCrAnList_append {𝓕 : FieldSpecification} (φs ψs : List 𝓕.CrAnFieldOp) : ofCrAnList (φs ++ ψs) = ofCrAnList φs * ofCrAnList ψs

theorem FieldSpecification.WickAlgebra.ofCrAnList_singleton {𝓕 : FieldSpecification} (φ : 𝓕.CrAnFieldOp) : ofCrAnList [φ] = ofCrAnOp φ

theorem FieldSpecification.WickAlgebra.ofFieldOpList_eq_sum {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) : ofFieldOpList φs = ∑ s : CrAnSection φs, ofCrAnList ↑s

def FieldSpecification.WickAlgebra.anPart {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) : 𝓕.WickAlgebra

For a field specification 𝓕, and an element φ of 𝓕.FieldOp, the annihilation part of 𝓕.FieldOp as an element of 𝓕.WickAlgebra. Thus for φ

• an incoming asymptotic state this is 0.
• a position based state this is ofCrAnOp ⟨φ, .create⟩.
• an outgoing asymptotic state this is ofCrAnOp ⟨φ, ()⟩.

Equations

• FieldSpecification.WickAlgebra.anPart φ = FieldSpecification.WickAlgebra.ι (FieldSpecification.FieldOpFreeAlgebra.anPartF φ)

theorem FieldSpecification.WickAlgebra.anPart_eq_ι_anPartF {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) : anPart φ = ι (FieldOpFreeAlgebra.anPartF φ)

@[simp]

theorem FieldSpecification.WickAlgebra.anPart_inAsymp {𝓕 : FieldSpecification} (φ : ((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum) : anPart (FieldOp.inAsymp φ) = 0

@[simp]

theorem FieldSpecification.WickAlgebra.anPart_position {𝓕 : FieldSpecification} (φ : ((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime) : anPart (FieldOp.position φ) = ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩

@[simp]

theorem FieldSpecification.WickAlgebra.anPart_outAsymp {𝓕 : FieldSpecification} (φ : ((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum) : anPart (FieldOp.outAsymp φ) = ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩

def FieldSpecification.WickAlgebra.crPart {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) : 𝓕.WickAlgebra

For a field specification 𝓕, and an element φ of 𝓕.FieldOp, the creation part of 𝓕.FieldOp as an element of 𝓕.WickAlgebra. Thus for φ

• an incoming asymptotic state this is ofCrAnOp ⟨φ, ()⟩.
• a position based state this is ofCrAnOp ⟨φ, .create⟩.
• an outgoing asymptotic state this is 0.

Equations

• FieldSpecification.WickAlgebra.crPart φ = FieldSpecification.WickAlgebra.ι (FieldSpecification.FieldOpFreeAlgebra.crPartF φ)

theorem FieldSpecification.WickAlgebra.crPart_eq_ι_crPartF {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) : crPart φ = ι (FieldOpFreeAlgebra.crPartF φ)

@[simp]

theorem FieldSpecification.WickAlgebra.crPart_inAsymp {𝓕 : FieldSpecification} (φ : ((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum) : crPart (FieldOp.inAsymp φ) = ofCrAnOp ⟨FieldOp.inAsymp φ, ()⟩

@[simp]

theorem FieldSpecification.WickAlgebra.crPart_position {𝓕 : FieldSpecification} (φ : ((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime) : crPart (FieldOp.position φ) = ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.create⟩

@[simp]

theorem FieldSpecification.WickAlgebra.crPart_outAsymp {𝓕 : FieldSpecification} (φ : ((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum) : crPart (FieldOp.outAsymp φ) = 0

theorem FieldSpecification.WickAlgebra.ofFieldOp_eq_crPart_add_anPart {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) : ofFieldOp φ = crPart φ + anPart φ

For field specification 𝓕, and an element φ of 𝓕.FieldOp the following relation holds:

ofFieldOp φ = crPart φ + anPart φ

That is, every field operator splits into its creation part plus its annihilation part.

theorem FieldSpecification.WickAlgebra.anPart_outAsymp_eq_ofFieldOp {𝓕 : FieldSpecification} (φ : ((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum) : anPart (FieldOp.outAsymp φ) = ofFieldOp (FieldOp.outAsymp φ)

theorem FieldSpecification.WickAlgebra.crPart_inAsymp_eq_ofFieldOp {𝓕 : FieldSpecification} (φ : ((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum) : crPart (FieldOp.inAsymp φ) = ofFieldOp (FieldOp.inAsymp φ)