Functoriality of Hⁿ on explicit cocycle representatives

Let $k$ be a commutative ring, let $G$ and $H$ be groups, let $A$ be a $k$-linear representation of $H$ and $B$ a $k$-linear representation of $G$ (all in Type), let $f : G \to H$ be a group homomorphism and let $\varphi : \mathrm{Res}_f A \to B$ be a morphism of $k$-linear $G$-representations from the restriction of $A$ along $f$ to $B$. Let $n$ be a natural number and let $x : (\mathrm{Fin}\,n \to H) \to A$ be an inhomogeneous $n$-cochain of $H$ with values in $A$, assumed to satisfy $d^n_A(x) = 0$, where $d^n_A$ is the degree-$n$ differential of the inhomogeneous cochain complex of $A$; and assume moreover that the pulled-back cochain $g \mapsto \varphi(x(f \circ g))$ on $(\mathrm{Fin}\,n \to G)$ with values in $B$ satisfies $d^n_B\bigl(g \mapsto \varphi(x(f \circ g))\bigr) = 0$. The conclusion is that the $k$-linear map $H^n(H, A) \to H^n(G, B)$ induced by the pair $(f, \varphi)$ carries the cohomology class of the $n$-cocycle determined by $x$ and its cocycle identity, taken under the projection groupCohomology.π from $n$-cocycles to $H^n(H,A)$, to the class of the $n$-cocycle determined by $g \mapsto \varphi(x(f \circ g))$ and its cocycle identity. The cocycle condition for the pulled-back cochain is thus a hypothesis rather than a consequence derived inside the statement.

This is the usual functoriality of group cohomology in the pair (group, module), made explicit on representatives: the induced map sends the class of an inhomogeneous cocycle $x$ to the class of $g \mapsto \varphi(x(f \circ g))$. It is used when reading explicit idèle-valued cocycles in local coordinates, namely after restriction along an inclusion of a decomposition group followed by a coefficient morphism, and specialises further in groupCohomology.map_id_pi_cocyclesMk_apply.