平坦局所準同型の次元公式と深さ公式

主定理の二つの等式を引き算すると
$$ \dim B-\operatorname{depth}B=(\dim A-\operatorname{depth}A)+(\dim F-\operatorname{depth}F) $$
である。Noether局所環では深さは次元以下なので（Cohen–Macaulay環 の補題「深さと随伴素の次元」）、右辺の二つの括弧はどちらも $0$ 以上の整数である。従って左辺が $0$ であることと、右辺の二つの括弧がともに $0$ であることは同値である。$\square$

$d=\dim A$、$e=\dim F$ とおく。パラメータ系 の定理「パラメータ系の存在」により、$A$ のパラメータ系 $t_1,\dots,t_d\in\mathfrak m$ と、$F$ のパラメータ系 $\bar v_1,\dots,\bar v_e$ がとれる。$\bar v_j$ を $B$ の元 $v_j\in\mathfrak n$ に持ち上げる。
$\sqrt{(t_1,\dots,t_d)}=\mathfrak m$ なので、ある $a\ge1$ について $\mathfrak m^a\subset(t_1,\dots,t_d)$ である（パラメータ系 の命題「極大根基、有限長、零次元」）。同様に $F$ では $(\mathfrak n/\mathfrak mB)^b\subset(\bar v_1,\dots,\bar v_e)$ となる $b\ge1$ があり、これを $B$ に戻すと $\mathfrak n^b\subset(v_1,\dots,v_e)+\mathfrak mB$ である。従って
$$ \mathfrak n^{ab}\subset\bigl((v)+\mathfrak mB\bigr)^a\subset(v)+\mathfrak m^aB\subset(v_1,\dots,v_e,t_1,\dots,t_d)B $$
となる（二つ目の包含は、$a$ 個の積を展開すると $(v)$ の元を一つでも含む項は $(v)$ に入ることによる）。よって $d+e$ 個の元で生成されるイデアル $(t,v)B$ の根基は $\mathfrak n$ であり、パラメータ系 の補題「極大根基の生成元数による次元上界」から $\dim B\le d+e$ を得る。$\square$

$A_{\mathfrak p}\to B_{\mathfrak q}$ が平坦であることを確かめる。$B\otimes_AA_{\mathfrak p}$ は $A_{\mathfrak p}$ 上平坦である（平坦加群 の命題「平坦加群の基底拡大」）。$B_{\mathfrak q}$ は $B\otimes_AA_{\mathfrak p}=B_{\mathfrak p}$（$\varphi(A\setminus\mathfrak p)$ による局所化）のさらに局所化であり、局所化は平坦なので（平坦加群 の例「局所化と有理数」）、平坦な加群を平坦な加群に重ねたテンソルとして $B_{\mathfrak q}$ も $A_{\mathfrak p}$ 上平坦である。$\varphi(A\setminus\mathfrak p)\cap\mathfrak q=\emptyset$ なので $\mathfrak pB_{\mathfrak q}\subset\mathfrak qB_{\mathfrak q}$ であり、$A_{\mathfrak p}\to B_{\mathfrak q}$ は局所準同型である。
よって 下降定理 の定理「平坦な準同型の下降定理」の仮定がみたされ、求める $\mathfrak q'$ が得られる。$\square$

