Idea behind Grothendieck's proof that formally smooth implies flat?

Question

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.

Answer 1

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

Answer 2

In Matsumura's Commutatuve Ring Theory, you will find the following weaker version of Grothendieck result (Theorem $28.10$):

Let $(A, \mathfrak{m},k)$ be a local ring and $B$ a flat $A$-algebra. Suppose that $B_0 = B \otimes_{A} k$ is $0$-smooth over $k$. Then $B$ is $\mathfrak{m}B$-smooth over $A$.

Matsumura proves it with basic commutative algebra. On the other hand, the geometric translation of Grothendieck's result seems to be rather clear:

let $f : X \longrightarrow Y$ be a morphism of schemes of finite type over a base field $k$. Let $x \in X$. Then $f$ is locally smooth around $x$ if and only if $f$ is locally flat around $x$ and the fiber $f^{-1}(f(x))$ is smooth at $x$ over $k$.

This is proved in Hartschorne as Theorem 10.2, with only elementary methods from commutative algebra. On the other hand I am slightly cheating by saying that the condition:

$B$ is formally smooth $A$-algebra for the $\mathfrak{n}$-adic topology

is translated geometrically into:

$f$ is locally smooth at $x$

But from a geometer's point of view, it's really what it looks like (at least on a formal neighborhood).