Physlib.Relativity.Tensors.Basic

The type of tensors associated with a list of indices of a given color sequence $c : \{0, \ldots, n-1\} \to C$, where $n$ is a natural number and $C$ is the set of colors.

Given a natural number $n$ and a sequence of index types $c : \{0, \dots, n-1\} \to C$ (for example, representing contravariant and covariant indices), this defines the type of component indices for a tensor with the index structure $c$. Mathematically, it is defined as the Cartesian product $\prod_{j=0}^{n-1} \{0, \dots, d_j - 1\}$, where $d_j$ is the dimension of the representation space associated with the index type $c_j$. For instance, an element of this type could be a multi-index like $(0, 2)$, corresponding to the indices of a tensor component such as $T^0_2$.

Let $n$ be a natural number and $c: \{0, \dots, n-1\} \to C$ be a sequence representing the index structure (colors) of a tensor. Let $b$ be a multi-index (component index) for this structure, where each component $b_k$ corresponds to the index at position $k$. For any two indices $i, j \in \{0, \dots, n-1\}$, if $i = j$, then the $i$-th component $b_i$ is equal to the $j$-th component $b_j$.

Given two natural numbers $n, m$ and two sequences of index types (colors) $c: \{0, \dots, n-1\} \to C$ and $cm: \{0, \dots, m-1\} \to C$, suppose the ranks are equal ($n = m$) and the color maps are equivalent ($c = cm \circ \text{cast}$). This function transforms a component index $b$ associated with the structure $c$ into the corresponding component index associated with the structure $cm$. Specifically, for an input multi-index $b = (b_0, b_1, \dots, b_{n-1})$, where each $b_i$ is an index for the representation space of color $c(i)$, the function returns the same multi-index viewed as an element of the component index type for $cm$.

The type of pure tensors associated to a list of indices $c : \{0, \dots, n-1\} \to C$ over a tensor species $S$. A pure tensor is a tensor which can be written in the form $v_1 \otimes v_2 \otimes \dots \otimes v_n$, and is formally defined as the dependent product of the vector spaces associated with the colors $c(i)$.

Given a tensor species $S$ over a field $k$ and a sequence of colors $c: \{0, \dots, n-1\} \to C$, let $p$ be a pure tensor of type $\text{Pure } S c$. For any indices $i, j \in \{0, \dots, n-1\}$, if $i = j$, then the $j$-th component $p(j)$ is equal to the $i$-th component $p(i)$ after transport via the canonical isomorphism induced by the equality of the indices.

