Creation and annihilation states

Called CrAnFieldOp for short here.

Given a field specification, in addition to defining states (see: PhysLean.QFT.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 CrAnFieldOp we also define some maps:

• The map crAnFieldOpToFieldOp takes a CrAnFieldOp to its state in FieldOp.
• The map crAnFieldOpToCreateAnnihilate takes a CrAnFieldOp to its corresponding CreateAnnihilate value.
• The map crAnStatistics takes a CrAnFieldOp to its corresponding FieldStatistic (bosonic or fermionic).

def FieldSpecification.fieldOpToCrAnType (𝓕 : FieldSpecification) : 𝓕.FieldOp → Type

To each field operator the specification of the type of creation and annihilation parts. For asymptotic states there is only one allowed part, whilst for position field operator there is two.

Equations

• 𝓕.fieldOpToCrAnType (FieldSpecification.FieldOp.inAsymp a) = Unit
• 𝓕.fieldOpToCrAnType (FieldSpecification.FieldOp.position a) = CreateAnnihilate
• 𝓕.fieldOpToCrAnType (FieldSpecification.FieldOp.outAsymp a) = Unit

instance FieldSpecification.instFintypeFieldOpToCrAnType (𝓕 : FieldSpecification) (i : 𝓕.FieldOp) : Fintype (𝓕.fieldOpToCrAnType i)

The instance of a finite type on 𝓕.fieldOpToCreateAnnihilateType i.

Equations

• 𝓕.instFintypeFieldOpToCrAnType (FieldSpecification.FieldOp.inAsymp a) = inferInstanceAs (Fintype Unit)
• 𝓕.instFintypeFieldOpToCrAnType (FieldSpecification.FieldOp.position a) = inferInstanceAs (Fintype CreateAnnihilate)
• 𝓕.instFintypeFieldOpToCrAnType (FieldSpecification.FieldOp.outAsymp a) = inferInstanceAs (Fintype Unit)

instance FieldSpecification.instDecidableEqFieldOpToCrAnType (𝓕 : FieldSpecification) (i : 𝓕.FieldOp) : DecidableEq (𝓕.fieldOpToCrAnType i)

The instance of a decidable equality on 𝓕.fieldOpToCreateAnnihilateType i.

Equations

• 𝓕.instDecidableEqFieldOpToCrAnType (FieldSpecification.FieldOp.inAsymp a) = inferInstanceAs (DecidableEq Unit)
• 𝓕.instDecidableEqFieldOpToCrAnType (FieldSpecification.FieldOp.position a) = inferInstanceAs (DecidableEq CreateAnnihilate)
• 𝓕.instDecidableEqFieldOpToCrAnType (FieldSpecification.FieldOp.outAsymp a) = inferInstanceAs (DecidableEq Unit)

def FieldSpecification.fieldOpToCreateAnnihilateTypeCongr (𝓕 : FieldSpecification) {i j : 𝓕.FieldOp} : i = j → 𝓕.fieldOpToCrAnType i ≃ 𝓕.fieldOpToCrAnType j

The equivalence between 𝓕.fieldOpToCreateAnnihilateType i and 𝓕.fieldOpToCreateAnnihilateType j from an equality i = j.

Equations

• 𝓕.fieldOpToCreateAnnihilateTypeCongr ⋯ = Equiv.refl (𝓕.fieldOpToCrAnType x✝)

def FieldSpecification.CrAnFieldOp (𝓕 : FieldSpecification) : Type

For a field specification 𝓕, the (sigma) type 𝓕.CrAnFieldOp corresponds to the type of creation and annihilation parts of field operators. It formally defined to consist of the following elements:

• For each incoming asymptotic field operator φ in 𝓕.FieldOp an element written as ⟨φ, ()⟩ in 𝓕.CrAnFieldOp, corresponding to the creation part of φ. Here φ has no annihilation part. (Here () is the unique element of Unit.)
• For each position field operator φ in 𝓕.FieldOp an element of 𝓕.CrAnFieldOp written as ⟨φ, .create⟩, corresponding to the creation part of φ.
• For each position field operator φ in 𝓕.FieldOp an element of 𝓕.CrAnFieldOp written as ⟨φ, .annihilate⟩, corresponding to the annihilation part of φ.
• For each outgoing asymptotic field operator φ in 𝓕.FieldOp an element written as ⟨φ, ()⟩ in 𝓕.CrAnFieldOp, corresponding to the annihilation part of φ. Here φ has no creation part. (Here () is the unique element of Unit.)

As an example, if f corresponds to a Weyl-fermion field, it would contribute the following elements to 𝓕.CrAnFieldOp

• For each spin s, an element corresponding to an incoming asymptotic operator: a(p, s).

• For each each Lorentz index a, an element corresponding to the creation part of a position operator:

  ∑ s, ∫ d³p/(…) (xₐ (p,s) a(p, s) e ^ (-i p x)).

• For each each Lorentz index a,an element corresponding to annihilation part of a position operator:

  ∑ s, ∫ d³p/(…) (yₐ(p,s) a†(p, s) e ^ (-i p x)).

• For each spin s, element corresponding to an outgoing asymptotic operator: a†(p, s).

Equations

• 𝓕.CrAnFieldOp = ((s : 𝓕.FieldOp) × 𝓕.fieldOpToCrAnType s)

def FieldSpecification.crAnFieldOpToFieldOp (𝓕 : FieldSpecification) : 𝓕.CrAnFieldOp → 𝓕.FieldOp

The map from creation and annihilation field operator to their underlying states.

Equations

• 𝓕.crAnFieldOpToFieldOp = Sigma.fst

@[simp]

theorem FieldSpecification.crAnFieldOpToFieldOp_prod (𝓕 : FieldSpecification) (s : 𝓕.FieldOp) (t : 𝓕.fieldOpToCrAnType s) : 𝓕.crAnFieldOpToFieldOp ⟨s, t⟩ = s

def FieldSpecification.crAnFieldOpToCreateAnnihilate (𝓕 : FieldSpecification) : 𝓕.CrAnFieldOp → CreateAnnihilate

For a field specification 𝓕, 𝓕.crAnFieldOpToCreateAnnihilate is the map from 𝓕.CrAnFieldOp to CreateAnnihilate taking φ to create if

• φ corresponds to an incoming asymptotic field operator or the creation part of a position based field operator.

otherwise it takes φ to annihilate.

Equations

• 𝓕.crAnFieldOpToCreateAnnihilate ⟨FieldSpecification.FieldOp.inAsymp a, snd⟩ = CreateAnnihilate.create
• 𝓕.crAnFieldOpToCreateAnnihilate ⟨FieldSpecification.FieldOp.position a, CreateAnnihilate.create⟩ = CreateAnnihilate.create
• 𝓕.crAnFieldOpToCreateAnnihilate ⟨FieldSpecification.FieldOp.position a, CreateAnnihilate.annihilate⟩ = CreateAnnihilate.annihilate
• 𝓕.crAnFieldOpToCreateAnnihilate ⟨FieldSpecification.FieldOp.outAsymp a, snd⟩ = CreateAnnihilate.annihilate

def FieldSpecification.crAnStatistics (𝓕 : FieldSpecification) : 𝓕.CrAnFieldOp → FieldStatistic

For a field specification 𝓕, and an element φ in 𝓕.CrAnFieldOp, the field statistic crAnStatistics φ is defined to be the statistic associated with the field 𝓕.Field (or the 𝓕.FieldOp) underlying φ.

The following notation is used in relation to crAnStatistics:

• For φ an element of 𝓕.CrAnFieldOp, 𝓕 |>ₛ φ is crAnStatistics φ.
• For φs a list of 𝓕.CrAnFieldOp, 𝓕 |>ₛ φs is the product of crAnStatistics φ over the list φs.

Equations

• 𝓕.crAnStatistics = 𝓕.fieldOpStatistic ∘ 𝓕.crAnFieldOpToFieldOp

def FieldSpecification.«term_|>ₛ__2» : Lean.TrailingParserDescr

For a field specification 𝓕, and an element φ in 𝓕.CrAnFieldOp, the field statistic crAnStatistics φ is defined to be the statistic associated with the field 𝓕.Field (or the 𝓕.FieldOp) underlying φ.

The following notation is used in relation to crAnStatistics:

• For φ an element of 𝓕.CrAnFieldOp, 𝓕 |>ₛ φ is crAnStatistics φ.
• For φs a list of 𝓕.CrAnFieldOp, 𝓕 |>ₛ φs is the product of crAnStatistics φ over the list φs.

Equations

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

def FieldSpecification.«term_|>ₛ__3» : Lean.TrailingParserDescr

For a field specification 𝓕, and an element φ in 𝓕.CrAnFieldOp, the field statistic crAnStatistics φ is defined to be the statistic associated with the field 𝓕.Field (or the 𝓕.FieldOp) underlying φ.

The following notation is used in relation to crAnStatistics:

• For φ an element of 𝓕.CrAnFieldOp, 𝓕 |>ₛ φ is crAnStatistics φ.
• For φs a list of 𝓕.CrAnFieldOp, 𝓕 |>ₛ φs is the product of crAnStatistics φ over the list φs.

Equations

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

def FieldSpecification.«term_|>ᶜ_» : Lean.TrailingParserDescr

The CreateAnnihilate value of a CrAnFieldOps, i.e. whether it is a creation or annihilation operator.

Equations

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