Rewriting using the definition of the diagonal tensor product representation, we have

which follows by simplification using \(\operatorname {tprod_apply}\) and \(\operatorname {TensorProduct.map_tmul}\). The result then follows immediately from the defining property of coinvariants: \(\operatorname {mk}((\rho _V \otimes \rho _W)(h)(x)) = \operatorname {mk}(x)\) for all \(h \in H\) and \(x \in V \otimes W\).

Apply the diagonal balance relation (Theorem 507) with \(h\) and with \(v\) replaced by \(\rho _V(h^{-1})(v)\) and \(w\) replaced by \(w\), obtaining:

We establish that \(\rho _V(h)(\rho _V(h^{-1})(v)) = v\). Indeed, \((\rho _V(h) \circ \rho _V(h^{-1}))(v) = (\rho _V(h \cdot h^{-1}))(v)\) by the homomorphism property, and since \(h \cdot h^{-1} = 1\) we get \(\rho _V(1)(v) = v\) by the identity axiom. Rewriting with this, the equation becomes \([v \otimes \rho _W(h)(w)] = [\rho _V(h^{-1})(v) \otimes w]\), which gives the result by symmetry.

Apply the balancing relation (Theorem 508) with \(h\) replaced by \(h^{-1}\), obtaining \([\rho _V(h^{-1\, -1})(v) \otimes w] = [v \otimes \rho _W(h^{-1})(w)]\). Simplifying \(h^{-1\, -1} = h\) by the involution property of group inversion gives the result.

We apply the coinvariants extensionality principle \(\operatorname {Coinvariants.hom_ext}\) for \(\rho _V \otimes \rho _W\), which reduces equality of maps from the quotient to equality on the span of pure tensors. It then suffices to check equality on pure tensors \(v \otimes w\), which is exactly the hypothesis. This follows by applying \(\operatorname {TensorProduct.ext’}\).

This follows directly from the general fact that coinvariant quotient maps are surjective: \(\operatorname {Coinvariants.mk_surjective}(\rho _V \otimes \rho _W)\).

We verify the two inverse conditions. Left inverse: Let \([x] \in V \otimes _H W\). By induction on coinvariants, it suffices to take \(x \in V \otimes _{\mathbb {F}_2} W\). Unfolding definitions, \(\iota (\overline{\operatorname {avg}}([x])) = [\operatorname {avg}(x)]\). We must show \([\operatorname {avg}(x)] = [x]\), i.e., \(\operatorname {avg}(x) - x \in \ker (\operatorname {mk})\). Expanding the averaging map, \(\operatorname {avg}(x) = \frac{1}{|H|}\sum _{h \in H} (\rho _V \otimes \rho _W)(h)(x)\). Using the fact that each \([(\rho _V \otimes \rho _W)(h)(x)] = [x]\) in coinvariants, we get \([\operatorname {avg}(x)] = \frac{1}{|H|} \cdot |H| \cdot [x] = [x]\) (using that \(|H|\) is invertible). This uses \(\operatorname {invOf_mul_self}\) and the coinvariant quotient property. Right inverse: Let \((x, hx) \in (V \otimes W)^H\) where \(hx\) is the invariance proof. Then \(\overline{\operatorname {avg}}(\iota (x)) = \overline{\operatorname {avg}}([x]) = \operatorname {avg}(x)\). Since \(x\) is invariant, \((\rho _V \otimes \rho _W)(h)(x) = x\) for all \(h\), so \(\operatorname {avg}(x) = \frac{1}{|H|} \cdot |H| \cdot x = x\), which follows from \(\operatorname {averageMap_id}\). The \(\mathbb {F}_2\)-linearity of the equivalence is inherited from \(\overline{\operatorname {avg}}\).

We show that \(\operatorname {rid} : V \otimes _{\mathbb {F}_2} \mathbb {F}_2 \xrightarrow {\sim } V\) maps the coinvariant kernel of \(\rho _V \otimes \mathbf{1}\) isomorphically onto the coinvariant kernel of \(\rho _V\), establishing

We prove both inclusions. Forward inclusion (\(\subseteq \)): By induction on the coinvariant kernel, it suffices to handle generators of the form \((\rho _V \otimes \mathbf{1})(g)(t) - t\) for \(g \in H\), \(t \in V \otimes \mathbb {F}_2\). By further induction on \(t\) using \(\operatorname {TensorProduct.induction_on}\): for zero tensors the result is trivial; for pure tensors \(v \otimes a\), using the trivial action \(\mathbf{1}(g) = \operatorname {id}\), we compute \(\operatorname {rid}((\rho _V \otimes \mathbf{1})(g)(v \otimes a) - v \otimes a) = a \cdot (\rho _V(g)(v) - v)\), which lies in \(\operatorname {Coinv.ker}(\rho _V)\) since \(\rho _V(g)(v) - v\) is a generator and the submodule is closed under scalar multiplication; the addition case follows by linearity of \(\operatorname {rid}\) and closure under addition. Backward inclusion (\(\supseteq \)): By induction on \(\operatorname {Coinv.ker}(\rho _V)\), generators have the form \(\rho _V(g)(v') - v'\). We exhibit a preimage: \(\rho _V(g)(v') \otimes 1 - v' \otimes 1 \in \operatorname {Coinv.ker}(\rho _V \otimes \mathbf{1})\) (using the trivial action on \(1 \in \mathbb {F}_2\)), and \(\operatorname {rid}(\rho _V(g)(v') \otimes 1 - v' \otimes 1) = \rho _V(g)(v') - v'\) as required; closures under addition and scalar multiplication are handled by decomposing preimages. The desired linear equivalence then follows from \(\operatorname {Submodule.Quotient.equiv}\) applied to \(\operatorname {rid}\) with this kernel compatibility.

The zero element \(0\) is an element of \(V \otimes _H W\), witnessing nonemptiness.