[Math] Idea behind Grothendieck’s proof that formally smooth implies flat

ac.commutative-algebraag.algebraic-geometryflatnessreference-requestschemes

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:

  1. Are there any English references for the proof of Grothendieck or of André?
  2. 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.

Best Answer

You have a very short proof by Jesús Conde in the paper

A short proof of smooth implies flat. Comm. Algebra 45 (2017), no. 2, 774–775.

https://doi.org/10.1080/00927872.2016.1175461

see, alternatively, https://arxiv.org/abs/1504.05709

Related Question