Physlib.Relativity.Tensors.Tensorial

For any tensor species $S$ and any index configuration $c: \{0, \dots, n-1\} \to C$, the module of tensors $S.\text{Tensor } c$ is equipped with a canonical `Tensorial` instance. The linear equivalence $\text{toTensor}$ that identifies the module with its tensor representation is defined as the identity map $\text{id} : S.\text{Tensor } c \cong S.\text{Tensor } c$.

For any tensor species $S$, any index configuration $c: \{0, \dots, n-1\} \to C$, and any tensor $t \in S.\text{Tensor } c$, the linear equivalence $\text{toTensor}$ provided by the canonical `Tensorial` instance for $S.\text{Tensor } c$ is the identity map. That is, $\text{toTensor}(t) = t$.

For an element $t$ in a type $M$ that carries a `Tensorial` instance with respect to a tensor species $S$ and an index configuration $c: \{0, \dots, n-1\} \to C$, the function returns the natural number $n$, representing the number of indices associated with the tensor representation of $t$.

For a type $M$ equipped with a `Tensorial` instance for a tensor species $S$ and a configuration of indices $c$, there exists a linear equivalence $\phi: M \cong S.\text{Tensor}(c)$. This definition provides a scalar multiplication (action) of the group $G$ on $M$, where for any $g \in G$ and $m \in M$, the action is defined by $g \cdot m = \phi^{-1}(g \cdot \phi(m))$.

Given a type $M$ equipped with a `Tensorial` instance for a tensor species $S$ and an index configuration $c$, this definition provides a group action of $G$ on $M$. The action is defined such that for any $g \in G$ and $m \in M$, $g \cdot m = \phi^{-1}(g \cdot \phi(m))$, where $\phi: M \cong S.\text{Tensor}(c)$ is the linear equivalence between $M$ and the space of tensors associated with the species $S$ and configuration $c$.

Let $M$ be a type equipped with a `Tensorial` instance for a tensor species $S$ and index configuration $c$. Let $\phi: M \cong S.\text{Tensor}(c)$ be the linear equivalence (denoted as `toTensor`) that identifies $M$ with its tensor representation. For any group element $g \in G$ and any element $t \in M$, the action of $g$ on $t$ is defined by the relation $g \cdot t = \phi^{-1}(g \cdot \phi(t))$.

Let $M$ be a type equipped with a `Tensorial` instance for a tensor species $S$ and index configuration $c$. Let $\phi: M \cong S.\text{Tensor}(c)$ be the linear equivalence (denoted as `toTensor`) that identifies elements of $M$ with their tensor representations. For any group element $g \in G$ and any element $t \in M$, the map $\phi$ is equivariant with respect to the group action, meaning $\phi(g \cdot t) = g \cdot \phi(t)$.

Let $M$ be a module equipped with a `Tensorial` instance for a tensor species $S$ and index configuration $c$. Let $\phi: M \cong S.\text{Tensor}(c)$ be the linear equivalence (denoted as `toTensor`) that identifies $M$ with its tensor representation. For any group element $g \in G$ and any tensor $t \in S.\text{Tensor}(c)$, the group action of $g$ on the element $\phi^{-1}(t) \in M$ satisfies the relation $g \cdot \phi^{-1}(t) = \phi^{-1}(g \cdot t)$.

Given a $k$-module $M$ equipped with a `Tensorial` instance for a tensor species $S$ and index configuration $c$, the group action of $G$ on $M$ is distributive. This means that for any $g \in G$ and $m, m' \in M$, the action satisfies $g \cdot (m + m') = g \cdot m + g \cdot m'$ and $g \cdot 0 = 0$. These properties are inherited from the action of $G$ on the space of tensors $S.\text{Tensor}(c)$ through the linear equivalence $\phi: M \cong S.\text{Tensor}(c)$.

Given a group element $g \in G$ and a $k$-module $M$ equipped with a tensorial structure (associated with a tensor species $S$ and index configuration $c$), this definition defines a $k$-linear map from $M$ to itself. The map sends an element $m \in M$ to $g \cdot m$, where the action is defined via the linear equivalence between $M$ and the corresponding tensor space.

Let $M$ be a $k$-module equipped with a tensorial structure for a tensor species $S$ and index configuration $c$. For any element $g$ of the group $G$ and any element $m \in M$, the application of the linear map $\text{smulLinearMap}(g)$ to $m$ is equal to the group action $g \cdot m$.

Let $M$ be a $k$-module equipped with a `Tensorial` instance for a tensor species $S$ and index configuration $c$. For any scalar $a \in k$, group element $g \in G$, and element $m \in M$, the group action of $G$ and the scalar multiplication by $k$ commute, such that $a \cdot (g \cdot m) = g \cdot (a \cdot m)$.

Let $M$ be a module equipped with a `Tensorial` instance for a tensor species $S$ and a collection of indices $c$. Let $\phi: M \cong \mathcal{T}$ be the linear equivalence (`toTensor`) between $M$ and the corresponding tensor space $\mathcal{T}$ of species $S$ with indices $c$. Let $\mathcal{B}$ be the canonical basis for $\mathcal{T}$ (`Tensor.basis c`). For any $m \in M$, the coordinate representation of $\phi(m)$ with respect to the basis $\mathcal{B}$ is equal to the coordinate representation of $m$ with respect to the basis on $M$ obtained by pulling back $\mathcal{B}$ via the inverse equivalence $\phi^{-1}$.

