Physlib.QFT.PerturbationTheory.Koszul.KoszulSign

Given a type of fields $\mathcal{F}$, a function $q: \mathcal{F} \to \text{FieldStatistic}$ that assigns a statistic to each field (where $1$ represents a fermion and $0$ a boson), and a decidable ordering relation $\le$ on $\mathcal{F}$, the Koszul sign of a list of fields $L$ is a value in $\mathbb{C}$. It is defined recursively such that the sign of an empty list is $1$, and for any other list, it provides a factor of $-1$ for every fermion-fermion swap required to sort the list according to $\le$.

Given a type of fields $\mathcal{F}$, a function $q: \mathcal{F} \to \text{FieldStatistic}$ that assigns a statistic to each field, and a decidable ordering relation $\le$ on $\mathcal{F}$, the Koszul sign of a singleton list containing only the field $\phi \in \mathcal{F}$ is equal to $1$.

Let $\mathcal{F}$ be a type of fields, $q: \mathcal{F} \to \text{FieldStatistic}$ a function assigning statistics to fields, and $\le$ a decidable ordering relation on $\mathcal{F}$. For any list of fields $L$, the product of the Koszul sign of $L$ with itself is equal to 1. That is, $$\text{koszulSign}(q, \le, L) \cdot \text{koszulSign}(q, \le, L) = 1.$$

Let $\mathcal{F}$ be a type of fields, $q: \mathcal{F} \to \text{FieldStatistic}$ be a function assigning a statistic to each field, and $\le$ be a decidable ordering relation on $\mathcal{F}$. For any field $\phi \in \mathcal{F}$, the Koszul sign of the list containing only that field (represented as an element of the free monoid) is 1. Mathematically: $$\text{koszulSign}(q, \le, [\phi]) = 1$$

Let $\mathcal{F}$ be a type representing fields and $q: \mathcal{F} \to \text{FieldStatistic}$ be a function that assigns a statistic (either bosonic or fermionic) to each field. Let $\le$ be a decidable relation on $\mathcal{F}$. For any field $\phi \in \mathcal{F}$ and any list of fields $\phi_s$, if the field at index $n$ in $\phi_s$ is bosonic, then the Koszul insertion sign of $\phi$ into the list $\phi_s$ with the $n$-th element removed is equal to the Koszul insertion sign of $\phi$ into the original list $\phi_s$. Mathematically, if $q(\phi_s[n]) = \text{bosonic}$, then: $$\text{koszulSignInsert}(q, \le, \phi, \text{eraseIdx}(\phi_s, n)) = \text{koszulSignInsert}(q, \le, \phi, \phi_s)$$

Let $\mathcal{F}$ be a type of fields and $q: \mathcal{F} \to \text{FieldStatistic}$ be a function assigning a statistic (bosonic or fermionic) to each field. Let $\le$ be a decidable ordering relation on $\mathcal{F}$. For any list of fields $\phi_s$ and any index $n$ into that list, if the field at index $n$ is bosonic ($q(\phi_s[n]) = \text{bosonic}$), then the Koszul sign of the list $\phi_s$ with the $n$-th element removed is equal to the Koszul sign of the original list $\phi_s$. Mathematically: $$\text{koszulSign}(q, \le, \text{eraseIdx}(\phi_s, n)) = \text{koszulSign}(q, \le, \phi_s)$$

Let $\mathcal{F}$ be a type of fields, $q: \mathcal{F} \to \text{FieldStatistic}$ be a function assigning statistics to these fields, and $\le$ be a total and transitive ordering relation on $\mathcal{F}$. For any list of fields $\phi_s$, any field $\phi \in \mathcal{F}$, and any index $n \leq \text{length}(\phi_s)$, let $L' = \text{insertIdx}(\phi_s, n, \phi)$ be the list obtained by inserting $\phi$ into $\phi_s$ at position $n$. The Koszul sign of the new list $L'$ is given by: $$\text{koszulSign}(L') = \mathcal{S}(q(\phi), Q(\phi_s|_{<n})) \cdot \text{koszulSign}(\phi_s) \cdot \mathcal{S}(q(\phi), Q(L'_{\text{sorted}}|_{<m}))$$ where: - $\text{koszulSign}(L)$ is the sign factor in $\mathbb{C}$ incurred by sorting list $L$ according to $\le$. - $\mathcal{S}(s_1, s_2)$ is the sign factor associated with the statistics $s_1$ and $s_2$ (typically $(-1)^{s_1 s_2}$). - $Q(L)$ is the aggregate statistic of the fields in list $L$ (calculated via `ofList`). - $\phi_s|_{<n}$ denotes the sublist consisting of the first $n$ elements of $\phi_s$. - $L'_{\text{sorted}}$ is the list $L'$ sorted according to the relation $\le$. - $m$ is the index of the newly inserted field $\phi$ in the sorted list $L'_{\text{sorted}}$.

