Formal unramifiedness iff Omega vanishes

Assume ${\mathrm{\Omega }}_{X\mathrm{/}S}=0$; we show that lifts are unique. Let $i\text{\hspace{0.17em}⁣}:T_0\hookrightarrow T$ be a square-zero thickening over $S$ and let $a_0\text{\hspace{0.17em}⁣}:T_0\to X$ be an $S$-morphism with two $S$-morphism lifts $a,b\text{\hspace{0.17em}⁣}:T\to X$. Since $a$ and $b$ have the same underlying map on points, the direct images $a_{\ast }{\mathcal{O}}_T$ and $b_{\ast }{\mathcal{O}}_T$ are the same sheaf of rings $\mathcal{F}={\mathcal{O}}_T$ pushed forward along this common map, and both $a^{\mathrm{♯}}$ and $b^{\mathrm{♯}}$ are maps ${\mathcal{O}}_X\to \mathcal{F}$; the difference $\delta :=b^{\mathrm{♯}}-a^{\mathrm{♯}}$ is a morphism of sheaves of abelian groups valued in $\mathcal{G}:=a_{\ast }\mathcal{I}$, where $\mathcal{I}=\ker ({\mathcal{O}}_T\to i_{\ast }{\mathcal{O}}_{T_0})$, because $a$ and $b$ agree on $T_0$ after composition with ${\mathcal{O}}_T\to i_{\ast }{\mathcal{O}}_{T_0}$. The sheaf $\mathcal{G}$ is an ${\mathcal{O}}_X$-module through $a^{\mathrm{♯}}$, and $\delta$ is an $S$-derivation: it is additive, and for local sections $x,y$ of ${\mathcal{O}}_X$ one has $\delta (xy)=b^{\mathrm{♯}}(x)\delta (y)+\delta (x)a^{\mathrm{♯}}(y)=a^{\mathrm{♯}}(x)\delta (y)+a^{\mathrm{♯}}(y)\delta (x)$, since $b^{\mathrm{♯}}(x)-a^{\mathrm{♯}}(x)\in \mathcal{G}$ and ${\mathcal{G}}^2\subseteq a_{\ast }{\mathcal{I}}^2=0$. It kills the image of ${\mathcal{O}}_S$ because $a$ and $b$ are $S$-morphisms. By [F3] with $\mathcal{G}$ and ${\mathrm{\Omega }}_{X\mathrm{/}S}=0$, ${\mathrm{Der}}_S({\mathcal{O}}_X,\mathcal{G})={\mathrm{Hom}}_{{\mathcal{O}}_X}(0,\mathcal{G})=0$, so $\delta =0$, that is $b^{\mathrm{♯}}=a^{\mathrm{♯}}$; by [F6] $a=b$. Hence $f$ is formally unramified.

Assume $f$ formally unramified; we show ${\mathrm{\Omega }}_{B\mathrm{/}A}=0$ on every affine chart. Let $U=\mathrm{Spec}B\subseteq X$ be affine over an affine open $V=\mathrm{Spec}A\subseteq S$, put $B^{\mathrm{\prime }}=(B{\otimes }_{A}B)\mathrm{/}{J}^2$ with $J=\ker (B{\otimes }_{A}B\to B)$, and let $q\text{\hspace{0.17em}⁣}:B^{\mathrm{\prime }}\to B$ be the quotient. The ideal $J\mathrm{/}{J}^2=\ker q$ has square zero, so $\mathrm{Spec}B\to \mathrm{Spec}{B}^{\mathrm{\prime }}$ is a square-zero thickening over $A$; the two $A$-algebra maps $p_1(b)=b\otimes 1$ and $p_2(b)=1\otimes b$ from $B$ to $B^{\mathrm{\prime }}$ both compose with $q$ to the identity, so the $S$-morphisms $c_i\text{\hspace{0.17em}⁣}:\mathrm{Spec}{B}^{\mathrm{\prime }}\to \mathrm{Spec}B\hookrightarrow X$ induced by $p_i$ agree on $\mathrm{Spec}B$. By [F1] applied to this thickening, $c_1=c_2$, and therefore the maps on global sections agree: $p_1=p_2$. Hence $b\otimes 1=1\otimes b$ in $B^{\mathrm{\prime }}$ for all $b\in B$, that is $J\mathrm{/}{J}^2=0$, and [F2] gives ${\mathrm{\Omega }}_{B\mathrm{/}A}=0$.

Conclusion. Step 1.1 proves that ${\mathrm{\Omega }}_{X\mathrm{/}S}=0$ implies that $f$ is formally unramified and step 1.2 that a formally unramified $f$ has ${\mathrm{\Omega }}_{B\mathrm{/}A}=0$ on every affine chart, hence ${\mathrm{\Omega }}_{X\mathrm{/}S}=0$ by [F4]. This proves the equivalence; nowhere were finiteness, flatness or separatedness used, and no lift was constructed, only used for uniqueness in step 1.1.