Mackey restriction formula (source code)

= Mackey restriction formula
{c}

= Mackey theorem
{c}
{synonym}

= Mackey's theorem
{c}
{synonym}

= Mackey decomposition
{c}
{synonym}

For $H,K\leq G$ and a $K$-representation $V$,
$$
\operatorname{Res}_H^G\operatorname{Ind}_K^GV
\cong
\bigoplus_{x\in H\backslash G/K}
\operatorname{Ind}_{H\cap xKx^{-1}}^H
\operatorname{Res}_{H\cap xKx^{-1}}^{xKx^{-1}}({}^xV),
$$
where ${}^xV(xkx^{-1})=V(k)$.

To prove the formula, write induction as $\mathbb C[G]\otimes_{\mathbb C[K]}V$ and decompose the $(H,K)$-bimodule
$$
\mathbb C[G]=\bigoplus_{x\in H\backslash G/K}\mathbb C[HxK].
$$
For $L_x=H\cap xKx^{-1}$, the map
$$
\mathbb C[H]\otimes_{\mathbb C[L_x]}{}^xV
\longrightarrow
\mathbb C[HxK]\otimes_{\mathbb C[K]}V,
\qquad h\otimes v\longmapsto hx\otimes v,
$$
is a well-defined $H$-equivariant isomorphism. Taking the direct sum over the double cosets proves the result.