Physlib.Relativity.Tensors.Evaluation

Let $S$ be a tensor species over a field $k$ and $c$ be a sequence of colors representing a collection of vector spaces $\{V_{c_j}\}_{j=0}^n$. A pure tensor $p \in \text{Pure}(S, c)$ is defined as an element of the dependent product $\prod_{j=0}^n V_{c_j}$, representing the tensor $v_0 \otimes v_1 \otimes \dots \otimes v_n$. Given an index $i \in \{0, \dots, n\}$ and a basis index $b \in \{0, \dots, \dim(V_{c_i}) - 1\}$, the function `evalPCoeff` returns the $b$-th coordinate of the $i$-th component vector $v_i$ with respect to the basis of $V_{c_i}$ provided by the tensor species.

Let $S$ be a tensor species over a field $k$ and $c: \{0, \dots, n\} \to C$ be a sequence of colors representing a collection of vector spaces $\{V_{c_j}\}_{j=0}^n$. Let $p \in \text{Pure}(S, c)$ be a pure tensor, representing the product $v_0 \otimes v_1 \otimes \dots \otimes v_n$. Let $\text{evalPCoeff}(i, b, p)$ be the function that returns the $b$-th coordinate of the $i$-th component vector $v_i$ with respect to the basis of $V_{c_i}$ provided by the species. For any index $i \in \{0, \dots, n\}$, basis index $b \in \{0, \dots, \dim(V_{c_i}) - 1\}$, and vector $x \in V_{c_i}$, the $b$-th basis coefficient of the $i$-th component of the pure tensor updated at index $i$ with $x$ is equal to the $b$-th basis coefficient of $x$: $$\text{evalPCoeff}(i, b, \text{update}(p, i, x)) = \text{repr}(x)_b$$ where $\text{repr}(x)_b$ denotes the $b$-th coordinate of $x$ in the basis of $V_{c_i}$.

Let $S$ be a tensor species over a field $k$ and $c: \{0, \dots, n\} \to C$ be a sequence of colors representing a collection of vector spaces $\{V_{c_m}\}_{m=0}^n$. Let $p$ be a pure tensor, defined as an element of the dependent product $\prod_{m=0}^n V_{c_m}$, which represents the simple tensor $v_0 \otimes v_1 \otimes \dots \otimes v_n$. Let $\text{evalPCoeff}(i, b, p)$ be the function that returns the $b$-th coordinate of the $i$-th component vector $v_i$ with respect to the basis of $V_{c_i}$. For any index $i \in \{0, \dots, n\}$ and $j \in \{0, \dots, n-1\}$, let $k = i.\text{succAbove } j$ denote an index in $\{0, \dots, n\}$ distinct from $i$. If the $k$-th component of $p$ is updated with a new vector $x \in V_{c_k}$, the $b$-th basis coefficient of the $i$-th component vector remains unchanged: $$\text{evalPCoeff}(i, b, \text{update } p \, k \, x) = \text{evalPCoeff}(i, b, p)$$

Let $S$ be a tensor species over a field $k$ and $c: \{0, \dots, n\} \to C$ be a sequence of colors. A pure tensor $p$ of type $c$ is a family of vectors $(v_0, v_1, \dots, v_n)$ representing the tensor product $v_0 \otimes v_1 \otimes \dots \otimes v_n$, where each $v_j$ belongs to the vector space $V_{c_j}$ associated with color $c_j$. Given an index $i \in \{0, \dots, n\}$ and a basis index $b$ for the vector space $V_{c_i}$, the function $\text{evalP } i \, b \, p$ returns the tensor of rank $n$ formed by evaluating the $i$-th index of $p$ at the $b$-th basis element. This is defined as: $$\text{evalP } i \, b \, p = (v_i)_b \cdot (v_0 \otimes \dots \otimes v_{i-1} \otimes v_{i+1} \otimes \dots \otimes v_n)$$ where $(v_i)_b$ is the $b$-th coordinate of the vector $v_i$ with respect to the basis of $V_{c_i}$ provided by the tensor species $S$.

