From this answer I learned that Grothendieck proved the following result.
Theorem. Every formally smooth morphism between locally noetherian schemes is flat.
The book Smoothness, Regularity, and Complete Intersection by Majadas and Rodicio cites the following result.
Theorem. Let $(A,\mathfrak m,K)\to (B,\mathfrak n, L)$ be a local homomorphism of noetherian local rings. Then TFAE.
- $B$ is a formally smooth $A$ algebra for the $\mathfrak n$-adic topology;
- $B$ is a flat $A$-module and the $K$ algebra $B\otimes_AK$ is geometrically regular.
The authors then write:
This result is due to Grothendieck [EGA 0$_{\rm{IV}}$ , (19.7.1)]. His proof is long, though it provides a lot of additional information. He uses this result in proving Cohen’s theorems on the structure of complete noetherian local rings. An alternative proof of (I) was given by M. André [An1], based on André –Quillen homology theory; it thus uses simplicial methods, that are not necessarily familiar to all commutative algebraists. A third proof was given by N. Radu [Ra2], making use of Cohen’s theorems on complete noetherian local rings.
Questions:
- Are there any English references for the proof of Grothendieck or of André?
- What is the conceptual outline of Grothendieck's proof?
André's Homologie des Algèbres Commutatives does not look very geometric to a novice like me and I was hoping perhaps Grothendieck's path was more geometric. I would also like to at least glimpse the big picture of the proof.