Ehresmannの補題

$n=\dim N$ とし、$q\in N$ を固定する。$q$ の座標近傍 $(V,\psi)$ で $\psi\colon V\to\mathbb{R}^n$ が微分同相写像かつ $\psi(q)=0$ となるものをとる（$q$ のまわりの任意の座標近傍は、$q$ を中心とする開球に縮めれば $\mathbb{R}^n$ と微分同相である）。$M':=f^{-1}(V)$ は $M$ の開部分多様体であり、$f':=\psi\circ f|_{M'}\colon M'\to\mathbb{R}^n$ は沈め込みである（$\psi$ の微分は同型）。また $f'$ は固有である：$K\subset\mathbb{R}^n$ がコンパクトなら $\psi^{-1}(K)$ は $V$ のコンパクト部分集合、したがって $N$ のコンパクト部分集合であり、$f'^{-1}(K)=f^{-1}(\psi^{-1}(K))$ は $f$ の固有性によりコンパクトである。$V$ 上の局所自明化を作るには $f'$ の $\mathbb{R}^n$ 上の（大域的な）自明化を作ればよいので、以下 $N=\mathbb{R}^n$、$q=0$、$f=f'$ と仮定し、$F:=f^{-1}(0)$ とおく。$F$ は rem-ehresmann-standard-facts の 1 により $M$ の閉部分多様体であり、$f$ の固有性によりコンパクトである。
$\mathbb{R}^n$ の座標を $y=(y_1,\dots,y_n)$、標準基底を $e_1,\dots,e_n$ と書く。lem-ehresmann-lift により、各 $j=1,\dots,n$ に対して $M$ 上のベクトル場 $X_j$ で $df(X_j)=\partial/\partial y_j$ を満たすものが存在し、lem-ehresmann-complete により $X_j$ は完備で、そのフロー $\theta^j\colon\mathbb{R}\times M\to M$ は滑らかで
$$ f(\theta^j_t(x))=f(x)+t\,e_j\qquad(t\in\mathbb{R},\ x\in M) $$
を満たす。ここで $\theta^j_t:=\theta^j(t,\cdot)$ と書く。フローの群性質 $\theta^j_s\circ\theta^j_t=\theta^j_{s+t}$ により各 $\theta^j_t$ は微分同相写像で、逆写像は $\theta^j_{-t}$ である。
写像 $\Phi\colon\mathbb{R}^n\times F\to M$ を
$$ \Phi(y,x):=\theta^1_{y_1}\bigl(\theta^2_{y_2}\bigl(\cdots\theta^n_{y_n}(x)\cdots\bigr)\bigr) $$
で定める。$\Phi$ は滑らかな写像 $\mathbb{R}^n\times M\to M$, $(y,z)\mapsto\theta^1_{y_1}\circ\cdots\circ\theta^n_{y_n}(z)$ の部分多様体 $\mathbb{R}^n\times F$ への制限なので滑らかである。$x\in F$ に対して $f(x)=0$ なので、上の等式を $j=n,n-1,\dots,1$ の順に適用して
$$ f(\Phi(y,x))=0+y_ne_n+y_{n-1}e_{n-1}+\cdots+y_1e_1=y, $$
すなわち $f\circ\Phi=\mathrm{pr}_1$ を得る。
次に写像 $\Psi\colon M\to\mathbb{R}^n\times M$ を、$z\in M$ に対し $y:=f(z)$ とおいて
$$ \Psi(z):=\bigl(y,\ \theta^n_{-y_n}\bigl(\theta^{n-1}_{-y_{n-1}}\bigl(\cdots\theta^1_{-y_1}(z)\cdots\bigr)\bigr)\bigr) $$
で定める。$\Psi$ は滑らかな写像の合成なので滑らかである。第 2 成分の $f$ による像は、上の等式を順に適用すると $y-y_1e_1-\cdots-y_ne_n=0$ なので、$\Psi$ の像は閉部分多様体 $\mathbb{R}^n\times F$ に含まれ、rem-ehresmann-standard-facts の 1 により $\Psi$ は $\mathbb{R}^n\times F$ への滑らかな写像とみなせる。
$\Phi$ と $\Psi$ が互いに逆であることを確かめる。$(y,x)\in\mathbb{R}^n\times F$ に対し $f(\Phi(y,x))=y$ なので
$$ \Psi(\Phi(y,x))=\bigl(y,\ \theta^n_{-y_n}\circ\cdots\circ\theta^1_{-y_1}\circ\theta^1_{y_1}\circ\cdots\circ\theta^n_{y_n}(x)\bigr)=(y,x) $$
であり（内側から順に $\theta^j_{-y_j}\circ\theta^j_{y_j}=\mathrm{id}$ を使う）、$z\in M$、$y=f(z)$ に対し
$$ \Phi(\Psi(z))=\theta^1_{y_1}\circ\cdots\circ\theta^n_{y_n}\circ\theta^n_{-y_n}\circ\cdots\circ\theta^1_{-y_1}(z)=z $$
である。よって $\Phi\colon\mathbb{R}^n\times F\to M$ は滑らかな全単射で滑らかな逆写像を持つ微分同相写像であり、$f\circ\Phi=\mathrm{pr}_1$ を満たす。これが求める自明化である。$\square$

各 $p\in M$ に対し、$p$ の座標近傍 $U_p$ と座標 $(x_1,\dots,x_m)$ で、$U_p$ 上 $x_j=y_j\circ f$（$j=1,\dots,n$）となるものが存在する。実際、$p$ のまわりの任意の座標 $(u_1,\dots,u_m)$ をとると、$f$ が沈め込みなので余接ベクトル $d(y_1\circ f)_p,\dots,d(y_n\circ f)_p$ は1次独立であり、$du_{k_1}|_p,\dots,du_{k_{m-n}}|_p$ を付け加えて $T_p^*M$ の基底にできる。写像 $(y_1\circ f,\dots,y_n\circ f,u_{k_1},\dots,u_{k_{m-n}})$ は $p$ で微分が同型なので、逆関数定理（Lee12 Chapter 4）により $p$ の近傍 $U_p$ で座標系をなす。これを $(x_1,\dots,x_m)$ とすれば、$f|_{U_p}$ はこの座標で $(x_1,\dots,x_m)\mapsto(x_1,\dots,x_n)$ と表される。$U_p$ 上のベクトル場 $X^{(p)}_j:=\partial/\partial x_j$ は、$U_p$ の各点で $df(\partial/\partial x_j)=\sum_k\frac{\partial(y_k\circ f)}{\partial x_j}\frac{\partial}{\partial y_k}=\frac{\partial}{\partial y_j}$ を満たす。
開被覆 $\{U_p\}_{p\in M}$ に従属する 1 の分割 $\{\rho_p\}_{p\in M}$ をとり（rem-ehresmann-standard-facts の 2）、
$$ X_j:=\sum_{p\in M}\rho_p\,X^{(p)}_j $$
とおく。$\rho_pX^{(p)}_j$ は $U_p$ の外で $0$ として $M$ 全体の滑らかなベクトル場に延び、台の族が局所有限なので和は各点の近傍で有限和であり、$X_j$ は $M$ 上の滑らかなベクトル場である。各点 $z\in M$ で、$df_z$ の線形性と $\sum_p\rho_p(z)=1$ により
$$ df_z\bigl((X_j)_z\bigr)=\sum_{p:\ z\in U_p}\rho_p(z)\,df_z\bigl((X^{(p)}_j)_z\bigr)=\sum_{p:\ z\in U_p}\rho_p(z)\,\frac{\partial}{\partial y_j}\Big|_{f(z)}=\frac{\partial}{\partial y_j}\Big|_{f(z)} $$
である。$\square$

$x\in M$ とし、$x$ を始点とする $X$ の極大積分曲線を $\gamma\colon(a,b)\to M$ とする。rem-ehresmann-standard-facts の 5 により $f\circ\gamma$ は $\mathbb{R}^n$ 上の定ベクトル場 $\partial/\partial y_j$ の積分曲線で、$f(\gamma(0))=f(x)$ なので、常微分方程式の解の一意性から $f(\gamma(t))=f(x)+t\,e_j$（$t\in(a,b)$）である。
$b<\infty$ と仮定する。$K:=\{f(x)+t\,e_j\mid t\in[0,b]\}$ は $\mathbb{R}^n$ の線分でコンパクトであり、$f$ の固有性から $f^{-1}(K)$ はコンパクトである。上の等式より $\gamma([0,b))\subset f^{-1}(K)$ であり、これは脱出補題（rem-ehresmann-standard-facts の 4）に反する。よって $b=\infty$ であり、同様に $a=-\infty$ である。したがって $X$ は完備で、フローは $\mathbb{R}\times M$ 全体で定義され、$f(\theta_t(x))=f(\gamma(t))=f(x)+t\,e_j$ が成り立つ。$\square$

$q\in N$ を固定し、$A:=\{q'\in N\mid f^{-1}(q')\text{ は }f^{-1}(q)\text{ と微分同相}\}$ とおく。$A$ は開集合である：$q'\in A$ に対し thm-ehresmann-main（全射性は不要。rem-ehresmann-assumptions の 1 を参照）の局所自明化 $\Phi\colon V\times f^{-1}(q')\to f^{-1}(V)$ をとると、$V$ の各点 $q''$ について $\Phi$ は $\{q''\}\times f^{-1}(q')$ を $f^{-1}(q'')$ の上に微分同相に写す（$f\circ\Phi=\mathrm{pr}_1$ により $\Phi^{-1}(f^{-1}(q''))=\{q''\}\times f^{-1}(q')$ であり、$\Phi$ は微分同相写像だからこの閉部分多様体の間の制限も微分同相写像である）ので、$V\subset A$ である。同じ議論で $N\setminus A$ も開集合である（$q'\notin A$ なら、$V$ の各点のファイバーは $f^{-1}(q')$ と微分同相なので $f^{-1}(q)$ と微分同相でない）。$A$ は $q$ を含む開かつ閉な集合なので、$q$ を含む連結成分を含む。$\square$