Let $S$ be a tensor species over a ring $k$. Suppose $M$ and $M_2$ are modules equipped with `Tensorial` instances for index configurations $c: \{0, \dots, n-1\} \to C$ and $c_2: \{0, \dots, n_2-1\} \to C$, respectively. The tensor product $M \otimes_k M_2$ is also a `Tensorial` module with the concatenated index configuration $c \mathbin{+\!+} c_2$ (denoted `Fin.append c c2`). The associated linear equivalence $\text{toTensor} : M \otimes_k M_2 \cong S.\text{Tensor}(c \mathbin{+\!+} c_2)$ is defined as the composition of the tensor product of the individual maps ($\text{toTensor}_M \otimes \text{toTensor}_{M_2}$) and the canonical isomorphism $S.\text{Tensor}(c) \otimes_k S.\text{Tensor}(c_2) \cong S.\text{Tensor}(c \mathbin{+\!+} c_2)$.

Let $S$ be a tensor species over a ring $k$. Suppose $M$ and $M_2$ are modules equipped with `Tensorial` instances for index configurations $c: \text{Fin } n \to C$ and $c_2: \text{Fin } n_2 \to C$, respectively. For any elements $m \in M$ and $m_2 \in M_2$, let $m \otimes m_2$ be their tensor product in $M \otimes_k M_2$. The linear equivalence $\text{toTensor}$ (which maps elements to the corresponding tensor space of the species $S$) satisfies: $$\text{toTensor}(m \otimes m_2) = \text{prodT}(\text{toTensor } m, \text{toTensor } m_2)$$ where $\text{prodT}$ is the $k$-bilinear map that computes the tensor product of two tensors within the tensor species $S$.

Let $S$ be a tensor species over a ring $k$ and $G$ a group. Suppose $M$ and $M_2$ are modules equipped with `Tensorial` instances for index configurations $c$ and $c_2$, respectively. For any group element $g \in G$ and any elements $m \in M$ and $m_2 \in M_2$, the group action on the tensor product $M \otimes_k M_2$ satisfies: $$g \cdot (m \otimes m_2) = (g \cdot m) \otimes (g \cdot m_2)$$ where $\otimes$ denotes the tensor product of elements and $\cdot$ denotes the action of $G$ on the respective tensorial modules.

Let $S$ be a tensor species over a ring $k$. Suppose $M$ and $M_2$ are modules equipped with `Tensorial` instances for index configurations $c: \text{Fin } n \to C$ and $c_2: \text{Fin } n_2 \to C$, respectively. Let $\text{toTensor}_M: M \cong S.\text{Tensor}(c)$ and $\text{toTensor}_{M_2}: M_2 \cong S.\text{Tensor}(c_2)$ be the associated linear equivalences. The basis of $M \otimes_k M_2$ induced by its `Tensorial` instance (for the concatenated configuration $c \mathbin{+\!+} c_2$) is obtained by mapping the canonical basis of $S.\text{Tensor}(c \mathbin{+\!+} c_2)$ through the inverse equivalence $\text{toTensor}_{M \otimes M_2}^{-1}$. This theorem states that this induced basis is equal to the tensor product of the induced bases of $M$ and $M_2$, reindexed by the canonical equivalence between the product of component indices and the concatenated component indices.

Let $M$ be a module over a field $k$. If $M$ is equipped with a `Tensorial` instance for a tensor species $S$ and a configuration of indices $c$, then $M$ is a finite-dimensional vector space over $k$.

For a topological module $M$ over a field $k$ that carries a `Tensorial` instance for a tensor species $S$ with index components $c$, this definition provides the continuous linear equivalence (topological isomorphism) between $M$ and the space of tensors $S.\text{Tensor}(c)$. The map $M \simeq_{L,k} S.\text{Tensor}(c)$ identifies elements of $M$ with their formal tensor representations while preserving both the linear structure and the topology, provided that $M$ is a Hausdorff space ($T_2$) with continuous addition and scalar multiplication.

Let $M$ be a topological $k$-module equipped with a `Tensorial` structure for a tensor species $S$ and index configuration $c$. For any group element $g \in G$, the map $m \mapsto g \cdot m$ defines a continuous $k$-linear map from $M$ to itself. This definition constructs the action as an element of the space of continuous linear maps $\mathcal{L}_k(M; M)$, utilizing the fact that the module $M$ is a Hausdorff space with continuous addition and scalar multiplication. In the context of physics-related tensor species, this represents the Lorentz action on the tensorial type $M$.

Let $M$ be a topological $k$-module that is a Hausdorff space with continuous scalar multiplication, and suppose $M$ is equipped with a `Tensorial` structure for a tensor species $S$ and index configuration $c$. For any group element $g \in G$ and any $m \in M$, applying the continuous linear map associated with the group action, denoted as $\text{actionCLM}_S(g)$, to the element $m$ is equal to the group action $g \cdot m$.