Physlib.Mathematics.PiTensorProduct

Let $R$ be a commutative ring and $M$ be an $R$-module. Let $s_1$ and $s_2$ be families of $R$-modules indexed by the sets $\iota_1$ and $\iota_2$, respectively. Suppose $f$ and $g$ are $R$-linear maps from the tensor product of two Pi tensor products, $\left(\bigotimes_{i \in \iota_1} s_1(i)\right) \otimes_R \left(\bigotimes_{j \in \iota_2} s_2(j)\right)$, to $M$. If for all elements $p \in \prod_{i \in \iota_1} s_1(i)$ and $q \in \prod_{j \in \iota_2} s_2(j)$, the maps satisfy $$f\left(\left(\bigotimes_{i \in \iota_1} p_i\right) \otimes \left(\bigotimes_{j \in \iota_2} q_j\right)\right) = g\left(\left(\bigotimes_{i \in \iota_1} p_i\right) \otimes \left(\bigotimes_{j \in \iota_2} q_j\right)\right),$$ then $f = g$. Here, $\bigotimes p_i$ denotes the canonical image (elementary tensor) of the element $p$ in the Pi tensor product.

Let $R$ be a commutative ring and $M$ be an $R$-module. Let $\iota_1, \iota_2, \iota_3$ be index sets, and let $s_1, s_2, s_3$ be families of $R$-modules indexed by these sets. Suppose $f$ and $g$ are $R$-linear maps from the triple tensor product $(\bigotimes_{i \in \iota_1} s_1(i)) \otimes_R (\bigotimes_{j \in \iota_2} s_2(j)) \otimes_R (\bigotimes_{k \in \iota_3} s_3(k))$ to $M$. If for all $p \in \prod_{i \in \iota_1} s_1(i)$, $q \in \prod_{j \in \iota_2} s_2(j)$, and $m \in \prod_{k \in \iota_3} s_3(k)$, the maps satisfy $$f\left(\left(\bigotimes_{i \in \iota_1} p_i\right) \otimes \left(\bigotimes_{j \in \iota_2} q_j\right) \otimes \left(\bigotimes_{k \in \iota_3} m_k\right)\right) = g\left(\left(\bigotimes_{i \in \iota_1} p_i\right) \otimes \left(\bigotimes_{j \in \iota_2} q_j\right) \otimes \left(\bigotimes_{k \in \iota_3} m_k\right)\right)$$ then $f = g$.

Let $R$ be a ring and $M$ an $R$-module. Let $s_1, s_2, s_3$ be families of $R$-modules indexed by $\iota_1, \iota_2, \iota_3$ respectively. Let $V_1 = \bigotimes_{i \in \iota_1} s_1(i)$, $V_2 = \bigotimes_{i \in \iota_2} s_2(i)$, and $V_3 = \bigotimes_{i \in \iota_3} s_3(i)$ be the corresponding Pi tensor products over $R$. For any two $R$-linear maps $f, g : (V_1 \otimes_R V_2) \otimes_R V_3 \to M$, if the maps agree on all pure tensors of the form $((\text{tprod}(p) \otimes \text{tprod}(q)) \otimes \text{tprod}(m))$ for all $p \in \prod s_1, q \in \prod s_2, m \in \prod s_3$, then $f = g$. Here, $\text{tprod}$ denotes the canonical multilinear map from the Cartesian product of a family of modules into its Pi tensor product.

Let $R$ be a commutative ring, $M$ and $N$ be $R$-modules, and $\{s_1(i)\}_{i \in \iota_1}$ be a family of $R$-modules indexed by $\iota_1$. Let $f, g : \left( \bigotimes_{i \in \iota_1} s_1(i) \right) \otimes_R N \to M$ be $R$-linear maps. If $$f\left(\left(\bigotimes_{i \in \iota_1} p_i\right) \otimes m\right) = g\left(\left(\bigotimes_{i \in \iota_1} p_i\right) \otimes m\right)$$ for all families of elements $p \in \prod_{i \in \iota_1} s_1(i)$ and all $m \in N$, then $f = g$. Here $\bigotimes_{i \in \iota_1} p_i$ denotes the canonical image of the family $p$ in the Pi tensor product.

