The Stacks project

Proof. The implications (1) $\Rightarrow $ (2), (1) $\Rightarrow $ (3), and (2) $\Rightarrow $ (4) follow from Lemma 37.11.5. The implication (3) $\Rightarrow $ (4) is immediate.

Assume (4). The proof that $f$ is formally smooth is the same as the second part of the proof of Lemma 37.11.7. Consider a solid commutative diagram

as in Definition 37.11.1. We will show the dotted arrow exists thereby proving that $f$ is formally smooth. Let $\mathcal{F}$ be the sheaf of sets on $T'$ of Lemma 37.9.4 as in the special case discussed in Remark 37.9.6. Let

be the sheaf of $\mathcal{O}_ T$-modules on $T$ with action $\mathcal{H} \times \mathcal{F} \to \mathcal{F}$ as in Lemma 37.9.5. The action $\mathcal{H} \times \mathcal{F} \to \mathcal{F}$ turns $\mathcal{F}$ into a pseudo $\mathcal{H}$-torsor, see Cohomology, Definition 20.4.1. Our goal is to show that $\mathcal{F}$ is a trivial $\mathcal{H}$-torsor. There are two steps: (I) To show that $\mathcal{F}$ is a torsor we have to show that $\mathcal{F}$ locally has a section. (II) To show that $\mathcal{F}$ is the trivial torsor it suffices to show that $H^1(T, \mathcal{H}) = 0$, see Cohomology, Lemma 20.4.3.

First we prove (I). To see this, for every $t \in T$ we can choose an affine open $W \subset T$ neighbourhood of $t$ such that $a(W)$ is contained in $U_{ji}$ for some $i, j$. Let $W' \subset T'$ be the corresponding open subscheme. By assumption (4) we can lift $a|_ W : W \to U_{ji}$ to a $V_ j$-morphism $a' : W' \to U_{ji}$ showing that $\mathcal{F}(W')$ is nonempty.

Finally we prove (II). By Lemma 37.11.8 we see that $\Omega _{U_{ji}/V_ j}$ locally projective. Hence $\Omega _{X/Y}$ is locally projective, see Properties, Lemma 28.21.2. Hence $a^*\Omega _{X/Y}$ is locally projective, see Properties, Lemma 28.21.3. Hence

by Lemma 37.11.9 as desired. $\square$