Let $S$ be a tensor species over a field $k$ 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 (formally an element of the dependent product $\prod_{m=0}^n V_{c(m)}$) representing the simple tensor $v_0 \otimes \dots \otimes v_n$. Let $\text{evalP}(i, b, p)$ be the operation that evaluates the $i$-th index of $p$ at the $b$-th basis element of $V_{c(i)}$, returning a tensor of rank $n$. For any indices $i, j \in \{0, \dots, n\}$, a basis index $b$ for $V_{c(i)}$, and vectors $x, y \in V_{c(j)}$, the evaluation operation is additive with respect to updating the $j$-th component of the pure tensor: $$\text{evalP}(i, b, \text{update}(p, j, x + y)) = \text{evalP}(i, b, \text{update}(p, j, x)) + \text{evalP}(i, b, \text{update}(p, j, y))$$ where $\text{update}(p, j, v)$ denotes the pure tensor $p$ with its $j$-th component replaced by $v$.

Let $S$ be a tensor species over a field $k$ and $c: \{0, \dots, n\} \to C$ be a sequence of colors, where $V_{c_m}$ denotes the vector space associated with color $c_m$. Let $p$ be a pure tensor of type $c$, representing the family of vectors $(v_0, \dots, v_n)$ where $v_m \in V_{c_m}$. For any indices $i, j \in \{0, \dots, n\}$, a basis index $b$ for the vector space $V_{c_i}$, a scalar $r \in k$, and a vector $x \in V_{c_j}$, the evaluation of the $i$-th index at basis index $b$ is homogeneous with respect to scalar multiplication in the $j$-th component: $$\text{evalP}(i, b, \text{update}(p, j, r \cdot x)) = r \cdot \text{evalP}(i, b, \text{update}(p, j, x))$$ where $\text{update}(p, j, x)$ denotes the pure tensor obtained by replacing the $j$-th component of $p$ with $x$, and $\text{evalP}(i, b, p)$ is the rank-$n$ tensor defined by $(v_i)_b \cdot (v_0 \otimes \dots \otimes v_{i-1} \otimes v_{i+1} \otimes \dots \otimes v_n)$, where $(v_i)_b$ is the $b$-th coordinate of $v_i$ with respect to the basis of $V_{c_i}$.

Let $S$ be a tensor species over a field $k$ and $c: \{0, \dots, n\} \to C$ be a sequence of colors. For a fixed index $i \in \{0, \dots, n\}$ and a basis index $b$ for the vector space $V_{c_i}$ (the space associated with color $c_i$), the function `evalPMultilinear i b` is the multilinear map from the product of vector spaces $\prod_{j=0}^n V_{c_j}$ to the space of tensors of rank $n$ with the color sequence $c \circ i.\text{succAbove}$ (where the $i$-th color is omitted). Given a tuple of vectors $(v_0, \dots, v_n)$, the map is defined by: $$(v_0, \dots, v_n) \mapsto (v_i)_b \cdot (v_0 \otimes \dots \otimes v_{i-1} \otimes v_{i+1} \otimes \dots \otimes v_n)$$ where $(v_i)_b$ is the $b$-th coordinate of the vector $v_i$ with respect to the basis of $V_{c_i}$ provided by the tensor species $S$.

Let $S$ be a tensor species over a field $k$ and $c: \{0, \dots, n\} \to C$ be a sequence of colors. For a fixed index $i \in \{0, \dots, n\}$ and a basis index $b$ for the vector space $V_{c_i}$ associated with the color $c_i$, the $k$-linear map $\text{evalT } i \text{ } b$ maps a tensor $t \in \text{Tensor } S c$ to a tensor of rank $n$ with the color sequence $c \circ i.\text{succAbove}$ (the original sequence $c$ with the $i$-th element omitted). This map is defined as the linear extension of the multilinear evaluation map, which acts on a pure tensor as: $$v_0 \otimes \dots \otimes v_n \mapsto (v_i)_b \cdot (v_0 \otimes \dots \otimes v_{i-1} \otimes v_{i+1} \otimes \dots \otimes v_n)$$ where $(v_i)_b$ is the $b$-th coordinate of the vector $v_i$ with respect to the basis of $V_{c_i}$ provided by the tensor species $S$.

