Definition of formal schemes as formal direct limits

My advisor showed me a definition of formal schemes as follows (acknowledging that these hypotheses may not be minimal): A formal Noetherian scheme is a sequence $$Y_1 \hookrightarrow Y_2 \hookrightarrow Y_4 \hookrightarrow \cdots$$ of closed immersions of Noetherian schemes such that for all $i$,
(a) $(Y_i)_{red} \to (Y_{i+1})_{red}$ is an isomorphism,
(b) $\mathcal{I}_m / \mathcal{I}_m^2 \leftarrow \mathcal{I}_{m+1} / \mathcal{I}_{m+1}^2$ is an isomorphism,
where $\mathcal{I}_m$ is the coherent ideal sheaf on $Y_m$ defining the closed subscheme $Y_1$.

Morphisms from $Y = (Y_n)$ to $Z = (Z_l)$ are then specified as $$\mathrm{Hom}(Y,Z) = \varprojlim_k \varinjlim_l \mathrm{Hom}(Y_k, Z_l).$$ Having specified morphisms, we can determine when two sets of data, even if quite distinct, give isomorphic formal schemes.

According to my advisor, this point of view is quite helpful for understanding certain results and proofs that use formal schemes in a not-entirely-essential way, such as the theorem on formal functions.

Can anyone point out a decent exposition of formal schemes from this point of view? I need to know, at least in a cursory way, about formal schemes (as a category), as well as coherent sheaves, sheaf cohomology, and higher direct images. And completions along a closed subset, of course.

-
That description "works", but I don't think it helps to understand the hard proofs. It's like defining completion of finite module over noetherian ring as inv. system rather than as a module: can make do with inv. system language, and useful (e.g., $\ell$-adic cohom.), but proofs of hard theorems about completion are much easier to understand (& state!) with completion as a module. Likewise, formal schemes are easier to understand and use as (topologically) ringed spaces, not inv. systems, and the proof of thm on formal fns is way more transparent this way. Look at "FGA Explained", Ch. 8. – BCnrd Sep 13 '10 at 19:19
Dear BCnrd, I am not altogether convinced. It is true that when one is dealing with nice modules (f.g. and such) where the topology is determined by the algebraic structure, completeness just comes as a bonus. However, when the topology really matters, working with prosystems seems to me to often be more convenient, working topologically one constantly has to add some topological argument. ML-conditions for instance have nice interpretations in terms of prosystems. – Torsten Ekedahl Sep 13 '10 at 20:19
Dear Torsten: Charles seemed focused on coherent sheaves and theorem on formal fns, hence the viewpoint in my comment. I agree that the Artin-Rees (or M-L) formalism is very convenient, and in topologically complicated setting can be easier. But for "understanding certain results and proofs...such as the theorem on formal functions" (and cousins such as formal GAGA, whose proof uses Ext-sheaves, as you know) it didn't make sense to me why Charles' advisor thinks the prosystems clarify things. Not that the prosystems aren't useful in that setting too, but helpful to understand the proofs?? – BCnrd Sep 13 '10 at 21:44
I think he meant helpful in the sense of making the proofs comprehensible with very little knowledge of formal schemes. – Charles Staats Sep 13 '10 at 23:02
Dear Charles: to learn what thm on formal fns has to do with formal schemes (even though can be stated without formal schemes), why not learn what a formal scheme is while you're at it? I refer back to the example of completions of modules. The deep results that underlie infinitesimal deformation thy are the formal GAGA thms, whose proofs involve treating a formal scheme as an "honest" geometric object, not a prosystem gadget; e.g.,use of Ext-sheaves in the proofs seems more intuitive that way. Lots with formal schemes is clearer without prosystems (e.g., rigid-analytic "generic fibers"). – BCnrd Sep 14 '10 at 0:59