Let A —> B be a finitely presented ring map. Then we can write B = A[x_1, …, x_n]/I and we get a two term complex

NL_{B/A} : I/I^2 —> ⨁ B dx_i

given by differentiation. In the stacks project we call this the naive cotangent complex of B over A, see Definition 07BN and Lemma 00S1. We say a ring map A —> B is smooth if it is finitely presented and NL_{B/A} is quasi-isomorphic to a projective module placed in degree 0, see Definition 00T2.

A ring map A —> B is said to be formally smooth if given a surjection C —> C’ of A-algebras with square zero kernel, any A-algebra map from B to C’ can be lifted to an A-algebra map from B to C, see Definition 00TI. A first result on smooth ring maps is that given a finitely presented ring map A —> B we have

A —> B is formally smooth if and only if A —> B is smooth.

See Proposition 00TN. This equivalence means in particular that our definition of smooth ring maps agrees with everybody else’s definition.

A standard smooth ring map is one of the form A —> B = A[x_1, …, x_n]/(f_1, …, f_c) with the matrix of partial derivatives df_j / dx_i for i,j = 1, …, c invertible in B, seeDefinition 00T6. A second result is that

a smooth ring map A —> B is Zariski locally on B standard smooth,

see Lemma 00TA.

A relative global complete intersection is a ring map of the form A —> B = A[x_1, …, x_n]/(f_1, …, f_c) such that the fibre rings have dimension n – c, see Definition 00SP. A third result, see Lemma 00T7, is that

a standard smooth ring map is a relative global complete intersection

The proof of this requires a bit of dimension theory; it is essentially the “Jacobian criterion”.

Lemma 00SV states that

a relative global complete intersection is flat.

You prove this by reducing to the Noetherian case and using the local criterion of flatness.

So far, besides some basic commutative algebra there are only ingredients needed to proceed along the lines above are some dimension theory and the local criterion of flatness.

A final result is Lemma 00TF which states that

a flat finitely presented ring map with smooth fibre rings is smooth.

The current proof of this in the stacks project uses a large amount of technical material including limit techniques to reduce to the Noetherian case and Zariski’s main theorem to bound dimensions in nearby fibres.

Some data regarding the dependency graph of the stacks project (on April 18, 2012).

We think of the bottom of the graph (height 0) as the vertices whose tags correspond to results whose proofs do not refer to any other result. Height 1 is those which refer to a result of height 0. Etc. The maximum height is 78 which is attained by 06RD. The next few are
Height 77 : 06RA 06RF 07BE
Height 76 : 06QK 06R9 06RC 06UF 06UG 07BA
Height 75 : 06QI 06QJ 06UD 06UE 06UI 07B4 07B9
Height 74 : 06MF 06N3 06QH 07B3
Height 73 : 06G3 06QG 077A 0783 07AQ 07B8 07BC
Height 72 : 06MX 06PL 0771
Height 71 : 06MT 06PK 0765 0782 07AP
Height 70 : 06MR 06PJ 075Z 0770 0775
Height 69 : 050B 06FI 076Z 0785

The distribution (number of tags per height for height > 0) looks like this

Go over to read Akhil Mathew’s very nice blog post before reading this one. Then read my comment on his post (which was somehow a bit off topic). My comment was a comment of the type: “Even though in the stacks project we use ZMT to prove such and such, we really don’t need to do this.”

But is that really the case? Let’s take for example Lemma Tag 00U9 which says that any etale ring map is a standard smooth ring map. In other words, if A —> B is smooth, then you can write B = A[x_1, …, x_n]/(f_1, …, f_n) with the Jacobian matrix invertible in B. The current proof of this in the stacks project has the following dependency graph (with ZMT in red).

However, if you look at the proof you see that we use Lemma Tag 00U7 (whose proof for some reason depends on ZMT, but that is another matter). However, we really could replace this by Lemma Tag 07CF whose proof is essentially trivial (and in particular doesn’t use ZMT). If we take out the use of 00U7 the new dependency matrix looks like this
As you can see ZMT isn’t used anymore. Not only that, the graph has become significantly simpler.

It is fun how you can test this kind of shortening of arguments before actually implementing them. I’ll add an update to this post when I’ve actually made the changes to the stacks project.

Update. OK, I’ve changed the proof and in fact it is now much simpler. Here is the the final dependency graph So yeah, the original proof was just ridiculously bad!