prop-flat-local-dimension-upper により $\dim B\le d+e$（$d=\dim A$、$e=\dim F$）なので、長さ $d+e$ の素イデアルの鎖を $B$ に作ればよい。
$F$ の長さ $e$ の素イデアルの鎖を $B$ に戻して $\mathfrak q_0\subsetneq\mathfrak q_1\subsetneq\cdots\subsetneq\mathfrak q_e=\mathfrak n$ と書く（$F$ は局所環なので、最大長の鎖の最後は極大イデアルにとれる）。各 $\mathfrak q_i$ は $\mathfrak mB$ を含むので、$\varphi^{-1}(\mathfrak q_i)\supset\mathfrak m$、従って $\varphi^{-1}(\mathfrak q_i)=\mathfrak m$ である。
次に $A$ の長さ $d$ の鎖 $\mathfrak p_0\subsetneq\cdots\subsetneq\mathfrak p_d=\mathfrak m$ を取る。lem-flat-local-going-down を $\mathfrak q_0$ と $\mathfrak p_{d-1}\subset\mathfrak m$ に使って $\mathfrak q_{-1}\subset\mathfrak q_0$、$\varphi^{-1}(\mathfrak q_{-1})=\mathfrak p_{d-1}$ を得る。これを繰り返して
$$ \mathfrak q_{-d}\subset\cdots\subset\mathfrak q_{-1}\subset\mathfrak q_0,\qquad\varphi^{-1}(\mathfrak q_{-i})=\mathfrak p_{d-i} $$
を作る。引き戻しが互いに異なるので、各包含は真である。こうして長さ $d+e$ の鎖 $\mathfrak q_{-d}\subsetneq\cdots\subsetneq\mathfrak q_e$ が得られ、$\dim B\ge d+e$ となる。$d=0$ や $e=0$ のときは対応する鎖を一点の鎖とすればよい。$\square$

1. $M_j:=\mathfrak m^jM$（$j\ge0$）とおく。$N$ が平坦なので、短完全列 $0\to M_{j+1}\to M_j\to M_j/M_{j+1}\to0$ に $-\otimes_AN$ を施しても完全であり、$M_j\otimes_AN\to M\otimes_AN$ は単射である。その像は $\mathfrak m^j(M\otimes_AN)$ に等しいので
   $$ (M/\mathfrak m^jM)\otimes_AN\cong(M\otimes_AN)/\mathfrak m^j(M\otimes_AN) $$
   となる。$y$ の掛け算はこれらすべての同型と可換する。
   $V_j:=M_j/M_{j+1}$ は $\mathfrak m$ に零化される有限生成 $A$ 加群、すなわち有限次元 $k$ ベクトル空間である。$V_j\cong k^{n_j}$ と書けば
   $$ V_j\otimes_AN\cong(k\otimes_AN)^{n_j}=(N/\mathfrak mN)^{n_j} $$
   であり、$y$ はこの上で成分ごとに $N/\mathfrak mN$ 上の $y$ として働くので単射である。
   $j$ に関する帰納法で、$y$ が $(M/\mathfrak m^jM)\otimes_AN$ 上単射であることを示す。$j=0$ では零加群である。短完全列 $0\to V_j\to M/M_{j+1}\to M/M_j\to0$ に $N$ をテンソルした完全列
   $$ 0\to V_j\otimes_AN\to(M/M_{j+1})\otimes_AN\to(M/M_j)\otimes_AN\to0 $$
   の両端で $y$ が単射なら中央でも単射である。実際、中央の元 $z$ が $yz=0$ を満たせば、右端での像は帰納法の仮定で $0$ なので $z$ は左端から来ており、左端で $y$ が単射なので $z=0$ である。
   最後に $z\in M\otimes_AN$ が $yz=0$ を満たすとする。上の同型により、すべての $j$ について $z\in\mathfrak m^j(M\otimes_AN)\subset\mathfrak n^j(M\otimes_AN)$ である。$M\otimes_AN$ は有限生成 $B$ 加群（$M$ と $N$ の生成元のテンソルで生成される）なので、Krullの交叉定理 の 2 により $\bigcap_j\mathfrak n^j(M\otimes_AN)=0$ であり、$z=0$ となる。
