被覆変換群

$e_0\cdot[\gamma]=e_0$ なら、$\gamma$ の $e_0$ からの持ち上げ $\tilde\gamma$ は $e_0$ を基点とするループで、$p\circ\tilde\gamma=\gamma$ だから $[\gamma]=p_*[\tilde\gamma]\in H$ である。逆に $[\gamma]\in H$ なら、$e_0$ を基点とするループ $\tilde\delta$ で $[\gamma]=[p\circ\tilde\delta]$ となるものがある。$p\circ\tilde\delta$ の $e_0$ からの持ち上げは $\tilde\delta$ 自身で、終点は $e_0$ である。$\gamma$ と $p\circ\tilde\delta$ はホモトピックなので、持ち上げの終点は一致し、$e_0\cdot[\gamma]=e_0$ である。$\square$

lem-deck-image は任意の基点について成り立つので、$[\delta]\in p_*\pi_1(E,e_1)$ は $e_1\cdot[\delta]=e_1$ と同値である。作用の性質から
$$ e_1\cdot[\delta]=e_1\iff e_0\cdot[\gamma][\delta]=e_0\cdot[\gamma]\iff e_0\cdot[\gamma][\delta][\gamma]^{-1}=e_0\iff[\gamma][\delta][\gamma]^{-1}\in H $$
であり、最後の条件は $[\delta]\in[\gamma]^{-1}H[\gamma]$ と同値である。$\square$

$\sigma$ と $\tau$ はどちらも連続写像 $p\colon E\to B$ の持ち上げである（$p\circ\sigma=p=p\circ\tau$）。$E$ は連結なので、被覆空間の記事の定理「持ち上げの一意性」により、1 点で一致すれば全体で一致する。後半は $\tau=\mathrm{id}$ の場合である。$\square$

$\tilde\gamma$ を $\gamma$ の $e$ からの持ち上げとすると、$p\circ\sigma\circ\tilde\gamma=p\circ\tilde\gamma=\gamma$ なので、$\sigma\circ\tilde\gamma$ は $\gamma$ の $\sigma(e)$ からの持ち上げである。その終点 $\sigma(\tilde\gamma(1))=\sigma(e\cdot[\gamma])$ が $\sigma(e)\cdot[\gamma]$ である。$\square$

必要性：$\tilde f$ があれば $f_*=(p\circ\tilde f)_*=p_*\circ\tilde f_*$ なので、$f_*\pi_1(Y,y_0)\subset p_*\pi_1(E,e_0)$ である。一意性は被覆空間の記事の定理「持ち上げの一意性」による。
十分性：$y\in Y$ に対し、$y_0$ から $y$ への道 $\alpha$ をとり、$f\circ\alpha$ の $e_0$ からの持ち上げの終点を $\tilde f(y)$ と定める。
この定義が道 $\alpha$ の選び方によらないこと（$f_*\pi_1(Y,y_0)\subset H$ を使う）、$p\circ\tilde f=f$ となること、$\tilde f$ が連続であること（局所弧状連結性を使う）を順に確かめる。

1 の必要性：$\sigma$ は同相写像なので $\sigma_*\pi_1(E,e_0)=\pi_1(E,e_1)$ であり、$p\circ\sigma=p$ から
$$ p_*\pi_1(E,e_1)=p_*\sigma_*\pi_1(E,e_0)=(p\circ\sigma)_*\pi_1(E,e_0)=H $$
である。
1 の十分性：lem-deck-lifting を、$Y=E$、$y_0=e_0$、$f=p$ と、基点 $e_1$ を始点とする持ち上げについて使う。$p_*\pi_1(E,e_0)=H=p_*\pi_1(E,e_1)$ なので、$p$ の持ち上げ $\sigma\colon E\to E$ で $\sigma(e_0)=e_1$ となるものがある。$p\circ\sigma=p$ である。役割を入れ替えて、$\tau\colon E\to E$ で $p\circ\tau=p$、$\tau(e_1)=e_0$ となるものもある。$\tau\circ\sigma$ は $p$ の持ち上げで $e_0$ を固定するので、lem-deck-rigid の証明と同じく持ち上げの一意性から $\tau\circ\sigma=\mathrm{id}$、同様に $\sigma\circ\tau=\mathrm{id}$ である。よって $\sigma$ は同相写像で、被覆変換である。
2（$\Phi$ が定まること）：$[\gamma]\in N(H)$ なら $[\gamma]^{-1}H[\gamma]=H$ であり、lem-deck-conjugate により $e_1:=e_0\cdot[\gamma]$ について $p_*\pi_1(E,e_1)=H$ である。1 により $\sigma(e_0)=e_1$ となる被覆変換があり、lem-deck-rigid によりただ 1 つである。
2（準同型）：$[\gamma],[\delta]\in N(H)$ とする。lem-deck-commute により
$$ \Phi([\gamma])\bigl(\Phi([\delta])(e_0)\bigr)=\Phi([\gamma])\bigl(e_0\cdot[\delta]\bigr)=\Phi([\gamma])(e_0)\cdot[\delta]=e_0\cdot[\gamma][\delta]=\Phi([\gamma][\delta])(e_0) $$
であり、2 つの被覆変換 $\Phi([\gamma])\circ\Phi([\delta])$ と $\Phi([\gamma][\delta])$ は $e_0$ で一致するので、lem-deck-rigid により等しい。
2（全射）：被覆変換 $\sigma$ をとる。$\sigma(e_0)\in p^{-1}(b_0)$ なので、モノドロミー作用の推移性から $\sigma(e_0)=e_0\cdot[\gamma]$ となる $[\gamma]$ がある。1 により $p_*\pi_1(E,\sigma(e_0))=H$、lem-deck-conjugate によりこれは $[\gamma]^{-1}H[\gamma]$ なので、$[\gamma]\in N(H)$ であり、$\Phi([\gamma])$ と $\sigma$ は $e_0$ で一致するので等しい。
2（核）：$\Phi([\gamma])=\mathrm{id}$ は $e_0\cdot[\gamma]=e_0$ と同値であり（lem-deck-rigid）、lem-deck-image によりこれは $[\gamma]\in H$ と同値である。準同型定理により $G(E/B)\cong N(H)/H$ である。$\square$