For any list $r$ and any natural number $n$ such that $n < \text{length}(r)$, let $r_n$ denote the element of $r$ at index $n$. If the element at index $n$ is removed from $r$, and then $r_n$ is inserted back into the resulting list at index $n$, the result is the original list $r$. In mathematical notation, this is expressed as $\text{insertIdx}(\text{eraseIdx}(r, n), n, r_n) = r$.

Let $\mathcal{F}$ be a type of fields, $q: \mathcal{F} \to \text{FieldStatistic}$ be a function assigning statistics to these fields, and $\le$ be a total and transitive ordering relation on $\mathcal{F}$. For any list of fields $\phi_s$ and any index $n < \text{length}(\phi_s)$, let $\phi_n$ denote the element at index $n$ and $\phi_s \setminus \{\phi_n\}$ be the list obtained by erasing this element. The Koszul sign of the resulting list is given by: $$\text{koszulSign}(\phi_s \setminus \{\phi_n\}) = \text{koszulSign}(\phi_s) \cdot \mathcal{S}(q(\phi_n), Q(\phi_s|_{<n})) \cdot \mathcal{S}(q(\phi_n), Q(L_{\text{sorted}}|_{<m}))$$ where: - $\text{koszulSign}(L)$ is the sign factor in $\mathbb{C}$ incurred by sorting list $L$ according to $\le$. - $\mathcal{S}(s_1, s_2)$ is the sign factor associated with the statistics $s_1$ and $s_2$. - $Q(L)$ is the aggregate statistic of the fields in list $L$ (calculated via `ofList`). - $\phi_s|_{<n}$ is the sublist consisting of the first $n$ elements of $\phi_s$. - $L_{\text{sorted}}$ is the list $\phi_s$ sorted according to the relation $\le$. - $m$ is the index of the original $n$-th element $\phi_n$ after the list $\phi_s$ has been sorted.

Let $\mathcal{F}$ be a type of fields equipped with a function $q: \mathcal{F} \to \text{FieldStatistic}$ that assigns a statistic to each field, and let $\le$ be a total and transitive ordering relation on $\mathcal{F}$. For any field $\phi \in \mathcal{F}$ and any list of fields $\phi_s$, let $L$ denote the list formed by prepending $\phi$ to $\phi_s$ (i.e., $L = \phi :: \phi_s$). Let $\phi_{\text{min}}$ be the minimum element of $L$ according to the relation $\le$, and let $n_{\text{min}}$ be the index of this element in $L$. The Koszul sign of the list obtained by erasing the element at index $n_{\text{min}}$ is given by: $$\text{koszulSign}(L \setminus \{\phi_{\text{min}}\}) = \text{koszulSign}(L) \cdot \mathcal{S}(q(\phi_{\text{min}}), Q(L|_{<n_{\text{min}}}))$$ where: - $\text{koszulSign}(L)$ is the sign factor in $\mathbb{C}$ incurred by sorting the list $L$ according to $\le$. - $\mathcal{S}(s_1, s_2)$ is the sign factor associated with the statistics $s_1$ and $s_2$. - $Q(L)$ is the aggregate statistic of the fields in list $L$. - $L|_{<n_{\text{min}}}$ is the sublist consisting of the first $n_{\text{min}}$ elements of $L$.

Let $\mathcal{F}$ be a type of fields, $q : \mathcal{F} \to \text{FieldStatistic}$ a function that assigns a statistic to each field, and $\le$ a decidable ordering relation on $\mathcal{F}$. For any fields $\phi, \psi \in \mathcal{F}$ such that $\phi \le \psi$ and $\psi \le \phi$, and for any list of fields $L$, the Koszul sign of the list formed by prepending $\phi$ and then $\psi$ to $L$ is equal to the Koszul sign of the list formed by prepending $\psi$ and then $\phi$ to $L$: $$\text{koszulSign}(q, \le, \phi :: \psi :: L) = \text{koszulSign}(q, \le, \psi :: \phi :: L)$$

Let $\mathcal{F}$ be a type of fields, $q : \mathcal{F} \to \text{FieldStatistic}$ be a function that assigns a statistic to each field (where $1$ represents a fermion and $0$ a boson), and $\le$ be a decidable ordering relation on $\mathcal{F}$. For any fields $\phi, \psi \in \mathcal{F}$ that are equivalent under the relation (i.e., $\phi \le \psi$ and $\psi \le \phi$), and for any lists of fields $L_1$ and $L_2$, the Koszul sign of the list formed by the concatenation of $L_1$, the elements $\phi, \psi$, and $L_2$ is equal to the Koszul sign of the list where the positions of $\phi$ and $\psi$ are swapped: $$\text{koszulSign}(q, \le, L_1 \mathbin{+\mkern-10mu+} (\phi :: \psi :: L_2)) = \text{koszulSign}(q, \le, L_1 \mathbin{+\mkern-10mu+} (\psi :: \phi :: L_2))$$