Physlib.Relativity.Tensors.RealTensor.CoVector.Basic

For any natural number $d$ representing spatial dimensions, the type of Lorentz covectors $\text{CoVector}(d)$, which are functions mapping the indices of a $(1+d)$-dimensional spacetime to the real numbers $\mathbb{R}$, is equipped with the structure of an additive commutative monoid. This implies that covectors can be added together associatively and commutatively, and there exists a zero covector serving as the additive identity.

For any natural number $d$ representing spatial dimensions, the space of Lorentz covectors $\text{CoVector}(d)$, defined as real-valued functions on the indices of a $(1+d)$-dimensional spacetime, is equipped with the structure of a vector space (module) over the real numbers $\mathbb{R}$.

For any natural number $d$ representing the number of spatial dimensions, the space of Lorentz covectors $\text{CoVector}(d)$ in a $(1+d)$-dimensional spacetime is equipped with the structure of an additive commutative group. This implies that for any two covectors, their sum is well-defined and commutative, there exists a zero covector serving as the additive identity, and every covector has a corresponding additive inverse.

For any natural number $d$ representing the number of spatial dimensions, the space of Lorentz covectors $\text{CoVector}(d)$ in a $(1+d)$-dimensional spacetime is a finite-dimensional vector space over the real numbers $\mathbb{R}$.

For a natural number $d$ representing the number of spatial dimensions, there exists a linear isomorphism between the space of Lorentz covectors $\text{CoVector}(d)$ and the Euclidean space $\mathbb{R}^{1 \oplus d}$ (represented as `EuclideanSpace ℝ (Fin 1 ⊕ Fin d)`). This isomorphism allows a Lorentz covector in $(1+d)$-dimensional spacetime to be treated as an element of a standard real Euclidean vector space.

For a natural number $d$ representing the number of spatial dimensions, the space of Lorentz covectors $\text{CoVector}(d)$ is equipped with a norm structure $\|\cdot\|$. The norm of a covector $v \in \text{CoVector}(d)$ is defined as the Euclidean norm of its image under the linear isomorphism $\text{equivEuclid} : \text{CoVector}(d) \cong \mathbb{R}^{1+d}$.

For a natural number $d$ representing the number of spatial dimensions and any Lorentz covector $v \in \text{CoVector}(d)$, the norm $\|v\|$ is equal to the Euclidean norm of its image under the linear isomorphism $\text{equivEuclid}_d : \text{CoVector}(d) \cong \mathbb{R}^{1+d}$.

For a natural number $d$ representing the number of spatial dimensions, the space of Lorentz covectors $\text{CoVector}(d)$ in a $(1+d)$-dimensional spacetime is a normed additive commutative group. This structure equips the additive group of covectors with a norm $\|\cdot\|$, such that it becomes a metric space where the distance between any two covectors $v, w \in \text{CoVector}(d)$ is given by the norm of their difference, $\|v - w\|$. The norm is defined via the standard isomorphism to $(1+d)$-dimensional Euclidean space.

For a natural number $d$ representing the number of spatial dimensions, the space of Lorentz covectors $\text{CoVector}(d)$ in a $(1+d)$-dimensional spacetime is a normed vector space over the real numbers $\mathbb{R}$. This structure equips the space with a norm $\|\cdot\|$ that is compatible with scalar multiplication, such that $\|c v\| = |c| \|v\|$ for any scalar $c \in \mathbb{R}$ and covector $v \in \text{CoVector}(d)$. The norm is defined via the standard linear isomorphism to the $(1+d)$-dimensional Euclidean space.

For a natural number $d$ representing the spatial dimensions, the space of Lorentz covectors $\text{CoVector}(d)$ is equipped with a real-valued inner product $\langle \cdot, \cdot \rangle$. For any two covectors $v, w \in \text{CoVector}(d)$, the inner product is defined as $\langle v, w \rangle = \langle \phi(v), \phi(w) \rangle_{\text{Euclidean}}$, where $\phi: \text{CoVector}(d) \cong \mathbb{R}^{1+d}$ is the standard linear isomorphism from the space of covectors to the $(1+d)$-dimensional Euclidean space.

