Physlib.Relativity.Tensors.Contraction.Pure

For any natural number $n$ and two indices $i, j \in \{0, \dots, n+1\}$, the function `dropPairEmb` defines an embedding from $\{0, \dots, n-1\}$ into $\{0, \dots, n+1\}$. This embedding is constructed by skipping the positions $i$ and $j$ in the target set. Specifically, for an input $m \in \{0, \dots, n-1\}$, the value is: - $m$ if $m < i$ and $m < j$; - $m+1$ if $j \le m < i-1$ or $i \le m < j-1$; - $m+2$ otherwise. In the special case where $i = j$, the function skips the indices $i$ and $i+1$. This operation is equivalent to the composition of two "successor above" maps which successively skip the specified indices.

For any natural number $n$, given an index $i \in \{0, \dots, n+1\}$ and an input $m \in \{0, \dots, n-1\}$, the value of the embedding $\text{dropPairEmb}$ when both skipped indices are the same (i.e., $i = j$) is given by: $$\text{dropPairEmb}(i, i, m) = \begin{cases} m & \text{if } m < i \\ m + 2 & \text{if } m \ge i \end{cases}$$ In this case, the embedding from $\text{Fin } n$ to $\text{Fin } (n+2)$ specifically skips the indices $i$ and $i+1$.

For any natural number $n$, let $i \in \text{Fin}(n+2)$ and $j \in \text{Fin}(n+1)$. The embedding $\text{dropPairEmb}(i, i.\text{succAbove}(j))$, which maps $\text{Fin } n$ to $\text{Fin}(n+2)$ by skipping the indices $i$ and $i.\text{succAbove}(j)$, is equal to the composition of the successor maps $i.\text{succAbove} \circ j.\text{succAbove}$. Here, $k.\text{succAbove}$ denotes the standard map that embeds $\text{Fin } m$ into $\text{Fin}(m+1)$ by skipping the index $k$.

For any natural number $n$ and any two indices $i, j \in \{0, \dots, n+1\}$, the function $\text{dropPairEmb}_{i,j} : \{0, \dots, n-1\} \to \{0, \dots, n+1\}$, which embeds $\text{Fin } n$ into $\text{Fin } (n+2)$ by skipping the indices $i$ and $j$, is injective.

For any natural number $n$ and two indices $i, j \in \{0, \dots, n+1\}$, let $\text{dropPairEmb}_{i,j} : \{0, \dots, n-1\} \to \{0, \dots, n+1\}$ be the embedding function that skips the indices $i$ and $j$. For all $m_1, m_2 \in \{0, \dots, n-1\}$, the equality $\text{dropPairEmb}_{i,j}(m_1) = \text{dropPairEmb}_{i,j}(m_2)$ holds if and only if $m_1 = m_2$.

For any natural number $n$ and two indices $i, j \in \{0, \dots, n+1\}$, let $\text{dropPairEmb}_{i,j} : \{0, \dots, n-1\} \to \{0, \dots, n+1\}$ be the embedding function that skips the indices $i$ and $j$. For all $m_1, m_2 \in \{0, \dots, n-1\}$, the inequality $\text{dropPairEmb}_{i,j}(m_1) \le \text{dropPairEmb}_{i,j}(m_2)$ holds if and only if $m_1 \le m_2$.

For any natural number $n$ and two indices $i, j \in \{0, \dots, n+1\}$, let $\text{dropPairEmb}_{i,j} : \{0, \dots, n-1\} \to \{0, \dots, n+1\}$ be the embedding function that skips the indices $i$ and $j$. For all $m_1, m_2 \in \{0, \dots, n-1\}$, the strict inequality $\text{dropPairEmb}_{i,j}(m_1) < \text{dropPairEmb}_{i,j}(m_2)$ holds if and only if $m_1 < m_2$.

