Degree-two Kummer comparison for S-units of the maximal extension

Fix a rational prime $p$ and a finite set $S$ of primes with $\langle p\rangle \in S$, let $F$ be an intermediate field of $\mathbb{Q} \subseteq \overline{\mathbb{Q}} =$ AlgebraicClosure ℚ, and let $D$ be a subgroup of $\mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$ contained in the fixing subgroup of $F$ (hypothesis hD). Write $E_S =$ sUnitsMaxRep S F for the $\mathbb{Z}$-representation of that fixing subgroup given by Additive of the subgroup sUnitsMaxStable S F of $\overline{\mathbb{Q}}^\times$, a subgroup stable under the fixing subgroup's action on units; the map sUnitsMaxRep.val S F sends an element of $E_S$ to the corresponding unit of $\overline{\mathbb{Q}}$. Let $X \colon D \times D \to E_S$ satisfy: $X$ lies in levelCocycles₂ for $D$ acting on $E_S$ by restriction along the inclusion $D \le F$'s fixing subgroup; the integer multiple $p \cdot X$ lies in the corresponding levelCoboundaries₂; and the composite $g \mapsto$ Additive.ofMul (sUnitsMaxRep.val S F (X g)), i.e. $X$ regarded with values in $\overline{\mathbb{Q}}^\times$ via the representation Rep.ofAlgebraAutOnUnits ℚ (AlgebraicClosure ℚ) restricted to $D$, lies in levelCoboundaries₂ there. The conclusion is that $X$ itself lies in levelCoboundaries₂ for $D$ acting on $E_S$.

This is the degree-two Kummer comparison for the module of $S$-units of the maximal extension unramified outside $S$: since $p \in S$, a class that is $p$-torsion in $H^2$ with $E_S$-coefficients and dies in $H^2$ with $\overline{\mathbb{Q}}^\times$-coefficients already vanishes, all cochains being taken at finite level. It is used in the proofs that the relevant continuous $H^2$ of the Galois $S$-units representation vanishes, in the forms groupCohomology.continuousH2Sr_galoisSUnitsRep_eq_zero_of_forall_res_extArithIndex_eq_zero and groupCohomology.continuousH2Sr_galoisSUnitsRep_eq_zero_of_res_adjoin_sqrt_neg_one_eq_zero.