Physlib.QFT.PerturbationTheory.FieldSpecification.CrAnFieldOp

For a given field specification $\mathcal{F}$, the function $\text{fieldOpToCrAnType}$ assigns to each field operator state $\phi \in \mathcal{F}.\text{FieldOp}$ the type (set) of allowed creation or annihilation labels. - If $\phi$ is an incoming or outgoing asymptotic state, the result is the singleton type $\text{Unit}$, reflecting that these states have a single fixed mode (typically creation for incoming and annihilation for outgoing states). - If $\phi$ is a position-space field operator, the result is the type $\text{CreateAnnihilate} = \{\text{create}, \text{annihilate}\}$, as these operators generally consist of both creation and annihilation parts.

For a given field specification $\mathcal{F}$ and any field operator $i \in \mathcal{F}.\text{FieldOp}$, the set of creation and annihilation modes associated with $i$, denoted as $\mathcal{F}.\text{fieldOpToCrAnType}(i)$, is a finite set. This finiteness holds because the mode type is either the singleton set $\text{Unit}$ (for asymptotic states) or the two-element set $\text{CreateAnnihilate}$ (for position-space states).

For a given field specification $\mathcal{F}$, and for any field operator $i \in \mathcal{F}.\text{FieldOp}$, the equality between elements of the type $\mathcal{F}.\text{fieldOpToCrAnType}(i)$ is decidable. This type represents the available creation and annihilation modes for the operator $i$, which is either a singleton set (for asymptotic states) or the set $\{\text{create}, \text{annihilate}\}$ (for position-space operators).

For a given field specification $\mathcal{F}$ and two field operators $i, j \in \mathcal{F}.\text{FieldOp}$, if $i = j$, then there is an equivalence between their corresponding types of creation and annihilation modes, denoted as $\mathcal{F}.\text{fieldOpToCrAnType}(i) \cong \mathcal{F}.\text{fieldOpToCrAnType}(j)$.

For a given field specification $\mathcal{F}$, the type $\mathcal{F}.\text{CrAnFieldOp}$ is the collection of creation and annihilation components of all field operators. It is formally defined as the dependent sum $\sum_{\phi \in \mathcal{F}.\text{FieldOp}} \text{fieldOpToCrAnType}(\phi)$, consisting of pairs $\langle \phi, \sigma \rangle$ where: - If $\phi$ is an incoming asymptotic field operator, $\sigma$ is the unique element of $\text{Unit}$, representing its creation component. - If $\phi$ is an outgoing asymptotic field operator, $\sigma$ is the unique element of $\text{Unit}$, representing its annihilation component. - If $\phi$ is a position-space field operator, $\sigma \in \{\text{create}, \text{annihilate}\}$ distinguishes between the creation part and the annihilation part of the field operator at that position.

For a given field specification $\mathcal{F}$, the function maps a creation or annihilation field operator $\varphi \in \mathcal{F}.\text{CrAnFieldOp}$ to its underlying field operator state $\phi \in \mathcal{F}.\text{FieldOp}$. Since $\mathcal{F}.\text{CrAnFieldOp}$ is defined as the dependent sum $\sum_{\phi \in \mathcal{F}.\text{FieldOp}} \text{fieldOpToCrAnType}(\phi)$, this map is the projection onto the first component, which sends a pair $\langle \phi, \sigma \rangle$ to $\phi$.

For a given field specification $\mathcal{F}$, let $s \in \mathcal{F}.\text{FieldOp}$ be a field operator and let $t \in \mathcal{F}.\text{fieldOpToCrAnType}(s)$ be a creation or annihilation label associated with $s$. Then the projection of the pair $\langle s, t \rangle$ (representing a creation or annihilation field operator) back to the space of field operators is equal to $s$: $$\text{crAnFieldOpToFieldOp}(\langle s, t \rangle) = s$$

For a given field specification $\mathcal{F}$, the function maps an element $\varphi \in \mathcal{F}.\text{CrAnFieldOp}$ to its corresponding classification in the set $\text{CreateAnnihilate} = \{\text{create}, \text{annihilate}\}$. Specifically, for an operator component $\varphi$ associated with an underlying field operator $\phi$: - If $\phi$ is an incoming asymptotic field operator, $\varphi$ is mapped to $\text{create}$. - If $\phi$ is an outgoing asymptotic field operator, $\varphi$ is mapped to $\text{annihilate}$. - If $\phi$ is a position-space field operator, $\varphi$ is mapped to its internal label $\sigma \in \{\text{create}, \text{annihilate}\}$ which specifies whether it is the creation or annihilation part of the field.

For a given field specification $\mathcal{F}$, the function maps a creation or annihilation operator $\varphi \in \mathcal{F}.\text{CrAnFieldOp}$ to its corresponding field statistic (bosonic or fermionic). This is defined by first projecting $\varphi$ to its underlying field operator $\phi \in \mathcal{F}.\text{FieldOp}$ and then identifying the statistic associated with $\phi$.

For a given field specification $\mathcal{F}$ and a creation or annihilation operator $\varphi$, the notation $\mathcal{F} \rhd_s \varphi$ represents the field statistic (bosonic or fermionic) associated with $\varphi$.

Given a field specification $\mathcal{F}$ and a sequence (list) of creation or annihilation operators $\phi$, the notation $\mathcal{F} \rhd_s \phi$ represents the collective field statistic (bosonic or fermionic) associated with the sequence $\phi$. This is calculated by mapping each operator in the list to its respective statistic (as defined by the specification $\mathcal{F}$) and determining the resulting statistic for the entire collection.

The infix notation $\phi \triangleright^c$ denotes the function that maps a creation-annihilation field operator $\phi$ to its status as either a creation or an annihilation operator.