Physlib.Relativity.Tensors.Product

Given natural numbers $n_1$ and $n_2$, and color sequence mappings $c : \{0, \ldots, n_1 - 1\} \to C$ and $c_1 : \{0, \ldots, n_2 - 1\} \to C$, this defines the equivalence between the component indices of the appended sequence, denoted as `ComponentIdx (Fin.append c c1)`, and the dependent product $\prod_{i \in \{0, \ldots, n_1 - 1\} \sqcup \{0, \ldots, n_2 - 1\}} \{0, \ldots, \text{repDim}(S_{(c \sqcup c_1)(i)}) - 1\}$, where $c \sqcup c_1$ represents the disjoint union (sum elimination) of the sequences $c$ and $c_1$.

Given color sequences $c: \{0, \dots, n_1-1\} \to C$ and $c_1: \{0, \dots, n_2-1\} \to C$, and component indices $b \in \text{ComponentIdx}(c)$ and $b_1 \in \text{ComponentIdx}(c_1)$, their product is a component index for the concatenated color sequence $c \mathbin{+\!+} c_1$. Specifically, for an index $i \in \{0, \dots, n_1+n_2-1\}$, the value of the product index at $i$ is $b(i)$ if $i < n_1$, and $b_1(i - n_1)$ if $n_1 \leq i < n_1 + n_2$.

Let $n_1, n_2 \in \mathbb{N}$ and let $c: \text{Fin}(n_1) \to C$ and $c_1: \text{Fin}(n_2) \to C$ be color sequences. For component indices $b \in \text{ComponentIdx}(c)$ and $b_1 \in \text{ComponentIdx}(c_1)$, their product $b \cdot b_1$ is a component index for the concatenated sequence $c \mathbin{+\!+} c_1$. Let $\phi: \text{Fin}(n_1) \oplus \text{Fin}(n_2) \xrightarrow{\simeq} \text{Fin}(n_1 + n_2)$ be the standard equivalence between the disjoint union and the finite set of the sum. For any $i \in \text{Fin}(n_1) \oplus \text{Fin}(n_2)$, the evaluation of the product index is given by: $$(b \cdot b_1)(\phi(i)) = \begin{cases} b(i) & \text{if } i \in \text{Fin}(n_1) \\ b_1(i) & \text{if } i \in \text{Fin}(n_2) \end{cases}$$

Let $S$ be a tensor species. For any two color sequences $c: \{0, \dots, n_1-1\} \to C$ and $c_1: \{0, \dots, n_2-1\} \to C$, let $\text{ComponentIdx}(c)$ be the set of basis indices for a tensor with colors $c$. This definition establishes a bijective correspondence (equivalence) between the component indices of the concatenated color sequence, $\text{ComponentIdx}(c \mathbin{+\!+} c_1)$, and the Cartesian product of the individual component index sets $\text{ComponentIdx}(c) \times \text{ComponentIdx}(c_1)$. Specifically, the forward map splits a combined index into its first $n_1$ and subsequent $n_2$ components, while the inverse map concatenates a pair of indices $(b, b_1)$ into a single index for the combined sequence.

Let $S$ be a tensor species, and let $c : \text{Fin}(n_1) \to C$ and $c_1 : \text{Fin}(n_2) \to C$ be index maps. This establishes an equivalence between the pure tensors of $S$ indexed by the concatenation of $c$ and $c_1$, and the dependent product $\prod_{i \in \text{Fin}(n_1) \sqcup \text{Fin}(n_2)} S.FD((c \sqcup c_1)(i))$, where $c \sqcup c_1$ is the induced map on the disjoint union $\text{Fin}(n_1) \sqcup \text{Fin}(n_2)$ and $S.FD$ is the functor mapping indices to their associated vector spaces.

Let $S$ be a tensor species. For any two pure tensors $p_1$ and $p_2$ with index maps $c: \text{Fin}(n_1) \to C$ and $c_1: \text{Fin}(n_2) \to C$ respectively, their tensor product $p_1 \otimes p_2$ is the pure tensor in $\text{Pure}(S, c \text{ append } c_1)$ defined by the concatenation of their components. Specifically, for an index $i \in \text{Fin}(n_1)$, the component of the product is $p_1(i)$, and for $j \in \text{Fin}(n_2)$, the component at the corresponding shifted index is $p_2(j)$, subject to the appropriate canonical isomorphisms between the vector spaces.

