Degree-two Kummer theory for μₚ⊂ℚ̄^×

Fix a prime $p$ and a subgroup $D$ of the group of $\mathbb{Q}$-algebra automorphisms of $\mathrm{AlgebraicClosure}\,\mathbb{Q}$, together with a unit $\zeta$ of $\mathrm{AlgebraicClosure}\,\mathbb{Q}$ that is a primitive $p$-th root of unity and is fixed by every $\sigma \in D$. Two coefficient systems for $D$ are used: the trivial representation Rep.trivial (ZMod p) ↥D (ZMod p), and the restriction along the inclusion D.subtype of the representation Rep.ofAlgebraAutOnUnits ℚ (AlgebraicClosure ℚ) of the automorphism group on the units of $\mathrm{AlgebraicClosure}\,\mathbb{Q}$, written additively via Additive. For a function $z : D \times D \to \mathbb{Z}/p$ put $\zeta^z : (g,h) \mapsto \zeta^{(z(g,h)).\mathrm{val}}$, the power taken along the natural-number representative of the residue and transported into the additive copy of the unit group. For both coefficient systems, cocycles and coboundaries in degree two are taken in the sense of levelCocycles₂ and levelCoboundaries₂ relative to the map D.subtype. The assertion is the conjunction of: (1) if $z$ lies in levelCocycles₂ for the trivial $\mathbb{Z}/p$-coefficients and $\zeta^z$ lies in levelCoboundaries₂ for the unit-group coefficients, then $z$ lies in levelCoboundaries₂ for the trivial coefficients; and (2) if $X : D \times D \to \mathrm{Additive}\,(\mathrm{AlgebraicClosure}\,\mathbb{Q})^\times$ lies in levelCocycles₂ and $(p : \mathbb{Z}) \cdot X$ lies in levelCoboundaries₂, then there is $z$ in levelCocycles₂ for the trivial $\mathbb{Z}/p$-coefficients with $X - \zeta^z$ in levelCoboundaries₂.

This is the degree-two part of the Kummer sequence $1 \to \mu_p \to \overline{\mathbb{Q}}^\times \to \overline{\mathbb{Q}}^\times \to 1$ in cocycle form: part (1) expresses injectivity and part (2) surjectivity onto the $p$-torsion of the map $[z] \mapsto [\zeta^z]$ from $H^2(D, \mathbb{Z}/p)$ to $H^2(D, \overline{\mathbb{Q}}^\times)$, for the degree-two cohomology computed by cocycles and coboundaries of the indicated level with respect to the inclusion of $D$. It feeds into groupCohomology.exists_forall_eq_res_continuousH2Sr_trivial_add_smul_of_exists_sq_eq_neg_one, where local classes are compared with classes coming from $\mathbb{Z}/p$-coefficients.