Physlib.Relativity.Tensors.Reindexing

Given two sequences of tensor index types (or "colors") $c: \{0, \dots, n-1\} \to C$ and $c_1: \{0, \dots, m-1\} \to C$, a map $\sigma: \{0, \dots, m-1\} \to \{0, \dots, n-1\}$ satisfies the `IsReindexing` property if $\sigma$ is a bijection and it preserves the index types such that $c(\sigma(i)) = c_1(i)$ for all $i$. This implies that the composition $c \circ \sigma$ is equal to $c_1$.

Let $c : \text{Fin } n \to C$ and $c_1 : \text{Fin } m \to C$ be sequences of tensor index types (or "colors"). If a map $\sigma : \text{Fin } m \to \text{Fin } n$ is a reindexing from $c$ to $c_1$ (meaning $\sigma$ is a bijection such that $c \circ \sigma = c_1$), then $\sigma$ is injective.

Let $c: \{0, \dots, n-1\} \to C$ and $c_1: \{0, \dots, m-1\} \to C$ be sequences of tensor index types (or "colors"). If the map $\sigma: \{0, \dots, m-1\} \to \{0, \dots, n-1\}$ is a reindexing from $c$ to $c_1$, then $\sigma$ is surjective.

Let $c$ and $c_1$ be two sequences of tensor index types (or colors) mapping $\{0, \dots, n-1\}$ to $C$. The identity map $\text{id} : \{0, \dots, n-1\} \to \{0, \dots, n-1\}$ is a reindexing from $c$ to $c_1$ if and only if $c(i) = c_1(i)$ for all $i \in \{0, \dots, n-1\}$.

Let $c$ and $c_1$ be two sequences of index colors from $\{0, \dots, n-1\}$ to $C$. If the identity map $\text{id}: \{0, \dots, n-1\} \to \{0, \dots, n-1\}$ is a valid reindexing from $c_1$ to $c$, then $\text{id}$ is also a valid reindexing from $c$ to $c_1$.

Given a map $\sigma: \{0, \dots, m-1\} \to \{0, \dots, n-1\}$ that is a reindexing from index colors $c$ to $c_1$ (which implies that $\sigma$ is a bijection and $c \circ \sigma = c_1$), this function represents the inverse map $\sigma^{-1}: \{0, \dots, n-1\} \to \{0, \dots, m-1\}$.

Given a reindexing map $\sigma: \{0, \dots, m-1\} \to \{0, \dots, n-1\}$ between index colorings $c$ and $c_1$ (which implies $\sigma$ is a bijection and $c \circ \sigma = c_1$), the definition provides an equivalence (bijection) between the index sets $\{0, \dots, n-1\} \simeq \{0, \dots, m-1\}$. In this equivalence, the forward mapping is the inverse function $\sigma^{-1}$, and the inverse mapping is the original map $\sigma$.

Let $c: \text{Fin } n \to C$ and $c_1: \text{Fin } m \to C$ be mappings from tensor indices to a set of colors $C$. Suppose $\sigma: \text{Fin } m \to \text{Fin } n$ is a reindexing from $c$ to $c_1$, which implies that $\sigma$ is a bijection satisfying $c \circ \sigma = c_1$. If $\sigma^{-1}: \text{Fin } n \to \text{Fin } m$ is the inverse of $\sigma$, then for any index $x \in \text{Fin } m$, it holds that $\sigma^{-1}(\sigma(x)) = x$.

Let $c: \{0, \dots, n-1\} \to C$ and $c_1: \{0, \dots, m-1\} \to C$ be sequences of tensor index colors. If $\sigma: \{0, \dots, m-1\} \to \{0, \dots, n-1\}$ is a reindexing from $c$ to $c_1$ and $\sigma^{-1}: \{0, \dots, n-1\} \to \{0, \dots, m-1\}$ is its inverse map, then for every index $x \in \{0, \dots, n-1\}$, it holds that $\sigma(\sigma^{-1}(x)) = x$.