Let $S$ be a tensor species. For any two pure tensors $p_1 \in \text{Pure}(S, c)$ and $p_2 \in \text{Pure}(S, c_1)$, where $c: \text{Fin}(n_1) \to C$ and $c_1: \text{Fin}(n_2) \to C$ are index maps, let $p_1 \otimes p_2$ denote their tensor product. Let $\phi : \text{Fin}(n_1) \oplus \text{Fin}(n_2) \cong \text{Fin}(n_1 + n_2)$ be the standard equivalence between the disjoint union and the combined finite set. For any index $i \in \text{Fin}(n_1) \oplus \text{Fin}(n_2)$, the component of the tensor product at $\phi(i)$ is given by: - If $i = \text{inl}(j)$ for $j \in \text{Fin}(n_1)$, then $(p_1 \otimes p_2)_{\phi(i)} = \psi_L(p_1(j))$, - If $i = \text{inr}(k)$ for $k \in \text{Fin}(n_2)$, then $(p_1 \otimes p_2)_{\phi(i)} = \psi_R(p_2(k))$, where $\psi_L$ and $\psi_R$ are canonical isomorphisms between the corresponding vector spaces in the tensor species (formally defined as the action of the functor $S.FD$ on the identity morphism).

Let $S$ be a tensor species. For any two pure tensors $p_1$ and $p_2$ with index maps $c: \text{Fin}(n_1) \to C$ and $c_1: \text{Fin}(n_2) \to C$ respectively, let $p_1 \otimes p_2$ denote their tensor product. For any index $i \in \text{Fin}(n_1)$, the component of the tensor product at the index $i$ (embedded into the combined index set $\text{Fin}(n_1 + n_2)$) is given by: $$(p_1 \otimes p_2)_i = \psi(p_1(i))$$ where $\psi$ is the canonical isomorphism between the vector spaces at the corresponding indices (formally defined as the action of the functor $S.FD$ on the identity morphism).

Let $S$ be a tensor species. For any two pure tensors $p_1$ and $p_2$ with index maps $c: \text{Fin}(n_1) \to C$ and $c_1: \text{Fin}(n_2) \to C$ respectively, let $p_1 \otimes p_2$ denote their tensor product. For any index $i \in \text{Fin}(n_2)$, the component of the tensor product at the shifted index $n_1 + i$ is given by: $$(p_1 \otimes p_2)_{n_1 + i} = \psi(p_2(i))$$ where $\psi$ is the canonical isomorphism between the vector spaces at the corresponding indices (formally defined as the action of the functor $S.FD$ on the identity morphism).

Let $S$ be a tensor species. For color sequences $c: \text{Fin}(n) \to C$ and $c_1: \text{Fin}(n_1) \to C$, let $b \in \text{ComponentIdx}(c)$ and $b_1 \in \text{ComponentIdx}(c_1)$ be component indices, and let $e_b$ and $e_{b_1}$ denote their corresponding pure basis vectors. The tensor product of these basis vectors is equal to the basis vector associated with the product of the component indices: $$e_b \otimes e_{b_1} = e_{b \cdot b_1}$$ where $\otimes$ denotes the product of pure tensors (`prodP`) and $b \cdot b_1$ denotes the product of component indices.

Let $S$ be a tensor species. For any two pure tensors $p$ and $p_1$ with color sequences $c: \text{Fin}(n) \to C$ and $c_1: \text{Fin}(m) \to C$ respectively, let $p \otimes p_1$ denote their tensor product. For any basis index $b$ of the concatenated color sequence $c \mathbin{+\!+} c_1$, the component of the product $p \otimes p_1$ at index $b$ is equal to the product of the individual components: $$(p \otimes p_1)_b = p_{b_1} \cdot (p_1)_{b_2}$$ where $(b_1, b_2)$ is the pair of indices in $\text{ComponentIdx}(c) \times \text{ComponentIdx}(c_1)$ corresponding to $b$ under the canonical equivalence.

Let $S$ be a tensor species and $G$ be a group acting on the tensors. For any group element $g \in G$ and any two pure tensors $p \in \text{Pure}(S, c)$ and $p_1 \in \text{Pure}(S, c_1)$, the tensor product operation is equivariant with respect to the group action: $$(g \cdot p) \otimes (g \cdot p_1) = g \cdot (p \otimes p_1)$$ where $\otimes$ denotes the tensor product of pure tensors (`prodP`) and $\cdot$ denotes the group action.

