Regular equals smooth over a perfect field

Finite-type affine charts. If $X$ is empty, its local regularity and smoothness conditions are vacuous. Otherwise, by [F1], every point has an affine open neighbourhood $U=\mathrm{Spec}A$ with $A$ of finite type over $k$. By [F2], $A\cong k[t_1,\dots ,t_n]\mathrm{/}I$ for some finite $n\ge 0$ and ideal $I$. We consider all such affine charts, so no simultaneous choice of a chart at every point is made.

Noetherianity of the chart rings. Fix any chart from step 1.1 and write $P=k[t_1,\dots ,t_n]$. Let $J\subseteq A$ be an ideal and let $\tilde{J}$ be its preimage under the quotient map $P\to A$. By [F3], $\tilde{J}$ has a finite generating list in $P$; the images of that list generate $J$ because $P\to A$ is surjective. Thus every ideal of $A$ is finitely generated. By [F4]–[F6], the left regular module of $A$ is Noetherian and $A$ is a Noetherian ring. The zero quotient $A=0$ is also Noetherian (its only ideal is generated by the finite list $[0]$) and is regular vacuously by [F11]; its spectrum is empty. Since these charts cover $X$, [F7] makes $X$ locally Noetherian.

Regularity transfers to each affine chart ring. Assume $X$ is regular and fix $U=\mathrm{Spec}A$ from step 1.1. For any $\mathfrak{p}\in \mathrm{Spec}A$, let $x$ be its point in $X$. The restricted structure sheaf [F8] identifies the stalk on $U$ with ${\mathcal{O}}_{X,x}$, and [F9] identifies it with $A_{\mathfrak{p}}$. Since $X$ is locally Noetherian by step 2.1, [F10] and the regularity hypothesis make $A_{\mathfrak{p}}$ regular local. We have already shown that $A$ is Noetherian, so [F11] gives that $A$ is a regular ring.

Smooth implies regular. Assume $X\to \mathrm{Spec}k$ is smooth. Fix any affine chart $U=\mathrm{Spec}A$. By [F15], each point of $U$ has a neighborhood on which the structure map has a standard smooth presentation; restricting these neighborhoods within $U$ and using [F16] shows that $k\to A$ is locally standard smooth. By [F14], $A$ is geometrically regular over $k$. The finitely generated extension $K=k$ is included in [F12], and the canonical isomorphism $A{\otimes }_{k}k\cong A$ therefore makes $A$ a regular Noetherian ring. By [F11], every $A_{\mathfrak{p}}$ is regular local; [F8]–[F10] identify this with regularity of each corresponding point of $X$. Since $X$ is locally Noetherian by step 2.1, $X$ is regular. This proves the reverse implication.

A regular chart is geometrically regular. Let $U=\mathrm{Spec}A$ be any chart and assume $X$ is regular. Step 3.1 makes $A$ a regular finite-type $k$-algebra. For every finitely generated field extension $K\mathrm{/}k$, [F13] gives that $A{\otimes }_{k}K$ is regular, and [F11] includes Noetherianity in the meaning of regular ring. Hence the defining condition [F12] holds and $A$ is geometrically regular over $k$.

Geometric regularity gives local standard smoothness. By [F14], the structure map $k\to A$ for each chart in step 4.1 is locally standard smooth.

Regular implies smooth. At each point of $X$, take a chart from step 1.1. The local standard-smooth presentations supplied by step 5.1 make the morphism smooth at that point under [F15]. This proves the forward implication at all points, including nonclosed points.

Boundary and nilpotent checks. For $X=\mathrm{Spec}k$, the local ring is $k$, with maximal ideal zero and both dimension and embedding dimension zero, so it is regular by [F19]. The map $k\to k$ has the standard smooth presentation with $n=c=0$ and $g=1$ by [F17], so $X$ is smooth. For $D_k=\mathrm{Spec}(k[ϵ]\mathrm{/}({ϵ}^2))$, the unique prime is $(ϵ)$ because every prime contains the nilpotent $ϵ$ and an element with nonzero constant term is a unit. The ring is two-dimensional over $k$, hence Noetherian; its local dimension is zero, whereas $(ϵ)\mathrm{/}(ϵ{)}^2$ is one-dimensional, so its embedding dimension is one and [F19] shows it is not regular. Consequently it is not geometrically regular, since [F12] includes the extension $K=k$. By [F14] its structure map is not locally standard smooth, and [F15] says it is not smooth. Thus nilpotents are retained, and the theorem does not silently replace $D_k$ by its reduced point. Step 6.1 proves regular $\Rightarrow$ smooth, while step 3.2 proves smooth $\Rightarrow$ regular. AC is used only through the stated suppliers [F13]–[F15]; the proof treats one chart or point at a time, and no DC is invoked. [F12, F13, F14, F15, F17, F18, F19, step 6.1, step 3.2, given, algebra] $\mathrm{\square }$