For any natural number $d$ representing the number of spatial dimensions and any two Lorentz covectors $v, w \in \text{CoVector}(d)$, the real inner product $\langle v, w \rangle_{\mathbb{R}}$ is equal to the Euclidean inner product of their images under the linear isomorphism $\phi: \text{CoVector}(d) \cong \mathbb{R}^{1+d}$ (where $\phi$ corresponds to the mapping `equivEuclid`).

For any natural number $d$ representing the number of spatial dimensions, the space of Lorentz covectors $\text{CoVector}(d)$ in a $(1+d)$-dimensional spacetime is a real inner product space. This structure equips the space with a real-valued inner product $\langle \cdot, \cdot \rangle$ that is consistent with the Euclidean inner product on $\mathbb{R}^{1+d}$ via the standard linear isomorphism $\phi: \text{CoVector}(d) \cong \mathbb{R}^{1+d}$. Specifically, for any $v, w \in \text{CoVector}(d)$, the inner product is defined as $\langle v, w \rangle = \langle \phi(v), \phi(w) \rangle_{\text{Euclidean}}$, satisfying the requirement that $\|v\|^2 = \langle v, v \rangle$.

For a natural number $d$, the space of Lorentz covectors $\text{CoVector}(d)$ in a $(1+d)$-dimensional spacetime is a charted space modeled on itself. This structure provides the space with a trivial manifold atlas consisting of the identity map from $\text{CoVector}(d)$ to itself.

For a natural number $d$, a Lorentz covector $v \in \text{CoVector}(d)$ is coerced to a function mapping an index $i \in \{0, 1, \dots, d\}$ (represented by the type $\text{Fin } 1 \oplus \text{Fin } d$) to its corresponding real-valued component $v_i \in \mathbb{R}$.

Let $d$ be a natural number representing the number of spatial dimensions. For any real scalar $c \in \mathbb{R}$, Lorentz covector $v \in \text{CoVector}(d)$, and spacetime index $i \in \text{Fin } 1 \oplus \text{Fin } d$, the $i$-th component of the scalar multiple $c \cdot v$ is equal to the product of $c$ and the $i$-th component of $v$, denoted as $(c \cdot v)_i = c \cdot v_i$.

Let $d$ be a natural number representing the number of spatial dimensions. For any Lorentz covectors $v, w \in \text{CoVector}(d)$ and any spacetime index $i \in \text{Fin } 1 \oplus \text{Fin } d$, the $i$-th component of the sum $v + w$ is equal to the sum of the $i$-th components of $v$ and $w$, denoted as $(v + w)_i = v_i + w_i$.

Let $d$ be a natural number representing the number of spatial dimensions. For any Lorentz covectors $v, w \in \text{CoVector}(d)$ and any spacetime index $i \in \text{Fin } 1 \oplus \text{Fin } d$, the $i$-th component of the difference $v - w$ is equal to the difference of the $i$-th components of $v$ and $w$, denoted as $(v - w)_i = v_i - w_i$.

Let $d$ be a natural number representing the number of spatial dimensions. For any Lorentz covector $v \in \text{CoVector}(d)$ and any spacetime index $i \in \text{Fin } 1 \oplus \text{Fin } d$, the $i$-th component of the additive inverse of $v$ is equal to the negation of the $i$-th component of $v$, denoted as $(-v)_i = -v_i$.

For any natural number $d$, the $i$-th component of the zero Lorentz covector $0 \in \text{CoVector}(d)$ is $0$, where $i \in \text{Fin } 1 \oplus \text{Fin } d$ is the spacetime index.

Given a spacetime with $d$ spatial dimensions, the component indices of a Lorentz covector (a tensor with a single "down" index) are equivalent to the sum type $\text{Fin } 1 \oplus \text{Fin } d$. This equivalence maps the spacetime index $\mu \in \{0, \dots, d\}$ to either a temporal index (represented by $\text{Fin } 1$) or a spatial index (represented by $\text{Fin } d$).

