Inflation is an isomorphism when H^{≥ 1}(N,A) vanishes

Let $k$ be a commutative ring and $G$ a group (both in the same universe), let $N$ be a normal subgroup of $G$, and let $A$ be a $k$-linear representation of $G$. Assume that for every natural number $i$ the group cohomology of the restriction of $A$ along the inclusion $N \hookrightarrow G$ in degree $i+1$ is a zero object, i.e. $H^{i+1}(N, A) = 0$ for all $i \ge 0$. Then for every natural number $n$ the type of isomorphisms $H^{n+1}(A^{N}) \cong H^{n+1}(G, A)$ is nonempty, where $A^{N}$ denotes the representation of the quotient $G/N$ on the $N$-invariants of $A$ given by Rep.quotientToInvariants, and where both sides are the group cohomology objects in the category of $k$-modules. Thus the assertion is the existence of some isomorphism between the two cohomology modules in each positive degree; the statement as formalised does not record that this isomorphism is the inflation map, although the proof produces it from the inflation map.

This is the degenerate case of the inflation–restriction sequence (equivalently, of the Lyndon–Hochschild–Serre spectral sequence) in which the cohomology of the normal subgroup vanishes in all positive degrees, so that inflation $H^{n+1}(G/N, A^{N}) \to H^{n+1}(G,A)$ is an isomorphism. It is used in the Tate-cohomology input to the $p$-group step recorded in Rep.isZero_tateCohomology_of_isPGroup_of_forall, where only the existence of an isomorphism, and hence the transport of vanishing, is needed.