Physlib.Relativity.Tensors.Contraction.Products

Given a natural number $n$, let $i$ and $j$ be two distinct indices in $\text{Fin}(n+2)$. For any index $m \in \text{Fin}(n)$, if $m < i$ and $m < j$, then the embedding map $\text{dropPairEmb}(i, j)$ (which maps indices from $\text{Fin}(n)$ to $\text{Fin}(n+2)$ by skipping positions $i$ and $j$) satisfies $\text{dropPairEmb}(i, j)(m) = m$.

Given natural numbers $n$ and $n_1$, let $i$ and $j$ be distinct indices in $\text{Fin}(n+2)$. Let $\text{dropPairEmb}$ be the order-preserving embedding from $\text{Fin}(n_1 + n)$ to $\text{Fin}(n_1 + n + 2)$ that skips the indices $n_1 + i$ and $n_1 + j$. For any index $m \in \text{Fin}(n_1)$, when $m$ is viewed as an element of $\text{Fin}(n_1 + n)$, the embedding satisfies $\text{dropPairEmb}(n_1 + i, n_1 + j)(m) = m$, where the result is viewed as an element of $\text{Fin}(n_1 + n + 2)$.

Let $n$ and $n_1$ be natural numbers, and let $i$ and $j$ be distinct indices in $\text{Fin}(n+2)$. Let $\text{dropPairEmb}_{n_1+i, n_1+j}$ be the order-preserving embedding from $\text{Fin}(n_1 + n)$ to $\text{Fin}(n_1 + n + 2)$ that skips the indices $n_1 + i$ and $n_1 + j$. The image of the range of the inclusion map $\text{Fin}(n_1) \hookrightarrow \text{Fin}(n_1 + n)$ under this embedding is the set of indices in $\text{Fin}(n_1 + n + 2)$ whose value is strictly less than $n_1$.

Let $n$ and $n_1$ be natural numbers, and let $i$ and $j$ be distinct indices in $\text{Fin}(n+2)$. Let $m$ be an index in $\text{Fin}(n)$. Let $\text{dropPairEmb}_{i, j} : \text{Fin}(n) \hookrightarrow \text{Fin}(n+2)$ be the order-preserving embedding that skips the indices $i$ and $j$. Let $\text{natAdd}_{n_1}$ denote the map that shifts an index by $n_1$ (i.e., $\text{natAdd}_{n_1}(x) = n_1 + x$). Then, shifting the index and the skipped pair by $n_1$ commutes with the embedding: $$\text{dropPairEmb}_{n_1+i, n_1+j}(n_1+m) = n_1 + \text{dropPairEmb}_{i, j}(m)$$

Let $n, n_1$ be natural numbers. Let $c : \text{Fin}(n+2) \to C$ and $c_1 : \text{Fin}(n_1) \to C$ be index maps. Let $i, j$ be distinct indices in $\text{Fin}(n+2)$ satisfying the duality condition $S.\tau(c(i)) = c(j)$. Let $i' = n_1 + i$ and $j' = n_1 + j$ be the shifted indices in the concatenated index space $\text{Fin}(n_1 + n + 2)$. The identity map $\text{id}$ satisfies the permutation condition between: 1. The concatenation of $c_1$ and $c$, composed with the embedding $\text{dropPairEmb}_{i', j'}$ that skips the shifted indices. 2. The concatenation of $c_1$ and the map $c$ restricted to the indices remaining after skipping $i$ and $j$ via $\text{dropPairEmb}_{i, j}$. Mathematically, this identity holds: $$(c_1 \text{ append } c) \circ \text{dropPairEmb}_{n_1+i, n_1+j} = c_1 \text{ append } (c \circ \text{dropPairEmb}_{i, j})$$

Let $S$ be a tensor species over a field $k$ and set of colors $C$ with a duality map $\tau$. Let $p_1$ be a pure tensor of rank $n_1$ and $p$ be a pure tensor of rank $n+2$. For any two distinct indices $i, j \in \{0, \dots, n+1\}$ such that the color of the $j$-th component of $p$ is dual to the color of the $i$-th component (i.e., $\tau(c_i) = c_j$), let $p_1 \otimes p$ denote the tensor product (concatenation) of $p_1$ and $p$. Then the contraction coefficient of $p_1 \otimes p$ at the indices shifted by $n_1$ is equal to the contraction coefficient of $p$ at the original indices: $$\text{contrPCoeff}(n_1 + i, n_1 + j, p_1 \otimes p) = \text{contrPCoeff}(i, j, p)$$