For any sequence of indices $c : \text{Fin } n \to C$ and an empty sequence of indices $c_1 : \text{Fin } 0 \to C$, the identity permutation $\text{id}$ satisfies the permutation condition between $c$ and the concatenation of $c$ and $c_1$.

Let $S$ be a tensor species. For any pure tensor $p \in \text{Pure}(S, c)$ with index map $c: \text{Fin}(n) \to C$ and any pure tensor $p_0 \in \text{Pure}(S, c_1)$ with an empty index map $c_1: \text{Fin}(0) \to C$, the tensor product $p \otimes p_0$ is equal to the pure tensor $p$ re-indexed via the identity permutation onto the concatenated index sequence $\text{Fin.append}(c, c_1)$.

For natural numbers \( n_1 \) and \( n_2 \), this defines the map between \( \text{Fin}(n_1 + n_2) \) and \( \text{Fin}(n_2 + n_1) \) formed by swapping the two blocks of elements.

For any natural numbers $n_1$ and $n_2$, and any index species mappings $c: \text{Fin } n_1 \to C$ and $c_2: \text{Fin } n_2 \to C$, the permutation $\text{prodSwapMap}(n_2, n_1)$—which swaps two blocks of indices of sizes $n_2$ and $n_1$—satisfies the permutation condition $\text{PermCond}$ relative to the concatenated index mappings $\text{Fin.append}(c, c_2)$ and $\text{Fin.append}(c_2, c)$. This ensures that the species of indices are preserved when the order of the tensor components is swapped.

Let $S$ be a tensor species. For any two pure tensors $p$ and $p_1$ with index mappings $c: \text{Fin } n \to C$ and $c_1: \text{Fin } n_1 \to C$ respectively, the tensor product $p \otimes p_1$ is equal to the permutation of the tensor product $p_1 \otimes p$ under the map $\text{prodSwapMap}(n, n_1)$, which swaps the block of $n$ indices with the block of $n_1$ indices. That is, $$p \otimes p_1 = \text{perm}_P(\text{prodSwapMap}(n, n_1))(p_1 \otimes p)$$ where $\text{perm}_P$ denotes the permutation of the indices of a pure tensor.

Given a natural number $n_2$ and a map $\sigma : \{0, \dots, n-1\} \to \{0, \dots, n'-1\}$, this defines the induced map $\{0, \dots, n+n_2-1\} \to \{0, \dots, n'+n_2-1\}$ which applies $\sigma$ to the first $n$ elements and acts as the identity on the remaining $n_2$ elements.

For any natural numbers $n$ and $n_2$, the induced map on the combined indices $\{0, \dots, n + n_2 - 1\}$ that applies the identity map $\text{id}$ to the first $n$ indices and acts as the identity on the remaining $n_2$ indices is equal to the identity map on $\{0, \dots, n + n_2 - 1\}$.

Let $n, n', n_2$ be natural numbers. Let $c : \text{Fin } n \to C$, $c' : \text{Fin } n' \to C$, and $c_2 : \text{Fin } n_2 \to C$ be index type assignments. Suppose a map $\sigma : \text{Fin } n' \to \text{Fin } n$ satisfies the permutation condition $\text{PermCond}(c, c', \sigma)$. Then the induced map $f : \text{Fin } (n' + n_2) \to \text{Fin } (n + n_2)$, which applies $\sigma$ to the first $n'$ indices and acts as the identity on the remaining $n_2$ indices, satisfies the permutation condition with respect to the concatenated index types $c \oplus c_2$ and $c' \oplus c_2$.

Let $S$ be a tensor species. Let $p$ be a pure tensor with index map $c: \text{Fin } n \to C$ and $p_2$ be a pure tensor with index map $c_2: \text{Fin } n_2 \to C$. For any map $\sigma: \text{Fin } n' \to \text{Fin } n$ satisfying the permutation condition $h$ between $c$ and $c'$, let $\text{permP}(\sigma, h, p)$ be the tensor $p$ with its indices permuted by $\sigma$. Then the tensor product of this permuted tensor with $p_2$ satisfies: $$(\text{permP} \ \sigma \ h \ p) \otimes p_2 = \text{permP} \ (f, h', p \otimes p_2)$$ where $f = \text{prodLeftMap}(n_2, \sigma)$ is the map on the combined index set $\text{Fin}(n' + n_2) \to \text{Fin}(n + n_2)$ that applies $\sigma$ to the first $n'$ indices and acts as the identity on the remaining $n_2$ indices, and $h'$ is the induced permutation condition for the concatenated index maps.