For a natural number $d$ representing spatial dimensions, the space of Lorentz covectors $\text{CoVector}(d)$ is canonically equivalent to the space of real Lorentz tensors with a single covariant (down) index. This "tensorial" property provides a linear equivalence between the type $\text{CoVector}(d)$ and the tensor space defined by the species $\text{realLorentzTensor}(d)$ and the index list $[\text{down}]$. The equivalence is constructed by identifying the components of a covector with the coefficients of the tensor in its canonical basis, utilizing the index equivalence between the tensor's component indices and the spacetime indices $\text{Fin } 1 \oplus \text{Fin } d$.

For a $(1+d)$-dimensional spacetime, let $p$ be a real Lorentz tensor with a single covariant (down) index. The covector corresponding to $p$ (obtained via the inverse of the canonical linear equivalence `toTensor`) is the function that assigns to each spacetime index $\mu \in \text{Fin } 1 \oplus \text{Fin } d$ the coefficient of $p$ in its canonical tensor basis. This value is determined by mapping the spacetime index $\mu$ to the corresponding tensor component index via the equivalence `indexEquiv`.

In a spacetime with $d$ spatial dimensions, let $p$ be a pure Lorentz tensor of rank 1 with a single down (covariant) index. For any spacetime index $i \in \text{Fin } 1 \oplus \text{Fin } d$, the $i$-th component of the Lorentz covector obtained by the inverse of the canonical linear equivalence $\text{toTensor}^{-1}(p.\text{toTensor})$ is equal to the coordinate of the constituent vector $p(0)$ at the index corresponding to $i$.

For a $(1+d)$-dimensional spacetime with $d$ spatial dimensions, the standard basis for the vector space of Lorentz covectors $\text{CoVector}(d)$ over $\mathbb{R}$ is indexed by the set of spacetime indices $\mu \in \{0\} \cup \{1, \dots, d\}$ (represented by the type $\text{Fin } 1 \oplus \text{Fin } d$). This basis consists of covectors $e_\mu$ such that their components satisfy $(e_\mu)_\nu = \delta_{\mu\nu}$, where $\delta_{\mu\nu}$ is the Kronecker delta.

In a $(1+d)$-dimensional spacetime, let $\{e_\mu\}$ be the standard basis for the space of Lorentz covectors $\text{CoVector}(d)$, where $\mu$ and $\nu$ are spacetime indices in $\{0, 1, \dots, d\}$. The $\nu$-th component of the $\mu$-th basis covector is given by the Kronecker delta $\delta_{\mu\nu}$: \[ (e_\mu)_\nu = \begin{cases} 1 & \text{if } \mu = \nu \\ 0 & \text{if } \mu \neq \nu \end{cases} \]

In a $(1+d)$-dimensional spacetime, let $\Phi: \text{CoVector}(d) \cong \text{Tensor}_{\text{down}}$ be the canonical linear equivalence between the space of Lorentz covectors and the space of real Lorentz tensors with a single covariant (down) index. For any spacetime index $\mu \in \{0, \dots, d\}$, let $e_\mu$ be the $\mu$-th element of the standard basis for covectors, and let $E_{i_\mu}$ be the basis element of the tensor space corresponding to the component index $i_\mu$ associated with $\mu$. The theorem states that the inverse of the linear equivalence maps the tensor basis element to the covector basis element: \[ \Phi^{-1}(E_{i_\mu}) = e_\mu \]

In a $(1+d)$-dimensional spacetime, let $\Phi: \text{CoVector}(d) \cong \text{Tensor}_{\text{down}}$ be the canonical linear equivalence between the space of Lorentz covectors and the space of real Lorentz tensors with a single covariant (down) index. For any spacetime index $\mu \in \{0, \dots, d\}$, let $e_\mu$ be the $\mu$-th element of the standard basis for covectors, and let $E_{i_\mu}$ be the basis element of the tensor space corresponding to the component index $i_\mu$ associated with $\mu$ via the index equivalence. The theorem states that the image of the covector basis element under the isomorphism is the corresponding tensor basis element: \[ \Phi(e_\mu) = E_{i_\mu} \]

