Physlib.Relativity.Tensors.ComplexTensor.Vector.Pre.Modules

This equivalence relates the module of contravariant complex Lorentz vectors, `ContrℂModule`, to the space of functions from the spacetime index set $\{0, 1, 2, 3\}$ (represented as the direct sum $\text{Fin } 1 \oplus \text{Fin } 3$) to the complex numbers $\mathbb{C}$. The mapping identifies a Lorentz vector with its four complex components $v^\mu$.

The module of contravariant complex Lorentz vectors, denoted as $\text{Contr}\mathbb{C}\text{Module}$, is equipped with the structure of an additive commutative monoid. This structure is induced by the equivalence between $\text{Contr}\mathbb{C}\text{Module}$ and the space of complex-valued functions $(\text{Fin } 1 \oplus \text{Fin } 3) \to \mathbb{C}$, where addition and the zero element are defined pointwise.

The module of complex contravariant Lorentz vectors, denoted as $\text{Contr}\mathbb{C}\text{Module}$, is equipped with the structure of an additive commutative group. This structure is induced by the equivalence between $\text{Contr}\mathbb{C}\text{Module}$ and the space of complex-valued functions over spacetime indices $(\text{Fin } 1 \oplus \text{Fin } 3) \to \mathbb{C}$, where the group operations (addition, negation, and the zero element) are defined component-wise.

The type of contravariant complex Lorentz vectors, denoted as $\text{Contr}\mathbb{C}\text{Module}$, is equipped with the structure of a module over the field of complex numbers $\mathbb{C}$. This module structure is induced by the equivalence between $\text{Contr}\mathbb{C}\text{Module}$ and the space of functions $(\text{Fin } 1 \oplus \text{Fin } 3) \to \mathbb{C}$, representing the four components of a Lorentz vector. Under this structure, scalar multiplication by $c \in \mathbb{C}$ is performed component-wise.

Let $\text{Contr}\mathbb{C}\text{Module}$ denote the module of complex contravariant Lorentz vectors. For any two vectors $\psi, \psi' \in \text{Contr}\mathbb{C}\text{Module}$, if their underlying values (components) are equal, i.e., $\psi.\text{val} = \psi'.\text{val}$, then the vectors themselves are equal: $\psi = \psi'$.

For any two contravariant complex Lorentz vectors $\psi$ and $\psi'$ in $\text{Contr}\mathbb{C}\text{Module}$, the underlying value of their sum is equal to the sum of their individual underlying values, expressed as $(\psi + \psi').\text{val} = \psi.\text{val} + \psi'.\text{val}$.

Let $\text{Contr}\mathbb{C}\text{Module}$ denote the module of complex contravariant Lorentz vectors. For any complex scalar $r \in \mathbb{C}$ and any vector $\psi \in \text{Contr}\mathbb{C}\text{Module}$, the underlying value of the scalar multiplication $r \cdot \psi$ is equal to the scalar multiplication of $r$ with the underlying value of $\psi$, expressed as $(r \cdot \psi).\text{val} = r \cdot \psi.\text{val}$.

This definition establishes a $\mathbb{C}$-linear equivalence (isomorphism of modules) between the module of complex contravariant Lorentz vectors, denoted as $\text{Contr}\mathbb{C}\text{Module}$, and the space of complex-valued functions over the spacetime index set $\text{Fin } 1 \oplus \text{Fin } 3 \to \mathbb{C}$. This mapping identifies a Lorentz vector with its four complex components $v^\mu$ in a way that preserves both addition and scalar multiplication by elements of $\mathbb{C}$.

For a complex contravariant Lorentz vector $\psi$ in the module $\text{Contr}\mathbb{C}\text{Module}$, this function returns its representation as a complex-valued function over the spacetime index set $(\text{Fin } 1 \oplus \text{Fin } 3) \to \mathbb{C}$ by applying the linear equivalence $\text{toFin13}\mathbb{C}\text{Equiv}$. Effectively, it maps the abstract vector to its four complex components $v^\mu$.

This definition establishes the group representation of the Lorentz group $\text{LorentzGroup } 3$ on the module of complex contravariant Lorentz vectors $\text{Contr}\mathbb{C}\text{Module}$ over the complex numbers $\mathbb{C}$. For a group element $M$ and a vector $v \in \text{Contr}\mathbb{C}\text{Module}$, the action is defined by converting $v$ to its component representation in $\mathbb{C}^4$, multiplying it by the complex matrix associated with $M$, and then mapping the resulting vector back to the module $\text{Contr}\mathbb{C}\text{Module}$ using the linear equivalence $\text{toFin13}\mathbb{C}\text{Equiv}$.

