The Stacks project

Proof. Let $\text{d}' : S' = S \otimes _ R R' \to \Omega _{S/R} \otimes _ R R'$ denote the map $\text{d}'( \sum a_ i \otimes x_ i ) = \sum \text{d}(a_ i) \otimes x_ i$. It exists because the map $S \times R' \to \Omega _{S/R} \otimes _ R R'$, $(a, x)\mapsto \text{d}a \otimes _ R x$ is $R$-bilinear. This is an $R'$-derivation, as can be verified by a simple computation. We will show that $(\Omega _{S/R} \otimes _ R R', \text{d}')$ satisfies the universal property. Let $D : S' \to M'$ be an $R'$-derivation into an $S'$-module. The composition $S \to S' \to M'$ is an $R$-derivation, hence we get an $S$-linear map $\varphi _ D : \Omega _{S/R} \to M'$. We may tensor this with $R'$ and get the map $\varphi '_ D : \Omega _{S/R} \otimes _ R R' \to M'$, $\varphi '_ D(\eta \otimes x) = x\varphi _ D(\eta )$. It is clear that $D = \varphi '_ D \circ \text{d}'$. $\square$