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
\[ (f)/(f^2) \to \Omega _{R/k} \otimes _ R R/fR \to \Omega _{(R/fR)/k} \to 0 \]
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$
Comments (0)