In a $(1+d)$-dimensional spacetime, let $\text{basis}$ be the standard basis for the space of Lorentz covectors $\text{CoVector}(d)$ indexed by spacetime indices $\mu \in \text{Fin } 1 \oplus \text{Fin } d$. Let $\text{Tensor.basis}$ be the canonical basis for the space of real Lorentz tensors with a single covariant (down) index, indexed by component indices $i$. Let $\Phi: \text{CoVector}(d) \cong \text{Tensor}_{\text{down}}$ be the canonical linear equivalence (isomorphism) between these spaces. The theorem states that the covector basis is equal to the tensor basis transformed by the inverse isomorphism $\Phi^{-1}$ and reindexed according to the equivalence $\text{indexEquiv}$ between component indices and spacetime indices: \[ \text{basis} = \text{reindex}(\Phi^{-1}(\text{Tensor.basis}), \text{indexEquiv}) \] Specifically, for any spacetime index $\mu$, the $\mu$-th basis covector $e_\mu$ is given by $\Phi^{-1}(E_{i_\mu})$, where $E_{i_\mu}$ is the basis tensor corresponding to the component index $i_\mu = \text{indexEquiv}^{-1}(\mu)$.

In a $(1+d)$-dimensional spacetime, let $\Phi: \text{CoVector}(d) \cong \text{Tensor}_{\text{down}}$ be the canonical linear equivalence (isomorphism) between the space of Lorentz covectors and the space of real Lorentz tensors with a single covariant (down) index. Let $\mathcal{B}_{\text{tensor}} = \{E_i\}$ be the canonical basis for the tensor space indexed by component indices $i$, and let $\mathcal{B}_{\text{covector}} = \{e_\mu\}$ be the standard basis for covectors indexed by spacetime indices $\mu \in \text{Fin } 1 \oplus \text{Fin } d$. Let $\psi: \text{ComponentIdx} \cong \text{Fin } 1 \oplus \text{Fin } d$ be the equivalence between these index types. The theorem states that applying the inverse isomorphism $\Phi^{-1}$ to the tensor basis is equivalent to reindexing the covector basis by the inverse index equivalence $\psi^{-1}$. That is: \[ \Phi^{-1}(E_i) = e_{\psi(i)} \] for every component index $i$.

In a $(1+d)$-dimensional spacetime, let $p$ be a Lorentz covector and let $\text{toTensor}(p)$ be its representation as a rank-1 tensor with a single "down" (covariant) index. For any tensor component index $\mu$, the $\mu$-th coordinate of $\text{toTensor}(p)$ with respect to the canonical tensor basis is equal to the value of the covector $p$ at the spacetime index corresponding to $\mu$ under the equivalence $\text{indexEquiv}$.

For any Lorentz covector $p$ in a $(1+d)$-dimensional spacetime and for any spacetime index $\mu \in \{0, 1, \dots, d\}$, the $\mu$-th component of $p$ with respect to the standard basis is equal to the value of the covector evaluated at that index, denoted $p_\mu$.

In a $(1+d)$-dimensional spacetime, let $\text{CoVector}(d)$ be the vector space of Lorentz covectors over $\mathbb{R}$ equipped with its standard basis. For any linear map $f: \text{CoVector}(d) \to \text{CoVector}(d)$ and any covector $p \in \text{CoVector}(d)$, the application of the map $f(p)$ is equal to the matrix-vector product $M \cdot p$, where $M$ is the matrix representation of $f$ with respect to the standard basis.

