Formally etale morphism

A morphism of schemes $f\text{\hspace{0.17em}⁣}:X\to S$ (Schemes and morphisms over a base) is formally etale if it is both formally smooth (Formally smooth morphism) and formally unramified (Formally unramified morphism).

Uniqueness of the local lifts. Explicitly, $f$ is formally etale exactly when every commutative $S$-diagram with a square-zero thickening $i\text{\hspace{0.17em}⁣}:T_0\hookrightarrow T$ admits lifts $T\to X$ extending the given $T_0\to X$ Zariski locally on $T$, and any two such local lifts agree on the overlaps of their domains of definition: local existence is formal smoothness, and uniqueness is formal unramifiedness. Consequently the local lifts glue uniquely, by Morphisms of schemes are local on compatible open covers, to a single $S$-morphism $T\to X$ extending the given morphism from $T_0$. Thus for a formally etale morphism every square-zero lifting problem has a unique lift, and the unique lift is obtained by gluing the local ones.

No finite-type, finite-presentation or flatness hypothesis is part of the definition: those enter the notion of an etale morphism of schemes, which is a formally etale morphism that is additionally locally of finite presentation (and flat); the comparison with that finite-presentation notion is made on a later page and is not claimed here.