Shapiro bijectivity for H¹(G,Hom(R,Coind Y))

Let $G$ be a group, $D \le G$ a subgroup, $R$ an object of $\mathrm{Rep}\,\mathbb{Z}\,G$ (a $\mathbb{Z}[G]$-module) and $Y$ an object of $\mathrm{Rep}\,\mathbb{Z}\,D$ (a $\mathbb{Z}[D]$-module). Consider the morphism of $\mathbb{Z}[D]$-modules obtained by composing, in diagrammatic order, Rep.resIhom along the inclusion $D \hookrightarrow G$ at the pair $(R, \mathrm{Coind}_{D}^{G} Y)$ — the map which is the identity on underlying carriers and identifies the restriction to $D$ of the internal hom $\mathrm{Hom}(R, \mathrm{Coind}_{D}^{G} Y)$ with the internal hom $\mathrm{Hom}(\mathrm{Res}\,R, \mathrm{Res}\,\mathrm{Coind}_{D}^{G} Y)$ of the restricted representations — with the image under the functor $\mathrm{Hom}(\mathrm{Res}\,R, -)$ of the component at $Y$ of the counit of Mathlib's restriction–coinduction adjunction Rep.resCoindAdjunction, i.e. post-composition with the evaluation of a coinduced function at $1$. Applying $H^{1}$-functoriality groupCohomology.map along $D \hookrightarrow G$ to this morphism in degree $1$ yields a homomorphism

The assertion is that the underlying function of this homomorphism is bijective.

This is Shapiro's lemma in degree one, in the form adapted to the isomorphism $\mathrm{Hom}(R, \mathrm{Coind}_{D}^{G} Y) \cong \mathrm{Coind}_{D}^{G}\mathrm{Hom}(\mathrm{Res}\,R, Y)$ of $G$-modules, with the comparison map written explicitly as restriction to $D$ followed by evaluation at $1$ inside the internal hom. It feeds the construction of the nondegenerate pairing in groupCohomology.exists_sha1_dualTwist_sha2_pairing_nondegenerate_of_ne_two, where local cohomology at a place is compared with global cohomology of a coinduced module.