(1)⇒(2)：$N(H)=\pi_1(B,b_0)$ なので、任意の $e_1=e_0\cdot[\gamma]$ について $\Phi([\gamma])(e_0)=e_1$ である。任意の 2 点は $e_0$ を経由して移り合う。(2)⇒(3)：thm-deck-main の 1 による。(3)⇒(1)：任意の $[\gamma]\in\pi_1(B,b_0)$ について、lem-deck-conjugate から $[\gamma]^{-1}H[\gamma]=p_*\pi_1(E,e_0\cdot[\gamma])=H$ なので、$H$ は正規である。最後の同型は thm-deck-main で $N(H)=\pi_1(B,b_0)$ とした場合である。$\square$

$\pi_1(E,e_0)$ は自明なので $H$ は自明な部分群であり、正規である。cor-deck-regular により $G(E/B)\cong\pi_1(B,b_0)/\{1\}=\pi_1(B,b_0)$ で、作用は推移的である。自由であること（単位元以外は固定点をもたないこと）は lem-deck-rigid による。$\square$

$e\in E$ をとり、$p(e)$ の均一被覆近傍 $U$ と、$e$ を含むシート $V$ をとる。被覆変換 $\sigma$ について $\sigma V\cap V\ni x$ とすると、$x=\sigma(v)$（$v\in V$）であり、$p(x)=p(\sigma(v))=p(v)$ で、$p|_V$ は単射なので $x=v$ である。よって $\sigma(v)=v$ となり、lem-deck-rigid により $\sigma=\mathrm{id}$ である。
後半：$p$ は軌道の上で一定なので、連続写像 $k\colon E/G(E/B)\to B$ を誘導する。$p$ は全射なので $k$ も全射である。$k$ が単射であること、すなわち各ファイバー $p^{-1}(b)$ が 1 つの軌道であることを示す。$e,e'\in p^{-1}(b)$ とし、$B$ の中の $b$ から $b_0$ への道 $\beta$ の、$e$ からの持ち上げ $\tilde\beta$ と $e'$ からの持ち上げ $\tilde\beta'$ をとる。cor-deck-regular により、被覆変換 $\sigma$ で $\sigma(\tilde\beta(1))=\tilde\beta'(1)$ となるものがある。$\sigma\circ\tilde\beta$ と $\tilde\beta'$ はどちらも $\beta$ の持ち上げで終点が一致するので、逆向きにたどった道は $\bar\beta$ の同じ点からの持ち上げであり、持ち上げの一意性から一致する。よって始点も一致し $\sigma(e)=e'$ である。被覆写像は開写像である（被覆空間の記事の命題「被覆写像の基本性質」の 1）。商写像を $\pi$ とすると、開集合 $O\subset E/G(E/B)$ について $k(O)=p(\pi^{-1}(O))$ は開集合なので、$k$ は開写像であり、同相写像である。$\square$

$q$ が被覆写像であることは上で引いた命題による。$Y/\Gamma$ は弧状連結空間の連続像として弧状連結であり、$q$ は開写像なので、弧状連結な開近傍の像が弧状連結な開近傍になり、局所弧状連結である。各 $g\in\Gamma$ は同相写像で $q\circ g=q$ をみたすので被覆変換である。逆に被覆変換 $\sigma$ と点 $y$ について、$q(\sigma(y))=q(y)$ なので $\sigma(y)=gy$ となる $g\in\Gamma$ があり、$\sigma$ と $g$ は $y$ で一致するので lem-deck-rigid により $\sigma=g$ である。作用が被覆空間作用なので、単位元以外の $g$ は固定点をもたず、異なる $g$ は異なる被覆変換を与える。ファイバー $q^{-1}(q(y))$ は軌道 $\Gamma y$ なので、被覆変換群は推移的に作用し、cor-deck-regular により $q$ は正則である。$\square$

$\Gamma=\{g_0,g_1,\dots,g_k\}$（$g_0$ は単位元）、$y\in Y$ とする。自由性から点 $g_0y,\dots,g_ky$ は相異なる（$g_iy=g_jy$ なら $g_j^{-1}g_i$ は $y$ を固定するので $g_i=g_j$）。Hausdorff 性から、互いに交わらない開集合 $W_i\ni g_iy$ がとれる。$W:=\bigcap_ig_i^{-1}(W_i)$ は $y$ の開近傍で、$g_iW\subset W_i$ である。$i\neq0$ なら $g_iW\cap W\subset W_i\cap W_0=\emptyset$ である。$\square$