Injectivity of degree-two inflation via continuous Hilbert 90

Let $K$ and $\Omega$ be fields with $\Omega$ a Galois extension of $K$ (an algebra instance together with IsGalois K Ω), and let $r \colon \mathrm{Gal}(\Omega/K) \to \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$ be a group homomorphism into the automorphism group of AlgebraicClosure ℚ over $\mathbb{Q}$. Assume the openness condition hopen: for every intermediate field $F$ of $\overline{\mathbb{Q}}/\mathbb{Q}$ that is finite-dimensional over $\mathbb{Q}$ there is an intermediate field $E$ of $\Omega/K$, finite-dimensional over $K$, such that every $\sigma \in \mathrm{Gal}(\Omega/K)$ lying in the fixing subgroup of $E$ has $r\,\sigma$ in the fixing subgroup of $F$. Let $L$ be an intermediate field of $\Omega/K$ which is finite-dimensional and normal over $K$, and let $f \colon \mathrm{Gal}(L/K) \times \mathrm{Gal}(L/K) \to$ Additive Lˣ be a $2$-cocycle, i.e. an element of cocycles₂ of the representation Rep.ofAlgebraAutOnUnits K L of $\mathrm{Gal}(L/K)$ on the unit group $L^\times$ written additively. Suppose that the inflated $2$-cochain unitsInflate₂ L f of $\mathrm{Gal}(\Omega/K)$ with values in Additive Ωˣ lies in levelCoboundaries₂ r (Rep.ofAlgebraAutOnUnits K Ω), the subgroup of coboundaries cut out using the level map $r$. Then $f$ itself lies in coboundaries₂ (Rep.ofAlgebraAutOnUnits K L), i.e. $f$ is the coboundary of a $1$-cochain $\mathrm{Gal}(L/K) \to L^\times$.

This is the degree-two inflation injectivity of the inflation–restriction sequence in its continuous form: the inflation map $H^2(\mathrm{Gal}(L/K), L^\times) \to H^2(\mathrm{Gal}(\Omega/K), \Omega^\times)$ is injective on classes whose inflation is bounded by a cochain satisfying the level condition attached to $r$, the required vanishing of $H^1$ of $\mathrm{Gal}(\Omega/L)$ being supplied by groupCohomology.exists_eq_smul_div_of_isMulCocycle1_fixingSubgroup. It is used in the construction and analysis of level $2$-cocycles attached to characters and in the splitting results for extensions obtained by adjoining roots of unity in the $p$-adic setting.