等質多様体

$V$は相対コンパクトな開近傍を動くものとする。proper性から $\set{g\in G}{\exists y\in \overline{V}\ gy\in \overline{V}}$ がコンパクトになる。また、あらゆる$V$に関する交叉は$\{e\}$となる。
$$\bigcap_V \set{g\in G}{\exists y\in \overline{V}\ gy\in \overline{V}}\setminus U=\emptyset$$
より、コンパクト性からある有限交叉が空、有向性からある$V$で空。

まず、各$x\in M$に対し$\Psi:G\ni g\longmapsto gx\in M$という写像がある。$X\in\g$を固定すると$d\Psi(X)\in T_x M$という接ベクトルが各$x\in M$で定まる。$Y_x:=d\Psi(X)$というベクトル場$Y$は$C^\infty$級である（作用$G\times M\to M$の$X$での偏導関数だから）。\
$t\mapsto\exp(tX)x$という$M$内の曲線は$Y$の積分曲線であるから、もしある$x\in M,X\in\g\setminus{0}$で$Y_x=0$となれば（ODEの解の一意性から）$\forall t\ \exp(tX)x=x$となって作用の自由性に反する。つまり、$\Psi$の微分は各$x\in M$で単射であることが言えた。\
$G$の次元を$n,$ $M$の次元を$m$とする。$x\in M$を通る曲面$S$であって$G$の軌道と横断的に交わるものを取る、つまり各$y\in S$で$T_y S+\im(d\Psi_y)=T_y M$となるものである。作用の制限$G\times S\to M$は先の補題から（$S$を十分$x$の近傍に制限すれば）単射であり、横断性から像への微分同相（更に像は開写像定理から開）である。$S\to M/G$は像（開集合）への同相だから、このような$S$を各$x\in M$で取ってきて、$M/G\supset GS/G\xrightarrow{\cong} S$を局所座標として微分構造を入れる。\
座標変換の$C^\infty$級性を確かめる。$GS/G\xrightarrow{\cong} S$と$GS'/G\xrightarrow{\cong} S'$の座標変換とは
[S\cap GS'\to (GS\cap GS')/G\to GS\cap S':\ x\longmapsto{}^{\exists!} gx\ \ \ (gx\in S')]
という写像であるが、$GS'\cong G\times S'$ が微分同相だから、第二成分への射影の制限$S\cap GS'\to S'$は像への微分同相。特に$C^\infty$級である。\
$GS=(\pi:M\to M/G)^{-1}(S)$は$S\times G$と微分同相だから、これにより局所自明化が与えられる。

作用$H\times G\to G$がproperかつ自由であることがすぐ分かる。故に、前定理から$M:=G/H$には自然に多様体構造が入る。掛け算$G\times M\to M$は、局所切断$G\times M\to G\times G$と掛け算$G\times G\to G$と射影$G\to M$の合成だから$C^\infty$級。\
更に$H$が正規部分群である場合の$G/H$の演算の$C^\infty$級性だが、同様に局所切断と$G$の演算と射影の合成であるため、OK。

$H$をある点$x\in M$のstabilizerとすればこれは$G$の閉部分群。orbit-stabilizer定理から次は全単射：
[\Psi:G/H\ni gH\longmapsto gx\in M]
局所切断$G/H\to G$と作用の制限$G\to M$の合成だから、$\Psi$は$C^\infty$級である。先の定理（捕鯨）の証明の前半と同様にして$\Psi$の微分が各点で単射であることが分かる。$X\in\g\setminus\h$を$G\ni g\mapsto gx\in M$で送ったものが0であるとして$\exp(tX)x=x$を導けば、$\exp(tX)\in H$より$X\in\h$となって矛盾する。\
もし$G/H$の次元より$M$の次元の方が大きければ、像の測度が0になって全単射性に矛盾する。故に同じ次元であり、$\Psi$の微分は各点で全単射になる。つまり$\Psi$は（$G$からの作用を保つ）微分同相。

$\phi:G/\ker\phi\to H$という写像は$C^\infty$級（局所切断$G/H\to G$を取る）である。故に単射なLie群の準同型を与え、これによって$\im\phi$にLie群としての構造を入れれば、トートロジカルな理由で$G/\ker\phi$と$\im\phi$は同型。Lie群の部分群をLie群と思う方法は高々一意的（積分多様体と書ける）だから、これ以外に$\im\phi$をLie群化する多様体の構造はない。そう言うと多少は非自明さが出てくる？