Kähler differentials of tensor product

You can find the standard proof in every complete treatment of commutative algebra (for example Bourbaki). So let me give another, more conceptual proof using the Yoneda Lemma (which one really cannot avoid; if one tries to, one actually reproves the Yoneda Lemma in a special case).

If $M$ is some $B \otimes_A C$-module, we have $-$ using the universal properties of direct sum, scalar extension and $\Omega^1$ $-$ a natural bijection $$\hom_{B \otimes_A C}(\bigl(\Omega^1_{B/A} \otimes_A C\bigr) \oplus \bigl(B \otimes_A \Omega^1_{C/A}\bigr),M) \cong \mathrm{Der}_A(B,M|_B) \times \mathrm{Der}_A(C,M|_C),$$ which we want to compare with $$\hom_{B \otimes_A C}(\Omega^1_{B \otimes_A C/A},M) \cong \mathrm{Der}_A(B \otimes_A C,M).$$ Given a pair of $A$-derivations $(\delta_1,\delta_2)$ on $B$ resp. $C$, the map $(b,c) \mapsto \delta_1(b) c + \delta_2(c) b$ is $A$-bilinear, hence lifts to an $A$-linear map $\delta : B \otimes_A C \to M$. It is a derivation since $$\delta((b \otimes c)(b' \otimes c'))=\delta(bb' \otimes cc')= \delta_1(bb')c' + \delta_2(cc')bb'$$ $$=(\delta_1(b)b' + \delta_1(b')b)cc' + (\delta_2(c)c' + \delta_2(c')c)bb'$$ $$=(\delta_1(b)c+\delta_2(c)b)(b' \otimes c')+(\delta_1(b')c'+\delta_2(c')b')((b \otimes c)$$ $$=\delta(b \otimes c)(b' \otimes c') + \delta(b' \otimes c')(b \otimes c).$$ Conversely, given a $A$-derivation $\delta: B \otimes_A C \to M$, we may compose with $- \otimes 1 : B \to B \otimes_A C$ and $1 \otimes - : C \to B \otimes_A C$ to optain a pair $(\delta_1,\delta_2)$ as above. These constructions are easily seen to be inverse to each other. For example, given $\delta$, we have $$\delta(b \otimes c) = \delta((b \otimes 1)(1 \otimes c)) = \delta(b \otimes 1)(1 \otimes c) + \delta(1 \otimes c)(b \otimes 1)=\delta_1(b)c + \delta_2(c)b.$$ This shows that $\bigl(\Omega^1_{B/A} \otimes_A C\bigr) \oplus \bigl(B \otimes_A \Omega^1_{C/A}\bigr)$ and $\Omega^1_{B \otimes_A C/A}$ represent the same functors, hence are isomorphic.

Notice that this proof works in quite general situations. In fact, the argument essentially doesn't use any elements and therefore works in arbitrary finitely cocomplete tensor categories; here $A$ is a commutative algebra object and $B,C$ are commutative $A$-algebras. Another corollary is $\mathrm{pr}_1^* \Omega^1_{X/S} \oplus \mathrm{pr}_2^* \Omega^1_{Y/S} \cong \Omega^1_{X \times_S Y / S}$ for $S$-schemes $X,Y$.