Given a natural number $n_2$ and a map $\sigma : \{0, \dots, n-1\} \to \{0, \dots, n'-1\}$, this defines the induced map $\{0, \dots, n_2+n-1\} \to \{0, \dots, n_2+n'-1\}$ that acts as the identity on the first $n_2$ elements and applies $\sigma$ to the remaining elements.

For any natural numbers $n_2$ and $n$, the induced map $\text{prodRightMap}$ on the set of indices $\{0, \dots, n_2 + n - 1\}$, which is defined to act as the identity on the first $n_2$ indices and apply the identity map $\text{id}$ to the remaining $n$ indices, is equal to the identity map on the entire set $\{0, \dots, n_2 + n - 1\}$.

Let $c : \{0, \dots, n-1\} \to C$ and $c' : \{0, \dots, n'-1\} \to C$ be maps assigning species to tensor indices. Let $\sigma : \{0, \dots, n'-1\} \to \{0, \dots, n-1\}$ be a map satisfying the permutation condition $\text{PermCond}(c, c', \sigma)$, which ensures that the species at index $i$ in $c'$ matches the species at $\sigma(i)$ in $c$. For any natural number $n_2$ and any species map $c_2 : \{0, \dots, n_2-1\} \to C$, let the induced map $\text{prodRightMap}(n_2, \sigma)$ be the map on indices $\{0, \dots, n_2 + n' - 1\}$ that acts as the identity on the first $n_2$ indices and applies $\sigma$ (offset by $n_2$) to the remaining $n'$ indices. This theorem states that the induced map satisfies the permutation condition for the concatenated species maps $(c_2 \oplus c)$ and $(c_2 \oplus c')$.

Let $S$ be a tensor species. Let $p$ be a pure tensor with index map $c: \text{Fin } n \to C$ and $p_2$ be a pure tensor with index map $c_2: \text{Fin } n_2 \to C$. For any map $\sigma: \text{Fin } n' \to \text{Fin } n$ satisfying the permutation condition $h$ between $c$ and $c'$, let $\text{permP}(\sigma, h, p)$ be the tensor $p$ with its indices permuted by $\sigma$. Then the tensor product of $p_2$ with this permuted tensor satisfies: $$p_2 \otimes (\text{permP} \ \sigma \ h \ p) = \text{permP} \ (f, h', p_2 \otimes p)$$ where $f = \text{prodRightMap}(n_2, \sigma)$ is the map on the combined index set $\text{Fin}(n_2 + n') \to \text{Fin}(n_2 + n)$ that acts as the identity on the first $n_2$ indices and applies $\sigma$ to the remaining $n'$ indices, and $h'$ is the induced permutation condition for the concatenated index maps.

The map between the finite sets of size $(n_1 + n_2) + n_3$ and $n_1 + (n_2 + n_3)$ formed by casting using the associativity of addition.

For any natural numbers $n_1, n_2, n_3$ and any index $i \in \text{Fin}(n_1)$, the product associativity map $\text{prodAssocMap} : \text{Fin}((n_1 + n_2) + n_3) \to \text{Fin}(n_1 + (n_2 + n_3))$ maps the index $i$, when embedded into the first block of the set $\text{Fin}((n_1 + n_2) + n_3)$, to the corresponding index in the first block of $\text{Fin}(n_1 + (n_2 + n_3))$. Specifically, $$\text{prodAssocMap}_{n_1, n_2, n_3}(\text{castAdd}_{n_3}(\text{castAdd}_{n_2}(i))) = \text{finSumFinEquiv}(\text{inl}(i))$$ where $\text{castAdd}_m$ denotes the inclusion of $\text{Fin}(n)$ into $\text{Fin}(n+m)$ as the first $n$ elements, and $\text{finSumFinEquiv}$ is the canonical isomorphism between the disjoint union $\text{Fin}(n_1) \oplus \text{Fin}(n_2 + n_3)$ and the set $\text{Fin}(n_1 + (n_2 + n_3))$.