$C$ は $M$ の閉集合である：局所座標で $df_p$ は $n\times m$ 行列で表され、$p\in C$ であることはその $n$ 次小行列式がすべて $0$ になることと同値であり、小行列式は $p$ の連続関数である。固有写像は閉写像である（Lee12 Appendix A）から $\Delta=f(C)$ は閉集合であり、$N\setminus\Delta$ は開集合、$M\setminus f^{-1}(\Delta)=f^{-1}(N\setminus\Delta)$ は $M$ の開集合である。
$\tilde f$ は沈め込みである：$p\in M\setminus f^{-1}(\Delta)$ なら $f(p)\notin\Delta$ であり、もし $p\in C$ なら $f(p)\in f(C)=\Delta$ となって矛盾するので $p\notin C$、すなわち $df_p$ は全射である。
$\tilde f$ は固有である：$K\subset N\setminus\Delta$ をコンパクトとすると、$K$ は $N$ のコンパクト部分集合でもあり、$\tilde f^{-1}(K)=f^{-1}(K)\cap(M\setminus f^{-1}(\Delta))=f^{-1}(K)$（$K\cap\Delta=\emptyset$ による）は $f$ の固有性によりコンパクトである。
残りの主張は thm-ehresmann-main（rem-ehresmann-assumptions の 1 により全射性は不要）と cor-ehresmann-fibers-diffeomorphic から従う。$\square$