Let $R$ be a commutative ring, $\iota_1$ an indexing set, and $\{s_1(i)\}_{i \in \iota_1}$ a family of $R$-modules. Let $N$ and $M$ be $R$-modules. Given two $R$-linear maps $f, g : N \otimes_R \left( \bigotimes_{i \in \iota_1} s_1(i) \right) \to M$, if $f(m \otimes (\otimes_{i \in \iota_1} p_i)) = g(m \otimes (\otimes_{i \in \iota_1} p_i))$ for all $m \in N$ and all families of elements $p \in \prod_{i \in \iota_1} s_1(i)$, then $f = g$.

Let $\iota_1$ and $\iota_2$ be indexing sets, and let $s_1 : \iota_1 \to \text{Type}$ and $s_2 : \iota_2 \to \text{Type}$ be families of types such that each $s_1(i)$ and $s_2(j)$ is an additive commutative monoid. For the disjoint union of the indexing sets $\iota_1 \oplus \iota_2$, this definition provides an additive commutative monoid structure for each type in the combined family $s: \iota_1 \oplus \iota_2 \to \text{Type}$ defined by the sum of $s_1$ and $s_2$. Specifically, for any index $i \in \iota_1 \oplus \iota_2$, the corresponding type inherits the additive commutative monoid instance from $s_1$ if $i$ is in the left injection or from $s_2$ if $i$ is in the right injection.

Let $R$ be a commutative ring, $\iota_1$ and $\iota_2$ be indexing sets, and $s_1 : \iota_1 \to \text{Type}$ and $s_2 : \iota_2 \to \text{Type}$ be families of types such that each $s_1(i)$ and $s_2(j)$ is an $R$-module. For the disjoint union $\iota_1 \oplus \iota_2$, this definition provides an $R$-module structure for each type in the combined family $s: \iota_1 \oplus \iota_2 \to \text{Type}$ defined by the sum of $s_1$ and $s_2$. Specifically, for any index $k \in \iota_1 \oplus \iota_2$, the corresponding type inherits the $R$-module instance from $s_1(i)$ if $k = \text{inl } i$ or from $s_2(j)$ if $k = \text{inr } j$.

Given two index sets $\iota_1$ and $\iota_2$ and families of types $s_1: \iota_1 \to \text{Type}$ and $s_2: \iota_2 \to \text{Type}$, let $f$ be a dependent function defined on the disjoint union $\iota_1 \oplus \iota_2$ such that for any $i \in \iota_1$, $f(\text{inl } i) \in s_1(i)$, and for any $j \in \iota_2$, $f(\text{inr } j) \in s_2(j)$. This function returns the restriction of $f$ to the first index set $\iota_1$, mapping each $i \in \iota_1$ to $f(\text{inl } i)$.

Given two families of types $s_1 : \iota_1 \to \text{Type}$ and $s_2 : \iota_2 \to \text{Type}$, and a function $f$ defined on the disjoint union $\iota_1 \oplus \iota_2$ such that $f(i) \in s_1(i)$ for $i \in \iota_1$ and $f(i) \in s_2(i)$ for $i \in \iota_2$, the function `pureInr` returns the restriction of $f$ to the index set $\iota_2$. Specifically, it is the map $f \circ \text{inr} : \iota_2 \to s_2$.

Let $\iota_1$ and $\iota_2$ be index sets and $s_1: \iota_1 \to \text{Type}$ and $s_2: \iota_2 \to \text{Type}$ be families of types. Let $f$ be a dependent function defined on the disjoint union $\iota_1 \oplus \iota_2$ such that $f(i) \in s_1(i)$ for $i \in \iota_1$ and $f(i) \in s_2(i)$ for $i \in \iota_2$. Let $f|_{\iota_1}$ denote the restriction of $f$ to the index set $\iota_1$ (mapping $i \in \iota_1$ to $f(\text{inl } i)$). For any $x \in \iota_1$ and $v_1 \in s_1(x)$, updating $f$ at the index $\text{inl } x$ with the value $v_1$ and then restricting the result to $\iota_1$ is equal to updating the restricted function $f|_{\iota_1}$ at index $x$ with $v_1$.

