Lemma 10.138.2. Let $R \to S$ be a formally smooth ring map. Let $R \to R'$ be any ring map. Then the base change $S' = R' \otimes _ R S$ is formally smooth over $R'$.

Proof. Let a solid diagram

$\xymatrix{ S \ar[r] \ar@{-->}[rrd] & R' \otimes _ R S \ar[r] \ar@{-->}[rd] & A/I \\ R \ar[u] \ar[r] & R' \ar[r] \ar[u] & A \ar[u] }$

as in Definition 10.138.1 be given. By assumption the longer dotted arrow exists. By the universal property of tensor product we obtain the shorter dotted arrow. $\square$

In your comment you can use Markdown and LaTeX style mathematics (enclose it like $\pi$). A preview option is available if you wish to see how it works out (just click on the eye in the toolbar).