For any natural number $n$ and two indices $i, j \in \{0, \dots, n+1\}$, the embedding function $\text{dropPairEmb}_{i,j} : \{0, \dots, n-1\} \to \{0, \dots, n+1\}$, which skips the indices $i$ and $j$, is monotone. That is, for any $m_1, m_2 \in \{0, \dots, n-1\}$, if $m_1 \le m_2$, then $\text{dropPairEmb}_{i,j}(m_1) \le \text{dropPairEmb}_{i,j}(m_2)$.

For any natural number $n$ and any two distinct indices $i, j \in \text{Fin}(n+2)$ (where $i \neq j$), the function $\text{dropPairEmb}_{i,j}: \text{Fin } n \to \text{Fin}(n+2)$ is equal to the unique order-preserving embedding from $\text{Fin } n$ onto the complement of the set $\{i, j\}$.

For any natural number $n$ and any two indices $i, j \in \text{Fin}(n+2)$, the embedding $\text{dropPairEmb}_{i,j} : \text{Fin } n \to \text{Fin}(n+2)$, which maps elements of $\text{Fin } n$ into $\text{Fin}(n+2)$ by skipping the indices $i$ and $j$, is symmetric in its indices, such that $\text{dropPairEmb}_{i,j} = \text{dropPairEmb}_{j,i}$.

For any natural number $n$, any function $c: \text{Fin}(n+2) \to C$, and any indices $i, j \in \text{Fin}(n+2)$, the value of $c$ at the image of $k \in \text{Fin } n$ under the embedding $\text{dropPairEmb}_{i,j}$ is equal to its value under the embedding $\text{dropPairEmb}_{j,i}$. That is, $c(\text{dropPairEmb}_{i,j}(k)) = c(\text{dropPairEmb}_{j,i}(k))$ for all $k \in \text{Fin } n$, where $\text{dropPairEmb}_{i,j}$ is the embedding that skips the indices $i$ and $j$.

For any natural number $n$ and distinct indices $i, j \in \text{Fin}(n+2)$, let $\text{dropPairEmb}_{i,j} : \text{Fin } n \to \text{Fin}(n+2)$ be the embedding that skips indices $i$ and $j$. For any $m \in \text{Fin } n$, the value $(\text{dropPairEmb}_{i,j}) \, m$ is equal to the image of $m$ under the unique order-preserving isomorphism from $\text{Fin } n$ onto the complement set $\{i, j\}^c \subseteq \text{Fin}(n+2)$.

For any natural number $n$ and distinct indices $i, j \in \{0, \dots, n+1\}$ (where $i \neq j$), the range of the embedding $\text{dropPairEmb}_{i,j}: \{0, \dots, n-1\} \to \{0, \dots, n+1\}$, which skips the indices $i$ and $j$, is equal to the complement of the set $\{i, j\}$ in $\{0, \dots, n+1\}$.

For any natural number $n$ and distinct indices $i, j \in \text{Fin}(n+2)$, let $\text{dropPairEmb}_{i,j}: \text{Fin } n \to \text{Fin}(n+2)$ be the embedding that skips the indices $i$ and $j$. For any subset $X \subseteq \text{Fin } n$, let $X^c$ denote its complement in $\text{Fin } n$. The image of $X^c$ under $\text{dropPairEmb}_{i,j}$ is equal to the complement in $\text{Fin}(n+2)$ of the union of $\{i, j\}$ and the image of $X$ under $\text{dropPairEmb}_{i,j}$: $$\text{dropPairEmb}_{i,j}(X^c) = (\{i, j\} \cup \text{dropPairEmb}_{i,j}(X))^c$$

For any natural number $n$ and any indices $i, j \in \{0, \dots, n+1\}$, let $\text{dropPairEmb}_{i,j}: \{0, \dots, n-1\} \to \{0, \dots, n+1\}$ be the embedding that skips the indices $i$ and $j$. For any $m \in \{0, \dots, n-1\}$, it holds that $i \neq \text{dropPairEmb}_{i,j}(m)$.