Let $S$ be a tensor species over a field $k$ and a set of colors $C$ with duality map $\tau$. Let $p$ be a pure tensor with index map $c: \text{Fin}(n+2) \to C$, and let $p_1$ be a pure tensor with index map $c_1: \text{Fin}(n_1) \to C$. Suppose $i$ and $j$ are two distinct indices in $\text{Fin}(n+2)$ such that the color of the $j$-th index is dual to the color of the $i$-th index, i.e., $\tau(c(i)) = c(j)$. Let $p \otimes p_1$ denote the tensor product of $p$ and $p_1$. Then the contraction coefficient of the product $p \otimes p_1$ at the indices corresponding to $i$ and $j$ (embedded into the first $n+2$ slots of the combined index set) is equal to the contraction coefficient of $p$ at indices $i$ and $j$.

Let $S$ be a tensor species over a field $k$ and a set of colors $C$ with a duality map $\tau$. Let $p_1$ be a pure tensor of rank $n_1$ and $p$ be a pure tensor of rank $n+2$. Let $i$ and $j$ be distinct indices in the index set $\{0, \dots, n+1\}$ of $p$ such that the color of the $j$-th component is dual to the color of the $i$-th component (i.e., $\tau(c(i)) = c(j)$). The theorem states that taking the tensor product of $p_1$ with the tensor formed by dropping the components at indices $i$ and $j$ from $p$ is equal to first taking the tensor product $p_1 \otimes p$ and then dropping the components at the shifted indices $n_1 + i$ and $n_1 + j$: $$p_1 \otimes \text{dropPair}_{i, j}(p) = \text{permP}(\text{id}, H, \text{dropPair}_{n_1+i, n_1+j}(p_1 \otimes p))$$ where $\otimes$ denotes the concatenation of pure tensors, $\text{dropPair}$ denotes the removal of a specific pair of components, and $\text{permP}$ denotes the canonical re-indexing (permutation) required to identify the resulting index spaces.

Let $S$ be a tensor species over a field $k$ and a set of colors $C$ with a duality map $\tau$. Let $p_1$ be a pure tensor of rank $n_1$ and $p$ be a pure tensor of rank $n+2$. Suppose $i$ and $j$ are two distinct indices in the index set $\{0, \dots, n+1\}$ of $p$ such that the color of the $i$-th component is dual to the color of the $j$-th component (i.e., $\tau(c_i) = c_j$). The theorem states that the tensor product of the tensor representation of $p_1$ and the contraction of $p$ at indices $i$ and $j$ is equal to the contraction of the concatenated pure tensor product $p_1 \otimes p$ at the shifted indices $n_1 + i$ and $n_1 + j$, followed by a canonical re-indexing: $$\text{prodT}(p_1.\text{toTensor}, \text{contrP}(i, j, p)) = \text{permT}(\text{id}, H, \text{contrP}(n_1+i, n_1+j, p_1 \otimes p))$$ where $n_1+i$ and $n_1+j$ represent the indices $i$ and $j$ shifted into the second part of the concatenated index space $\text{Fin}(n_1 + n + 2)$, and $H$ is the permutation condition identifying the resulting index maps.

Let $S$ be a tensor species over a field $k$. Let $t_1$ be a tensor of rank $n_1$ with index color sequence $c_1$, and $t$ be a tensor of rank $n+2$ with index color sequence $c$. Suppose $i$ and $j$ are distinct indices in $\{0, \dots, n+1\}$ such that the color of the $i$-th component is dual to the color of the $j$-th component, satisfying $S.\tau(c(i)) = c(j)$. The theorem states that the tensor product of $t_1$ with the contraction of $t$ at indices $i$ and $j$ is equal to the contraction of the concatenated tensor product $t_1 \otimes t$ at the shifted indices $n_1 + i$ and $n_1 + j$, followed by a canonical re-indexing: $$\text{prodT}(t_1, \text{contrT}(i, j, t)) = \text{permT}(\text{id}, H, \text{contrT}(n_1+i, n_1+j, \text{prodT}(t_1, t)))$$ where $n_1+i$ and $n_1+j$ represent the original indices $i$ and $j$ shifted into the second part of the concatenated index space, and $H$ is the permutation condition identifying the resulting index maps.

Let $S$ be a tensor species over a field $k$. Let $t_1$ be a tensor of rank $n_1$ with index color sequence $c_1$, and $t$ be a tensor of rank $n+2$ with index color sequence $c$. Suppose $i$ and $j$ are distinct indices in $\{0, \dots, n+1\}$ such that the color of the $i$-th component is dual to the color of the $j$-th component, satisfying $S.\tau(c(i)) = c(j)$. The theorem states that the contraction of the concatenated tensor product $t_1 \otimes t$ at the shifted indices $n_1 + i$ and $n_1 + j$ is equal to the tensor product of $t_1$ and the contraction of $t$ at indices $i$ and $j$, followed by a canonical re-indexing: $$\text{contrT}(n_1+i, n_1+j, \text{prodT}(t_1, t)) = \text{permT}(\text{id}, H, \text{prodT}(t_1, \text{contrT}(i, j, t)))$$ where $n_1+i$ and $n_1+j$ represent the original indices $i$ and $j$ of $t$ shifted into the second part of the concatenated index space, and $H$ is the permutation condition identifying the resulting index maps.