Openness of the regular locus over a perfect field

Setup. Since $X\to \mathrm{Spec}k$ is of finite type it is locally of finite type [F5], so every point of $X$ has an affine open neighbourhood $U=\mathrm{Spec}B$ with the structure map $k\to B$ of finite type, and by [F6] such a $B$ is isomorphic as a $k$-algebra to $k[x_1,\dots ,x_n]\mathrm{/}\mathfrak{a}$ for some $n\ge 0$ and some ideal $\mathfrak{a}$. The polynomial ring $k[x_1,\dots ,x_n]$ is Noetherian by [F7], hence so is its quotient $B$; as the point was arbitrary, $X$ has an affine open cover by spectra of Noetherian rings and is locally Noetherian by [F8]. Consequently the regular locus $X_{\mathrm{r}\mathrm{e}\mathrm{g}}$ is defined by [F3] and the regular-point predicate of [F4] applies to $X$.

Locality of openness. It suffices to prove that every point of $X_{\mathrm{r}\mathrm{e}\mathrm{g}}$ has an open neighbourhood contained in $X_{\mathrm{r}\mathrm{e}\mathrm{g}}$: if that holds, then $X_{\mathrm{r}\mathrm{e}\mathrm{g}}$ is the union of the family of all open subsets of $X$ contained in $X_{\mathrm{r}\mathrm{e}\mathrm{g}}$, and this union is open by (T2) [F12]. The family is specified by a property of its members rather than by a selection, so no choice is used here.

The chart at a regular point. Fix $x\in X_{\mathrm{r}\mathrm{e}\mathrm{g}}$. By [F5] the point $x$ has an affine open neighbourhood $U=\mathrm{Spec}B$ with the structure map $k\to B$ of finite type, and [F6] gives an isomorphism $B\cong k[x_1,\dots ,x_n]\mathrm{/}\mathfrak{a}$ of $k$-algebras for some $n\ge 0$ and some ideal $\mathfrak{a}\subseteq k[x_1,\dots ,x_n]$; this chart is chosen for the single fixed point $x$.

Stalks on the chart and the equivalence. Let $y\in U$ correspond to the prime $\mathfrak{p}\subseteq B$. The open neighbourhoods of $y$ contained in $U$ are cofinal among all open neighbourhoods of $y$ in $X$, because the intersection of any open neighbourhood with the open set $U$ is again an open neighbourhood of $y$ inside $U$; since the structure sheaf of the open subscheme $U$ is the restriction ${\mathcal{O}}_X{\mathrm{\mid }}_U$ [F9], the stalk colimits of [F10] agree on these cofinal systems and give ${\mathcal{O}}_{X,y}\cong {\mathcal{O}}_{U,y}$, while [F11] gives ${\mathcal{O}}_{U,y}\cong B_{\mathfrak{p}}$. It follows that for $y\in U$ one has $y\in X_{\mathrm{r}\mathrm{e}\mathrm{g}}$ if and only if $B_{\mathfrak{p}}$ is a regular local ring, both directions being the definition of $X_{\mathrm{r}\mathrm{e}\mathrm{g}}$ in [F3] together with the regular-point criterion [F4]; hence $X_{\mathrm{r}\mathrm{e}\mathrm{g}}\cap U=\{\mathfrak{p}\in \mathrm{Spec}B:B_{\mathfrak{p}}\text{ is a regular local ring}\}$.

The supplier. The field $k$ is perfect [F2], and $B\cong k[x_1,\dots ,x_n]\mathrm{/}\mathfrak{a}$ with $n\ge 0$ by step 2.1, so clause 3 of [F13] applies with $P=k[x_1,\dots ,x_n]$ and $I=\mathfrak{a}$: the set $\{\mathfrak{p}\in \mathrm{Spec}B:B_{\mathfrak{p}}\text{ is a regular local ring}\}$ is open in $\mathrm{Spec}B$. By step 3.1 this set is $X_{\mathrm{r}\mathrm{e}\mathrm{g}}\cap U$, so $X_{\mathrm{r}\mathrm{e}\mathrm{g}}\cap U$ is open in $U$; since $U$ is open in $X$, such an open subset of $U$ is open in $X$, and $X_{\mathrm{r}\mathrm{e}\mathrm{g}}\cap U$ is an open neighbourhood of $x$ contained in $X_{\mathrm{r}\mathrm{e}\mathrm{g}}$.

Conclusion and boundaries. The point $x\in X_{\mathrm{r}\mathrm{e}\mathrm{g}}$ of step 2.1 was arbitrary, so step 4.1 shows that every point of $X_{\mathrm{r}\mathrm{e}\mathrm{g}}$ has an open neighbourhood contained in $X_{\mathrm{r}\mathrm{e}\mathrm{g}}$, and step 1.2 then makes $X_{\mathrm{r}\mathrm{e}\mathrm{g}}$ open in $X$, which is the assertion. Boundaries. If $X$ is empty then $X_{\mathrm{r}\mathrm{e}\mathrm{g}}=\mathrm{\varnothing }$ is open by (T1) [F12] and the argument is vacuous. If the chart of step 2.1 has $n=0$ then $B\cong k\mathrm{/}\mathfrak{a}$ is a quotient of the field $k$ and clause 3 of [F13] still applies, covering $X=\mathrm{Spec}k$ (one point, whose local ring is the field $k$ and is regular) and $X=\mathrm{Spec}(k[ϵ]\mathrm{/}({ϵ}^2))$ (no regular point). The scheme $X$ may be reducible or nonequidimensional: no purity, irreducibility, or dimension-uniformity input occurs, the supplier being applied chart by chart, and its clause 3 speaks about every point of the spectrum and not only the closed ones, so nonclosed points are covered as well. Nilpotents are retained and no reduction is performed, so the argument does not use reducedness and in fact proves the statement for arbitrary finite-type $k$-schemes over a perfect field. AC is declared as [F1] and enters only through the supplier [F13], which assumes it; the chart of step 2.1 is chosen for one fixed point, and the union of step 1.2 is defined by a property, so no further choice occurs. The statement is not an if-and-only-if assertion; the one equivalence used, the characterization of $X_{\mathrm{r}\mathrm{e}\mathrm{g}}\cap U$ in step 3.1, is proved in both directions.