Physlib.Relativity.Tensors.ComplexTensor.Basic

The inductive type `complexLorentzTensor.Color` represents the set of labels, or "colors," assigned to the various complex representations of the group $SL(2, \mathbb{C})$ used in relativistic physics. These colors identify the specific representation space to which a tensor index belongs, such as the standard contravariant and covariant Lorentz vector representations denoted by `Color.up` and `Color.down`.

The equality of any two representation labels (or "colors") $c_1, c_2$ in the type `complexLorentzTensor.Color` is decidable. This means there is an algorithmic procedure to determine whether two indices belong to the same representation of $SL(2, \mathbb{C})$, specifically distinguishing between left-handed spinors ($\text{upL}, \text{downL}$), right-handed spinors ($\text{upR}, \text{downR}$), and Lorentz vectors ($\text{up}, \text{down}$).

The structure `complexLorentzTensor` defines the **tensor species** for complex Lorentz tensors over the field $\mathbb{C}$ with the symmetry group $SL(2, \mathbb{C})$. It specifies a systematic framework for tensors whose indices belong to various representations of $SL(2, \mathbb{C})$, organized by "colors": - **Weyl Spinors**: Includes left-handed ($L$) and right-handed ($R$) representations of dimension 2, along with their associated "alt" (dual/conjugate) representations. - **Lorentz Vectors**: Includes the standard contravariant (up) and covariant (down) representations of dimension 4. For each index type, the definition provides: 1. The associated representation space $V$ (e.g., `Fermion.leftHanded` or `Lorentz.complexContr`). 2. An involution $\tau$ that pairs dual index types (e.g., $\text{up} \leftrightarrow \text{down}$ and $\text{upL} \leftrightarrow \text{downL}$). 3. Canonical contraction morphisms (intertwining operators) $V \otimes V^* \to \mathbb{C}$. 4. Invariant metrics (such as the Minkowski metric $\eta_{\mu\nu}$ for vectors and the $\epsilon$ tensor for spinors) and unit tensors (Kronecker deltas $\delta^\mu_\nu$). 5. Standard bases for the underlying vector spaces.

The syntax $\mathbb{C}T[t_1, t_2, \dots, t_n]$ defines a notation for representing a complex Lorentz tensor constructed from a sequence of terms $t_1, t_2, \dots, t_n$.

For a given representation type $c$ (referred to as a "color"), the notation $\mathbb{C}T(c)$ denotes the space of complex-valued Lorentz tensors of that type. In the context of the Lorentz group, $c$ typically specifies the index structure, such as vector indices (up or down) or spinor indices.

In the context of the complex Lorentz tensor species, let $c$ be a representation color (such as a Lorentz vector or Weyl spinor index type) and $\tau(c)$ be its dual color. Let $\{e_i\}$ be the standard basis for the representation space associated with $c$, and $\{e^*_j\}$ be the standard basis for the dual representation space associated with $\tau(c)$. The contraction of the tensor product of two basis elements $e_i \otimes e^*_j$ yields 1 if the indices are equal and 0 otherwise: $$\text{contr}(e_i \otimes e^*_j) = \delta_{ij}$$ where $\delta_{ij}$ is the Kronecker delta.

For any natural number $n$ and any function $c : \{0, \dots, n-1\} \to \text{Color}$ that assigns $SL(2, \mathbb{C})$ representation colors to indices, the domain of the corresponding object in the over color category (which is the finite set $\{0, \dots, n-1\}$) has decidable equality.

For any natural number $n$ and any function $c: \{0, \dots, n-1\} \to \text{Color}$ that assigns $SL(2, \mathbb{C})$ representation colors to indices, the domain of the corresponding object in the over-color category (which is the set of indices $\{0, \dots, n-1\}$) is a finite type.

For any natural numbers $n$ and $m$, and any functions $c: \{0, \dots, n-1\} \to \text{Color}$ and $c_1: \{0, \dots, m-1\} \to \text{Color}$ that assign $SL(2, \mathbb{C})$ representation colors to indices, the equality of any two morphisms $\sigma, \sigma'$ between the corresponding objects in the over-color category $\text{OverColor.mk } c$ and $\text{OverColor.mk } c_1$ is decidable.

For any index $i \in \{0, 1, 2, 3\}$, the $i$-th basis vector of the contravariant Lorentz representation (labeled as `Color.up`) within the `complexLorentzTensor` species is equal to the $i$-th vector of the standard complex contravariant Lorentz basis, denoted as $\text{complexContrBasisFin4}_i$.

For any index $i \in \{0, 1, 2, 3\}$, the $i$-th basis vector of the covariant Lorentz representation (labeled as `Color.down`) within the `complexLorentzTensor` species is equal to the $i$-th vector of the standard complex covariant Lorentz basis, denoted as $\text{complexCoBasisFin4}_i$.

In the `complexLorentzTensor` species, the basis defined for the contravariant Lorentz representation (associated with the color `Color.up`) is identical to the standard basis for complex contravariant Lorentz vectors, $\text{complexContrBasisFin4}$.

The basis for the covariant Lorentz representation (identified by the color `Color.down`) within the `complexLorentzTensor` species is equal to the standard basis for complex covariant Lorentz vectors, denoted by $\text{complexCoBasisFin4}$.

