The Stacks project

Proof. We are going to use the construction of $B'$ from the proof of Lemma 10.149.1 although in principle it should be possible to deduce these results formally from the definition. Namely, we choose a presentation $B = P/J$, where $P = A[x_ i]$ is a polynomial ring over $A$. Next, we choose elements $f_ i \in J$ such that $\text{d}f_ i = \text{d}x_ i \otimes 1$ in $\Omega _{P/A} \otimes _ P B$. Having made these choices we have $B' = P/J'$ with $J' = (f_ i) + J^2$, see proof of Lemma 10.149.1.

Consider the canonical exact sequence

see Lemma 10.131.9. By construction the classes of the $f_ i \in J'$ map to elements of the module $\Omega _{P/A} \otimes _ P B'$ which generate it modulo $J'/J^2$ by construction. Since $J'/J^2$ is a nilpotent ideal, we see that these elements generate the module altogether (by Nakayama's Lemma 10.20.1). This proves that $\Omega _{B'/A} = 0$ and hence that $B'$ is formally unramified over $A$, see Lemma 10.148.2.

Since $P$ is a polynomial ring over $A$ we have $\Omega _{P/R} = \Omega _{A/R} \otimes _ A P \oplus \bigoplus P\text{d}x_ i$. We are going to use this decomposition. Consider the following exact sequence

see Lemma 10.131.9. We may tensor this with $B$ and obtain the exact sequence

If we remember that $J' = (f_ i) + J^2$ then we see that the first arrow annihilates the submodule $J^2/(J')^2$. In terms of the direct sum decomposition $\Omega _{P/R} \otimes _ P B = \Omega _{A/R} \otimes _ A B \oplus \bigoplus B\text{d}x_ i $ given we see that the submodule $(f_ i)/(J')^2 \otimes _{B'} B$ maps isomorphically onto the summand $\bigoplus B\text{d}x_ i$. Hence what is left of this exact sequence is an isomorphism $\Omega _{A/R} \otimes _ A B \to \Omega _{B'/R} \otimes _{B'} B$ as desired. $\square$