The submersion criterion between smooth varieties

Put $C_{x}X={\mathfrak{m}}_x\mathrm{/}{\mathfrak{m}}_x^2$ and $C_{y}Y={\mathfrak{m}}_y\mathrm{/}{\mathfrak{m}}_y^2$, and let $\alpha :C_{y}Y\to C_{x}X$ be the cotangent map induced by $f$. By [F2], $x,y$ are $k$-rational; by [F5] their structural smoothness assumptions give standard-smooth charts, and [F6] records that $f$ is finite type. Hence [F9] applies and says $f$ is smooth at $x$ exactly when $\alpha$ is injective.

By [F7], $C_{x}X$ and $C_{y}Y$ are finite-dimensional; the differential is $d_{x}f={\alpha }^{\ast }$ by [F8]. A linear map and its dual have equal rank, so $\alpha$ is injective iff $\mathrm{rank}(\alpha )=\dim C_{y}Y=\dim T_{y}Y=\mathrm{rank}({\alpha }^{\ast })$, iff $d_{x}f$ is surjective. With step 1.1 this proves both directions.

If these equivalent conditions hold (step 2.1), [F10] gives a regular local ring for the scheme-theoretic fibre at $x$, of dimension $\dim {\mathcal{O}}_{X,x}-\dim {\mathcal{O}}_{Y,y}$. By [F3] and [F4], these stalk dimensions equal ${\dim }_{x}X$ and ${\dim }_{y}Y$. This proves the stated local fibre dimension; no regularity at other fibre points is asserted.

Let $D=\mathrm{Spec}(k[ϵ]\mathrm{/}({ϵ}^2))$. By [F8], $v\in T_{x}X$ is represented by a based map $\gamma :D\to X$, and $d_{x}f(v)$ by $f\circ \gamma$. By [F11]–[F13] and the fibre-product universal property, based maps $D\to X_y$ at $x$ correspond to based $\gamma :D\to X$ whose composite is the constant map $D\to \mathrm{Spec}k\stackrel{y}{\to }Y$. That constant map represents zero in $T_{y}Y$, so these are exactly the $v$ with $d_{x}f(v)=0$. The correspondence is linear and canonical, proving $T_x(X_y)=\ker (d_{x}f)$ even when $f$ is not smooth at $x$.

If $T_{y}Y=0$, every differential to it is surjective and $C_{y}Y=0$ makes $\alpha$ injective, so [F9] gives smoothness; if $T_{x}X=0$ but $T_{y}Y\mathrm{\ne }0$, neither condition holds, and when both vanish the fibre has local dimension zero. The identity ${\mathbb{A}}_k^1\to {\mathbb{A}}_k^1$ at $0$ has differential $1$ and point fibre $\mathrm{Spec}k$, regular of dimension zero. For $t\mapsto t^2$ at $0$, the derivative $2tdt$ vanishes in every characteristic, so [F8, F9] show the differential is zero and the map is not smooth. Its fibre is $\mathrm{Spec}(k[t]\mathrm{/}(t^2))$; since $t$ is nilpotent the only prime is $(t)$, so the local dimension is zero, while its maximal ideal $\mathfrak{m}=(t)$ has ${\mathfrak{m}}^2=0$ and $\mathfrak{m}\mathrm{/}{\mathfrak{m}}^2\cong k$. Thus the local ring is not regular and its one-dimensional tangent space is the full kernel. This checks the degenerate case and shows regularity is asserted only under smoothness. If $X$ has no classical points there is no $x$ to check; the dimension difference is nonnegative when $f$ is smooth by steps 2.1 and 3.1. AC is inherited only through [F1], [F4], [F5], and [F9]; linear algebra and the fibre-product argument add no choice principle.