Coinduced module (${\mathrm{Coind}}_K^{G}X$)

For a subgroup $K\le G$ and a $\mathbb{Z}K$-module $X$, the coinduced module is

Shapiro's lemma gives a natural isomorphismIt follows by applying the Hom functor adjunction for a coinduced module to a projective resolution and observing that restriction from $G$ to $K$ preserves projective modules.

For a $\mathbb{Z}G$-module $P$ and a $\mathbb{Z}K$-module $X$,Evaluation at $1\in G$ gives the forward map. If $a:P\to X$ is $\mathbb{Z}K$-linear, its inverse sends $a$ to $p\mapsto (r\mapsto a(rp))$.