Exactness of inflation–restriction in degree two

Let $k$ be a commutative ring, $G$ a group, $A$ a $k$-linear representation of $G$, and $S$ a normal subgroup of $G$. Assume that the group cohomology object $H^1$ of the restriction of $A$ along the inclusion S.subtype vanishes, i.e. groupCohomology (Rep.res S.subtype A) 1 is a zero object of the ambient category of $k$-modules. Consider two morphisms in degree $2$: the inflation map, namely the map on $H^2$ induced by the quotient homomorphism QuotientGroup.mk' S : G → G ⧸ S together with the $G$-equivariant inclusion of the representation A.quotientToInvariants S of $G ⧸ S$ (the $S$-invariants of $A$ with its induced $G/S$-action) into $A$ given by A.ρ.quotientToInvariants_lift S; and the restriction map, the map on $H^2$ induced by S.subtype together with the identity of Rep.res S.subtype A. The conclusion asserts, for the underlying $k$-linear maps of these two morphisms, that inflation $H^2(G/S, A^S) \to H^2(G,A)$ is injective and that its range coincides with the kernel of restriction $H^2(G,A) \to H^2(S,A)$.

This is the degree-two segment of the inflation–restriction (Hochschild–Serre) exact sequence, under the hypothesis $H^1(S,A)=0$: exactness of $0 \to H^2(G/S,A^S) \to H^2(G,A) \to H^2(S,A)$, stated on underlying linear maps in the same shape as Mathlib's degree-one version. It is used in the local part of the argument, for instance in the construction and characterisation of local fundamental classes and in comparisons of inflation with restriction on $H^2$.