Lemma 10.138.16. Let $R \to S$ be a ring map. Let $R \to R'$ be a faithfully flat ring map. Set $S' = S \otimes _ R R'$. Then $R \to S$ is formally smooth if and only if $R' \to S'$ is formally smooth.

**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$

## Post a comment

Your email address will not be published. Required fields are marked.

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).

Unfortunately JavaScript is disabled in your browser, so the comment preview function will not work.

All contributions are licensed under the GNU Free Documentation License.

## Comments (0)

There are also: