Physlib.Relativity.Tensors.ComponentIdx.Contraction

For any natural number $n$, index structure $c: \text{Fin}(n+2) \to C$, and pair of indices $i, j \in \text{Fin}(n+2)$, let $b \in \text{ComponentIdx}(c \circ \text{succSuccAbove}_{i,j})$ be a multi-index of a tensor with two positions removed, and let $b' \in \text{ComponentIdx}(c)$ be a multi-index of the original tensor. Then $b'$ is an element of the set $\text{DropPairSection}(b)$ if and only if for every $m \in \text{Fin}(n)$, the component of $b'$ at the position $\text{succSuccAbove}_{i,j}(m)$ is equal to the component $b(m)$.

Let $n \in \mathbb{N}$ and $c : \text{Fin}(n+2) \to C$ be an index structure for a tensor of rank $n+2$. Let $i, j \in \text{Fin}(n+2)$ be distinct indices ($i \neq j$). Given a reduced multi-index $b$ for the structure $c \circ \text{succSuccAbove}_{i,j}$ and a pair of coordinate values $x = (x_1, x_2)$ for the positions $i$ and $j$ (where $x_1 \in \text{basisIdx}(c_i)$ and $x_2 \in \text{basisIdx}(c_j)$), the multi-index constructed by inserting $x$ into $b$, denoted as $\text{ofFin}_{i,j}(b, x)$, is an element of the fiber $\text{DropPairSection}(b)$.

Let $n$ be a natural number and let $c: \{0, \dots, n+1\} \to C$ define the index structure of a tensor. For any multi-index $r \in \text{ComponentIdx}(c)$ and any two distinct index positions $i, j \in \{0, \dots, n+1\}$, let $\text{dropPair}_{i,j}(r)$ be the reduced multi-index of length $n$ obtained by removing the components of $r$ at positions $i$ and $j$. The theorem states that if we restore the dropped components by applying the equivalence $\text{ofFinEquiv}_{i,j}$ to the reduced index $\text{dropPair}_{i,j}(r)$ and the original values at those positions $(r_i, r_j)$, the result is equal to the original multi-index $r$.