This is the third in a three-part post about a proof that I contributed to the Stacks project. The result was already there, but I found a slightly easier proof. The proof is given in my previous post. In this post, I will present the application that caused me to look at the result in the first place.
Remark. Recall that a morphism of schemes is smooth of relative dimension if all of the following hold:
- is locally of finite presentation;
- is flat;
- all nonempty fibres have dimension ;
- is locally free of rank .
If is smooth of relative dimension 0, then is étale. In this case, the third condition follows from the other ones.
Example. To show that the third condition is really necessary, consider any finite inseparable field extension. This is clearly flat of finite presentation. Moreover, is a vector space of dimension , with basis given by a -basis of . Yet the (unique) fibre has dimension 0.
Definition. Let be a scheme of prime characteristic . Then the absolute Frobenius on is given by the morphism which is the identity on the underlying topological space, and is given by on . This definition makes sense because for a ring of characteristic , the Frobenius induces the identity on .
Definition. Suppose that is a morphism of schemes of characteristic . Then the absolute Frobenius factors through , and therefore induces a morphism in the following diagram
where the square is a pullback (i.e. , where is viewed as an -scheme along ). The morphism is called the relative Frobenius of over .
Lemma. Assume is étale, with a scheme of characteristic . Then is an isomorphism. In other words, the square
is a pullback.
Proof. Note that is universally bijective, hence so is . Similarly, is universally bijective. Therefore so is , since .
On the other hand, is étale, hence by base change so is . But any map between schemes étale over is étale (see Tag 02GW, or for a nice geometric proof taken from Milne’s book on étale cohomology, see Corollary 1.1.9 of my Master’s Thesis), so in particular is étale.
Now is étale and universally bijective, so the result follows from my previous post.
Remark. Recall (see Tag 054L) that if is smooth of relative dimension , then around every there exist ‘smooth coordinates’ in the following sense: there exist affine opens , with , such that factors as
where is étale. In particular, this forces , by the first fundamental exact sequence.
Corollary. Assume is smooth of relative dimension , with a scheme of characteristic . Then is locally free of rank .
Proof. The question is local on both and . By the remark above, we may assume is étale over , with both and affine. We have a diagram
where the horizontal compositions are the absolute Frobenii on and respectively. Here, denotes the unique map making the top right square commutative. (Exercise: use the various universal properties to show that the top left square commutes).
The bottom right square and the right large rectangle are pullback squares, hence so is the top right square. The top large rectangle is a pullback by the lemma above. Hence, since the top right square is a pullback, so is the top left square. Hence, it suffices to prove the case , since the result is stable under base change.
But in this case, if , then , and , with the relative Frobenius given by the -linear (!) map
But in this case the result is clear: an explicit basis is
thank you for posting this lemma. An important consequence of it is that for a Deligne-Mumford stack locally of finite type over S the relative Frobenius is finite. Namely by your lemma this holds over an étale presentation of the stack. I suggest to add this result to the stacks project. Would you like to take care of this?
Thanks for your comment. I am not personally very involved with the Stacks project. But you can always ask Johan de Jong to include it (or even send him a draft that he can incorporate in the Stacks project).