Ultimately, we are headed towards a characterization of formal smoothness for reasonable morphisms (e.g. the types one encounters in classical algebraic geometry): we want to show that they are precisely the flat morphisms whose fibers are smooth varieties. This will be a much more usable criterion in practice (formal smoothness is given by a somewhat abstract lifting property, but checking that a concrete variety is smooth is much easier). This is the intuition between smoothness: one should think of a flat map is a “continuously varying” family of fibers, and one wishes the fibers to be regular. This corresponds to the fact from differential topology that a submersion has submanifolds as its fibers.
It is actually far from obvious that a formally smooth (and finitely presented) morphism is even flat. Ultimately, the idea of the proof is going to be write the ring as a quotient of a localization of a polynomial ring. The advantage is that this auxiliary ring will be clearly flat, and it will also have fibers that are regular local rings. In a regular local ring, we have a large supply of regular sequences, and the point is that we will be able to lift the regularity of these sequences from the fiber to the full ring.
Thus we shall use the following piece of local algebra.
Theorem Let be a local homomorphism of local noetherian rings. Let be a finitely generated -module, which is flat over .
Let . Then the following are equivalent:
- is flat over and is injective.
- is injective where .
This is a useful criterion of checking when an element is -regular by checking on the fiber. That is, what really matters is that we can deduce the first statement from the second.
Proof: All functors here will be over . If is -flat and is injective, then the sequence
leads to a long exact sequence
But since is flat, it follows that is injective.
The other direction is more subtle. Suppose multiplication by is a monomorphism on . Now write the exact sequence
where are the kernel and cokernel. We can also consider the image , to split this into two exact sequences
Here the map is given by multiplication by , so it is injective by hypothesis. This implies that is injective. So is actually an isomorphism because it is obviously surjective, and we have just seen it is injective. Next, since is surjective, is also injective.
(Given a sequence such that is surjective, is injective, it follows that is itself injective: for if a nonzero mapped to zero in , then is hit by something in , nonzero. Then that would go to zero in , contradiction.)
Let us tensor these two exact sequences with . We get
because is flat. We also get
We’ll start by using the second sequence. Now was just said to be injective, so that . By the local criterion for flatness (Theorem 4.2 in the chapter on flatness in the CRing project), it follows that is a flat -module as well. But , so this gives one part of what we wanted.
Now, we want to show finally that . Now, is flat; indeed, it is the kernel of a surjection of flat maps , so the long exact sequence shows that it is flat. So we have a short exact sequence
which shows now that (as was just shown to be injective earlier). By Nakayama . This implies that is -regular.
Corollary 7 Let be a morphism of noetherian local rings. Suppose is a finitely generated -module, which is flat over .Let . Suppose that is a regular sequence on . Then it is a regular sequence on and, in fact, is flat over .
Proof: This is now clear by induction.