 Hom functor adjunction for a coinduced module

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))$.