Second proof of Lemma 00RW

Thanks to Jeroen Sijsling
http://stacks.math.columbia.edu/tag/00RW#comment-1694

CONTRIBUTORS

@@ -163,6 +163,7 @@ Michele Serra
 Chung-chieh Shan
 Liran Shaul
 Minseon Shin
+Jeroen Sijsling
 Thomas Smith
 Tanya Kaushal Srivastava
 Jason Starr

algebra.tex

@@ -32038,7 +32038,33 @@ \section{Differentials}
 $a \text{d} b \mapsto a \otimes b - ab \otimes 1$.
 \end{lemma}
 
-\begin{proof}
+\begin{proof}[First proof]
+Apply Lemma \ref{lemma-differential-seq-split} to the commutative diagram
+$$
+\xymatrix{
+S \otimes_R S \ar[r] & S \\
+S \ar[r] \ar[u] & S \ar[u]
+}
+$$
+where the left vertical arrow is $a \mapsto a \otimes 1$. We get the
+exact sequence
+$0 \to J/J^2 \to
+\Omega_{S \otimes_R S/S} \otimes_{S \otimes_R S} S \to \Omega_{S/S} \to 0$.
+By Lemma \ref{lemma-trivial-differential-surjective}
+the term $\Omega_{S/S}$ is $0$, and we obtain an
+isomorphism between the other two terms. We have
+$\Omega_{S \otimes_R S/S} = \Omega_{S/R} \otimes_S (S \otimes_R S)$
+by Lemma \ref{lemma-differentials-base-change} as $S \to S \otimes_R S$
+is the base change of $R \to S$ and hence
+$$
+\Omega_{S \otimes_R S/S} \otimes_{S \otimes_R S} S =
+\Omega_{S/R} \otimes_S (S \otimes_R S) \otimes_{S \otimes_R S} S =
+\Omega_{S/R}
+$$
+We omit the verification that the map is given by the rule of the lemma.
+\end{proof}
+
+\begin{proof}[Second proof]
 First we show that the rule $a \text{d} b \mapsto a \otimes b - ab \otimes 1$
 is well defined. In order to do this we have to show
 that $\text{d}r$ and $a\text{d}b + b \text{d}a - d(ab)$ map to zero.