Shapiro's lemma for H¹ with ramification restricted to S

Fix a prime $p$ and a finite set $S$ of rational primes. Let $K$ be an intermediate field of $\overline{\mathbb{Q}}/\mathbb{Q}$ (inside AlgebraicClosure ℚ) which is unramified outside $S$ in the sense of IntermediateField.IsUnramifiedOutside: $K$ is finite-dimensional over $\mathbb{Q}$, and for every prime $q \notin S$ and every valuation subring $A$ of $\overline{\mathbb{Q}}$ with $q$ in the nonunits of $A$, the image in $\mathrm{Aut}(\overline{\mathbb{Q}}/\mathbb{Q})$ of the inertia subgroup of $A$ over $\mathbb{Q}$ is contained in the fixing subgroup $\Gamma_K = K.\mathrm{fixingSubgroup}$. Let $N$ be a representation of $\Gamma_K$ on a finite-dimensional $\mathbb{Z}/p$-vector space, and assume that every vector $n \in N$ is stabilised by an open subgroup of $S$-level type: there is an intermediate field $F$, unramified outside $S$ in the same sense, such that every $s \in \Gamma_K$ whose underlying automorphism lies in $F.\mathrm{fixingSubgroup}$ satisfies $\rho(s)\,n = n$. The conclusion asserts that a certain type is nonempty, namely that there exists a $\mathbb{Z}/p$-linear isomorphism between continuousH1S S applied to the representation of $\mathrm{Aut}(\overline{\mathbb{Q}}/\mathbb{Q})$ coinduced from $N$ along the inclusion $\Gamma_K \hookrightarrow \mathrm{Aut}(\overline{\mathbb{Q}}/\mathbb{Q})$ — that is, the image under H1π of the submodule of $1$-cocycles cut out by levelCocyclesS₁ S — and continuousH1Sr for that same inclusion, $S$ and $N$, the image under H1π of the submodule of $1$-cocycles cut out by levelCocyclesSr₁. No isomorphism is named; only its existence is asserted.

This is Shapiro's lemma in degree one, adapted to cohomology with ramification restricted to $S$: the $S$-restricted $H^1$ of a coinduced module over the absolute group agrees with the $S$-restricted $H^1$ of the subgroup $\Gamma_K$ acting on $N$. It feeds the corresponding dimension count in degree two, groupCohomology.finiteDimensional_continuousH2S_coind_and_finrank_eq, and hence the Euler-characteristic bookkeeping for the restricted-ramification cohomology groups.