For any natural numbers $n_1, n_2, n_3$ and any index $i \in \text{Fin } n_2$, the product associativity map $\text{prodAssocMap} : \text{Fin}((n_1 + n_2) + n_3) \to \text{Fin}(n_1 + (n_2 + n_3))$ satisfies: $$\text{prodAssocMap}(\text{Fin.castAdd } n_3 (\text{Fin.natAdd } n_1 i)) = \text{finSumFinEquiv}(\text{Sum.inr }(\text{finSumFinEquiv }(\text{Sum.inl } i)))$$ In this context, $\text{Fin } n$ represents the set of natural numbers $\{0, 1, \dots, n-1\}$. The expression $\text{Fin.castAdd } n_3 (\text{Fin.natAdd } n_1 i)$ identifies $i$ as an element of the "middle" block of size $n_2$ within the range $(n_1 + n_2) + n_3$, yielding the value $n_1 + i$. The function $\text{finSumFinEquiv}$ is the standard equivalence between the sum of finite sets $\text{Fin } a \oplus \text{Fin } b$ and the finite set $\text{Fin}(a + b)$. Thus, the theorem states that $\text{prodAssocMap}$ maps the index $n_1 + i$ from the first grouping to the corresponding index $n_1 + i$ in the second grouping.

For any natural numbers $n_1, n_2, n_3$ and an index $i \in \text{Fin } n_3$, the product associativity map $f: \text{Fin}((n_1 + n_2) + n_3) \to \text{Fin}(n_1 + (n_2 + n_3))$ maps the index $i$ (offset by $n_1 + n_2$) to the result of nested right-injections into the sum type structure. Specifically: $$f(i + n_1 + n_2) = \text{equiv}(\text{inr}(\text{equiv}(\text{inr } i)))$$ where $\text{equiv}$ denotes the canonical equivalence between a sum type $\text{Fin } a \oplus \text{Fin } b$ and the finite set $\text{Fin }(a + b)$, and $\text{inr}$ is the right injection into a sum type.

For any natural numbers $n_1, n_2, n_3$ and maps $c: \text{Fin } n_1 \to C$, $c_2: \text{Fin } n_2 \to C$, and $c_3: \text{Fin } n_3 \to C$ assigning species labels to indices, the product associativity map $\text{prodAssocMap} : \text{Fin}((n_1 + n_2) + n_3) \to \text{Fin}(n_1 + (n_2 + n_3))$ satisfies the permutation condition relating the two ways of concatenating these maps. Specifically, the species assigned to an index $i \in \text{Fin}((n_1 + n_2) + n_3)$ in the regrouped concatenation $(c \oplus c_2) \oplus c_3$ is identical to the species assigned to its image $\text{prodAssocMap}(i)$ in the concatenation $c \oplus (c_2 \oplus c_3)$.

Let $S$ be a tensor species. For any three pure tensors $p$, $p_1$, and $p_2$ with index maps $c : \text{Fin } n \to C$, $c_1 : \text{Fin } n_1 \to C$, and $c_2 : \text{Fin } n_2 \to C$ respectively, the tensor product operation $\otimes$ (denoted formally as `prodP`) is associative up to a canonical re-indexing. Specifically: $$(p \otimes p_1) \otimes p_2 = \text{permP}(\phi, p \otimes (p_1 \otimes p_2))$$ where $\phi : \text{Fin}((n + n_1) + n_2) \to \text{Fin}(n + (n_1 + n_2))$ is the `prodAssocMap`, which regroups the indices based on the associativity of natural number addition, and `permP` is the operation that permutes the indices of the pure tensor.

Given natural numbers $n_1$, $n_2$, and $n_3$, this function provides the map from $\mathrm{Fin}(n_1 + (n_2 + n_3))$ to $\mathrm{Fin}(n_1 + n_2 + n_3)$ formed by casting using the associativity of addition.

For any natural numbers $n_1, n_2, n_3$ and any index $i \in \text{Fin } n_1$, the associativity map $\text{prodAssocMap}' : \text{Fin}(n_1 + (n_2 + n_3)) \to \text{Fin}((n_1 + n_2) + n_3)$ maps $i$ (embedded as an element of the first summand of the right-associated sum) to the index corresponding to $i$ in the first summand of the left-associated sum. Mathematically, this is expressed as: $$\text{prodAssocMap}' (i) = i$$ where the left side treats $i$ as an element of $\text{Fin}(n_1 + (n_2 + n_3))$ via the natural inclusion `Fin.castAdd`, and the right side represents the nested inclusion of $i$ into the first summand of $(n_1 + n_2) + n_3$.

