Grothendieck (EGA I 0.7 & 1.10) defined a category of (topologically Noetherian) "formal rings" and a corresponding global category of formal schemes. Roughly, a formal ring is a topological commutative ring $R$ whose topology is $I$-adic for $I\subset R$ an open ideal. Its formal Spec is $Spf(R) : = Spec(R\_{red})$ for $R\_{red}$ the "maximal topologically reduced quotient", equivalently the reduced quotient of $R/I$. In the special case $I=0$ (discrete topology), we get the category of ordinary schemes as a full subcategory of formal schemes.


Given a formal ring $R$, we have a category $Mod(R)$ of suitably nice topological modules; these have a theory of *completed* tensor product and pullback. Again, this globalizes to a category of formal quasicoherent sheaves on a formal scheme.


Now in order to have pushforwards for formal sheaves, we need to allow new topological modules over ordinary rings. The fundamental example is the topological module $k[[t]]$ over $k[t]$ (the pushforward of the constant sheaf on the formal neighborhood of $0$). Since the completed stalk of $k[[t]]$ is zero at all points $0\neq x\in \mathbb{A}^1,$ it makes sense to think of this as a "formal sheaf on $\mathbb{A}^1$ supported at $0$". 


I would like to understand a category of topological coherent sheaves on an ordinary scheme which includes such "formal" objects, and especially a derived category of such objects (I'm particularly interested in a category of "constructible" formal sheaves, which I would define as repeated extensions of pushforwards of coherent sheaves on formal completions of closed subschemes). For some reason, I can't seem to find anyone who has written about this, except for in the very general context of ind-schemes à la Gaitsgory-Rozenblyum. Do people here know of a good source? 



A derived category of formal sheaves
For a start, you have an approach to ind-coherent sheaves and its derived category in


Duality and Flat Base Change on Formal Schemes
*Contemp. Math.* **244** (1999), pp. 3-90.


[On line version, with some corrections incorporated.](http://www.math.purdue.edu/~lipman/papers/formal-duality.pdf)


The theory gets interesting because this derived category contains two subcategories, one of *quasi-coherent torsion* sheaves and another one of complete complexes, where Grothendieck duality takes a specially nice form. These categories turn out to be equivalent, but the equivalence does not respect the inclusion functors.


It might be interesting to point out that the full subcategory of the derived category of complexes with *coherent* homology is contained in the subcategory of complete complexes.


All of this is discussed in the cited paper.


