f:A\toB
N\subseteqC
B\toC/N
B\toC
Formally smooth maps were defined by Alexander Grothendieck in Éléments de géométrie algébrique IV.
For finitely presented morphisms, formal smoothness is equivalent to usual notion of smoothness.
All smooth morphisms
f:X\toS
One method for detecting formal smoothness of a scheme is using infinitesimal lifting criterion. For example, using the truncation morphism
k[\varepsilon]/(\varepsilon3)\tok[\varepsilon]/(\varepsilon2)
where\begin{matrix} X&\leftarrow&Spec\left(
k[\varepsilon] (\varepsilon2) \right)\\ \downarrow&&\downarrow\\ S&\leftarrow&Spec\left(
k[\varepsilon] (\varepsilon3) \right) \end{matrix}
X,S\inSch/S
then consider the tangent vector at the originandX=Spec\left(
k[x,y] (xy) \right)
Y=Spec(k)
(0,0)\inX(k)
sending
k[x,y] (xy) \to
k[\varepsilon] (\varepsilon2)
Note because\begin{align} x&\mapsto\varepsilon\\ y&\mapsto\varepsilon \end{align}
xy\mapsto\varepsilon2=0
is of the form
Spec\left( k[\varepsilon] (\varepsilon3) \right)\toX
and\begin{align} x&\mapsto\varepsilon+a\varepsilon2\\ y&\mapsto\varepsilon+b\varepsilon2 \end{align}
xy\mapsto\varepsilon2+(a+b)\varepsilon3=\varepsilon2
X\inSch/k