Let $S$ be a tensor species over a field $k$ and $c: \{0, \dots, n\} \to C$ be a sequence of colors. For any index $i \in \{0, \dots, n\}$, any basis index $b$ for the vector space $V_{c_i}$ associated with the color $c_i$, and any pure tensor $p$ (representing the tuple of vectors $(v_0, \dots, v_n)$), the $k$-linear evaluation map $\text{evalT } i \, b$ applied to the tensor $\bigotimes_{j=0}^n v_j$ is equal to the direct evaluation of the pure tensor $\text{evalP } i \, b \, p$. That is, $$\text{evalT } i \, b (p.\text{toTensor}) = \text{evalP } i \, b \, p$$ where $p.\text{toTensor}$ is the image of the vectors in the tensor product space, and $\text{evalP}$ is defined as $(v_i)_b \cdot (v_0 \otimes \dots \otimes v_{i-1} \otimes v_{i+1} \otimes \dots \otimes v_n)$.

Let $S$ be a tensor species over a field $k$ and $c: \{0, \dots, n\} \to C$ be a sequence of colors. Let $e_b$ denote the basis element of the tensor space $\text{Tensor } S c$ corresponding to the multi-index $b \in \text{ComponentIdx } c$. For any index position $i \in \{0, \dots, n\}$ and any basis index $x$ of the vector space $V_{c_i}$, the evaluation of the $i$-th index of $e_b$ at $x$ is given by: $$\text{evalT } i \ x \ (e_b) = \begin{cases} e_{b \circ i.\text{succAbove}} & \text{if } b_i = x \\ 0 & \text{if } b_i \neq x \end{cases}$$ where $b \circ i.\text{succAbove}$ is the multi-index of length $n$ obtained by removing the $i$-th component from $b$, and $e_{b \circ i.\text{succAbove}}$ is the corresponding basis element in the reduced tensor space $\text{Tensor } S (c \circ i.\text{succAbove})$.

