The Stacks project

Proof. Assume $S$ is formally smooth over $R$. By Lemma 10.138.5 this means there exists an $R$-algebra map $S \to P/J^2$ which is a right inverse to the canonical map $P/J^2 \to S$. By Lemma 10.131.11 we have $\Omega _{P/R} \otimes _ P S = \Omega _{(P/J^2)/R} \otimes _{P/J^2} S$. By Lemma 10.131.10 the sequence is split.

Assume the exact sequence of the lemma is split exact. Choose a splitting $\sigma : \Omega _{S/R} \to \Omega _{P/R} \otimes _ P S$. For each $\lambda \in S$ choose $x_\lambda \in P$ which maps to $\lambda $. Next, for each $\lambda \in S$ choose $f_\lambda \in J$ such that

in the middle term of the exact sequence. We claim that $s : \lambda \mapsto x_\lambda - f_\lambda \mod J^2$ is an $R$-algebra homomorphism $s : S \to P/J^2$. To prove this we will repeatedly use that if $h \in J$ and $\text{d}h = 0$ in $\Omega _{P/R} \otimes _ R S$, then $h \in J^2$. Let $\lambda , \mu \in S$. Then $\sigma (\text{d}\lambda + \text{d}\mu - \text{d}(\lambda + \mu )) = 0$. This implies

which means that $x_\lambda + x_\mu - x_{\lambda + \mu } - f_\lambda - f_\mu + f_{\lambda + \mu } \in J^2$, which in turn means that $s(\lambda ) + s(\mu ) = s(\lambda + \mu )$. Similarly, we have $\sigma (\lambda \text{d}\mu + \mu \text{d}\lambda - \text{d}\lambda \mu ) = 0$ which implies that

in the middle term of the exact sequence. Moreover we have

in the middle term again. Combined these equations mean that $x_\lambda x_\mu - x_{\lambda \mu } - \mu f_\lambda - \lambda f_\mu + f_{\lambda \mu } \in J^2$, hence $(x_\lambda - f_\lambda )(x_\mu - f_\mu ) - (x_{\lambda \mu } - f_{\lambda \mu }) \in J^2$ as $f_\lambda f_\mu \in J^2$, which means that $s(\lambda )s(\mu ) = s(\lambda \mu )$. If $\lambda \in R$, then $\text{d}\lambda = 0$ and we see that $\text{d}f_\lambda = \text{d}x_\lambda $, hence $\lambda - x_\lambda + f_\lambda \in J^2$ and hence $s(\lambda ) = \lambda $ as desired. At this point we can apply Lemma 10.138.5 to conclude that $S/R$ is formally smooth. $\square$