Much improved proof of Tag 00TR

Thanks to Maxim Mornev
http://stacks.math.columbia.edu/tag/00TR#comment-1212

CONTRIBUTORS

@@ -97,6 +97,7 @@ Florent Martin
 Akhil Mathew
 Daniel Miller
 Yogesh More
+Maxim Mornev
 Yusuf Mustopa
 David Mykytyn
 Josh Nichols-Barrer

algebra.tex

@@ -34428,51 +34428,20 @@ \section{Smooth algebras over fields}
 \end{lemma}
 
 \begin{proof}
-Since $k$ is algebraically closed we have $\kappa(\mathfrak m) = k$.
-We may choose a presentation
-$0 \to I \to k[x_1, \ldots, x_n] \to S \to 0$ such that
-all $x_i$ end up in $\mathfrak m$. Write $I = (f_1, \ldots, f_m)$.
-Note that each $f_i$ is contained in $(x_1, \ldots, x_n)$, i.e., each
-$f_i$ has zero constant term. Hence we may write
-$$
-f_j = \sum a_{ij} x_i + \text{h.o.t.}
-$$
-By Lemma \ref{lemma-differential-seq} there is an exact sequence
-$$
-\bigoplus S \cdot f_j
-\to
-\bigoplus S \cdot \text{d}x_i
-\to
-\Omega_{S/k}
-\to
-0.
-$$
-Tensoring with $\kappa(\mathfrak m) = k$ we get
-an exact sequence
-$$
-\bigoplus k \cdot f_j
-\to
-\bigoplus k \cdot \text{d}x_i
-\to
-\Omega_{S/k} \otimes \kappa(\mathfrak m)
-\to
-0.
-$$
-The matrix of the map is given by the partial derivatives of
-the $f_j$ evaluated at $0$. In other words by the matrix $(a_{ij})$.
-Similarly there is a short exact sequence
+Consider the exact sequence
 $$
-(f_1, \ldots, f_m)/(x_1 f_1, \ldots, x_n f_m)
-\to
-(x_1, \ldots, x_n)/(x_1, \ldots, x_n)^2
-\to
-\mathfrak m/\mathfrak m^2
-\to
-0.
+\mathfrak m/\mathfrak m^2 \to
+\Omega_{S/k} \otimes_S \kappa(\mathfrak m) \to
+\Omega_{\kappa(\mathfrak m)/k} \to 0
 $$
-Note that the first map is given by expanding the $f_j$
-in terms of the $x_i$, i.e., by the same matrix $(a_{ij})$.
-Hence the two numbers are the same.
+of Lemma \ref{lemma-differential-seq}. We would like to show that the
+first map is an isomorphism. Since $k$ is algebraically closed the
+composition $k \to \kappa(\mathfrak m)$ is an isomorphism by
+Theorem \ref{theorem-nullstellensatz}.
+So the surjection $S \to \kappa(\mathfrak m)$ splits as a map of
+$k$-algebras, and Lemma \ref{lemma-differential-seq-split} shows
+that the sequence above is exact
+on the left. Since $\Omega_{\kappa(\mathfrak m)/k} = 0$, we win.
 \end{proof}
 
 \begin{lemma}