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!