Let $S$ be a tensor species and $p$ be a pure tensor with color mapping $c: \{0, \dots, n-1\} \to C$. Suppose $i, j \in \{0, \dots, n-1\}$ are indices and $c' \in C$ is a color such that $i = j$, $c(i) = c'$, and $c(j) = c'$. Let $V_a$ denote the vector space associated with color $a \in C$, and let $\tau_{a, b}: V_a \to V_b$ denote the canonical isomorphism induced by the equality of colors $a = b$. Then the $i$-th component of the pure tensor $p$ mapped to $V_{c'}$ is equal to the $j$-th component of $p$ mapped to $V_{c'}$, i.e., $$\tau_{c(i), c'}(p(i)) = \tau_{c(j), c'}(p(j))$$

Let $S$ be a tensor species, and let $p$ and $p'$ be pure tensors with index colorings $c: \{0, \dots, n-1\} \to C$ and $c_1: \{0, \dots, n_1-1\} \to C$, respectively. Suppose there exist indices $i$ and $j$ and a color $c' \in C$ such that the colors match, i.e., $c(i) = c'$ and $c_1(j) = c'$. Let $\tau_{a,b}: V_a \to V_b$ denote the canonical isomorphism between the vector spaces associated with colors $a$ and $b$ (where $V_a$ is defined by the functor $S.FD$). Then, the $i$-th component of $p$ mapped to $V_{c'}$ is equal to the $j$-th component of $p'$ mapped to $V_{c'}$ if and only if the $i$-th component of $p$ mapped directly to $V_{c_1(j)}$ is equal to the $j$-th component of $p'$. That is, $$\tau_{c(i), c'}(p_i) = \tau_{c_1(j), c'}(p'_j) \iff \tau_{c(i), c_1(j)}(p_i) = p'_j$$

Let $S$ be a tensor species over a field $k$ and a set of colors $C$. Let $p$ be a pure tensor of type $c: \{0, \dots, n-1\} \to C$, such that its $i$-th component $p(i)$ belongs to the vector space $V_{c(i)}$ associated with the color $c(i)$. Given morphisms $f: c(i) \to c_1$ and $g: c_1 \to c_2$ in the discrete category of colors, let $S.FD(f): V_{c(i)} \to V_{c_1}$ and $S.FD(g): V_{c_1} \to V_{c_2}$ be the linear maps induced by the functor $S.FD$. Then, the application of these maps sequentially to the component $p(i)$ satisfies the composition rule: $$S.FD(g)(S.FD(f)(p(i))) = S.FD(f \gg g)(p(i))$$ where $f \gg g$ is the composition of the morphisms in the category of colors.

Given a tensor species $S$ over a field $k$, let $c: \{0, \dots, n-1\} \to C$ be a sequence of colors where each color corresponds to a specific vector space. For a pure tensor $p$ (formally an element of the dependent product $\prod_{i=0}^{n-1} V_{c(i)}$), this function returns the corresponding element in the tensor product space $S.\text{Tensor } c \cong \bigotimes_{i=0}^{n-1} V_{c(i)}$. Specifically, it maps the family of vectors $p$ to the tensor product $\bigotimes_{i \in \{0, \dots, n-1\}} p(i)$.

Let $S$ be a tensor species over a field $k$ and $C$ be a set of colors. For a sequence of $n$ colors $c: \{0, \dots, n-1\} \to C$, let $p$ be a pure tensor, which is formally an element of the dependent product $\prod_{i=0}^{n-1} V_{c(i)}$ where each $V_{c(i)}$ is the vector space associated with the color $c(i)$. The result of the mapping `toTensor` applied to $p$ is equal to the canonical tensor product of the family of vectors $p(i)$ over the field $k$, denoted as $\bigotimes_{i=0}^{n-1} p(i)$.

Given a tensor species $S$ and a sequence of $n$ colors $c: \{0, \dots, n-1\} \to C$, let $V_{c(j)}$ denote the vector space associated with the color $c(j)$. A pure tensor $p$ is an element of the dependent product $\prod_{j=0}^{n-1} V_{c(j)}$, which can be identified with the simple tensor $v_0 \otimes v_1 \otimes \dots \otimes v_{n-1}$ where $v_j \in V_{c(j)}$. For a given index $i \in \{0, \dots, n-1\}$ and an element $x \in V_{c(i)}$, the update function returns a new pure tensor $p'$ such that the $i$-th component is replaced by $x$. Specifically, $p'(i) = x$ and $p'(j) = p(j)$ for all $j \neq i$, corresponding to the tensor $v_0 \otimes \dots \otimes v_{i-1} \otimes x \otimes v_{i+1} \otimes \dots \otimes v_{n-1}$.

Let $S$ be a tensor species and $c: \{0, \dots, n-1\} \to C$ be a sequence of colors, where each $c(j)$ corresponds to a vector space $V_{c(j)}$. Let $p$ be a pure tensor, which is an element of the dependent product $\prod_{j=0}^{n-1} V_{c(j)}$. For any index $i \in \{0, \dots, n-1\}$ and any vector $x \in V_{c(i)}$, the $i$-th component of the pure tensor $p$ updated at index $i$ with $x$ is equal to $x$: $$(\text{update } p, i, x)_i = x$$

Let $S$ be a tensor species and $c: \{0, \dots, n\} \to C$ be a sequence of colors, where each $c(m)$ corresponds to a vector space $V_{c(m)}$. Let $p$ be a pure tensor, which is an element of the dependent product $\prod_{m=0}^{n} V_{c(m)}$. For any index $i \in \{0, \dots, n\}$ and $j \in \{0, \dots, n-1\}$, let $x$ be a vector in $V_{c(i.\text{succAbove } j)}$. Then updating the $(i.\text{succAbove } j)$-th component of $p$ with $x$ does not change the value of the pure tensor at index $i$: $$(\text{update } p, i.\text{succAbove } j, x)_i = p_i$$ where $i.\text{succAbove } j$ denotes the $j$-th index in $\{0, \dots, n\}$ excluding $i$.

Let $S$ be a tensor species over a field $k$ and $c: \{0, \dots, n-1\} \to C$ be a sequence of colors, where each $c(j)$ corresponds to a vector space $V_{c(j)}$. Let $p$ be a pure tensor (an element of the dependent product $\prod_{j=0}^{n-1} V_{c(j)}$), $i$ be an index in $\{0, \dots, n-1\}$, and $x, y$ be vectors in $V_{c(i)}$. Then the tensor product operation $\text{toTensor}$ is additive in the $i$-th component, such that: $$\text{toTensor}(\text{update } p, i, x + y) = \text{toTensor}(\text{update } p, i, x) + \text{toTensor}(\text{update } p, i, y)$$ In terms of simple tensors, this states that: $$p(0) \otimes \dots \otimes (x + y) \otimes \dots \otimes p(n-1) = (p(0) \otimes \dots \otimes x \otimes \dots \otimes p(n-1)) + (p(0) \otimes \dots \otimes y \otimes \dots \otimes p(n-1))$$ where the $i$-th entry is the only one being modified.

Let $S$ be a tensor species over a field $k$ and $c: \{0, \dots, n-1\} \to C$ be a sequence of colors, where each $c(j)$ corresponds to a vector space $V_{c(j)}$. Let $p$ be a pure tensor (an element of the dependent product $\prod_{j=0}^{n-1} V_{c(j)}$), $i$ be an index in $\{0, \dots, n-1\}$, $r$ be a scalar in $k$, and $y$ be a vector in $V_{c(i)}$. Then the tensor product operation $\text{toTensor}$ is homogeneous with respect to scalar multiplication in the $i$-th component, such that: $$\text{toTensor}(\text{update } p, i, r \cdot y) = r \cdot \text{toTensor}(\text{update } p, i, y)$$ In terms of simple tensors, this states that: $$p(0) \otimes \dots \otimes (r \cdot y) \otimes \dots \otimes p(n-1) = r \cdot (p(0) \otimes \dots \otimes y \otimes \dots \otimes p(n-1))$$ where the $i$-th entry is the only one being modified.

Let $S$ be a tensor species over a field $k$. Given a sequence of colors $c : \{0, \dots, n\} \to C$ and a pure tensor $p$ of type $c$ (which can be represented as $v_0 \otimes v_1 \otimes \dots \otimes v_n$), the function $\text{drop } p \, i$ returns a new pure tensor of rank $n$ by removing the $i$-th component. Formally, for an index $i \in \{0, \dots, n\}$, the resulting pure tensor has the type $c \circ \text{succAbove}_i$, where $\text{succAbove}_i : \{0, \dots, n-1\} \to \{0, \dots, n\}$ is the order-preserving map that skips $i$. The $j$-th component of the resulting tensor is given by $p(\text{succAbove}_i(j))$. For example, if $n = 2$ and $p = v_0 \otimes v_1 \otimes v_2$, then $\text{drop } p \, 1 = v_0 \otimes v_2$.

Let $S$ be a tensor species over a field $k$. Let $p$ be a pure tensor of rank $n+1$ associated with a sequence of colors $c: \{0, \dots, n\} \to C$. Let $\text{drop}(p, i)$ denote the pure tensor of rank $n$ obtained by removing the $i$-th component of $p$ at index $i \in \{0, \dots, n\}$. Let $\text{succAbove}_i : \{0, \dots, n-1\} \to \{0, \dots, n\}$ be the order-preserving map that skips $i$. For any index $k \in \{0, \dots, n-1\}$ and any vector $x \in V_{c(\text{succAbove}_i(k))}$, the result of updating the component of $p$ at index $\text{succAbove}_i(k)$ and then dropping the $i$-th component is the same as dropping the $i$-th component of $p$ first and then updating the $k$-th component of the resulting rank-$n$ tensor: $$(\text{update}(p, \text{succAbove}_i(k), x)).\text{drop}(i) = (\text{drop}(p, i)).\text{update}(k, x)$$

Let $p$ be a pure tensor of rank $n+1$ associated with a sequence of colors $c: \{0, \dots, n\} \to C$, which can be viewed as an element of the dependent product $\prod_{j=0}^{n} V_{c(j)}$. Let $\text{update}(p, i, x)$ denote the pure tensor obtained by replacing the $i$-th component of $p$ with a vector $x \in V_{c(i)}$. Let $\text{drop}(p, i)$ denote the rank-$n$ pure tensor obtained by removing the $i$-th component of $p$. For any index $i \in \{0, \dots, n\}$ and any vector $x \in V_{c(i)}$, the result of updating the $i$-th component and then dropping it is identical to dropping the original $i$-th component: $$(\text{update}(p, i, x)).\text{drop}(i) = \text{drop}(p, i)$$

Let $S$ be a tensor species over a field $k$. Given two pure tensors $t$ and $t_1$ of ranks $n_1$ and $n_2$ respectively, let $t.\text{toTensor} = \bigotimes_{i=0}^{n_1-1} t_i$ and $t_1.\text{toTensor} = \bigotimes_{j=0}^{n_2-1} (t_1)_j$ be the corresponding tensors. The lax monoidal morphism $\mu$ of the tensor species functor maps the tensor product of these two tensors to the tensor product of the concatenated vector family: $$\mu(t.\text{toTensor} \otimes t_1.\text{toTensor}) = \bigotimes_{k \in \text{Fin } n_1 \sqcup \text{Fin } n_2} v_k$$ where the family of vectors $v$ is defined by $v_{\text{inl}(i)} = t_i$ for $i \in \{0, \dots, n_1-1\}$ and $v_{\text{inr}(j)} = (t_1)_j$ for $j \in \{0, \dots, n_2-1\}$.

Given a pure tensor $p$ of rank $n$ with index structure $c: \{0, \dots, n-1\} \to C$ and a multi-index $b = (b_0, \dots, b_{n-1})$, the function returns the scalar component of $p$ at index $b$. This is defined as the product of the coordinates of each constituent vector $p_i$ relative to the basis $\mathcal{B}_{c(i)}$ associated with the index color $c(i)$: $$\text{component}(p, b) = \prod_{i=0}^{n-1} (p_i)_{b_i}$$ where $(p_i)_{b_i}$ denotes the $b_i$-th coordinate of the $i$-th vector $p_i$ of the pure tensor with respect to the basis provided by the tensor species $S$.

Let $S$ be a tensor species over a field $k$. For a pure tensor $p$ of rank $n$ (which can be viewed as a sequence of vectors $p_0, p_1, \dots, p_{n-1}$) with index structure $c: \{0, \dots, n-1\} \to C$, and a multi-index $b = (b_0, b_1, \dots, b_{n-1})$, the component of $p$ at index $b$ is equal to the product of the coordinates of each constituent vector $p_i$ with respect to the basis $\mathcal{B}_{c(i)}$ at index $b_i$: $$\text{component}(p, b) = \prod_{i=0}^{n-1} (p_i)_{b_i}$$ where $(p_i)_{b_i}$ is the coordinate of the $i$-th vector $p_i$ corresponding to the basis element indexed by $b_i$.

Let $S$ be a tensor species over a field $k$. For a pure tensor $p$ of rank $n+1$ with index structure $c: \{0, \dots, n\} \to C$, a multi-index $b$, and any specific index $i \in \{0, \dots, n\}$, the component of $p$ at $b$ satisfies the recursive relation: $$\text{component}(p, b) = (p_i)_{b_i} \cdot \text{component}(\text{drop } p \, i, b \circ \text{succAbove}_i)$$ where $(p_i)_{b_i}$ is the $b_i$-th coordinate of the $i$-th constituent vector $p_i$ of the pure tensor with respect to the basis $\mathcal{B}_{c(i)}$, and $\text{drop } p \, i$ is the pure tensor of rank $n$ obtained by removing the $i$-th vector from the product. The term $b \circ \text{succAbove}_i$ represents the multi-index $b$ with its $i$-th entry removed.

Let $S$ be a tensor species over a field $k$. Let $p$ be a pure tensor of rank $n$ with index structure $c: \{0, \dots, n-1\} \to C$, which can be viewed as a product of vectors $v_0 \otimes v_1 \otimes \dots \otimes v_{n-1}$. For any index $i \in \{0, \dots, n-1\}$, vectors $x$ and $y$ in the vector space $V_{c(i)}$ associated with color $c(i)$, and multi-index $b$, the component of the updated pure tensor satisfies: $$\text{component}(\text{update}(p, i, x + y), b) = \text{component}(\text{update}(p, i, x), b) + \text{component}(\text{update}(p, i, y), b)$$ where $\text{update}(p, i, v)$ denotes the pure tensor $p$ with its $i$-th constituent vector replaced by $v$, and $\text{component}(p, b)$ is the scalar component of the pure tensor at multi-index $b$.

Let $S$ be a tensor species over a field $k$. Let $p$ be a pure tensor of rank $n$ with index structure $c: \{0, \dots, n-1\} \to C$, which can be viewed as a product of vectors $v_0 \otimes v_1 \otimes \dots \otimes v_{n-1}$. For any index $i \in \{0, \dots, n-1\}$, scalar $x \in k$, vector $y$ in the vector space $V_{c(i)}$ associated with color $c(i)$, and multi-index $b$, the component of the updated pure tensor satisfies: $$\text{component}(\text{update}(p, i, x \cdot y), b) = x \cdot \text{component}(\text{update}(p, i, y), b)$$ where $\text{update}(p, i, v)$ denotes the pure tensor $p$ with its $i$-th constituent vector replaced by $v$, and $\text{component}(p, b)$ is the scalar component of the pure tensor at multi-index $b$.

Given a sequence of index types $c : \{0, \dots, n-1\} \to C$, let $V_{c(i)}$ denote the vector space associated with the index color $c(i)$ in a tensor species $S$. The function `componentMap` is a $k$-multilinear map from the Cartesian product of these vector spaces $\prod_{i=0}^{n-1} V_{c(i)}$ to the space of scalar-valued functions on the set of multi-indices $\text{ComponentIdx}(c)$. For any tuple of vectors $p = (v_0, v_1, \dots, v_{n-1})$, the map returns the function that assigns to each multi-index $b = (b_0, b_1, \dots, b_{n-1})$ the product of the coordinates of each vector: $$(v_0, \dots, v_{n-1}) \mapsto \left( b \mapsto \prod_{i=0}^{n-1} (v_i)_{b_i} \right)$$ where $(v_i)_{b_i}$ is the $b_i$-th coordinate of the vector $v_i$ with respect to the basis associated with the index type $c(i)$.

Let $S$ be a tensor species over a field $k$. For a rank $n$ index structure $c: \{0, \dots, n-1\} \to C$ and a pure tensor $p$ with that index structure, the evaluation of the multilinear map $\text{componentMap}(c)$ at $p$ is equal to the scalar component function of $p$. That is, $$\text{componentMap}(c)(p) = \text{component}(p)$$ where $\text{component}(p)$ is the function mapping a multi-index $b$ to the scalar $\prod_{i=0}^{n-1} (p_i)_{b_i}$, with $(p_i)_{b_i}$ being the coordinate of the $i$-th vector of the pure tensor relative to the basis associated with color $c(i)$.

Given a tensor species $S$ and a sequence of index types $c = (c_0, c_1, \dots, c_{n-1})$, let $e_{j}^{(c_i)}$ denote the basis vector indexed by $j$ in the vector space associated with the index type $c_i$. For a multi-index $b = (b_0, b_1, \dots, b_{n-1}) \in \text{ComponentIdx}(c)$, the basis vector is the pure tensor defined by the tensor product of the basis vectors corresponding to each index: $$e_{b_0}^{(c_0)} \otimes e_{b_1}^{(c_1)} \otimes \dots \otimes e_{b_{n-1}}^{(c_{n-1})}$$ Formally, this is constructed as the dependent function that maps each $i \in \{0, \dots, n-1\}$ to the $b_i$-th basis vector of the space $S(c_i)$.

Let $S$ be a tensor species over a field $k$. For a rank $n$ tensor space with index structure $c: \{0, \dots, n-1\} \to C$, let $e_{b_1}$ be the basis vector corresponding to the multi-index $b_1 = (b_{1,0}, \dots, b_{1,n-1})$. The component of $e_{b_1}$ evaluated at a multi-index $b_2 = (b_{2,0}, \dots, b_{2,n-1})$ is $1$ if $b_1 = b_2$ and $0$ otherwise. That is, $$\text{component}(e_{b_1}, b_2) = \delta_{b_1, b_2}$$ where $\delta_{b_1, b_2}$ is the Kronecker delta, which is $1$ if $b_1 = b_2$ and $0$ if $b_1 \neq b_2$.

Let $S$ be a tensor species over a field $k$. For a sequence of colors $c: \{0, \dots, n-1\} \to C$, let $S.\text{Tensor } c$ be the corresponding tensor product space $\bigotimes_{i=0}^{n-1} V_{c(i)}$. Let $P$ be a property (predicate) defined on $S.\text{Tensor } c$. If the following conditions hold: 1. $P$ holds for every pure tensor $p$ (i.e., $P$ holds for all elements of the form $v_0 \otimes v_1 \otimes \dots \otimes v_{n-1}$); 2. $P$ is closed under scalar multiplication: for any $r \in k$ and tensor $t$, $P(t) \implies P(r \cdot t)$; 3. $P$ is closed under addition: for any tensors $t_1$ and $t_2$, $P(t_1) \land P(t_2) \implies P(t_1 + t_2)$; then $P(t)$ holds for all tensors $t \in S.\text{Tensor } c$.

Let $S$ be a tensor species over a field $k$. For a sequence of index colors $c: \{0, \dots, n-1\} \to C$, let $S.\text{Tensor } c$ denote the tensor product space $\bigotimes_{i=0}^{n-1} V_{c(i)}$, where $V_{c(i)}$ is the vector space associated with the color $c(i)$. The function `componentMap` is the $k$-linear map from the tensor space to the space of scalar-valued functions on multi-indices: $$\text{componentMap} : S.\text{Tensor } c \to (\text{ComponentIdx}(c) \to k)$$ This map assigns to each tensor $T$ a function that, for any multi-index $b = (b_0, \dots, b_{n-1})$, returns the component $T_b$ of the tensor with respect to the coordinate basis. For a pure tensor $p = v_0 \otimes v_1 \otimes \dots \otimes v_{n-1}$, the resulting function maps the multi-index $b$ to the product of the vector components: $$\text{componentMap}(v_0 \otimes \dots \otimes v_{n-1})(b) = \prod_{i=0}^{n-1} (v_i)_{b_i}$$