Let $c: \text{Fin } n \to C$ and $c_1: \text{Fin } m \to C$ be mappings from tensor indices to a set of colors $C$. If $\sigma: \text{Fin } m \to \text{Fin } n$ is a reindexing from $c$ to $c_1$, then for every index $x \in \text{Fin } m$, the color $c_1(x)$ is equal to the color $c(\sigma(x))$, or equivalently, $c_1 = c \circ \sigma$.

Let $c: \text{Fin } n \to C$ and $c_1: \text{Fin } m \to C$ be mappings from tensor indices to a set of colors $C$. If $\sigma: \text{Fin } m \to \text{Fin } n$ is a reindexing from $c$ to $c_1$ (which implies that $\sigma$ is a bijection such that $c \circ \sigma = c_1$), then for every index $x \in \text{Fin } n$, the color $c_1(\sigma^{-1}(x))$ is equal to $c(x)$, where $\sigma^{-1}$ denotes the inverse of the reindexing map.

Let $n, m \in \mathbb{N}$ and let $c: \text{Fin } n \to C$ and $c_1: \text{Fin } m \to C$ be sequences of tensor index colors. If $\sigma: \text{Fin } m \to \text{Fin } n$ is a reindexing from $c$ to $c_1$ (meaning $\sigma$ is a bijection such that $c \circ \sigma = c_1$), then for any index $x \in \text{Fin } m$, the color $c(\sigma(x))$ is equal to $c_1(x)$, where $\sigma$ corresponds to the inverse mapping of the equivalence $\text{Fin } n \simeq \text{Fin } m$ induced by the reindexing.

Let $n, m \in \mathbb{N}$ and let $c: \text{Fin } n \to C$ and $c_1: \text{Fin } m \to C$ be sequences of tensor index colors. If a map $\sigma: \text{Fin } m \to \text{Fin } n$ is a reindexing from $c$ to $c_1$ (meaning $\sigma$ is a bijection and $c \circ \sigma = c_1$), then its inverse map $\sigma^{-1}: \text{Fin } n \to \text{Fin } m$ is a reindexing from $c_1$ to $c$.

Let $n$ be a natural number and $c, c_1: \{0, \dots, n-1\} \to C$ be two sequences of tensor index colors. If the identity map $\text{id}$ is a valid reindexing from $c$ to $c_1$, then $\text{id}$ is also a valid reindexing from $c_1$ to $c$. (A map $\sigma$ is a reindexing if it is a bijection and $c \circ \sigma = c_1$).

Let $n, n_1,$ and $n_2$ be natural numbers, and let $c: \text{Fin } n \to C$, $c_1: \text{Fin } n_1 \to C$, and $c_2: \text{Fin } n_2 \to C$ be sequences of tensor index types (colors). If $\sigma: \text{Fin } n_1 \to \text{Fin } n$ is a reindexing from $c$ to $c_1$ and $\sigma_2: \text{Fin } n_2 \to \text{Fin } n_1$ is a reindexing from $c_1$ to $c_2$, then the composition $\sigma \circ \sigma_2: \text{Fin } n_2 \to \text{Fin } n$ is a reindexing from $c$ to $c_2$. A map $\sigma$ is defined as a reindexing if it is a bijection that preserves index types such that the composition of the color map and the reindexing map matches the target color map ($c \circ \sigma = c_1$).

Let $c : \text{Fin } n \to C$, $c' : \text{Fin } n' \to C$, and $c_2 : \text{Fin } n_2 \to C$ be sequences of tensor index colors. If $\sigma : \text{Fin } n' \to \text{Fin } n$ is a reindexing from $c$ to $c'$ (meaning $\sigma$ is a bijection such that $c \circ \sigma = c'$), then the map $\Sigma : \text{Fin}(n' + n_2) \to \text{Fin}(n + n_2)$, defined by the concatenation of $\sigma$ (mapping into the first $n$ slots) and the identity map (mapping into the last $n_2$ slots), is a reindexing from the concatenated color sequence $c \text{ append } c_2$ to $c' \text{ append } c_2$.