For any natural number $n$ and any indices $i, j \in \{0, \dots, n+1\}$, let $\text{dropPairEmb}_{i,j}: \{0, \dots, n-1\} \to \{0, \dots, n+1\}$ be the embedding that skips the indices $i$ and $j$. For any $m \in \{0, \dots, n-1\}$, it holds that $\text{dropPairEmb}_{i,j}(m) \neq i$.

For any natural number $n$ and any indices $i, j \in \{0, \dots, n+1\}$, let $\text{dropPairEmb}_{i,j}: \{0, \dots, n-1\} \to \{0, \dots, n+1\}$ be the embedding that skips the indices $i$ and $j$. For any $m \in \{0, \dots, n-1\}$, it holds that $j \neq \text{dropPairEmb}_{i,j}(m)$.

For any natural number $n$ and any indices $i, j \in \{0, \dots, n+1\}$, the embedding function $\text{dropPairEmb}(i, j, m)$, which maps elements of $\{0, \dots, n-1\}$ to $\{0, \dots, n+1\}$ by skipping the indices $i$ and $j$, satisfies $\text{dropPairEmb}(i, j, m) \neq j$ for all $m \in \{0, \dots, n-1\}$.

For any natural number $n$, let $i \in \text{Fin}(n+2)$ and $j \in \text{Fin}(n+1)$. The embedding $\text{dropPairEmb}(i, i.\text{succAbove}(j))$, which maps $\text{Fin } n$ to $\text{Fin}(n+2)$ by skipping the indices $i$ and $i.\text{succAbove}(j)$, is equal to the composition of the successor maps $i.\text{succAbove} \circ j.\text{succAbove}$. Here, $k.\text{succAbove}$ denotes the standard embedding that maps $\text{Fin } m$ into $\text{Fin}(m+1)$ by skipping the index $k$.

Given $n \in \mathbb{N}$ and two distinct indices $i, j \in \{0, 1, \dots, n+1\}$, let $m \in \{0, 1, \dots, n+1\}$ be an index such that $m \neq i$ and $m \neq j$. The function returns the index of $m$ in the ordered set formed by removing $i$ and $j$ from $\{0, 1, \dots, n+1\}$. Formally, for $i, j, m \in \text{Fin}(n+2)$, the mapping is defined as: \[ f(i, j, m) = \begin{cases} m & \text{if } m < i \text{ and } m < j \\ m - 1 & \text{if } \min(i, j) < m < \max(i, j) \\ m - 2 & \text{if } m > i \text{ and } m > j \end{cases} \] This value represents the preimage of $m$ under the embedding that maps $\text{Fin } n$ to the complement of $\{i, j\}$ in $\text{Fin}(n+2)$.

Let $n$ be a natural number and $i, j \in \{0, \dots, n+1\}$ be two distinct indices. For any $m \in \{0, \dots, n+1\}$ such that $m \neq i$ and $m \neq j$, let $\text{dropPairEmbPre}(i, j, m)$ be the index of $m$ in the ordered set formed by removing $i$ and $j$ from $\{0, \dots, n+1\}$. Furthermore, let $\text{dropPairEmb}(i, j, \cdot)$ be the embedding from $\{0, \dots, n-1\}$ into $\{0, \dots, n+1\}$ that skips the indices $i$ and $j$. Then, applying the embedding to the relative index of $m$ returns the original index: $$\text{dropPairEmb}(i, j, \text{dropPairEmbPre}(i, j, m)) = m$$

Let $n$ be a natural number and let $i, j \in \text{Fin}(n+2)$ be two distinct indices. For any index $m \in \text{Fin}(n+2)$ such that $m \neq i$ and $m \neq j$, let $\text{dropPairEmbPre}(i, j, m)$ be the index of $m$ in the ordered set formed by removing $i$ and $j$ from $\{0, \dots, n+1\}$. Then $\text{dropPairEmbPre}(i, j, m)$ is equal to the image of $m$ under the inverse of the unique order-preserving isomorphism from $\text{Fin } n$ onto the complement set $\{i, j\}^c \subseteq \text{Fin}(n+2)$.

