The Stacks project

Proof. If $R \to S$ is formally smooth, then $R' \to S'$ is formally smooth by Lemma 10.138.2. To prove the converse, assume $R' \to S'$ is formally smooth. Note that $N \otimes _ R R' = N \otimes _ S S'$ for any $S$-module $N$. In particular $S \to S'$ is faithfully flat also. Choose a polynomial ring $P = R[\{ x_ i\} _{i \in I}]$ and a surjection of $R$-algebras $P \to S$ with kernel $J$. Note that $P' = P \otimes _ R R'$ is a polynomial algebra over $R'$. Since $R \to R'$ is flat the kernel $J'$ of the surjection $P' \to S'$ is $J \otimes _ R R'$. Hence the split exact sequence (see Lemma 10.138.7)

is the base change via $S \to S'$ of the corresponding sequence

see Lemma 10.131.9. As $S \to S'$ is faithfully flat we conclude two things: (1) this sequence (without ${}'$) is exact too, and (2) $\Omega _{S/R}$ is a projective $S$-module. Namely, $\Omega _{S'/R'}$ is projective as a direct sum of the free module $\Omega _{P'/R'} \otimes _{P'} S'$ and $\Omega _{S/R} \otimes _ S {S'} = \Omega _{S'/R'}$ by what we said above. Thus (2) follows by descent of projectivity through faithfully flat ring maps, see Theorem 10.95.6. Hence the sequence $0 \to J/J^2 \to \Omega _{P/R} \otimes _ P S \to \Omega _{S/R} \to 0$ is exact also and we win by applying Lemma 10.138.7 once more. $\square$