Double coset formula for the degree-2 corestriction

Let $k$ be a commutative ring, $G$ a finite group and $A$ a $k$-linear representation of $G$; let $H, D \le G$ be subgroups. A Cores.Transversal H is a normalised section of the left cosets: a map $\sigma \colon G/H \to G$ with $\sigma(q) \in q$ for all $q$ and $\sigma(H) = 1$; let $\tau$ be such a transversal for $H$, and let $\mathrm{cores}$ denote the resulting degree-$2$ transfer $H^2(H, A|_H) \to H^2(G, A)$, obtained from the cochain-level corestriction attached to $\tau$ by passage to cohomology. Let $\iota$ be a finite type and $g \colon \iota \to G$ a family such that $i \mapsto D g_i H$ is a bijection of $\iota$ onto the double coset space $D \backslash G / H$, and assume $g_{i_0} = 1$ for some $i_0$. For each $i$ write $K_i \le D$ for the subgroup of $D$ with underlying set $D \cap g_i H g_i^{-1}$ (the subgroup (MulAut.conj (g i) • H).subgroupOf D), and suppose given: a normalised transversal $\tau_{D,i}$ of $K_i$ in $D$; a group homomorphism $c_i \colon K_i \to H$ with $c_i(x) = g_i^{-1} x g_i$ in $G$; and a morphism $T_i$ of representations of $K_i$ from $A|_H$ restricted along $c_i$ to $A|_D$ restricted along the inclusion $K_i \le D$, whose underlying map is $a \mapsto \rho_A(g_i)\,a$. Then for every $y \in H^2(H, A|_H)$, the restriction of $\mathrm{cores}_\tau(y)$ along the inclusion $D \le G$ (with the identity coefficient map on $A|_D$) equals the finite sum over $i \in \iota$ of the transfers $\mathrm{cores}_{\tau_{D,i}}$ from $K_i$ to $D$ of the images of $y$ under the degree-$2$ cohomology maps induced by $(c_i, T_i)$.

This is the double coset (Mackey) formula expressing the restriction to $D$ of a corestriction from $H$ as a sum of corestrictions over the double cosets $D \backslash G / H$, here in degree $2$ and with the transfer normalised through an explicit transversal. It is used in the computation of Herbrand quotients, in the reduction of sums of corestrictions over a family of subgroups to sums over intersections.