Let $S$ be a tensor species over a field $k$. Let $c: \text{Fin}(n+1) \to C$ and $c': \text{Fin}(m+1) \to C$ be two color sequences, and let $\sigma: \text{Fin}(n+1) \to \text{Fin}(m+1)$ be a reindexing (a bijection such that $c' \circ \sigma = c$). For any tensor $t \in \text{Tensor } S \ c'$, any index $i \in \text{Fin}(n+1)$, and any basis index $x$ of the vector space $V_{c_i}$, the evaluation of the $i$-th index of the permuted tensor $\text{permT}(\sigma, h, t)$ at $x$ is equal to: $$\text{evalT}_i \ x \ (\text{permT} \ \sigma \ h \ t) = \text{permT} \ (\sigma') \ (h.\text{succAbove } i) \ (\text{evalT}_{\sigma(i)} \ x' \ t)$$ where: 1. $x'$ is the basis index $x$ viewed as an index for $V_{c'_{\sigma(i)}}$ (noting that $c_i = c'_{\sigma(i)}$). 2. $\sigma'$ is the induced reindexing on the reduced color sequences after removing $i$ from the target and $\sigma(i)$ from the source. 3. $\text{permT}$ is the linear map that reorders tensor indices. 4. $\text{evalT}$ is the linear map that evaluates a tensor index at a specific basis element.

Let $S$ be a tensor species over a field $k$, and let $t$ be a tensor of rank $n+3$ with color sequence $c: \text{Fin}(n+3) \to C$. For an index $k \in \text{Fin}(n+3)$ and a basis index $\phi$ of the vector space $V_{c_k}$, let $\text{evalT}_k(\phi, t)$ be the evaluation of $t$ at the $k$-th index. Let $i, j \in \text{Fin}(n+2)$ be two distinct indices such that the contraction $\text{contrT}_{i,j}$ is well-defined on the evaluated tensor (i.e., the color at $j$ is the dual of the color at $i$ in the sequence $c \circ k.\text{succAbove}$). Then, evaluating the $k$-th index and then contracting the pair $(i, j)$ is equivalent to first contracting the corresponding pair $(i', j')$ in the original tensor and then evaluating the residual index $k'$, up to a canonical reindexing: $$\text{contrT}_{i,j}(\text{evalT}_k(\phi, t)) = \text{permT}(\text{id}, h) \left( \text{evalT}_{k'}(\phi', \text{contrT}_{i', j'}(t)) \right)$$ where: 1. $i' = \text{succAbove}_k(i)$ and $j' = \text{succAbove}_k(j)$ are the indices in the original rank $n+3$ tensor that map to $i$ and $j$ after $k$ is removed. 2. $k' = \text{predPredAbove}_{i', j'}(k)$ is the index in the rank $n+1$ tensor corresponding to the original index $k$ after indices $i'$ and $j'$ are removed via contraction. 3. $\phi'$ is the basis index $\phi$ under the canonical identification of color spaces. 4. $\text{permT}(\text{id}, h)$ is the reindexing map corresponding to the commutativity of skipping one index and skipping a pair of indices ($\text{IsReindexing.succAbove\_succSuccAbove\_comm}$).

Let $S$ be a tensor species over a field $k$. Let $t$ be a tensor of rank $n$ with color sequence $c$, and $t_1$ be a tensor of rank $n_1 + 1$ with color sequence $c_1$. For any index $i \in \{0, \dots, n_1\}$ and any basis index $x$ of the vector space associated with color $c_1(i)$, the evaluation of the $i$-th index of the right factor $t_1$ commutes with the tensor product operation: $$t \otimes \text{evalT}_i(x, t_1) = \text{permT}(\text{id}, h) (\text{evalT}_{n+i}(x, t \otimes t_1))$$ where $\otimes$ denotes the tensor product `prodT`, $\text{evalT}_k$ is the evaluation map at the $k$-th index, and $\text{permT}(\text{id}, h)$ is the canonical reindexing (permutation) that identifies the color sequence of $t \otimes \text{evalT}_i(x, t_1)$ with the color sequence of $t \otimes t_1$ after the $(n+i)$-th index has been removed.

Let $S$ be a tensor species over a field $k$. For a color $c \in C$, let $e_b$ denote the basis vector of the rank-1 tensor space $S.\text{Tensor } [c]$ corresponding to the index $b \in \text{basisIdx}(c)$. Let $\text{evalT}_0(x, \cdot)$ be the linear map that evaluates the $0$-th index of a tensor at the basis index $x$, and let $\text{toField}$ be the linear isomorphism that maps a rank-0 tensor to its corresponding scalar in $k$. Then, evaluating the basis tensor $e_b$ at the index $x$ yields the Kronecker delta: $$\text{toField}(\text{evalT}_0(x, e_b)) = \delta_{bx} = \begin{cases} 1 & \text{if } b = x \\ 0 & \text{if } b \neq x \end{cases}$$ where the comparison $b = x$ is performed under the canonical identification of the index types.

Let $S$ be a tensor species over a field $k$, and let $c: \{0, \dots, n\} \to C$ be a sequence of colors defining a tensor space. For any two tensors $t_1, t_2$ of rank $n+1$ with color sequence $c$, if for every index $i \in \{0, \dots, n\}$ and every basis index $\phi$ of the associated vector space $V_{c_i}$, the evaluations $\text{evalT}_i(\phi, t_1)$ and $\text{evalT}_i(\phi, t_2)$ are equal, then $t_1 = t_2$. Here, $\text{evalT}_i(\phi, t)$ denotes the tensor of rank $n$ obtained by evaluating the $i$-th slot of $t$ at the $\phi$-th basis vector.

Let $S$ be a tensor species over a field $k$, and let $c: \{0, \dots, n\} \to C$ be a sequence of colors. Let $t_1$ and $t_2$ be tensors in $\text{Tensor } S c$. If there exists a fixed index $i \in \{0, \dots, n\}$ such that for every basis index $\phi$ of the vector space associated with the color $c_i$, the evaluation of the $i$-th tensor index satisfies $\text{evalT } i \text{ } \phi(t_1) = \text{evalT } i \text{ } \phi(t_2)$, then $t_1 = t_2$.