2. $M=A$ として $y$ は $N$ 上単射である。$y\in\mathfrak n$ と Nakayamaの補題 により $N/yN\ne0$ である。平坦性を示す。$A$ の有限生成イデアル $I$ を取る。完全列 $0\to N\xrightarrow{y}N\to N/yN\to0$ から得られる Tor の長完全列（Tor関手 の命題「長完全列」）の一部
   $$ \operatorname{Tor}_1^A(A/I,N)\to\operatorname{Tor}_1^A(A/I,N/yN)\to(A/I)\otimes_AN\xrightarrow{\ y\ }(A/I)\otimes_AN $$
   において、左端は $N$ の平坦性から $0$ であり（Tor関手 の命題「平坦加群に対する消滅」）、右の写像は 1 を $M=A/I$ に使えば単射である。よって $\operatorname{Tor}_1^A(A/I,N/yN)=0$ であり、平坦性のイデアル判定 により $N/yN$ は平坦である。$\square$

$r=\operatorname{depth}A$、$s=\operatorname{depth}F$ とおく。$\mathfrak m$ の中の延長できない $A$ 正則列 $x_1,\dots,x_r$ と、$\mathfrak n/\mathfrak mB$ の中の延長できない $F$ 正則列 $\bar y_1,\dots,\bar y_s$ を取り、$\bar y_j$ を $y_j\in\mathfrak n$ に持ち上げる。
段階 1：$x$ の部分。 $J_i=(x_1,\dots,x_{i-1})$ とおく。$x_i$ の掛け算 $A/J_i\to A/J_i$ は単射なので、平坦な $B$ をテンソルした $B/J_iB\to B/J_iB$ も単射である（$B\otimes_AA/J_i=B/J_iB$）。$J_{r+1}B\subset\mathfrak mB\subset\mathfrak n$ より各商は $0$ でないので、$x_1,\dots,x_r$ は $B$ 正則列である。$\bar A:=A/(x)$、$\bar B:=B/(x)B=B\otimes_A\bar A$ とおくと、$\bar A\to\bar B$ は Noether局所環の平坦局所準同型で（平坦加群 の命題「平坦加群の基底拡大」）、その閉ファイバーは $\bar B/\mathfrak m\bar B=B/\mathfrak mB=F$ である。
段階 2：$y$ の部分。 $N_0:=\bar B$、$N_j:=\bar B/(y_1,\dots,y_j)\bar B$ とおく。$N_{j-1}$ が $\bar A$ 上平坦で $N_{j-1}/\mathfrak mN_{j-1}=F/(\bar y_1,\dots,\bar y_{j-1})F$ のとき、$\bar y_j$ はこの上で単射なので、lem-flat-local-lift-regular を $\bar A\to\bar B$ と $N=N_{j-1}$ に使うと、$y_j$ は $N_{j-1}$ 正則元で $N_j$ は $\bar A$ 上平坦である。帰納法により $x_1,\dots,x_r,y_1,\dots,y_s$ は長さ $r+s$ の $B$ 正則列であり、$C:=N_s=B/(x,y)B$ は $\bar A$ 上平坦で、$C/\mathfrak mC=F/(\bar y)F$ となる。
段階 3：延長できないこと。 $x$ は延長できないので $\operatorname{depth}\bar A=0$ であり、深さ の命題「深さ零の判定」により $\bar A$ 加群の単射 $k\hookrightarrow\bar A$ がある。平坦な $C$ をテンソルすると、$B$ 加群の単射
$$ C/\mathfrak mC=k\otimes_{\bar A}C\hookrightarrow\bar A\otimes_{\bar A}C=C $$
を得る。同様に $\bar y$ は延長できないので $\operatorname{depth}_B(F/(\bar y)F)=0$ であり、単射 $k'\hookrightarrow F/(\bar y)F=C/\mathfrak mC$ がある。合成すると $k'\hookrightarrow C$ となり、$\operatorname{depth}_BC=0$、すなわち $\mathfrak n$ のどの元も $C$ の零因子である。従って $B$ 正則列 $x,y$ は延長できず、深さ の定理「正則列とExtによる深さ」により $\operatorname{depth}B=r+s$ である。$\square$