Let $n$ be a natural number and $i, j \in \text{Fin}(n+2)$ be two distinct indices. Let $\text{dropPairEmbPre}(i, j, m)$ be the function that maps an index $m \in \text{Fin}(n+2)$ (where $m \neq i$ and $m \neq j$) to its relative position in the ordered set formed by removing $i$ and $j$ from $\{0, \dots, n+1\}$. For any two indices $m_1, m_2 \in \text{Fin}(n+2)$ such that $m_1, m_2 \notin \{i, j\}$, their relative indices are equal if and only if the original indices are equal: $$\text{dropPairEmbPre}(i, j, m_1) = \text{dropPairEmbPre}(i, j, m_2) \iff m_1 = m_2$$

Let $n$ be a natural number and let $i, j \in \{0, \dots, n+1\}$ be two distinct indices. For any $m \in \{0, \dots, n-1\}$, there exists an index $m' \in \{0, \dots, n+1\}$ such that $m' \neq i$ and $m' \neq j$, and the relative index of $m'$ in the ordered set formed by removing $i$ and $j$ from $\{0, \dots, n+1\}$ (denoted as $\text{dropPairEmbPre}(i, j, m')$) is equal to $m$. That is, the mapping $\text{dropPairEmbPre}$ is surjective.

Let $n$ be a natural number and let $i, j \in \{0, \dots, n+1\}$ be distinct indices. Let $\text{dropPairEmb}(i, j, \cdot) : \text{Fin } n \to \text{Fin } (n+2)$ be the embedding that maps the set $\{0, \dots, n-1\}$ into $\{0, \dots, n+1\}$ by skipping the indices $i$ and $j$. For any $m' \in \text{Fin } (n+2)$ such that $m' \neq i$ and $m' \neq j$, let $\text{dropPairEmbPre}(i, j, m')$ be the relative index of $m'$ in the ordered set formed by removing $i$ and $j$ from $\{0, \dots, n+1\}$. Then, for any $m \in \text{Fin } n$, it holds that $$\text{dropPairEmbPre}(i, j, \text{dropPairEmb}(i, j, m)) = m$$

Let $n$ be a natural number. 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. We define the following transformed indices: - $i_2' = \text{dropPairEmb}_{i_1, j_1}(i_2)$ and $j_2' = \text{dropPairEmb}_{i_1, j_1}(j_2)$, which are the images of $i_2$ and $j_2$ under the embedding that skips $i_1$ and $j_1$. - $i_1' = \text{dropPairEmbPre}_{i_2', j_2'}(i_1)$ and $j_1' = \text{dropPairEmbPre}_{i_2', j_2'}(j_1)$, which are the relative indices of $i_1$ and $j_1$ in the set formed by removing $i_2'$ and $j_2'$. Then, the composition of the embeddings that skip these pairs of indices is commutative in the following sense: $$\text{dropPairEmb}_{i_1, j_1} \circ \text{dropPairEmb}_{i_2, j_2} = \text{dropPairEmb}_{i_2', j_2'} \circ \text{dropPairEmb}_{i_1', j_1'}$$

Let $n$ be a natural number. 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. We define the following transformed indices: - $i_2' = \text{dropPairEmb}_{i_1, j_1}(i_2)$ and $j_2' = \text{dropPairEmb}_{i_1, j_1}(j_2)$, which are the images of $i_2$ and $j_2$ under the embedding that skips $i_1$ and $j_1$. - $i_1' = \text{dropPairEmbPre}_{i_2', j_2'}(i_1)$ and $j_1' = \text{dropPairEmbPre}_{i_2', j_2'}(j_1)$, which are the relative indices of $i_1$ and $j_1$ in the set formed by removing $i_2'$ and $j_2'$. For any $m \in \text{Fin } n$, applying the two skip-embeddings in the order $(i_1', j_1')$ then $(i_2', j_2')$ is equivalent to applying them in the order $(i_2, j_2)$ then $(i_1, j_1)$: $$\text{dropPairEmb}_{i_2', j_2'}(\text{dropPairEmb}_{i_1', j_1'}(m)) = \text{dropPairEmb}_{i_1, j_1}(\text{dropPairEmb}_{i_2, j_2}(m))$$

Let $n$ be a natural number and $c : \text{Fin}(n+4) \to C$ be a function mapping indices to a set $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. We define the following transformed indices: - $i_2' = \text{dropPairEmb}_{i_1, j_1}(i_2)$ and $j_2' = \text{dropPairEmb}_{i_1, j_1}(j_2)$ are the images of $i_2$ and $j_2$ under the embedding that skips $i_1$ and $j_1$. - $i_1' = \text{dropPairEmbPre}_{i_2', j_2'}(i_1)$ and $j_1' = \text{dropPairEmbPre}_{i_2', j_2'}(j_1)$ are the relative indices of $i_1$ and $j_1$ in the set formed by removing $i_2'$ and $j_2'$. Then the composition of the index mappings $(c \circ \text{dropPairEmb}_{i_2', j_2'}) \circ \text{dropPairEmb}_{i_1', j_1'}$ and $(c \circ \text{dropPairEmb}_{i_1, j_1}) \circ \text{dropPairEmb}_{i_2, j_2}$ satisfies the permutation condition with the identity map. Specifically, the two composed functions are equal: $$(c \circ \text{dropPairEmb}_{i_2', j_2'}) \circ \text{dropPairEmb}_{i_1', j_1'} = (c \circ \text{dropPairEmb}_{i_1, j_1}) \circ \text{dropPairEmb}_{i_2, j_2}$$

Given natural numbers $n$ and $n_1$, a bijection $\sigma : \text{Fin}(n_1 + 2) \to \text{Fin}(n + 2)$, and two distinct indices $i, j \in \text{Fin}(n_1 + 2)$, the function `dropPairOfMap` defines a map from $\text{Fin } n_1$ to $\text{Fin } n$. For an input $m \in \text{Fin } n_1$, the output is calculated by: 1. Mapping $m$ to an index in $\text{Fin}(n_1 + 2)$ using an embedding that skips $i$ and $j$. 2. Applying the bijection $\sigma$ to this index. 3. Mapping the resulting index in $\text{Fin}(n + 2)$ back to $\text{Fin } n$ using the logic of a preimage that skips the values $\sigma(i)$ and $\sigma(j)$. This represents the induced map between the remaining elements after removing $\{i, j\}$ from the domain and $\{\sigma(i), \sigma(j)\}$ from the codomain.

Let $n, n_1$ be natural numbers and let $\sigma : \text{Fin}(n_1 + 2) \to \text{Fin}(n + 2)$ be a bijective map. For any two distinct indices $i, j \in \text{Fin}(n_1 + 2)$, the induced map $f: \text{Fin } n_1 \to \text{Fin } n$ (defined as `dropPairOfMap i j hij σ hσ`) is injective. This induced map $f$ is defined by taking an index $m \in \text{Fin } n_1$, embedding it into $\text{Fin}(n_1 + 2)$ by skipping the indices $i$ and $j$, applying the bijection $\sigma$, and then mapping the result back to $\text{Fin } n$ by identifying its position in the set $\text{Fin}(n + 2)$ excluding $\sigma(i)$ and $\sigma(j)$.

Let $n, n_1$ be natural numbers and let $\sigma : \text{Fin}(n_1 + 2) \to \text{Fin}(n + 2)$ be a bijective map. For any two distinct indices $i, j \in \text{Fin}(n_1 + 2)$, the induced map $f: \text{Fin } n_1 \to \text{Fin } n$ (defined as `dropPairOfMap i j hij σ hσ`) is surjective. This induced map $f$ is defined by taking an index $m \in \text{Fin } n_1$, embedding it into $\text{Fin}(n_1 + 2)$ by skipping the indices $i$ and $j$, applying the bijection $\sigma$, and then mapping the result back to $\text{Fin } n$ by identifying its position in the set $\text{Fin}(n + 2)$ excluding $\sigma(i)$ and $\sigma(j)$.

Let $n, n_1$ be natural numbers and let $\sigma : \text{Fin}(n_1 + 2) \to \text{Fin}(n + 2)$ be a bijective map. For any two distinct indices $i, j \in \text{Fin}(n_1 + 2)$, the induced map $f: \text{Fin } n_1 \to \text{Fin } n$ (defined as `dropPairOfMap i j hij σ hσ`) is bijective. This map $f$ is defined by taking an index $m \in \text{Fin } n_1$, embedding it into $\text{Fin}(n_1 + 2)$ by skipping the indices $i$ and $j$, applying the bijection $\sigma$, and then mapping the result back to $\text{Fin } n$ by identifying its position in the set $\text{Fin}(n + 2)$ excluding $\sigma(i)$ and $\sigma(j)$.

Let $n, n_1$ be natural numbers and $C$ be a set of index colors. Consider two index colorings $c: \text{Fin}(n+2) \to C$ and $c_1: \text{Fin}(n_1+2) \to C$. Suppose there exists a map $\sigma: \text{Fin}(n_1+2) \to \text{Fin}(n+2)$ that satisfies the permutation condition for $c$ and $c_1$ (meaning $\sigma$ is a bijection such that $c \circ \sigma = c_1$). For any two distinct indices $i, j \in \text{Fin}(n_1+2)$, let $\sigma': \text{Fin } n_1 \to \text{Fin } n$ be the induced map defined by `dropPairOfMap`, which removes $\{i, j\}$ from the domain and $\{\sigma(i), \sigma(j)\}$ from the codomain. Then $\sigma'$ satisfies the permutation condition for the reduced colorings $c \circ \text{dropPairEmb}(\sigma(i), \sigma(j))$ and $c_1 \circ \text{dropPairEmb}(i, j)$.

Let $n_1$ be a natural number and let $i, j \in \text{Fin}(n_1 + 2)$ be distinct indices. Let $\text{id}$ denote the identity function on $\text{Fin}(n_1 + 2)$. Then the map $\text{dropPairOfMap}$ induced by $\text{id}$ after removing the indices $i$ and $j$ is the identity function on $\text{Fin } n_1$. That is, $$\text{dropPairOfMap}(i, j, \text{id}) = \text{id}_{\text{Fin } n_1}$$

Given a tensor species $S$, a sequence of colors $c : \text{Fin}(n+2) \to C$, and a pure tensor $p$ of type $\text{Pure } S \, c$, let $i$ and $j$ be two distinct indices in $\text{Fin}(n+2)$. The function `dropPair` produces a new pure tensor of type $\text{Pure } S \, (c \circ \text{dropPairEmb}_{i, j})$ by removing the $i$-th and $j$-th components of $p$. Specifically, for any $m \in \text{Fin } n$, the $m$-th component of the resulting tensor corresponds to the component of $p$ at the index $\text{dropPairEmb}(i, j, m)$.

Let $S$ be a tensor species over a field $k$ and a group $G$. Let $c: \text{Fin}(n+2) \to C$ be a sequence of colors, and let $i, j$ be two distinct indices in $\text{Fin}(n+2)$. For any pure tensor $p$ of type $\text{Pure}(S, c)$ and any group element $g \in G$, the operation of dropping the $i$-th and $j$-th components of the tensor is equivariant with respect to the group action of $G$. Specifically, $$\text{dropPair}_{i, j}(g \cdot p) = g \cdot \text{dropPair}_{i, j}(p),$$ where $\cdot$ denotes the component-wise action of $G$ on the pure tensor.