Differentials of a smooth morphism

Fix a smooth point $x\in X$ and write $s=f(x)$. By [F1] and [F2] there are affine opens $U=\mathrm{Spec}B\ni x$ and $V=\mathrm{Spec}A\ni s$ with $f(U)\subseteq V$ and $A\to B$ of finite presentation, and the local ring map $A_{\mathfrak{p}}\to B_{\mathfrak{q}}$, $\mathfrak{p}=\mathfrak{q}\cap A$ for the prime $\mathfrak{q}$ corresponding to $x$, is flat while the fibre $B{\otimes }_A\kappa (\mathfrak{p})$ is geometrically regular at $\mathfrak{q}$, these being the chart-level forms of flatness at $x$ and geometric regularity of the fibre at $x$.

By [F4] the finitely presented map $A\to B$ is standard smooth at $\mathfrak{q}$, so by [F3] there are $h\in B\setminus \mathfrak{q}$, integers $m\ge c\ge 0$, elements $f_1,\dots ,f_c\in A[x_1,\dots ,x_m]$ and $g\in A[x_1,\dots ,x_m]$ with $B_h\cong (A[x_1,\dots ,x_m]\mathrm{/}(f_1,\dots ,f_c){)}_g$, the leading $c\times c$ Jacobian block $J_0=(\mathrm{\partial }{f}_j\mathrm{/}\mathrm{\partial }{x}_i{)}_{1\le i,j\le c}$ having unit determinant in $B_h$.

Put $P=A[x_1,\dots ,x_m]$ and $B_0=P\mathrm{/}(f_1,\dots ,f_c)$, so that $B_h=(B_0{)}_g$; by [F8] applied over the chart, ${\mathrm{\Omega }}_{X\mathrm{/}S}(D(h))\cong {\mathrm{\Omega }}_{B_h\mathrm{/}A}$, and by [F7] (and localisation of the presentation $B_h=(B_0{)}_g$) the module ${\mathrm{\Omega }}_{B_h\mathrm{/}A}$ is the cokernel of the $B_h$-linear map $B_h^c\to B_h^m$ whose columns are the gradients $\mathrm{\nabla }{f}_j$ with coordinates in $B_h$.

This cokernel is free of rank $m-c$: writing the matrix of the map as the block matrix $J=\left(\genfrac{}{}{0px}{}{J_0}{J_2}\right)$ with $J_0$ invertible over $B_h$, the product $UJ=\left(\genfrac{}{}{0px}{}{I_c}{0}\right)$ with the invertible matrix $U=\left(\begin{array}{cc}{J}_0^{-1}& 0\\ -J_2{J}_0^{-1}& I_{m-c}\end{array}\right)$ (inverse $\left(\begin{array}{cc}{J}_0& 0\\ J_2& I_{m-c}\end{array}\right)$) shows that after the change of basis $U$ of $B_h^m$ the image of the map is exactly $B_h^c\oplus 0$, so the cokernel is $B_h^m\mathrm{/}(B_h^c\oplus 0)\cong B_h^{m-c}$, free of rank $m-c$.

Hence ${\mathrm{\Omega }}_{X\mathrm{/}S}$ is free of rank $m-c$ on the open neighbourhood $D(h)$ of $x$, which is one half of the theorem; it remains to identify the number with the relative dimension. Let $K\mathrm{/}\kappa (s)$ be a field extension and let $y\in X_{s,K}$ lie over $x$; then $y$ lies in the open part $D(h)$ of the fibre (the point $x$ itself lies in $D(h)$), so ${\dim }_y{X}_{s,K}$ equals the local dimension of $\mathrm{Spec}(B_h{\otimes }_{A}K)$ at the corresponding point, and $B_h$ is standard smooth over $A$ of relative dimension $m-c$ by [F3], so by [F5] every irreducible component of that spectrum has dimension $m-c$, whence the local dimension is $m-c$ by the component description in [F6].

The value in step 5.1 is independent of $K$ and of $y$ over $x$, so $f$ has relative dimension $m-c$ at $x$ by the definition recorded in [F6]; combined with step 4.1 this says ${\mathrm{\Omega }}_{X\mathrm{/}S}$ is free of rank equal to the relative dimension of $f$ at $x$ on a neighbourhood of $x$.

Since the smooth point $x\in X$ was arbitrary, every smooth point of $X$ has an open neighbourhood on which ${\mathrm{\Omega }}_{X\mathrm{/}S}$ is free of finite rank, namely a rank that is the relative dimension at the point, so on the smooth locus ${\mathrm{\Omega }}_{X\mathrm{/}S}$ is locally free of finite rank with rank function the relative dimension by [F9] and [F10]. If $f$ is smooth of pure relative dimension $n$, the rank is $n$ at every point, so ${\mathrm{\Omega }}_{X\mathrm{/}S}$ is locally free of rank $n$. The Axiom of Choice [F11] is used exactly through the cited criterion [F4] and the cited standard-smooth fibre computation [F5], both of which declare it; no further choice is made. [F9, F10, F11, step 6.1] $\mathrm{\square }$