Field 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.FieldOpAlgebra (𝓕 : FieldSpecification) : Type

For a field specification 𝓕, the algebra 𝓕.FieldOpAlgebra 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

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

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

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

Equations

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

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

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

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

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

𝓕.FieldOpFreeAlgebra →ₐ[ℂ] 𝓕.FieldOpAlgebra

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

Equations

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

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

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

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

theorem FieldSpecification.FieldOpAlgebra.ι_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.FieldOpAlgebra.ι_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.FieldOpAlgebra.ι_superCommuteF_of_diff_statistic {𝓕 : FieldSpecification} {φ ψ : 𝓕.CrAnFieldOp} (h : 𝓕.crAnStatistics φ ≠ 𝓕.crAnStatistics ψ) : ι ((FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φ)) (FieldOpFreeAlgebra.ofCrAnOpF ψ)) = 0

theorem FieldSpecification.FieldOpAlgebra.ι_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.FieldOpAlgebra.ι_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.FieldOpAlgebra.ι_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.FieldOpAlgebra.ι_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.FieldOpAlgebra.ι_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.FieldOpAlgebra.ι_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.FieldOpAlgebra.ι_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.FieldOpAlgebra.ι_superCommuteF_ofCrAnOpF_ofCrAnOpF_mem_center {𝓕 : FieldSpecification} (φ ψ : 𝓕.CrAnFieldOp) : ι ((FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φ)) (FieldOpFreeAlgebra.ofCrAnOpF ψ)) ∈ Subalgebra.center ℂ 𝓕.FieldOpAlgebra

The kernel of ι

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

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

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

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

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

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

Constructors

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

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

Equations

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

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

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

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

Equations

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

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

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

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

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

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

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

Equations

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

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

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

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

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

Equations

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

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

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

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

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

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

For a field specification 𝓕, and an element φ of 𝓕.FieldOp, the annihilation part of 𝓕.FieldOp as an element of 𝓕.FieldOpAlgebra. 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.FieldOpAlgebra.anPart φ = FieldSpecification.FieldOpAlgebra.ι (FieldSpecification.FieldOpFreeAlgebra.anPartF φ)

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

@[simp]

theorem FieldSpecification.FieldOpAlgebra.anPart_negAsymp {𝓕 : FieldSpecification} (φ : ((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ)) : anPart (FieldOp.inAsymp φ) = 0

@[simp]

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

@[simp]

theorem FieldSpecification.FieldOpAlgebra.anPart_posAsymp {𝓕 : FieldSpecification} (φ : ((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ)) : anPart (FieldOp.outAsymp φ) = ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩

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

For a field specification 𝓕, and an element φ of 𝓕.FieldOp, the creation part of 𝓕.FieldOp as an element of 𝓕.FieldOpAlgebra. 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.FieldOpAlgebra.crPart φ = FieldSpecification.FieldOpAlgebra.ι (FieldSpecification.FieldOpFreeAlgebra.crPartF φ)

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

@[simp]

theorem FieldSpecification.FieldOpAlgebra.crPart_negAsymp {𝓕 : FieldSpecification} (φ : ((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ)) : crPart (FieldOp.inAsymp φ) = ofCrAnOp ⟨FieldOp.inAsymp φ, ()⟩

@[simp]

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

@[simp]

theorem FieldSpecification.FieldOpAlgebra.crPart_posAsymp {𝓕 : FieldSpecification} (φ : ((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ)) : crPart (FieldOp.outAsymp φ) = 0

theorem FieldSpecification.FieldOpAlgebra.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.