Restriction and corestriction in group cohomology

Assume the Axiom of Dependent Choice and supplied injective resolution data on all left $G$-modules and all left $H$-modules, for $H\le G$. Use the resolution-independent group cohomology of Group cohomology as a derived functor. On the category of $G$-modules, both $H^{\ast }(G;-)$ and $T^{\ast }=H^{\ast }(H;\mathrm{Res}(-))$ are cohomological delta functors; for $T$ this follows by composing with the exact restriction functor. The first is positively effaceable by injectives by Positive right derived functors are effaceable by injectives, hence universal by Effaceable cohomological delta functors are universal. Define restriction as its unique delta-functor morphism extending the natural inclusion $M^G\hookrightarrow M^H$: ${\mathrm{res}}_H^G:H^n(G;M)⟶H^n(H;\mathrm{Res}M)\mathrm{.}$

For corestriction assume in addition $[G:H]<\mathrm{\infty }$. A transversal $X$ for the left cosets $G\mathrm{/}H$ exists by finite choice, which requires no additional choice axiom. Define $N_H^G:M^H⟶M^G,N_H^G(m)={\sum }_{x\in X}xm\mathrm{.}$ Replacing $x$ by $xh$, for $h\in H$, leaves $xm$ unchanged; multiplication by any $g\in G$ permutes the left cosets. Thus the sum is representative-independent and $G$-invariant, and it commutes with $G$-module maps.

The finite transversal supplies the hypothesis of The group ring is free over a subgroup ring on the right $\mathbb{Z}[H]$-module $\mathbb{Z}[G]$. Hence induction is a finite direct sum on underlying abelian groups and is exact. Its adjunction with restriction, Induction and coinduction are the two adjoints, shows that a $G$-injective $I$ restricts to an $H$-injective: to extend an $H$-map across a monomorphism, apply exact induction, extend into $I$, and use the adjunction back. Consequently a supplied $G$-injective embedding effaces every positive $T^n$, since the target restricts to an injective. The effaceability theorem therefore makes $T$ universal on $G$-modules. Define corestriction as the unique delta-functor morphism extending $N_H^G$: ${\mathrm{cor}}_H^G:H^n(H;\mathrm{Res}M)⟶H^n(G;M)\mathrm{.}$