Formally smooth map

In algebraic geometry and commutative algebra, a ring homomorphism formula_1 is called formally smooth (from French: "Formellement lisse") if it satisfies the following infinitesimal lifting property: 
Suppose "B" is given the structure of an "A"-algebra via the map "f". Given a commutative "A"-algebra, "C", and a nilpotent ideal formula_2, any "A"-algebra homomorphism formula_3 may be lifted to an "A"-algebra map formula_4. If moreover any such lifting is unique, then "f" is said to be formally étale.
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.
Examples.
Smooth morphisms.
All smooth morphisms formula_5 are equivalent to morphisms locally of finite presentation which are formally smooth. Hence formal smoothness is a slight generalization of smooth morphisms.
Non-example.
One method for detecting formal smoothness of a scheme is using infinitesimal lifting criterion. For example, using the truncation morphism formula_6 the infinitesimal lifting criterion can be described using the commutative squareformula_7where formula_8. For example, ifformula_9 and formula_10then consider the tangent vector at the origin formula_11 given by the ring morphismformula_12sendingformula_13Note because formula_14, this is a valid morphism of commutative rings. Then, since a lifting of this morphism toformula_15is of the formformula_16and formula_17, there cannot be an infinitesimal lift since this is non-zero, hence formula_18 is not formally smooth. This also proves this morphism is not smooth from the equivalence between formally smooth morphisms locally of finite presentation and smooth morphisms.