Lemma 10.140.3. Let $k$ be any field. Let $S$ be a finite type $k$-algebra. Let $X = \mathop{\mathrm{Spec}}(S)$. Let $\mathfrak q \subset S$ be a prime corresponding to $x \in X$. The following are equivalent:

1. The $k$-algebra $S$ is smooth at $\mathfrak q$ over $k$.

2. We have $\dim _{\kappa (\mathfrak q)} \Omega _{S/k} \otimes _ S \kappa (\mathfrak q) \leq \dim _ x X$.

3. We have $\dim _{\kappa (\mathfrak q)} \Omega _{S/k} \otimes _ S \kappa (\mathfrak q) = \dim _ x X$.

Moreover, in this case the local ring $S_{\mathfrak q}$ is regular.

Proof. If $S$ is smooth at $\mathfrak q$ over $k$, then there exists a $g \in S$, $g \not\in \mathfrak q$ such that $S_ g$ is standard smooth over $k$, see Lemma 10.137.10. A standard smooth algebra over $k$ has a module of differentials which is free of rank equal to the dimension, see Lemma 10.137.7 (use that a relative global complete intersection over a field has dimension equal to the number of variables minus the number of equations). Thus we see that (1) implies (3). To finish the proof of the lemma it suffices to show that (2) implies (1) and that it implies that $S_{\mathfrak q}$ is regular.

Assume (2). By Nakayama's Lemma 10.20.1 we see that $\Omega _{S/k, \mathfrak q}$ can be generated by $\leq \dim _ x X$ elements. We may replace $S$ by $S_ g$ for some $g \in S$, $g \not\in \mathfrak q$ such that $\Omega _{S/k}$ is generated by at most $\dim _ x X$ elements. Let $K \supset k$ be an algebraically closed field extension such that there exists a $k$-algebra map $\psi : \kappa (\mathfrak q) \to K$. Consider $S_ K = K \otimes _ k S$. Let $\mathfrak m \subset S_ K$ be the maximal ideal corresponding to the surjection

$\xymatrix{ S_ K = K \otimes _ k S \ar[r] & K \otimes _ k \kappa (\mathfrak q) \ar[r]^-{\text{id}_ K \otimes \psi } & K. }$

Note that $\mathfrak m \cap S = \mathfrak q$, in other words $\mathfrak m$ lies over $\mathfrak q$. By Lemma 10.116.6 the dimension of $X_ K = \mathop{\mathrm{Spec}}(S_ K)$ at the point corresponding to $\mathfrak m$ is $\dim _ x X$. By Lemma 10.114.6 this is equal to $\dim ((S_ K)_{\mathfrak m})$. By Lemma 10.131.12 the module of differentials of $S_ K$ over $K$ is the base change of $\Omega _{S/k}$, hence also generated by at most $\dim _ x X = \dim ((S_ K)_{\mathfrak m})$ elements. By Lemma 10.140.2 we see that $S_ K$ is smooth at $\mathfrak m$ over $K$. By Lemma 10.137.18 this implies that $S$ is smooth at $\mathfrak q$ over $k$. This proves (1). Moreover, we know by Lemma 10.140.2 that the local ring $(S_ K)_{\mathfrak m}$ is regular. Since $S_{\mathfrak q} \to (S_ K)_{\mathfrak m}$ is flat we conclude from Lemma 10.110.9 that $S_{\mathfrak q}$ is regular. $\square$

Comment #726 by Keenan Kidwell on

In the proof that (1) implies (3), we know that $\Omega_{S/k}$ is free over $S$ of rank $\dim(S)$. But why is $\dim(S)=\dim_x(X)$? I can't think of an expression for $\dim_x(X)$ that makes this equality clear. We have $\dim_x(X)=\dim(S_\mathfrak{q})+\mathrm{trdeg}_k(k(\mathfrak{q}))=\dim(S_\mathfrak{q})+\dim(S/\mathfrak{q})$, but this can be strictly less than $\dim(S)$ if $S$ is not a domain, right?

Comment #728 by on

OK, I added a remark which hopefully clarifies the logic. I also fixed the other things you pointed out in the other comments. See this commit. Thanks!

Comment #731 by Keenan Kidwell on

I think your remark justifies the equality $\dim(S)=\mathrm{rank}_S(\Omega_{S/k})$, but for the equality $\dim(S)=\dim_x(X)$, which I thought about some more, maybe it should be remarked that global complete intersections over $k$ are equidimensional, and this implies via 00OT (2) that $\dim_x(X)=\dim(S)$.

Comment #732 by on

@#731: Actually, the discussion immediately following Definition 10.135.1 (in Section 10.135) shows that a global complete intersection over a field is equidimensional. The idea of a discussion following a definition is that reader keep this in mind as (s)he is reading the text. Of course, this is kind of impossible with something like the Stacks project, so your criticism is valid and a reference to this discussion would be useful to the reader. Hmm...

... but one of the things the Stacks project does not do well is show the surrounding text for any given tag, especially for definitions and equations. I will put in a bug for the stacks-website project and see if Pieter can come up with something suitable to fix this.

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).