Naturality of Shapiro's isomorphism in the coefficients

Let $k$ be a commutative ring and $G$ a group (both in the same universe), let $S \le G$ be a subgroup, let $A$ and $B$ be $k$-linear representations of $S$, i.e. objects of Rep k S, let $\varphi : A \to B$ be a morphism of such representations, and let $n$ be a natural number. The coinduction functor Rep.coindFunctor k S.subtype along the inclusion S.subtype : S →* G carries $\varphi$ to a morphism $\operatorname{coind}_S^G A \to \operatorname{coind}_S^G B$ of representations of $G$, and groupCohomology.map applied to the identity homomorphism of $G$ and to this morphism gives the induced map $H^n(G, \operatorname{coind}_S^G A) \to H^n(G, \operatorname{coind}_S^G B)$; likewise groupCohomology.map applied to the identity homomorphism of $S$ and to $\varphi$ gives $H^n(S,A) \to H^n(S,B)$. Writing groupCohomology.coindIso A n for Shapiro's isomorphism $H^n(G, \operatorname{coind}_S^G A) \cong H^n(S,A)$, the assertion is the commutativity of the square: the induced map on $H^n(G,-)$ followed by the forward direction of Shapiro's isomorphism for $B$ equals the forward direction of Shapiro's isomorphism for $A$ followed by the induced map on $H^n(S,-)$.

This is the naturality of Shapiro's (Eckmann–Shapiro) isomorphism with respect to change of coefficient representation, in each cohomological degree. It is used in the construction relating corestriction, restriction and norm maps, where the semilocal description of cohomology must be transported along maps of coefficient modules.