Cup product of level-constant 1-cocycles is level-constant

Let $k$ be a commutative ring and $G$ a group, and let $r \colon G \to \operatorname{Aut}_{\mathbb{Q}}(\overline{\mathbb{Q}})$ be a group homomorphism into the group of $\mathbb{Q}$-algebra automorphisms of AlgebraicClosure ℚ (the level map). Let $A$, $B$, $N$ be $k$-linear representations of $G$ and let $\varphi \colon A \to B \to N$ be a $k$-bilinear map which satisfies Rep.IsEquivariantBilinear, i.e. $\varphi(\rho_A(g)a, \rho_B(g)b) = \rho_N(g)\varphi(a,b)$ for all $g \in G$, $a \in A$, $b \in B$. Assume $B$ is smooth for $r$ in the following sense: for every $b \in B$ there is an intermediate field $F$ of $\overline{\mathbb{Q}}/\mathbb{Q}$ with $F$ finite-dimensional over $\mathbb{Q}$ such that $\rho_B(s)b = b$ for every $s \in G$ with $r(s)$ in the fixing subgroup of $F$. Finally let $f$ be a $1$-cocycle of $A$ and $g$ a $1$-cocycle of $B$, both level-constant for $r$ in the sense of the predicate IsLevelConstant₁. The conclusion is that the underlying function $G \times G \to N$ of the cup product cup φ hφ f g, namely $(s,t) \mapsto \varphi(f(s), \rho_B(s)(g(t)))$, lies in levelCocycles₂ r N, the set of level-constant $2$-cocycles of $N$ for $r$.

This is the statement that the degree $(1,1)$ cup product of group cohomology preserves level-constancy, so that it descends to a pairing on the continuous (level-constant) cohomology groups $H^1 \times H^1 \to H^2$ attached to the level map $r$. It is used in the comparison results identifying continuous cohomology of induced, coinduced and retracted modules with the corresponding algebraic cohomology.