Smooth over a field implies regular

Lemma 33.25.3. Let $X \to \mathop{\mathrm{Spec}}(k)$ be a smooth morphism where $k$ is a field. Then $X$ is a regular scheme.

Proof. (See also Lemma 33.12.6.) By Algebra, Lemma 10.139.3 every local ring $\mathcal{O}_{X, x}$ is regular. And because $X$ is locally of finite type over $k$ it is locally Noetherian. Hence $X$ is regular by Properties, Lemma 28.9.2. $\square$

Comment #1049 by Lenny Taelman on

Suggested slogan: Smooth over a field implies regular

In your comment you can use Markdown and LaTeX style mathematics (enclose it like $\pi$). A preview option is available if you wish to see how it works out (just click on the eye in the toolbar).