This definition establishes the group representation of $SL(2, \mathbb{C})$ on the complex module of contravariant Lorentz vectors $\text{Contr}\mathbb{C}\text{Module}$. The representation is constructed by pulling back the representation of the Lorentz group $\text{LorentzGroup } 3$ on $\text{Contr}\mathbb{C}\text{Module}$ along the group homomorphism from $SL(2, \mathbb{C})$ to the Lorentz group. Specifically, for an element $A \in SL(2, \mathbb{C})$, its action on a vector is given by the Lorentz transformation corresponding to $A$ acting on that vector.

The equivalence identifies the module of complex covariant Lorentz vectors, $\text{Co}\mathbb{C}\text{Module}$, with the space of complex-valued functions defined on the spacetime index set $\text{Fin } 1 \oplus \text{Fin } 3$. This map associates a covariant vector with its components in $\mathbb{C}^4$, where the index set distinguishes the temporal component ($\text{Fin } 1$) and the spatial components ($\text{Fin } 3$).

The space of complex covariant Lorentz vectors, denoted as $\text{Co}\mathbb{C}\text{Module}$, is equipped with the structure of an additive commutative monoid. This structure is induced by the equivalence between $\text{Co}\mathbb{C}\text{Module}$ and the space of complex-valued functions on the spacetime index set $\text{Fin } 1 \oplus \text{Fin } 3 \to \mathbb{C}$.

The space of complex covariant Lorentz vectors, denoted as $\text{Co}\mathbb{C}\text{Module}$, is equipped with an additive commutative group structure. This structure is induced by the equivalence between $\text{Co}\mathbb{C}\text{Module}$ and the space of complex-valued functions on the spacetime index set, $(\text{Fin } 1 \oplus \text{Fin } 3) \to \mathbb{C}$.

The space of complex covariant Lorentz vectors, denoted as $\text{Co}\mathbb{C}\text{Module}$, is equipped with a module structure over the field of complex numbers $\mathbb{C}$. This $\mathbb{C}$-module structure is induced by the equivalence between $\text{Co}\mathbb{C}\text{Module}$ and the space of complex-valued functions on the spacetime index set, $(\text{Fin } 1 \oplus \text{Fin } 3) \to \mathbb{C}$.

The linear equivalence between the module of complex covariant Lorentz vectors, $\text{Co}\mathbb{C}\text{Module}$, and the space of complex-valued functions defined on the spacetime index set, $(\text{Fin } 1 \oplus \text{Fin } 3) \to \mathbb{C}$. This map provides a $\mathbb{C}$-linear identification between a covariant vector and its components in $\mathbb{C}^4$, where the index set $\text{Fin } 1 \oplus \text{Fin } 3$ distinguishes the temporal and spatial components.

Given a complex covariant Lorentz vector $\psi$ in the module $\text{Co}\mathbb{C}\text{Module}$, this function returns its representation as a complex-valued function on the spacetime index set $(\text{Fin } 1 \oplus \text{Fin } 3) \to \mathbb{C}$. This is achieved by applying the $\mathbb{C}$-linear equivalence $\text{toFin13ℂEquiv}$ to $\psi$, effectively identifying the vector with its components in $\mathbb{C}^4$ where the indices distinguish temporal and spatial parts.

This definition constructs the representation of the Lorentz group $O(1, 3)$ on the space of complex covariant Lorentz vectors $\text{Co}\mathbb{C}\text{Module}$. For a group element $M \in O(1, 3)$, the representation maps $M$ to a linear endomorphism of $\text{Co}\mathbb{C}\text{Module}$. The action of $M$ on a vector $\psi$ is defined by transforming its components in $\mathbb{C}^4$ through multiplication by the inverse transpose of the complex matrix representation of $M$, denoted as $(M^{-1})^T$. This ensures that the vector transforms covariantly with respect to the spacetime indices.

This definition constructs the representation of the group $SL(2, \mathbb{C})$ on the space of complex covariant Lorentz vectors, denoted as $\text{Co}\mathbb{C}\text{Module}$. The representation is defined by the composition of the representation of the Lorentz group on $\text{Co}\mathbb{C}\text{Module}$ (where vectors transform via the inverse transpose of the Lorentz matrix) and the standard group homomorphism from $SL(2, \mathbb{C})$ to the Lorentz group $O(1, 3)$.