Frobenius相互律

$\Lambda(T)$ が $H$ の表現の射であること：$h\in H$ について、$h\otimes w=1\otimes hw$ に注意すると
$$ \Lambda(T)(hw)=T(1\otimes hw)=T(h\cdot(1\otimes w))=h\,T(1\otimes w)=h\,\Lambda(T)(w) $$
である。
$T_\varphi$ が well-defined な $G$ の表現の射であること：$(x,w)\mapsto x\varphi(w)$ は $F$ 双線形で、$h\in H$ について $(xh)\varphi(w)=x(h\varphi(w))=x\varphi(hw)$（$\varphi$ が $H$ の表現の射）なので、誘導表現 の定義の前の段落によりテンソル積 $F[G]\otimes_{F[H]}W$ 上の線形写像を定める。$T_\varphi(g(x\otimes w))=gx\varphi(w)=g\,T_\varphi(x\otimes w)$ なので表現の射である。
互いに逆であること：$\Lambda(T_\varphi)(w)=1\cdot\varphi(w)=\varphi(w)$ である。逆に $T_{\Lambda(T)}(x\otimes w)=x\,T(1\otimes w)=T(x\otimes w)$（$T$ は $F[G]$ 加群の準同型）であり、$x\otimes w$ の形の元は $\operatorname{Ind}_H^GW$ を張るので $T_{\Lambda(T)}=T$ である。
自然性：$\Lambda(b\circ T\circ\operatorname{Ind}(a))(w')=b\bigl(T(1\otimes a(w'))\bigr)=b\bigl(\Lambda(T)(a(w'))\bigr)$ である。$\square$

誘導表現 の命題「剰余類による分解」により、$\operatorname{Ind}_H^GW$ の元は $\sum_{t\in R}t\otimes w_t$ と一意に書けるので、$\pi$ は well-defined な線形写像である。
$\pi$ は $H$ の表現の射である：$h\in H$、$t\in R$ について $ht\in t'H$（$t'\in R$）とすると、$h(t\otimes w)$ は $t'\otimes W$ に属し、$t'=1$ となるのは $ht\in H$、すなわち $t=1$ のときに限る。$t=1$ なら $h(1\otimes w)=h\otimes w=1\otimes hw$ である。よって $\pi(hu)=h\,\pi(u)$ である。したがって $\pi\circ\Psi$ は $H$ の表現の射である。
$\Phi_\varphi$ が $G$ の表現の射であること：まず和は代表系の取り方によらない。$t$ を $th$（$h\in H$）に替えると $th\otimes\varphi(h^{-1}t^{-1}v)=t\otimes h\varphi(h^{-1}t^{-1}v)=t\otimes\varphi(t^{-1}v)$ だからである。$g\in G$ について、$\{gt\}_{t\in R}$ も $G/H$ の代表系なので
$$ g\,\Phi_\varphi(v)=\sum_{t\in R}gt\otimes\varphi\bigl((gt)^{-1}gv\bigr)=\Phi_\varphi(gv) $$
である。
互いに逆であること：$\pi(\Phi_\varphi(v))$ は $t=1$ の項の成分で $\varphi(v)$ である。逆に、$u=\sum_{s\in R}s\otimes w_s$ について $t^{-1}u=\sum_st^{-1}s\otimes w_s$ の剰余類 $H$ の成分は $t^{-1}s\in H$、すなわち $s=t$ の項から来るので、$\pi(t^{-1}u)=w_t$ である。よって $G$ の表現の射 $\Psi$ について
$$ \Phi_{\pi\Psi}(v)=\sum_{t\in R}t\otimes\pi\bigl(\Psi(t^{-1}v)\bigr)=\sum_{t\in R}t\otimes\pi\bigl(t^{-1}\Psi(v)\bigr)=\Psi(v) $$
である。
自然性：$H$ の表現の射 $a\colon W\to W'$ について、$\operatorname{Ind}(a)$ は各成分 $t\otimes w$ を $t\otimes a(w)$ に移すので $\pi_{W'}\circ\operatorname{Ind}(a)=a\circ\pi_W$ である。よって $G$ の表現の射 $b\colon V'\to V$ について $\pi_{W'}\circ(\operatorname{Ind}(a)\circ\Psi\circ b)=a\circ(\pi_W\circ\Psi)\circ b$ となる。$\square$

要点：$\operatorname{Hom}_G(V,W)$ は $\operatorname{Hom}_{\mathbb{C}}(V,W)$ の $G$ 固定点であり、平均 $P=\frac{1}{|G|}\sum_g(g\cdot)$ はその上への射影なので、次元は $P$ の跡 $\frac{1}{|G|}\sum_g\chi_W(g)\chi_V(g^{-1})$ に等しい。

定義を代入すると、左辺は
$$ \frac{1}{|G|\,|H|}\sum_{\substack{(g,x)\in G\times G\\ x^{-1}gx\in H}}\psi(x^{-1}gx)\overline{\varphi(g)} $$
である。$x^{-1}gx\in H$ を満たす組 $(g,x)$ と $H\times G$ の組 $(h,x)$ は、$h=x^{-1}gx$、$g=xhx^{-1}$ で 1 対 1 に対応する。$\varphi$ は類関数なので $\varphi(xhx^{-1})=\varphi(h)$ であり、左辺は
$$ \frac{1}{|G|\,|H|}\sum_{x\in G}\sum_{h\in H}\psi(h)\overline{\varphi(h)}=\frac{1}{|H|}\sum_{h\in H}\psi(h)\overline{\varphi(h)}=\langle\psi,\operatorname{Res}^G_H\varphi\rangle_H $$
となる。$\square$

有限群の複素表現 $U$ は既約表現の直和 $U=\bigoplus_iE_i$ に分かれる（群の表現 の定理「有限群の実・複素表現の完全可約性」）。Schur の補題（群の表現 の定理「Schur の補題」）により、既約表現 $E$ について $\dim\operatorname{Hom}_G(U,E)=\sum_i\dim\operatorname{Hom}_G(E_i,E)$ は $E_i\cong E$ となる $i$ の個数であり、とくにこの個数は分け方によらない。同様に、$H$ の表現 $U'$ と既約表現 $W$ について、$\dim\operatorname{Hom}_H(W,U')$ は $U'$ の直和分解で $W$ と同型な成分の個数である。thm-fr-main により $\dim\operatorname{Hom}_G(\operatorname{Ind}_H^GW,E)=\dim\operatorname{Hom}_H(W,\operatorname{Res}^G_HE)$ であり、左辺は前者の個数、右辺は後者の個数である。$\square$