Let $\iota_1$ and $\iota_2$ be index sets, and let $s_1 : \iota_1 \to \text{Type}$ and $s_2 : \iota_2 \to \text{Type}$ be families of types. Let $f$ be a function defined on the disjoint union $\iota_1 \oplus \iota_2$ such that $f(i) \in s_1(i)$ for $i \in \iota_1$ and $f(i) \in s_2(i)$ for $i \in \iota_2$. Let $\text{pureInr}(f)$ denote the restriction of $f$ to the index set $\iota_2$, specifically defined as the map $j \mapsto f(\text{inr } j)$ for all $j \in \iota_2$. For any index $x \in \iota_1$ and any value $v \in s_1(x)$, let $f'$ be the function $f$ updated at the position $\text{inl}(x)$ with value $v$. Then the restriction of $f'$ to the index set $\iota_2$ is equal to the restriction of the original function $f$ to $\iota_2$. In mathematical notation: $\text{pureInr}(\text{update } f (\text{inl } x) v) = \text{pureInr } f$.

Let $\iota_1$ and $\iota_2$ be index sets, and let $s_1 : \iota_1 \to \text{Type}$ and $s_2 : \iota_2 \to \text{Type}$ be families of types. Let $f$ be a dependent function defined on the disjoint union $\iota_1 \oplus \iota_2$ such that $f(i) \in s_1(i)$ for $i \in \iota_1$ and $f(i) \in s_2(i)$ for $i \in \iota_2$. Let $\text{pureInr}(f)$ denote the restriction of $f$ to the index set $\iota_2$, specifically defined as the map $j \mapsto f(\text{inr } j)$ for all $j \in \iota_2$. For any index $x \in \iota_2$ and any value $v \in s_2(x)$, updating $f$ at the position $\text{inr}(x)$ with value $v$ and then restricting the result to $\iota_2$ is equal to updating the restricted function $\text{pureInr}(f)$ at index $x$ with the value $v$. In mathematical notation: $\text{pureInr}(\text{update } f (\text{inr } x) v) = \text{update } (\text{pureInr } f) x v$.

Let $\iota_1$ and $\iota_2$ be index sets, and let $s_1 : \iota_1 \to \text{Type}$ and $s_2 : \iota_2 \to \text{Type}$ be families of types. Let $f$ be a dependent function defined on the disjoint union $\iota_1 \oplus \iota_2$ such that $f(\text{inl } i) \in s_1(i)$ for $i \in \iota_1$ and $f(\text{inr } j) \in s_2(j)$ for $j \in \iota_2$. Let $\text{pureInl}(f)$ denote the restriction of $f$ to the index set $\iota_1$, defined as the map $i \mapsto f(\text{inl } i)$ for all $i \in \iota_1$. For any index $x \in \iota_2$ and any value $v \in s_2(x)$, let $f'$ be the function $f$ updated at the position $\text{inr}(x)$ with value $v$. Then the restriction of $f'$ to the index set $\iota_1$ is equal to the restriction of the original function $f$ to $\iota_1$. In mathematical notation: $\text{pureInl}(\text{update } f (\text{inr } x) v) = \text{pureInl } f$.

Let $R$ be a commutative ring. Let $\iota_1$ and $\iota_2$ be index sets, and let $s_1: \iota_1 \to \text{Type}$ and $s_2: \iota_2 \to \text{Type}$ be families of $R$-modules. This definition constructs an $R$-multilinear map from the family of modules indexed by the disjoint union $\iota_1 \oplus \iota_2$ (where the module at $k \in \iota_1 \oplus \iota_2$ is $s_1(i)$ if $k = \text{inl } i$ and $s_2(j)$ if $k = \text{inr } j$) to the tensor product of two Pi tensor products: \[ \text{MultilinearMap}_R \left( \text{Sum.elim } s_1 s_2, \left( \bigotimes_{i \in \iota_1} s_1(i) \right) \otimes_R \left( \bigotimes_{j \in \iota_2} s_2(j) \right) \right) \] For a given dependent function $f \in \prod_{k \in \iota_1 \oplus \iota_2} (\text{Sum.elim } s_1 s_2)_k$, the map is defined by: \[ f \mapsto \left( \bigotimes_{i \in \iota_1} f(\text{inl } i) \right) \otimes \left( \bigotimes_{j \in \iota_2} f(\text{inr } j) \right) \] where the right-hand side is the tensor product of the pure tensors formed from the restrictions of $f$ to $\iota_1$ and $\iota_2$ respectively.

