Relative Jacobian criterion with its presentation hypothesis

Fix $x\in X$ with $s=f(x)$ and choose affine open neighbourhoods $U=\mathrm{Spec}C\subseteq X$ of $x$ and $V=\mathrm{Spec}A\subseteq S$ of $s$ with $f(U)\subseteq V$; let $\mathfrak{q}\subseteq C$ be the prime defining $x$. Since $f$ is locally of finite presentation, $A\to C$ is a ring map of finite presentation.

Suppose first that $f$ is smooth at $x$. By [F2] the map $A\to C$ is flat at $\mathfrak{q}$ and its fibre at $\mathfrak{q}$ is geometrically regular. By the pointwise criterion [F4] applied to the finitely presented map $A\to C$ at $\mathfrak{q}$, the map is standard smooth at $\mathfrak{q}$: there is $h\in C\setminus \mathfrak{q}$ with $C_h\cong (A[t_1,\dots ,t_m]\mathrm{/}(f_1,\dots ,f_r){)}_g$ and an $r\times r$ Jacobian minor whose image in $C_h$ is a unit. Thus the required chart exists and the 'only if' direction of the theorem holds.

Conversely, suppose such data $U$, $V$, $h$, $m$, $r$, $f_j$, $g$ and an invertible minor are given at $x$. Then $A\to C_h$ is a standard smooth $A$-algebra in the sense of [F3], so by [F5] it is flat and finitely presented over $A$; by [F6] its geometric fibres are regular, with every irreducible component of dimension $m-r$. Since $f$ is moreover locally of finite presentation, the pointwise criterion [F2] applies at $x$ and shows that $f$ is smooth at $x$. This proves the 'if' direction and identifies the chart as flat with geometrically regular fibres.

Dimension clause. By [F6], every irreducible component of the fibre of the chart over any field extension of $\kappa (\mathfrak{p})$ has dimension $m-r$, so for a point $y$ of the geometric fibre lying over the image of $x$, every open neighbourhood of $y$ in that fibre has dimension $m-r$ and the local dimension of Relative dimension of a smooth morphism at a point equals $m-r$; this is independent of the field extension. Hence the chart has relative dimension $m-r$ at $x$ in the convention fixed on this page, and the same computation is what makes the integer attached to a smooth point well defined there.

Presentation warning. The presentation produced in step 1.2 is existential, and the criterion must not be applied to an arbitrary equation list: over a field $k$, the algebra $k=k[t]\mathrm{/}(t)$ is smooth of relative dimension $0$ and has the presentation $k[t]\mathrm{/}(t)$, whose $1\times 1$ Jacobian matrix has entry $1$, an invertible minor; but the redundant list $(t,t^2)$ writes the same quotient with $r=2$ and $m=1$, so the Jacobian matrix is $2\times 1$ and has no $2\times 2$ minor at all. By [F7] the module of differentials is unchanged by the redundant presentation; only the existence of one good presentation is asserted.

Choice audit. The Axiom of Choice is used as declared in [F1], through [F4], [F5] and [F6]. The affine chart, prime and generator selections of steps 1.1 and 1.2 are finite. No other choice principle and no incompatible-axiom branch is invoked.