For any group element $\Lambda \in SL(2, \mathbb{C})$, the representation map $\rho(\Lambda)$ associated with the contravariant vector color `Color.up` in the `complexLorentzTensor` species is equal to the representation map of the complex contravariant Lorentz representation `Lorentz.complexContr`.

For any group element $\Lambda \in SL(2, \mathbb{C})$, the representation map $\rho(\Lambda)$ associated with the covariant vector color `Color.down` in the `complexLorentzTensor` species is equal to the representation map of the complex covariant Lorentz representation `Lorentz.complexCo`.

For any index $i \in \{0, 1\}$, the $i$-th basis vector associated with the contravariant left-handed spinor color (`Color.upL`) in the complex Lorentz tensor species is equal to the $i$-th element of the standard left-handed fermion basis: $$\text{basis}_{\text{upL}}(i) = \text{basis}_{\text{left}}(i)$$

For any index $i \in \{0, 1\}$, the $i$-th basis vector associated with the covariant left-handed spinor color (`Color.downL`) in the complex Lorentz tensor species is equal to the $i$-th element of the standard alternative left-handed fermion basis: $$\text{basis}_{\text{downL}}(i) = \text{basis}_{\text{altLeft}}(i)$$

For any index $i \in \{0, 1\}$, the $i$-th basis vector associated with the contravariant right-handed spinor color (`Color.upR`) in the complex Lorentz tensor species is equal to the $i$-th element of the standard right-handed fermion basis: $$\text{basis}_{\text{upR}}(i) = \text{basis}_{\text{right}}(i)$$

For any index $i \in \{0, 1\}$, the $i$-th basis vector associated with the covariant right-handed spinor color ($\text{Color.downR}$) in the complex Lorentz tensor species is equal to the $i$-th element of the standard alternative right-handed fermion basis: $$\text{basis}_{\text{downR}}(i) = \text{basis}_{\text{altRight}}(i)$$

For any element $\Lambda \in SL(2, \mathbb{C})$, let $\rho(\Lambda)$ denote the representation of $\Lambda$ acting on the space of complex contravariant Lorentz vectors (associated with the label `Color.up`). Given the standard basis $\{e_0, e_1, e_2, e_3\}$ for this space, for any indices $b, i \in \{0, 1, 2, 3\}$, the $i$-th component of the transformed basis vector $\rho(\Lambda)e_b$ is equal to the $(i, b)$ entry of the complex Lorentz transformation matrix $L(\Lambda)$ corresponding to $\Lambda$. Mathematically, this is expressed as: $$[\rho(\Lambda) e_b]_i = L(\Lambda)_{ib}$$ where the indices $i$ and $b$ on the right-hand side are mapped to the spacetime coordinate system $\{0, 1, 2, 3\}$ via the standard equivalence between $\text{Fin } 4$ and $\text{Fin } 1 \oplus \text{Fin } 3$.

Suppose $c_0$ is a representation color such that $c_0 = \text{Color.up}$ (the color associated with complex contravariant Lorentz vectors). For any element $\Lambda \in SL(2, \mathbb{C})$, let $\rho(\Lambda)$ be the representation of $\Lambda$ acting on the vector space corresponding to $c_0$. Given the standard basis $\{e_b\}$ for this space, for any indices $b$ and $i$, the $i$-th component of the transformed basis vector $\rho(\Lambda)e_b$ is equal to the $(i, b)$ entry of the complex Lorentz transformation matrix $L(\Lambda)$ corresponding to $\Lambda$. Mathematically, this is expressed as: $$[\rho(\Lambda) e_b]_i = L(\Lambda)_{ib}$$ where the indices $i$ and $b$ are mapped to the spacetime coordinate system $\{0, 1, 2, 3\}$ via the standard equivalence between $\text{Fin } 4$ and $\text{Fin } 1 \oplus \text{Fin } 3$.

For any element $\Lambda \in SL(2, \mathbb{C})$ and indices $b, i \in \{0, 1, 2, 3\}$, let $e_b$ be the $b$-th basis vector of the covariant Lorentz representation space (associated with the color `Color.down`). The $i$-th component of the transformed vector $\rho(\Lambda) e_b$ in this basis is given by the $(b, i)$-th entry of the inverse complexified Lorentz matrix $M(\Lambda)^{-1}$, where $M(\Lambda)$ is the Lorentz group element corresponding to $\Lambda$.

Let $c_0$ be a representation color equal to $\text{Color.down}$, which designates the covariant Lorentz vector representation space $V$. For any element $\Lambda \in SL(2, \mathbb{C})$, let $\rho(\Lambda): V \to V$ be the corresponding representation operator. Given indices $b, i \in \{0, 1, 2, 3\}$, let $e_b$ be the $b$-th vector of the standard basis for $V$. The $i$-th component of the transformed basis vector $\rho(\Lambda) e_b$ is given by the $(b, i)$-th entry of the inverse complexified Lorentz matrix $M(\Lambda)^{-1}$, where $M(\Lambda)$ is the Lorentz group matrix associated with $\Lambda$.