Let $R$ be a commutative ring. Let $\iota_1$ and $\iota_2$ be index sets, and let $s_1: \iota_1 \to \text{Type}$ and $s_2: \iota_2 \to \text{Type}$ be families of $R$-modules. This definition constructs an $R$-linear map from the Pi tensor product indexed by the disjoint union $\iota_1 \oplus \iota_2$ to the tensor product of two Pi tensor products: \[ \left( \bigotimes_{k \in \iota_1 \oplus \iota_2} (\text{Sum.elim } s_1 s_2)_k \right) \to \left( \bigotimes_{i \in \iota_1} s_1(i) \right) \otimes_R \left( \bigotimes_{j \in \iota_2} s_2(j) \right) \] where $\text{Sum.elim } s_1 s_2$ is the family of modules where the module at index $k$ is $s_1(i)$ if $k = \text{inl } i$ and $s_2(j)$ if $k = \text{inr } j$. For any pure tensor $\bigotimes_{k \in \iota_1 \oplus \iota_2} f(k)$, the map is defined by: \[ \bigotimes_{k \in \iota_1 \oplus \iota_2} f(k) \mapsto \left( \bigotimes_{i \in \iota_1} f(\text{inl } i) \right) \otimes \left( \bigotimes_{j \in \iota_2} f(\text{inr } j) \right) \] In other words, it expands a Pi tensor product whose index set is a disjoint union into a tensor product of two Pi tensor products.

Given two index sets $\iota_1$ and $\iota_2$, two families of types $s_1: \iota_1 \to \text{Type}$ and $s_2: \iota_2 \to \text{Type}$, and two functions $p \in \prod_{i \in \iota_1} s_1(i)$ and $q \in \prod_{j \in \iota_2} s_2(j)$, this definition constructs a function $f$ on the disjoint union $\iota_1 \oplus \iota_2$ such that $f(i) = p(i)$ for $i \in \iota_1$ and $f(j) = q(j)$ for $j \in \iota_2$. This function is used to represent the underlying map of a pure tensor in the product $\bigotimes_{i \in \iota_1 \oplus \iota_2} (\text{Sum.elim } s_1 s_2)_i$.

Let $\iota_1$ and $\iota_2$ be index sets, and let $s_1: \iota_1 \to \text{Type}$ and $s_2: \iota_2 \to \text{Type}$ be families of types. Suppose $p \in \prod_{i \in \iota_1} s_1(i)$ and $q \in \prod_{j \in \iota_2} s_2(j)$ are functions. Let $\text{elimPureTensor}(p, q)$ be the function on the disjoint union $\iota_1 \oplus \iota_2$ that restricts to $p$ on $\iota_1$ and $q$ on $\iota_2$. For any $y \in \iota_2$ and $r \in s_2(y)$, updating the function $q$ at index $y$ with value $r$ before combining it with $p$ is equivalent to updating the combined function $\text{elimPureTensor}(p, q)$ at the corresponding index $\text{inr } y$ with the value $r$. That is, $$\text{elimPureTensor}(p, q[y \mapsto r]) = (\text{elimPureTensor}(p, q))[\text{inr } y \mapsto r]$$ where $f[x \mapsto v]$ denotes the update of function $f$ at index $x$ with value $v$.

Let $\iota_1$ and $\iota_2$ be index sets, and let $s_1: \iota_1 \to \text{Type}$ and $s_2: \iota_2 \to \text{Type}$ be families of types. For any functions $p \in \prod_{i \in \iota_1} s_1(i)$ and $q \in \prod_{j \in \iota_2} s_2(j)$, let $\text{elimPureTensor}(p, q)$ denote the combined function on the disjoint union $\iota_1 \oplus \iota_2$ such that its restriction to $\iota_1$ is $p$ and its restriction to $\iota_2$ is $q$. For any index $x \in \iota_1$ and value $r \in s_1(x)$, the following identity holds: $$\text{elimPureTensor}(\text{update}(p, x, r), q) = \text{update}(\text{elimPureTensor}(p, q), \text{inl}(x), r)$$ where $\text{update}(f, i, v)$ denotes the function $f$ with the value at index $i$ replaced by $v$, and $\text{inl}: \iota_1 \to \iota_1 \oplus \iota_2$ is the canonical injection.

