The Stacks project

Proof. In characteristic zero any field extension is separable and hence the equivalence of (1) and (3) follows from Lemma 10.140.5. Also (1) implies (2) by definition of smooth algebras. Assume that $\Omega _{S/k, \mathfrak q}$ is free over $S_{\mathfrak q}$. We are going to use the notation and observations made in the proof of Lemma 10.140.5. So $R = S_{\mathfrak q}$ with maximal ideal $\mathfrak m$ and residue field $\kappa$. Our goal is to prove $R$ is regular.

If $\mathfrak m/\mathfrak m^2 = 0$, then $\mathfrak m = 0$ and $R \cong \kappa$. Hence $R$ is regular and we win.

If $\mathfrak m/ \mathfrak m^2 \not= 0$, then choose any $f \in \mathfrak m$ whose image in $\mathfrak m/ \mathfrak m^2$ is not zero. By Lemma 10.140.4 we see that $\text{d}f$ has nonzero image in $\Omega _{R/k}/\mathfrak m\Omega _{R/k}$. By assumption $\Omega _{R/k} = \Omega _{S/k, \mathfrak q}$ is finite free and hence by Nakayama's Lemma 10.20.1 we see that $\text{d}f$ generates a direct summand. We apply Lemma 10.140.6 to deduce that $f$ is a nonzerodivisor in $R$. Furthermore, by Lemma 10.131.9 we get an exact sequence

This implies that $\Omega _{(R/fR)/k}$ is finite free as well. Hence by induction we see that $R/fR$ is a regular local ring. Since $f \in \mathfrak m$ was a nonzerodivisor we conclude that $R$ is regular, see Lemma 10.106.7. $\square$