Smoothness over a field by geometric regularity

Finite-type affine charts and the assumption. The structural morphism $X\to \mathrm{Spec}k$ is of finite type, so around each $x\in X$ there is an affine open $U=\mathrm{Spec}A$ with $A$ of finite type over $k$ [F1, F2]. The field-change scheme $X_K$ and its affine restrictions are those of [F8]. AC is carried in the hypotheses of the standard-smooth equivalence [F5], the all-field field-test [F6], and the field-change construction [F8], so it is declared here [F13]. The field-change theorem says its AC use is only to index a pointwise affine cover and that the set of all affine opens also gives a choice-free construction [F8]. The proof below uses one chart at a time and makes no simultaneous choice of charts or local generators.

Smoothness implies regularity after every field change. Assume $X\to \mathrm{Spec}k$ is smooth, fix any extension $K\mathrm{/}k$, and let $z\in X_K$ map to $x\in X$. By [F3], there is an affine neighbourhood $V=\mathrm{Spec}C$ of $x$ on which $k\to C$ is standard smooth at the prime for $x$; shrinking further by a principal open gives $W=\mathrm{Spec}B\subseteq V$ containing $x$ with $B$ standard smooth over $k$. Thus $k\to B$ is locally standard smooth, so [F5] makes $B$ geometrically regular. By [F6], $B{\otimes }_{k}K$ is a regular ring. By [F8], $W_K=\mathrm{Spec}(B{\otimes }_{k}K)$ is an open neighbourhood of $z$ in $X_K$. If $\mathfrak{q}$ is the prime for $z$ in this chart, [F12] identifies its local ring with $(B{\otimes }_{k}K{)}_{\mathfrak{q}}$; this is regular by [F7], and hence the local ring of $z$ is regular in the sense of [F9]. Since $K$ and $z$ were arbitrary, every local ring of every $X_K$ is regular.

Regularity after every field change implies smoothness. Suppose every local ring of $X_K$ is regular for every extension $K\mathrm{/}k$. Fix $x\in X$ and choose a finite-type affine neighbourhood $U=\mathrm{Spec}A$ as in step 1.1. For every finitely generated extension $K\mathrm{/}k$, [F8] identifies $U_K$ with the open subscheme $\mathrm{Spec}(A{\otimes }_{k}K)\subseteq X_K$. All its local rings are regular by hypothesis and [F12], and the ring is Noetherian because it is a finite-type algebra over the field $K$ [F4]. It is therefore regular by [F7]. This holds for every finitely generated $K\mathrm{/}k$, hence $A$ is geometrically regular by [F4]. The equivalence [F5] gives that $k\to A$ is locally standard smooth, in particular standard smooth at the prime for $x$. As this applies at every $x$, [F3] says that $X\to \mathrm{Spec}k$ is smooth. The empty scheme satisfies both conditions vacuously.

Boundary calculations. For $X=\mathrm{Spec}k$, every field change is $\mathrm{Spec}K$ and its only local ring is the field $K$, so the zero-dimensional one-point case is smooth. For the nonreduced point $D_k$ of [F11], the field change has coordinate ring $K[ϵ]\mathrm{/}({ϵ}^2)$: the map $(a+bϵ)\otimes \lambda \mapsto a\lambda +b\lambda ϵ$ is a ring isomorphism with inverse $c+dϵ\mapsto 1\otimes c+ϵ\otimes d$. Every prime contains the nilpotent $ϵ$, and every element with nonzero constant term is a unit, so $(ϵ)$ is the unique prime and maximal ideal. The ring is a two-dimensional $K$-vector space, so its ideals are finite-dimensional $K$-subspaces and it is Noetherian. Its unique local ring has dimension zero, while its maximal ideal has square zero and one-dimensional quotient by its square; it is not regular local by [F10]. Thus the criterion detects the nilpotent structure and correctly says $D_k$ is not smooth. Taking $K=k$ shows the original scheme itself is included among the required field changes; no interval or endpoint parameter occurs.