Let $R$ be a commutative ring. Given two families of $R$-modules $s_1: \iota_1 \to \text{Type}$ and $s_2: \iota_2 \to \text{Type}$, this definition constructs an $R$-multilinear map from the product $\prod_{i \in \iota_1} s_1(i)$ to the space of $R$-multilinear maps from $\prod_{j \in \iota_2} s_2(j)$ to the Pi tensor product $\bigotimes_{k \in \iota_1 \oplus \iota_2} S_k$, where $S$ is the combined family of modules defined on the disjoint union of the index sets $\iota_1 \oplus \iota_2$. Specifically, for any $p \in \prod_{i \in \iota_1} s_1(i)$ and $q \in \prod_{j \in \iota_2} s_2(j)$, the map sends $p$ to a multilinear map that, when applied to $q$, results in the pure tensor $p \otimes q$ within the product space $\bigotimes_{k \in \iota_1 \oplus \iota_2} S_k$.

Let $R$ be a commutative ring and $\iota_1, \iota_2$ be indexing sets. Given two families of $R$-modules $s_1: \iota_1 \to \text{Type}$ and $s_2: \iota_2 \to \text{Type}$, let $s: \iota_1 \oplus \iota_2 \to \text{Type}$ be the combined family defined by the sum of $s_1$ and $s_2$ (where $s(\text{inl } i) = s_1(i)$ and $s(\text{inr } j) = s_2(j)$). This definition is the $R$-linear map $$\left( \bigotimes_{i \in \iota_1} s_1(i) \right) \otimes_R \left( \bigotimes_{j \in \iota_2} s_2(j) \right) \to \bigotimes_{k \in \iota_1 \oplus \iota_2} s(k)$$ which collapses the binary tensor product of two Pi tensor products into a single Pi tensor product indexed by the disjoint union of the original index sets. On pure tensors, this map sends $(\bigotimes_{i \in \iota_1} p_i) \otimes (\bigotimes_{j \in \iota_2} q_j)$ to the pure tensor $\bigotimes_{k \in \iota_1 \oplus \iota_2} x_k$, where $x$ is the concatenation of the families of elements $p$ and $q$.

Let $R$ be a commutative ring and $\iota_1, \iota_2$ be indexing sets. Given two families of $R$-modules $s_1: \iota_1 \to \text{Type}$ and $s_2: \iota_2 \to \text{Type}$, let $s: \iota_1 \oplus \iota_2 \to \text{Type}$ be the combined family defined by the sum of $s_1$ and $s_2$ (specifically, $s(\text{inl } i) = s_1(i)$ and $s(\text{inr } j) = s_2(j)$). This definition provides the $R$-linear equivalence \[ \left( \bigotimes_{i \in \iota_1} s_1(i) \right) \otimes_R \left( \bigotimes_{j \in \iota_2} s_2(j) \right) \cong \bigotimes_{k \in \iota_1 \oplus \iota_2} s(k) \] formed by combining a binary tensor product of two Pi tensor products into a single Pi tensor product indexed by the disjoint union of the original index sets. On pure tensors, this equivalence maps $(\bigotimes_{i \in \iota_1} p_i) \otimes (\bigotimes_{j \in \iota_2} q_j)$ to the pure tensor $\bigotimes_{k \in \iota_1 \oplus \iota_2} x_k$, where $x$ is the concatenation of the families $p$ and $q$.

Let $R$ be a commutative ring and let $\iota_1, \iota_2$ be indexing sets. Suppose $s_1: \iota_1 \to \text{Type}$ and $s_2: \iota_2 \to \text{Type}$ are families of $R$-modules. For any functions $p \in \prod_{i \in \iota_1} s_1(i)$ and $q \in \prod_{j \in \iota_2} s_2(j)$, the linear equivalence $\text{tmulEquiv}$ maps the tensor product of the pure tensors, $(\bigotimes_{i \in \iota_1} p_i) \otimes_R (\bigotimes_{j \in \iota_2} q_j)$, to the pure tensor $\bigotimes_{k \in \iota_1 \oplus \iota_2} x_k$, where $x$ is the combination of $p$ and $q$ on the disjoint union $\iota_1 \oplus \iota_2$ (i.e., $x(i) = p(i)$ for $i \in \iota_1$ and $x(j) = q(j)$ for $j \in \iota_2$).