For any natural numbers $n_1$, $n_2$, and $n_3$, the associativity casting map $\mathrm{prodAssocMap}' : \mathrm{Fin}(n_1 + (n_2 + n_3)) \to \mathrm{Fin}((n_1 + n_2) + n_3)$ maps an index $i \in \mathrm{Fin}(n_2)$ located in the "middle" block (i.e., shifted by $n_1$) to the corresponding index in the reassociated sum. Specifically, it maps the index $n_1 + i$ in $\mathrm{Fin}(n_1 + (n_2 + n_3))$ to the index $n_1 + i$ in $\mathrm{Fin}((n_1 + n_2) + n_3)$, which is identified as being the right-hand part of the first $(n_1 + n_2)$ indices.

For any natural numbers $n_1$, $n_2$, and $n_3$, the associativity casting map $\mathrm{prodAssocMap}' : \mathrm{Fin}(n_1 + (n_2 + n_3)) \to \mathrm{Fin}((n_1 + n_2) + n_3)$ maps an index $i \in \mathrm{Fin}(n_3)$ located in the third block (i.e., shifted by $n_2$ and then by $n_1$) to the corresponding index in the reassociated sum. Specifically, it maps the index $n_1 + n_2 + i$ in $\mathrm{Fin}(n_1 + (n_2 + n_3))$ to the index $n_1 + n_2 + i$ in $\mathrm{Fin}((n_1 + n_2) + n_3)$, which is identified as being the right-hand summand of the final sum.

For any natural numbers $n_1, n_2, n_3$ and index color configurations $c : \text{Fin } n_1 \to C, c_2 : \text{Fin } n_2 \to C, c_3 : \text{Fin } n_3 \to C$, the associativity map $\text{prodAssocMap}' : \text{Fin}(n_1 + (n_2 + n_3)) \to \text{Fin}((n_1 + n_2) + n_3)$ satisfies the permutation condition $\text{PermCond}$ between the concatenated colorings $((c \oplus c_2) \oplus c_3)$ and $(c \oplus (c_2 \oplus c_3))$. This indicates that the map correctly preserves the colors of the indices when reassociating the product of three tensors.

Let $S$ be a tensor species. For any natural numbers $n, n_1, n_2$ and pure tensors $p$, $p_1$, and $p_2$ with index color configurations $c: \text{Fin } n \to C$, $c_1: \text{Fin } n_1 \to C$, and $c_2: \text{Fin } n_2 \to C$ respectively, the product of pure tensors is associative up to a reindexing of the indices. Specifically: $$p \otimes (p_1 \otimes p_2) = \text{permP}_{\phi} ((p \otimes p_1) \otimes p_2)$$ where $\otimes$ denotes the pure tensor product (`prodP`), $\phi: \text{Fin}(n + (n_1 + n_2)) \to \text{Fin}((n + n_1) + n_2)$ is the canonical associativity casting map (`prodAssocMap'`), and $\text{permP}_{\phi}$ is the operation that permutes the indices of a pure tensor according to $\phi$.

Given a tensor species $S$ and color configurations $c : \text{Fin } n_1 \to C$ and $c_1 : \text{Fin } n_2 \to C$, this defines the linear equivalence over a field $k$ between the type $S.F.\text{obj}(\text{OverColor.mk}(\text{Sum.elim}(c, c_1)))$ and the tensor space $S.\text{Tensor}(\text{Fin.append}(c, c_1))$.

Let $S$ be a tensor species over a field $k$. For index color configurations $c : \text{Fin } n_1 \to C$ and $c_1 : \text{Fin } n_2 \to C$, let $p$ be a pure tensor indexed by the concatenation of $c$ and $c_1$. The theorem states that the inverse of the product index equivalence, $\text{prodIndexEquiv}^{-1}$, applied to the tensor representation of $p$, is equal to the tensor product $\bigotimes_{i \in \text{Fin } n_1 \oplus \text{Fin } n_2} v_i$, where $\{v_i\}$ is the family of vectors that constitute the pure tensor $p$.

For a tensor species $S$ over a ring $k$, and index color configurations $c: \text{Fin } n_1 \to C$ and $c_1: \text{Fin } n_2 \to C$, the function $\text{prodT}$ is the $k$-bilinear map that takes a tensor $t \in S.\text{Tensor}(c)$ and a tensor $t_1 \in S.\text{Tensor}(c_1)$ and produces their tensor product in the space $S.\text{Tensor}(c \oplus c_1)$, where $c \oplus c_1$ (represented by `Fin.append c c1`) is the concatenation of the two index configurations.