Physlib.Relativity.Tensors.Contraction.UnitTensorContraction

Let $S$ be a tensor species over a ring $k$. Let $t_1$ be a tensor in $\text{Tensor}_S(c_A)$ of rank $n_A + 1$, and let $i$ be an index in $\{0, \dots, n_A\}$ such that the color of the $i$-th slot is $c$ (i.e., $c_A(i) = c$). Let $\text{unitTensor}(c)$ be the unit tensor associated with color $c$, which has the color sequence $(\tau(c), c)$, where $\tau$ denotes the duality map. The contraction of the $i$-th slot of $t_1$ against the first slot (index $0$) of $\text{unitTensor}(c)$ is equivalent to a permutation of $t_1$ that moves the $i$-th index to the last position. Specifically, $$\text{crossToEnd}(i, 0, h_{\text{dual}}, t_1, \text{unitTensor}(c)) = \text{permT}(\sigma, h_{\text{reindex}}, t_1)$$ where $h_{\text{dual}}$ is the proof that $S.\tau(c_A(i))$ matches the color of the first slot of the unit tensor, and $\sigma$ is the permutation that maps the first $n_A$ indices to the surviving indices of $t_1$ (skipping $i$) and maps the last index to $i$.

Let $S$ be a tensor species and $a, b, d, e$ be index colors. If $a = S.\tau e$ (the dual color of $e$ is $a$), then the identity map $\text{id}: \{0, 1\} \to \{0, 1\}$ is a reindexing from the color sequence $(S.\tau e, e)$ to the sequence $(a, e)$ formed by taking the first color of $(a, d)$ and the second color of $(b, e)$.

Let $S$ be a tensor species and $c: \{0, \dots, n\} \to C$ be a sequence of colors. Let $t \in \text{Tensor}_S(c)$ be a tensor of rank $n+1$. Let $M_1$ be a rank-2 tensor of colors $(\tau(c_i), d)$ and $M_2$ be a rank-2 tensor of colors $(\tau(d), c_i)$, where $i \in \{0, \dots, n\}$ and $d \in C$. Suppose that contracting the second slot of $M_1$ with the first slot of $M_2$ results in the unit tensor of color $c_i$: $$\text{crossToEnd}(1, 0, \text{rfl}, M_1, M_2) = \text{unitTensor}(c_i)$$ (where the identity reindexing is understood). Then, performing a "round trip" contraction—first contracting the $i$-th slot of $t$ with the first slot of $M_1$, and then contracting the resulting last slot (corresponding to the index $d$) with the first slot of $M_2$—is equivalent to applying a permutation to the original tensor $t$. Specifically: $$\text{crossToEnd}(\text{last}, 0, \text{h}, (\text{crossToEnd}(i, 0, \text{rfl}, t, M_1)), M_2) = \text{permT}(\sigma, h', t)$$ where the permutation $\sigma: \{0, \dots, n\} \to \{0, \dots, n\}$ is defined by $\text{append}(i.\text{succAbove}, \text{last})$, which effectively moves the $i$-th slot of $t$ to the final position.

Let $S$ be a tensor species and $t$ be a tensor with color sequence $c = (c_0, \dots, c_n)$. Let $i$ be a specific slot index and let $e = c_i$ be the color at that slot. Consider two rank-2 tensors $M$ with colors $(a, d)$ and $M'$ with colors $(b, e)$, where $a = \tau(e)$ (the dual color of $e$) and $b = \tau(d)$ (the dual color of $d$). Suppose that contracting the second slot of $M$ with the first slot of $M'$ results in the unit tensor of color $e$: $$\text{crossToEnd}(1, 0, M, M') = \delta_e$$ (where $\delta_e$ is the unit tensor associated with color $e$). Then, performing a "round trip" contraction on the $i$-th slot of $t$—first contracting it with $M$ (which replaces the color $c_i$ with $d$) and then contracting the resulting $i$-th slot with $M'$ (which replaces $d$ back with $e$)—recovers the original tensor $t$: $$\text{crossToSlot}_i(M', \text{crossToSlot}_i(M, t)) = t$$ The equality holds up to an identity reindexing of the color sequence.

Let $S$ be a tensor species over a ring $k$ and $t$ be a tensor with color sequence $c$. Let $i$ be a specific slot index such that the color at that slot is $c_i = e$. Consider two rank-2 tensors $M$ and $M'$ with color sequences $(a, d)$ and $(b, e)$ respectively, where $a$ is the dual color of $c_i$ ($a = \tau(e)$) and $b$ is the dual color of $d$ ($b = \tau(d)$). Assuming $M$ and $M'$ form a matched pair that contracts to the unit tensor, then first "raising" the index at slot $i$ by contracting it with $M$ (using `crossToSlot`) and then "lowering" it back using $M'$ (using `crossToSlotInv`) returns the original tensor $t$: $$\text{crossToSlotInv}_i(M', \text{crossToSlot}_i(M, t)) = t$$

Let $S$ be a tensor species over a ring $k$. Let $c: \{0, \dots, n\} \to C$ be a color sequence, $i \in \{0, \dots, n\}$ be a slot index, and $e = c(i)$ be the color at that slot. Let $d \in C$ be a color, and let $a, b \in C$ be colors such that $a = \tau(e)$ and $b = \tau(d)$, where $\tau$ is the duality map. Let $M$ be a rank-2 tensor with colors $(a, d)$ and $M'$ be a rank-2 tensor with colors $(b, e)$. For any tensor $t$ with the color sequence $c$ updated at index $i$ to color $d$ (denoted as $c[i \mapsto d]$), applying the inverse result-to-slot contraction `crossToSlotInv` with $M'$ followed by the result-to-slot contraction `crossToSlot` with $M$ at index $i$ returns the original tensor $t$: $$\text{crossToSlot}_i(M, \text{crossToSlotInv}_i(M', t)) = t$$ This identity demonstrates that "raising" an index (contracting with $M$) is the left inverse of "lowering" (the inverse operation with $M'$) under the assumption that $M$ and $M'$ are a matched pair of dual tensors.

Let $S$ be a tensor species over a ring $k$. Given a color sequence $c: \{0, \dots, n\} \to C$, an index $i \in \{0, \dots, n\}$, and a target color $d \in C$, the map `crossToSlotEquiv` is a $k$-linear equivalence between the tensor spaces: $$\text{Tensor}(S, c) \cong \text{Tensor}(S, c[i \mapsto d])$$ where $c[i \mapsto d]$ denotes the color sequence $c$ with the $i$-th entry updated to $d$. This equivalence is constructed using a pair of rank-2 tensors $M$ and $M'$ (such as a metric and its inverse) that are mutually inverse, meaning their contractions in both orders result in the unit tensor. The forward map is defined by the result-to-slot contraction `crossToSlot` at index $i$ with $M$, and the inverse map is `crossToSlotInv` at index $i$ with $M'$. This formalizes the physical operation of raising or lowering the $i$-th index of a tensor.