The function model of induction agrees with the tensor-product model $k[G]{\otimes }_{k[H]}W$

The present page defines induction by $H$-covariant functions because that model is self-contained in the library's existing module language. When $R$ is commutative and $[G:H]$ is finite, this is the same object as the tensor-product model.

Indeed, the subgroup inclusion makes $R[G]$ an $(R[G],R[H])$-bimodule ($(S,R)$-bimodules and commuting left and right scalar actions), so $R[G]{\otimes }_{R[H]}W$ is defined by the universal property of the tensor product (Universal property of the tensor product for balanced maps into abelian groups). The elementary formula

$[g]\otimes w⟼f_{g,w},f_{g,w}(gh):=h^{-1}\cdot w,$

with $f_{g,w}$ zero off the left coset $gH$, is balanced in the $R[H]$-variable and therefore descends uniquely (A formula on elementary tensors defines a homomorphism exactly when its underlying pairing is balanced). Comparing both sides on a finite left transversal shows that this descended map is a $G$-equivariant isomorphism

$$R[G]{\otimes }_{R[H]}W\cong {\mathrm{Ind}}_H^{G}W\mathrm{.}$$

Thus, in the finite-index setting used for finite-group character theory, the function model and the tensor-product model are two descriptions of the same induced module. For infinite index, the displayed function model is instead larger: the tensor product corresponds to the finitely supported covariant functions.