SGA 1 introduces formally smooth in a very non-canonical way. The way I usually saw it introduced was through the universal lifting property, i.e., for all $A$-algebra $C$ and all $J\subset C$ nilpotent, every homomorphism $B\to C/J$ lifts to a homomorphism $B\to C$.


Grothendieck defers this definition to section 2, however, and instead spends extensive time treating the definition of formally smooth given by:


Let $u: A\to B$ be a local homomorphism of local rings, and suppose the residue field of $B$ is finite over the residue field of $A$. Then $u$ is formally smooth (or, Grothendieck states, $B$ is formally smooth over $A$) if there exists a locally finite $\hat{A}$-algebra $A'$ which is free over $\hat{A}$ such that the (and I hope I translated the French correctly here) localizations of the semi-local ring $\hat{B}\otimes\_{\hat{A}}A'$ are $A'$-isomorphic to the formal series over $A'$.


I guess this definition is deferred to EGA for more intuition in the footnote, but I was wondering why this helps with our understanding of formally smooth, and how this relates to previous concepts Grothendieck introduced which would help with our understanding (e.g., does it generalize, in some sense, quasi-finite?)



formally smooth definition in SGA 1
I guess you are referring to exposé III in SGA 1. The key point in infinitesimal properties in algebraic geometry is that infinitesimal isomorphism does **not** imply local isomorphism. In other words, an etale map can not be trivialized in small opens because Zariski opens are not small enough. Therefore something smooth that should be "locally an affine space" becomes locally an affine space followed by an etale morphism. This is the "working definition" that it is used in exposé 2, that I recommend you to get some intuition on the meaning of the definition.


That said, Grothendieck wanted a definition that did not involve a finiteness condition. Notice that in EGA IV smooth means "formally smooth + finite presentation". So, what is the nonfinite analog on of an affine space? A ring of formal power series over the completion at a certain point. Now the formal counterpart of *"locally an affine space followed by an etale morphism"* is at the completion of the point "a formal power series after replacing the completed local ring of the point by a flat cover". (Flat cover = finite locally free morphism). I guess you can figure out the analogy now.


The great idea of Grothendieck is that this condition can be expressed in a more compact way as a lifting property of infinitesimal morphisms. With this notion one is not plagued by noetherian hypothesis and it's unnecessary to appeal to the completion along the maximal ideal. In a sense, it is a very conceptual and useful definition and that is the approach taken in EGA IV.


The price one has to pay for this slick way of defining infinitesimal properties is that now the intuition behind smoothness is lost and beginners have to trace their way back to the simple cases to fully grasp the meaning of the definition.