In a $(1+d)$-dimensional spacetime, for any Lorentz transformation $\Lambda \in \text{LorentzGroup}(d)$ and any Lorentz covector $p \in \text{CoVector}(d)$, the $i$-th component of the transformed covector $\Lambda \cdot p$ is equal to the sum over all spacetime indices $j$ of the product of the $(j, i)$-th entry of the inverse Lorentz transformation matrix $\Lambda^{-1}$ and the $j$-th component of $p$: $$(\Lambda \cdot p)_i = \sum_{j} (\Lambda^{-1})_{ji} p_j$$ where $(\Lambda^{-1})_{ji}$ denotes the entry at row $j$ and column $i$ of the matrix representation of $\Lambda^{-1}$.

In a $(1+d)$-dimensional spacetime, let $\Lambda \in \text{LorentzGroup}(d)$ be a Lorentz transformation and $p \in \text{CoVector}(d)$ be a Lorentz covector. The action of the Lorentz group on the covector, denoted $\Lambda \cdot p$, is equal to the matrix-vector product of the transpose of the inverse of $\Lambda$ and the covector $p$: $$\Lambda \cdot p = (\Lambda^{-1})^\intercal p$$ where $(\Lambda^{-1})^\intercal$ denotes the transpose of the matrix representation of the inverse Lorentz transformation $\Lambda^{-1}$.

In a $(1+d)$-dimensional spacetime, for any Lorentz transformation $\Lambda \in \text{LorentzGroup}(d)$ and any two Lorentz covectors $p, q \in \text{CoVector}(d)$, the action of the Lorentz group distributes over covector addition such that $\Lambda \cdot (p + q) = \Lambda \cdot p + \Lambda \cdot q$.

In a $(1+d)$-dimensional spacetime, for any Lorentz transformation $\Lambda \in \text{LorentzGroup}(d)$ and any two Lorentz covectors $p, q \in \text{CoVector}(d)$, the action of the Lorentz group distributes over covector subtraction such that $$\Lambda \cdot (p - q) = \Lambda \cdot p - \Lambda \cdot q$$

In a $(1+d)$-dimensional spacetime, for any Lorentz transformation $\Lambda \in \text{LorentzGroup}(d)$, the action of the Lorentz group on the zero covector $0 \in \text{CoVector}(d)$ results in the zero covector: $$\Lambda \cdot 0 = 0$$

For any natural number $d$, given a Lorentz transformation $\Lambda \in \text{LorentzGroup}(d)$ and a Lorentz covector $p \in \text{CoVector}(d)$, the action of $\Lambda$ on the additive inverse of $p$ is equal to the additive inverse of the action of $\Lambda$ on $p$: $$\Lambda \cdot (-p) = -(\Lambda \cdot p)$$

Given a Lorentz transformation $\Lambda \in \text{LorentzGroup}(d)$ acting on a $(1+d)$-dimensional spacetime, the function $\text{actionCLM}(\Lambda)$ is the continuous linear map from the space of Lorentz covectors $\text{CoVector}(d)$ to itself, defined by the group action $v \mapsto \Lambda \cdot v$. This map satisfies the properties of a linear operator over the real numbers $\mathbb{R}$.

Let $d$ be a natural number representing the number of spatial dimensions. For any Lorentz transformation $\Lambda \in \text{LorentzGroup}(d)$ and any Lorentz covector $p \in \text{CoVector}(d)$, the application of the continuous linear map $\text{actionCLM}(\Lambda)$ to $p$ is equal to the Lorentz group action $\Lambda \cdot p$.

In a $(1+d)$-dimensional spacetime, let $\{e_\mu\}$ be the standard basis for the space of Lorentz covectors $\text{CoVector}(d)$, where $\mu$ and $\nu$ are spacetime indices in $\{0, 1, \dots, d\}$. For any Lorentz transformation $\Lambda \in \text{LorentzGroup}(d)$, the action of $\Lambda$ on the $\mu$-th basis covector $e_\mu$ is given by the linear combination: $$\Lambda \cdot e_\mu = \sum_{\nu} (\Lambda^{-1})_{\mu\nu} e_\nu$$ where $(\Lambda^{-1})_{\mu\nu}$ denotes the component at row $\mu$ and column $\nu$ of the matrix representation of the inverse Lorentz transformation $\Lambda^{-1}$.