Smooth density and normal codimension over a perfect field

On each finite-type affine chart $\mathrm{Spec}A$, write $A=k[t_1,\dots ,t_n]\mathrm{/}I$. By [F1], the polynomial ring is noetherian, so $I$ is finitely generated and $A$ is both noetherian and finitely presented over $k$. Thus $X$ is noetherian and its structure morphism is locally finitely presented. By [F2] its smooth locus $U$ is open.

Each irreducible component of a scheme has a generic point $\eta$. By reducedness and [F4], ${\mathcal{O}}_{X,\eta }$ is a field and hence regular local. The pointwise input [F3] therefore gives $\eta \in U$. By [F4], $U\cap C$ is dense open in each component $C$. This also covers the empty scheme vacuously.

Now suppose $X$ normal. By step 1.1 and [F5], its components are open-and-closed integral normal schemes. Fix one component $C$ and a point $x$ of codimension one in it. Choose an affine neighborhood $\mathrm{Spec}A\subset C$ of $x$. The component reduction [F5] makes $A$ a finite product of noetherian integrally closed domains; since its spectrum is a nonempty open subset of the irreducible space $C$, it is irreducible, so there is only one nonzero factor. Thus $A$ is a noetherian integrally closed domain. The prime $\mathfrak{p}$ corresponding to $x$ has height one: chains of primes below $\mathfrak{p}$ correspond to chains of irreducible closed subsets of $C$ ending at $\overline{\{x\}}$, because intersecting with this open neighborhood and taking closures are inverse on such chains. By [F5], ${\mathcal{O}}_{X,x}\cong A_{\mathfrak{p}}$ is a discrete valuation ring and hence regular local.

The generic point of $C$ is smooth by step 2.1, and every codimension-one point is smooth by step 2.2 and [F3]. Hence $C\setminus U$ contains no point of codimension zero or one. Applying [F6] proves its codimension is at least two. AC is used through the explicitly AC-dependent suppliers [F2], [F4] and [F5].