So I am gearing up to write a bit about Grothendieck’s existence theorem.
Let R be a Noetherian ring complete with respect to an ideal I. Let X be a proper scheme over R. Let O_n = O_X/I^nO_X. Consider an inverse system (F_n) of sheaves on X, such that F_n is a coherent O_n-module and such that the maps F_{n + 1} —> F_n induce isomorphisms F_n = F_{n + 1} ⊗_{O_{n + 1}} O_n. The statement of the theorem is that given any such system there exists a coherent O_X-module F such that F_n ≅ F/I^nF (compatible with transition maps and module structure).
Mike Artin told me Grothendieck was proud of this result.
Because it is all the rage, let’s try to construct F directly from the system via category theory. So consider the functor
G |—-> lim_n Hom_{O_X}(G, F_n)
on QCoh(O_X). Since QCoh(O_X) is a Grothendieck abelian category (see Akhil Mathew’s post) and since this functor transforms colimits into limits, we can apply the folklore result Lemma Tag 07D7. Thus there exists a quasi-coherent sheaf F such that
Hom_{O_X}(G, F) = lim_n Hom_{O_X}(G, F_n)
The existence of F comes for free. (A formula for F is F = Q(lim F_n) where Q is the coherator as in Lemma Tag 077P).
Of course, now the real problem is to show that F is coherent and that F/I^nF = F_n, and I don’t see how proving this is any easier than attacking the original problem. Do you?
This sounds pretty interesting. I just wanted to say that I think the fact that quasi-coherent sheaves form a Grothendieck abelian category is easier than what I wrote in that post. Namely, to give a quasi-coherent sheaf on a scheme $latex X$ is equivalent to giving, for every Zariski affine open $latex \mathrm{Spec} A \to X$, an $latex A$-module, together with coherent isomorphisms between the various modules. In other words it’s the homotopy limit of the categories of modules, and it is a homotopy limit of presentable categories under nice, left-adjoint functors, and hence automatically presentable. Ben-Zvi/Francis/Nadler seem to do something like this.
Completeness of R has to be used somewhere; i.e., you could begin with X proper over an R that’s not complete for I and the “inverse system” viewpoint can’t tell the difference between X and its base change X^ over R^. So it seems impossible to deduce coherence relative to X^ (rather than X) without doing something real (i.e., going beyond abstract nonsense with category theory, which doesn’t really keep track of completeness properties for R, right?).
By the way, Oort told me (some years ago) that Grothendieck was very proud of this result. I always assumed you would have heard it from him too!
Yes, I agree, completeness has to be used somewhere.
Cool, that we know from two sources that Grothendieck was proud of this result. As far as I can remember, I never discussed this with Oort.
A feature of the proof of the Existence Theorem that I have always liked is that (inspired by the proof of GAGA) the crucial use of Ext^1’s and exact sequences requires working with the formal scheme as a genuine ringed space (not just pro-system formalism, as in “elementary” treatments of formal schemes that don’t prove hard theorems about them), since only there can we work in a convenient way with exact sequence arguments. A proof of the Existence Theorem entirely in terms of inverse systems (in the spirit of the viewpoint suggested in the above posting) would seem to have to avoid exact sequence manipulations in F, lest one get caught in a chain of higher Ext’s that spirals out of control. That would be incredible.
Yes. I think there are main points in the proof: (a) deal with exact sequences, and (b) show that there the F from the post above is nonzero if the F_n are nonzero.
Mike made his comment to me while working on the paper “Abstract Hilbert Schemes” with James Zhang. Although they do not use formal schemes as such, the proof in that paper follows Grothendieck; this is a comment they make in the introduction. They use a category of formal objects as a replacement for the category of modules on the formal scheme.
The paper by Hartmann and Harbater (“Patching over fields”) proves a kind of existence theorem over the generic point (eg for a relative curve over a cdvr) in a completely different way.