Let $c: \{0, \dots, n-1\} \to C$ and $c': \{0, \dots, n'-1\} \to C$ be two sequences of tensor index types (or "colors"), and let $\sigma: \{0, \dots, n'-1\} \to \{0, \dots, n-1\}$ be a reindexing from $c$ to $c'$. For any additional sequence of index types $c_2: \{0, \dots, n_2-1\} \to C$, the map $\Sigma: \{0, \dots, n_2+n'-1\} \to \{0, \dots, n_2+n-1\}$ defined by: $$\Sigma(i) = \begin{cases} i & \text{if } 0 \le i < n_2 \\ n_2 + \sigma(i - n_2) & \text{if } n_2 \le i < n_2 + n' \end{cases}$$ is a reindexing from the concatenated sequence $(c_2 \text{ append } c)$ to the concatenated sequence $(c_2 \text{ append } c')$.

For any natural number $n$, let $c : \text{Fin}(n) \to C$ be a sequence of tensor index types and $c_1 : \text{Fin}(0) \to C$ be an empty sequence. Then the identity map $\text{id} : \text{Fin}(n) \to \text{Fin}(n)$ is a reindexing from $c$ to the concatenated sequence $c \text{ append } c_1$.

For any natural numbers $n, n_2$ and sequences of tensor index types $c : \text{Fin}(n) \to C$ and $c_2 : \text{Fin}(n_2) \to C$, let $\sigma : \text{Fin}(n_2 + n) \to \text{Fin}(n + n_2)$ be the block-swapping map defined by $\sigma(i) = n + i$ for $i < n_2$ and $\sigma(n_2 + j) = j$ for $j < n$. Then $\sigma$ is a reindexing from the concatenated sequence $c \text{ append } c_2$ to the sequence $c_2 \text{ append } c$.

For any natural numbers $n_1, n_2, n_3$ and sequences of tensor index types $c_1: \text{Fin}(n_1) \to C$, $c_2: \text{Fin}(n_2) \to C$, and $c_3: \text{Fin}(n_3) \to C$, the canonical bijection $\text{cast}: \text{Fin}((n_1 + n_2) + n_3) \to \text{Fin}(n_1 + (n_2 + n_3))$ is a reindexing from the concatenated sequence $c_1 \text{ append } (c_2 \text{ append } c_3)$ to the sequence $(c_1 \text{ append } c_2) \text{ append } c_3$.

For any three sequences of tensor index colors $c_1: \text{Fin } n_1 \to C$, $c_2: \text{Fin } n_2 \to C$, and $c_3: \text{Fin } n_3 \to C$, the identity map (realized as the canonical type cast $\text{Fin } ((n_1 + n_2) + n_3) \to \text{Fin } (n_1 + (n_2 + n_3))$) is a valid reindexing from the left-associated concatenation $(c_1 \oplus c_2) \oplus c_3$ to the right-associated concatenation $c_1 \oplus (c_2 \oplus c_3)$.

Let $n$ and $n_1$ be natural numbers. Let $c: \text{Fin } n \to C$ and $c_1: \text{Fin } (n_1+1) \to C$ be sequences of index colors. For any index $i \in \text{Fin } (n_1 + 1)$, the identity map $\text{id}$ is a reindexing from the color sequence $(c \boxplus c_1) \circ (n+i).\text{succAbove}$ to the color sequence $c \boxplus (c_1 \circ i.\text{succAbove})$. Here, $\boxplus$ denotes the concatenation of sequences (the `Fin.append` operation), and the map $k.\text{succAbove}: \text{Fin } m \to \text{Fin } (m+1)$ is the increasing embedding that skips the index $k$. The index $n+i$ is represented by `Fin.natAdd n i`.

For any natural numbers $n$ and $n_1$, given color sequences $c: \text{Fin}(n+1) \to C$ and $c_1: \text{Fin}(n_1+1) \to C$, and an index $i \in \text{Fin}(n+1)$, the identity map (via a type cast) is a reindexing from the sequence $(\text{append}(c, c_1) \circ \text{succAbove}(\text{castAdd}(n_1+1, i)))$ to the sequence $(\text{append}(c \circ \text{succAbove}(i), c_1))$.

For any natural numbers $n$ and $n_1$, given a sequence of colors $c: \text{Fin}(n+2) \to C$ and a sequence of colors $c_1: \text{Fin}(n_1) \to C$, and two indices $i, j \in \text{Fin}(n+2)$, the identity map is a reindexing from the color sequence $(\text{Fin.append } c_1 \ c) \circ \text{succSuccAbove}_{n_1+i, n_1+j}$ to the color sequence $\text{Fin.append } c_1 \ (c \circ \text{succSuccAbove}_{i, j})$. This states that removing the $i$-th and $j$-th entries from the right component $c$ before appending $c_1$ is equivalent to removing the $(n_1+i)$-th and $(n_1+j)$-th entries from the concatenated sequence $c_1 \oplus c$.

Let $c : \text{Fin}(n + 1) \to C$ and $c_1 : \text{Fin}(n_1 + 1) \to C$ be two sequences of tensor index types (colors). Let $\sigma : \text{Fin}(n_1 + 1) \to \text{Fin}(n + 1)$ be a reindexing from $c$ to $c_1$, which is a bijection satisfying $c \circ \sigma = c_1$. If for some index $i \in \text{Fin}(n_1 + 1)$, we have $\sigma(i) = 0$, then there exists a reindexing between the sequences $c \circ \text{Fin.succ}$ and $c_1 \circ i.\text{succAbove}$ given by the map $j \mapsto \text{pred}(\sigma(i.\text{succAbove}(j)))$. In this context, $i.\text{succAbove}$ is the map from $\text{Fin}(n_1)$ to $\text{Fin}(n_1 + 1)$ that skips $i$, and $\text{Fin.succ}$ is the map from $\text{Fin}(n)$ to $\text{Fin}(n + 1)$ that skips $0$.

Let $c : \text{Fin}(n+1) \to C$ and $c_1 : \text{Fin}(n_1+1) \to C$ be sequences of tensor index colors. Let $\sigma : \text{Fin}(n_1+1) \to \text{Fin}(n+1)$ be a reindexing of $c$ by $c_1$, defined as a bijection such that $c \circ \sigma = c_1$. Given an index $i \in \text{Fin}(n_1+1)$ such that $\sigma(i) \neq 0$, removing the $i$-th entry of $c_1$ and the $\sigma(i)$-th entry of $c$ yields a new reindexing from the reduced sequence $c \circ (\sigma(i)).\text{succAbove}$ to the reduced sequence $c_1 \circ i.\text{succAbove}$ via the map $(\text{Fin.pred}(\sigma(i))).\text{predAbove} \circ \sigma \circ i.\text{succAbove}$.

Let $c: \text{Fin}(n+1) \to C$ and $c_1: \text{Fin}(n_1+1) \to C$ be sequences of tensor index types (colors). Suppose $\sigma: \text{Fin}(n_1+1) \to \text{Fin}(n+1)$ is a reindexing, defined as a bijection such that $c \circ \sigma = c_1$. For any index $i \in \text{Fin}(n_1+1)$, removing the $i$-th entry from $c_1$ and the corresponding $\sigma(i)$-th entry from $c$ yields a new reindexing between the reduced sequences $c_1 \circ i.\text{succAbove}$ and $c \circ (\sigma(i)).\text{succAbove}$. The resulting reindexing map $\sigma'$ is defined by: $$\sigma'(j) = \begin{cases} \text{pred}(\sigma(i.\text{succAbove}(j))) & \text{if } \sigma(i) = 0 \\ \text{predAbove}(\text{pred}(\sigma(i)), \sigma(i.\text{succAbove}(j))) & \text{if } \sigma(i) \neq 0 \end{cases}$$ where $i.\text{succAbove}$ is the map that skips the $i$-th index, and $\text{pred}$ and $\text{predAbove}$ are the predecessor operations on finite sets that shift indices to account for the removed entry.

Let $c : \text{Fin}(n+2) \to C$ and $c_1 : \text{Fin}(n_1+2) \to C$ be sequences of tensor index colors. Suppose $\sigma : \text{Fin}(n_1+2) \to \text{Fin}(n+2)$ is a reindexing of $c$ by $c_1$, which means $\sigma$ is a bijection such that $c \circ \sigma = c_1$. For any two distinct indices $i, j \in \text{Fin}(n_1+2)$, removing the $i$-th and $j$-th entries from $c_1$ and the corresponding $\sigma(i)$-th and $\sigma(j)$-th entries from $c$ results in a new reindexing between the reduced sequences. Specifically, the map $\sigma' : \text{Fin}(n_1) \to \text{Fin}(n)$ induced by $\sigma$ after skipping $i$ and $j$ (formally defined as `funPredPredAbove`) is a reindexing from the color sequence $c \circ \text{succSuccAbove}_{\sigma(i), \sigma(j)}$ to $c_1 \circ \text{succSuccAbove}_{i, j}$, where $\text{succSuccAbove}_{i, j}$ is the order-preserving embedding that skips indices $i$ and $j$.

For any natural number $n$ and color sequence $c : \text{Fin}(n+4) \to C$, let $i_1, j_1 \in \text{Fin}(n+4)$ be distinct indices and $i_2, j_2 \in \text{Fin}(n+2)$ be distinct indices. Define the shifted indices: - $i_2' = \text{succSuccAbove}(i_1, j_1, i_2)$ and $j_2' = \text{succSuccAbove}(i_1, j_1, j_2)$, which are the indices in $\text{Fin}(n+4)$ corresponding to $i_2, j_2$ after $i_1$ and $j_1$ are inserted. - $i_1' = \text{predPredAbove}(i_2', j_2', i_1)$ and $j_1' = \text{predPredAbove}(i_2', j_2', j_1)$, which are the indices in $\text{Fin}(n+2)$ corresponding to $i_1, j_1$ after $i_2'$ and $j_2'$ are removed. Then, the identity map is a reindexing between the color list obtained by first removing $i_1, j_1$ and then $i_2, j_2$, and the color list obtained by first removing $i_2', j_2'$ and then $i_1', j_1'$. That is: $$(c \circ \text{succSuccAbove}_{i_2', j_2'}) \circ \text{succSuccAbove}_{i_1', j_1'} = (c \circ \text{succSuccAbove}_{i_1, j_1}) \circ \text{succSuccAbove}_{i_2, j_2}$$ This theorem shows that removing two pairs of indices from a color list in different orders (adjusting the indices accordingly) results in the same sequence of colors.

Let $n \in \mathbb{N}$ and $c : \text{Fin}(n+3) \to C$ be a sequence of tensor index colors. Let $k \in \text{Fin}(n+3)$ be an index and $i, j \in \text{Fin}(n+2)$ be two distinct indices ($i \neq j$). We define the shifted indices $i' = \text{succAbove}_k(i)$ and $j' = \text{succAbove}_k(j)$ in $\text{Fin}(n+3)$, and the shifted index $k' = \text{predPredAbove}_{i', j'}(k)$ in $\text{Fin}(n+1)$. The theorem states that the identity map $\text{id}$ is a reindexing from the color list obtained by removing the pair of entries at $i'$ and $j'$ and then removing the entry at $k'$, to the color list obtained by first removing the entry at $k$ and then removing the pair of entries at $i$ and $j$. That is: $$(c \circ \text{succSuccAbove}_{i', j'}) \circ \text{succAbove}_{k'} = (c \circ \text{succAbove}_k) \circ \text{succSuccAbove}_{i, j}$$ This result demonstrates that the operations of evaluation (removing one index) and contraction (removing two indices) commute when the indices are properly shifted.

For any natural number $n$ and any map $c : \text{Fin}(n+3) \to C$ representing tensor index types, let $k \in \text{Fin}(n+1)$ and $i, j \in \text{Fin}(n+3)$ be indices. We define the following shifted indices: - $k' = \text{succSuccAbove}_{i,j}(k)$ (the position of $k$ in $\text{Fin}(n+3)$ after skipping $i$ and $j$) - $k'' = \text{predAbove}_{0}(k')$ - $i' = \text{predAbove}_{k''}(i)$ - $j' = \text{predAbove}_{k''}(j)$ Then the identity map is a valid reindexing between the resulting color maps, which implies the following equality: $$(c \circ \text{succAbove}_{k'}) \circ \text{succSuccAbove}_{i',j'} = (c \circ \text{succSuccAbove}_{i,j}) \circ \text{succAbove}_k$$ This demonstrates that the operations of omitting two indices (via $\text{succSuccAbove}$) and omitting one index (via $\text{succAbove}$) commute when the indices are appropriately adjusted.

Let $n$ be a natural number and $c : \text{Fin}(n+2) \to C$ be a sequence of colors representing the types of tensor indices. For any indices $k_1 \in \text{Fin}(n+2)$ and $k_2 \in \text{Fin}(n+1)$, let $k_2' = \text{succAbove}(k_1, k_2)$ and $k_1' = \text{predAbove}(k_2, k_1)$. Then the identity map $\text{id}$ is a reindexing from the color sequence $(c \circ \text{succAbove}_{k_2'}) \circ \text{succAbove}_{k_1'}$ to the color sequence $(c \circ \text{succAbove}_{k_1}) \circ \text{succAbove}_{k_2}$, which implies that removing the two entries from $c$ in either order results in the same sequence of colors: $$(c \circ \text{succAbove}_{k_2'}) \circ \text{succAbove}_{k_1'} = (c \circ \text{succAbove}_{k_1}) \circ \text{succAbove}_{k_2}$$ Here, $\text{succAbove}_k$ denotes the map that embeds $\text{Fin}(m)$ into $\text{Fin}(m+1)$ by skipping the index $k$, and $\text{predAbove}$ is its partial inverse. This result confirms that the commutation of two index evaluations (removing two indices from a tensor) preserves the underlying color list.

Let $c : \{0, \dots, n\} \to C$ be a sequence of colors (index types) for a tensor. Let $c|_{<n} : \{0, \dots, n-1\} \to C$ denote the sequence of the first $n$ entries of $c$, and let $c_n$ denote the last entry of $c$. Then the identity map $\text{id}$ is a reindexing from the sequence formed by appending $c_n$ to $c|_{<n}$ to the original sequence $c$. This expresses that splitting a sequence into its first $n$ entries and its last entry and then concatenating them recovers the original sequence.

Given a sequence of tensor index colors $c : \text{Fin}(n + 1) \to C$, let $c_0$ denote the first color $c(0)$ and $c_{rest} : \text{Fin}(n) \to C$ denote the sequence of the remaining $n$ colors, defined by $c_{rest}(i) = c(i + 1)$ (or $c \circ \text{succAbove}_0$). Then the identity map $\text{id} : \text{Fin}(n+1) \to \text{Fin}(1+n)$ is a reindexing from the concatenation of $[c_0]$ and $c_{rest}$ to the original sequence $c$. In other words, appending the first entry of a color list to the list of its remaining entries recovers the original list via a canonical reindexing.

Let $n$ and $n_1$ be natural numbers and let $h: n_1 = n$ be an equality. For any sequence of tensor index types $c: \{0, \dots, n-1\} \to C$, the canonical bijection $\text{cast}_h : \{0, \dots, n_1-1\} \to \{0, \dots, n-1\}$ is a reindexing from $c$ to the sequence $c \circ \text{cast}_h$.

Let $c: \text{Fin } n \to C$ be a sequence of tensor index colors and $i \in \text{Fin } n$ be a specific index. Let $c_{\text{ext}}$ be the sequence of $n+2$ colors obtained by appending two copies of the dual color $S.\tau(c_i)$ to the end of $c$. Let $\sigma_{\text{skip}}: \text{Fin } n \to \text{Fin }(n+2)$ be the order-preserving embedding that skips the indices $i$ and $n$ (the first index of the appended pair). The theorem states that the inverse of the cyclic permutation $\text{cycleIcc}(i, n-1)$ is a reindexing from the contracted color sequence $c_{\text{ext}} \circ \sigma_{\text{skip}}$ to the sequence $c$ where the color at index $i$ has been replaced by its dual $S.\tau(c_i)$.