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.SpaceAndTime.SpaceTime.Basic public import Physlib.Units.WithDim.Momentum public import Physlib.QFT.PerturbationTheory.FieldStatistics.OfFinset

Field specification

In this module is the definition of a field specification. A field specification is a structure consisting of a type of fields and a the field statistics of each field.

From each field we can create three different types of FieldOp.

    Negative asymptotic states.

    Position states.

    Positive asymptotic states.

These states carry the same field statistic as the field they are derived from.

Some references

    https://particle.physics.ucdavis.edu/modernsusy/slides/slideimages/spinorfeynrules.pdf

@[expose] public section

The structure FieldSpecification is defined to have the following content:

    A type Field whose elements are the constituent fields of the theory.

    For every field f in Field, a type PositionLabel f whose elements label the different position operators associated with the field f. For example,

      For f a real-scalar field, PositionLabel f will have a unique element.

      For f a complex-scalar field, PositionLabel f will have two elements, one for the field operator and one for its conjugate.

      For f a Dirac fermion, PositionLabel f will have eight elements, one for each Lorentz index of the field and its conjugate.

      For f a Weyl fermion, PositionLabel f will have four elements, one for each Lorentz index of the field and its conjugate.

    For every field f in Field, a type AsymptoticLabel f whose elements label the different types of incoming asymptotic field operators associated with the field f (this also matches the types of outgoing asymptotic field operators). For example,

      For f a real-scalar field, AsymptoticLabel f will have a unique element.

      For f a complex-scalar field, AsymptoticLabel f will have two elements, one for the field operator and one for its conjugate.

      For f a Dirac fermion, AsymptoticLabel f will have four elements, two for each spin.

      For f a Weyl fermion, AsymptoticLabel f will have two elements, one for each spin.

    For each field f in Field, a field statistic statistic f which classifies f as either bosonic or fermionic.

A type whose elements are the constituent fields of the theory.

For every field f in Field, the type PositionLabel f has elements that label the different position operators associated with the field f.

For every field f in Field, the type AsymptoticLabel f has elements that label the different asymptotic based field operators associated with the field f.

For every field f in Field, the field statistic statistic f classifies f as either bosonic or fermionic.

structure FieldSpecification where Field : Type PositionLabel : Field Type AsymptoticLabel : Field Type statistic : Field FieldStatistic

For a field specification 𝓕, the inductive type 𝓕.FieldOp is defined to contain the following elements:

    For every f in 𝓕.Field, element of e of AsymptoticLabel f and 3-momentum p, an element labelled inAsymp f e p corresponding to an incoming asymptotic field operator of the field f, of label e (e.g. specifying the spin), and momentum p.

    For every f in 𝓕.Field, element of e of PositionLabel f and space-time position x, an element labelled position f e x corresponding to a position field operator of the field f, of label e (e.g. specifying the Lorentz index), and position x.

    For every f in 𝓕.Field, element of e of AsymptoticLabel f and 3-momentum p, an element labelled outAsymp f e p corresponding to an outgoing asymptotic field operator of the field f, of label e (e.g. specifying the spin), and momentum p.

As an example, if f corresponds to a Weyl-fermion field, then

    For inAsymp f e p, e would correspond to a spin s, and inAsymp f e p would, once represented in the operator algebra, be proportional to the creation operator a(p, s).

    position f e x, e would correspond to a Lorentz index a, and position f e x would, once represented in the operator algebra, be proportional to the operator

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

    outAsymp f e p, e would correspond to a spin s, and outAsymp f e p would, once represented in the operator algebra, be proportional to the annihilation operator a†(p, s).

inductive FieldOp (𝓕 : FieldSpecification) where | inAsymp : (Σ f, 𝓕.AsymptoticLabel f) × (Momentum 3) 𝓕.FieldOp | position : (Σ f, 𝓕.PositionLabel f) × SpaceTime 𝓕.FieldOp | outAsymp : (Σ f, 𝓕.AsymptoticLabel f) × (Momentum 3) 𝓕.FieldOp

The bool on FieldOp which is true only for position field operator.

def statesIsPosition : 𝓕.FieldOp Bool | FieldOp.position _ => true | _ => false

For a field specification 𝓕, 𝓕.fieldOpToField is defined to take field operators to their underlying field.

def fieldOpToField : 𝓕.FieldOp 𝓕.Field | FieldOp.inAsymp (f, _) => f.1 | FieldOp.position (f, _) => f.1 | FieldOp.outAsymp (f, _) => f.1

For a field specification 𝓕, and an element φ of 𝓕.FieldOp. The field statistic fieldOpStatistic φ is defined to be the statistic associated with the field underlying φ.

The following notation is used in relation to fieldOpStatistic:

    For φ an element of 𝓕.FieldOp, 𝓕 |>ₛ φ is fieldOpStatistic φ.

    For φs a list of 𝓕.FieldOp, 𝓕 |>ₛ φs is the product of fieldOpStatistic φ over the list φs.

    For a function f : Fin n → 𝓕.FieldOp and a finite set a of Fin n, 𝓕 |>ₛ ⟨f, a⟩ is the product of fieldOpStatistic (f i) for all i ∈ a.

def fieldOpStatistic : 𝓕.FieldOp FieldStatistic := 𝓕.statistic 𝓕.fieldOpToField
@[inherit_doc fieldOpStatistic] scoped[FieldSpecification] notation 𝓕 "|>ₛ" φ => fieldOpStatistic 𝓕 φ@[inherit_doc fieldOpStatistic] scoped[FieldSpecification] notation 𝓕 "|>ₛ" φ => FieldStatistic.ofList (fieldOpStatistic 𝓕) φ@[inherit_doc fieldOpStatistic] scoped[FieldSpecification] notation 𝓕 "|>ₛ" "⟨" f ","a "⟩" => FieldStatistic.ofFinset (fieldOpStatistic 𝓕) f a