要点：thm-fr-main で左辺を $F[G/H]$ の $K$ 固定点の次元に直し、固定点の基底として $K$ 軌道の和をとる。

有限群の $0$ でない複素表現 $U=\bigoplus_iE_i^{m_i}$（$E_i$ は互いに同型でない既約表現）について、Schur の補題により $\dim\operatorname{End}_G(U)=\sum_im_i^2$ なので、$U$ が既約であることは $\dim\operatorname{End}_G(U)=1$ と同値である。$H$ の表現についても同じである。
$S$ を $H\backslash G/H$ の代表系で $1\in S$ となるものとする。thm-fr-main、Mackey の分解公式（$K=H$）、thm-fr-second（$H_s$ は $H$ で指数有限）を順に使うと
$$ \operatorname{End}_G(\operatorname{Ind}_H^GW)\cong\operatorname{Hom}_H\bigl(W,\operatorname{Res}^G_H\operatorname{Ind}_H^GW\bigr)\cong\bigoplus_{s\in S}\operatorname{Hom}_H\bigl(W,\operatorname{Ind}_{H_s}^H{}^sW\bigr)\cong\bigoplus_{s\in S}\operatorname{Hom}_{H_s}\bigl(\operatorname{Res}^H_{H_s}W,{}^sW\bigr) $$
を得る。$s=1$ の項は $H_1=H$、${}^1W=W$ なので $\operatorname{End}_H(W)$ であり、$W\neq0$ なので次元は $1$ 以上である。よって左辺の次元が $1$ であることは、$\dim\operatorname{End}_H(W)=1$（すなわち $W$ が既約）かつ $s\neq1$ のすべての項が $0$ であることと同値である。$s\in G\setminus H$ は $S\setminus\{1\}$ のどれかと同じ両側剰余類 $HsH$ に属し、$s'=h_1sh_2$（$h_i\in H$）なら $H_{s'}=h_1H_sh_1^{-1}$ であり、共役 $x\mapsto h_1xh_1^{-1}$ で $H_s$ と $H_{s'}$ を同一視すると、$\operatorname{Res}^H_{H_{s'}}W$ は $\sigma(h_1)$ によって $\operatorname{Res}^H_{H_s}W$ と、${}^{s'}W$ は $\sigma(h_2)$ によって ${}^sW$ と同型になる（$s'^{-1}h_1xh_1^{-1}s'=h_2^{-1}(s^{-1}xs)h_2$）。よって項が $0$ かどうかは両側剰余類だけで決まる。したがって条件は 1 と 2 に一致する。$\square$

$H$ が正規なら $H_s=H$ である。既約表現 ${}^sW$ と $W$ が互いに素であることは、Schur の補題により同型でないことと同値である（${}^sW$ も $W$ と同じ部分空間を不変にするので既約である）。thm-fr-mackey-criterion から従う。$\square$