Let me try again to find a tweak to the proof of Grothendieck’s existence theorem.

Let X be a Noetherian scheme, Z ⊂ X a closed subscheme, and U ⊂ X the complement. Denote X’ the completion of X along Z (this is a formal scheme). Suppose that we have a triple (F, G, a) where F is a coherent O_X-module, G is a coherent O_{X’}-module, and a : F’ —> G is a map of the completion F’ of F along Z to G whose kernel and cokernel are annihilated by a power of the ideal sheaf of Z. Then there exists a unique coherent O_X-module H with H’ = G and a map F –> H which produces a on completion along Z. This follows from the results on formal glueing which we discussed in this blog post, although this particular statement is a bit easier to prove.

Suppose now that X —> Spec(R) is a proper morphism of schemes with R a Noetherian ring complete wrt an ideal I. Let G be a coherent module on the completion of X along the ideal IO_X. We want to show that G is the completion of a coherent module on X. By Noetherian induction we may assume this is the case whenever G is supported on a proper closed subscheme of X. Chow’s lemma gives U ⊂ X an dense open subscheme and f : Y —> X a U-admissible blowup such that Y is projective over R. By the projective case (which is “easy”) we know that f^*G is the completion of a coherent module H on Y. Let J ⊂ O_X be a quasi-coherent ideal sheaf with Z = V(J) = X – U. Let X’ be the completion of X along Z. By our induction hypotheses the modules G/J^mG are I-adic completions of coherent O_X/J^m modules E_m. The system E_m gives rise to a coherent module E on X’. Then for some n > 0 we obtain a triple (J^nf_*H, E, a) for some map a (this is actually part of Grothendieck’s proof). Applying the result of the previous paragraph we obtain a coherent module F on X. I think it is pretty clear that the completion of F gives G as desired.

What I like about this argument is that it avoids dealing with extensions of formal modules. Note however, that one of the steps of the proof of formal glueing is an Ext computation, so we are not actually avoiding this issue altogether.

Update 10/12/12: Yesterday I finished adding this material to the stacks project. The proof in the projective case is short and sweet, see Section Tag 087V. The proof for the general case is in Section Tag 0886. The exposition avoids working with formal schemes (because it would take several hundred pages to introduce them) and instead consistently works with certain systems of coherent modules. This also has the advantage that the exact same arguments will work in the setting of algebraic spaces (and possibly algebraic stacks).