Jacobian rank detects regularity at closed points

Since $A$ is a quotient of the finite-variable polynomial ring $P$, [F1] makes $A_{\mathfrak{m}}$ a Noetherian local ring. The algebra $A$ is finite type over $k$, so [F2] makes $L\mathrm{/}k$ finite. If $k$ is perfect, [F3] then makes $L\mathrm{/}k$ separable; this verifies the residue-field hypothesis in [F4] without assuming that $\mathfrak{m}$ is rational.

Now let $k$ be any field and let $\mathfrak{m}$ be $k$-rational. By [F11], $T_x(\mathrm{Spec}A)\cong \ker J(\mathfrak{m})$, so rank-nullity gives ${\dim }_k{T}_x(\mathrm{Spec}A)=n-{\mathrm{rank}}_{k}J(\mathfrak{m})$. Applying [F10] proves the same equivalence without a perfectness assumption. This argument uses the rational-point theorem only in the case $L=k$.

In the reduced classical case, [F12] identifies $A$ with the coordinate ring $k[X]$. Under the stated AC assumption, [F13] gives $\dim A_{\mathfrak{m}}={\max }_{x\in X_i}\dim X_i$, and [F14] identifies this maximum with ${\dim }_{x}X$. This is the claimed classical dimension formula; AC enters this clause through the local-dimension lemma [F13] and the fixed-field convention in [F14].

In the perfect-field case put $R=A_{\mathfrak{m}}$ and $\mathfrak{n}=\mathfrak{m}R$. By [F4], $\mathfrak{n}\mathrm{/}{\mathfrak{n}}^2\cong {\mathrm{\Omega }}_{R\mathrm{/}k}{\otimes }_{R}L$. Applying [F5] and then [F6] identifies this with ${\mathrm{\Omega }}_{A\mathrm{/}k}{\otimes }_{A}L$.

By [F7], ${\mathrm{\Omega }}_{A\mathrm{/}k}$ is the cokernel of $A^r\to A^n$ represented by the derivative vectors of $f_1,\dots ,f_r$. Right exactness [F8] identifies ${\mathrm{\Omega }}_{A\mathrm{/}k}{\otimes }_{A}L$ with the cokernel of $L^r\to L^n$ represented by those same vectors after mapping their entries to $L$. This is the transpose presentation of the equation-row matrix $J(\mathfrak{m})$, so the map has rank ${\mathrm{rank}}_{L}J(\mathfrak{m})$. Hence ${\dim }_L(\mathfrak{n}\mathrm{/}{\mathfrak{n}}^2)=n-{\mathrm{rank}}_{L}J(\mathfrak{m})$. Since this cokernel is finite-dimensional, [F9] gives ${\dim }_L{T}_x(\mathrm{Spec}A)=n-{\mathrm{rank}}_{L}J(\mathfrak{m})$.

The local-ring definition [F10] says $A_{\mathfrak{m}}$ is regular exactly when its tangent dimension equals $\dim A_{\mathfrak{m}}$. Substituting the dimension computed in step 3.1 gives $A_{\mathfrak{m}}$ regular iff $n-{\mathrm{rank}}_{L}J(\mathfrak{m})=\dim A_{\mathfrak{m}}$, equivalently iff ${\mathrm{rank}}_{L}J(\mathfrak{m})=n-\dim A_{\mathfrak{m}}$. This proves both directions for every closed point over a perfect field.

The degenerate cases fit the same calculations. If $I=P$, then $A=0$ has no maximal ideal and the pointwise assertions are vacuous. If $n=0$ and a maximal ideal exists, then $A=k$, $\mathfrak{m}=0$, the local ring is a field of dimension zero, and the empty-column Jacobian has rank zero; if $r=0$, the map $L^0\to L^n$ has rank zero and the cokernel calculation in step 3.1 still applies. For one equation in one variable, $A=k[t]\mathrm{/}(t)$ at $(t)$ has local ring $k$, Jacobian $[1]$, and rank $1=n-0$, so it is regular. In contrast, $A=k[t]\mathrm{/}(t^2)$ at $(t)$ has a unique prime $(t)$, local dimension zero, one-dimensional cotangent space $(t)\mathrm{/}(t^2)$, and Jacobian entry $2t=0$ in the residue field (including characteristic two); it is not regular and its rank $0$ does not equal $n-\dim A_{(t)}=1$. The equivalence in steps 1.2 and 4.1 handles both iff directions. At local dimension zero the regularity equality requires full Jacobian rank; when tangent dimension is the ambient dimension $n$, it requires rank zero. No separate dimension-range assertion is used. No minimality of the generator list or reducedness of $I$ entered [F7], and the cokernel's dimension is independent of the chosen list. The general-field rational proof and the perfect-field proof use no choice or DC; AC enters only the classical clause through [F13] and [F14].