Add second proof of lemma in algebra

Thanks to Ryo Suzuki
https://stacks.math.columbia.edu/tag/00RR#comment-7704
https://stacks.math.columbia.edu/tag/00RR#comment-7713
https://stacks.math.columbia.edu/tag/00RR#comment-7714

algebra.tex

@@ -33567,7 +33567,9 @@ \section{Differentials}
 To construct the map just use the obvious map
 between the presentations for $\Omega_{S/R}$ and $\Omega_{S'/R'}$.
 Namely,
-$$
+\begin{equation}
+\label{equation-map-presentations}
+\vcenter{
 \xymatrix{
 \bigoplus S'[(a', b')]
 \oplus
@@ -33591,7 +33593,8 @@ \section{Differentials}
 } &
 \bigoplus S[a] \ar[uu]_{[a] \mapsto [\varphi(a)]}
 }
-$$
+}
+\end{equation}
 The result is simply that $f\text{d}g \in \Omega_{S/R}$ is
 mapped to $\varphi(f)\text{d}\varphi(g)$.
 
@@ -33625,10 +33628,9 @@ \section{Differentials}
 (This includes in particular the elements $\text{d}(i)$, $i \in I$.)
 \end{lemma}
 
-\begin{proof}
-We urge the reader to find their own (hopefully different) proof
-of this lemma.
-Consider the map of presentations above. Clearly the right vertical
+\begin{proof}[First proof]
+Consider the map of presentations (\ref{equation-map-presentations}).
+Clearly the right vertical
 map of free modules is surjective. Thus the map is surjective.
 Suppose that some element $\eta$ of $\Omega_{S/R}$ maps to zero in
 $\Omega_{S'/R'}$. Write $\eta$ as the image of $\sum s_i[a_i]$ for some
@@ -33658,6 +33660,43 @@ \section{Differentials}
 $a' = \varphi(a)$ is in the image of $\beta$ and we're done as well.
 \end{proof}
 
+\begin{proof}[Second proof]
+We will use the universal property of modules of differentials
+given in Lemma \ref{lemma-universal-omega} without further mention.
+
+\medskip\noindent
+In (\ref{equation-functorial-omega}) let $R'' = S \times_{S'} R'$.
+Then we have following diagram:
+$$
+\xymatrix{
+S \ar[r] & S \ar[r] & S' \\
+R \ar[r] \ar[u] & R'' \ar[r] \ar[u] & R' \ar[u]
+}
+$$
+Let $M$ be an $S$-module. It follows immediately from the definitions that
+an $R$-derivation $D : S \to M$ is an $R''$-derivation if and only if
+it annihilates the elements in the image of $R'' \to S$. The universal
+property translates this into the statement that the natural map
+$\Omega_{S/R} \to \Omega_{S/R''}$ is surjective with kernel generated
+as an $S$-module by the image of $R''$.
+
+\medskip\noindent
+From the previous paragraph we see that it suffices to show that
+$\Omega_{S/R} \to \Omega_{S'/R'}$ is an isomorphism
+when $S \to S'$ is surjective
+and $R = S \times_{S'} R'$. Let $M'$ be an $S'$-module. Observe that any
+$R'$-derivation $D' : S' \to M'$ gives an $R$-derivation by precomposing
+with $S \to S'$. Conversely, suppose $M$ is an $S$-module and $D : S \to M$
+is an $R$-derivation. If $i \in I$, then there exist an $a \in R$ with
+$\alpha(a) = i$ (as $R = S \times_{S'} R'$). It follows that $D(i) = 0$
+and hence $0 = D(is) = iD(s)$ for all $s \in S$. Thus the image of $D$
+is contained in the submodule $M' \subset M$ of elements annihilated by $I$
+and moreover the induced map $S \to M'$ factors through an $R'$-derivation
+$S' \to M'$. It is an exercise to use the universal property to see that
+this means $\Omega_{S/R} \to \Omega_{S'/R'}$ is an isomorphism; details
+omitted.
+\end{proof}
+
 \begin{lemma}
 \label{lemma-exact-sequence-differentials}
 Let $A \to B \to C$ be ring maps.