Formal Schemes Mittag Leffler Here is a question that I'm just copying from Math Stack Exchange that I asked awhile ago. It has just been sitting there unanswered, and although I haven't really thought about it since I posted it, I'm still very interested in a nice example if it exists.
Suppose $(\mathfrak{X}, \mathcal{O}_\mathfrak{X})$ is a Noetherian formal scheme and let $\mathcal{I}$ be an ideal of definition. Then we have a system of schemes $X_n=(|\mathfrak{X}|, \mathcal{O}_\mathfrak{X}/\mathcal{I}^n)$.
If the inverse system $\Gamma (X_n, \mathcal{O}_{X_n})\to \Gamma (X_{n-1},\mathcal{O}_{X_{n-1}})$ satisfies the Mittag-Leffler condition (the images eventually stabilize), then we get some particularly nice properties such as $Pic(\mathfrak{X})=\lim Pic(X_n)$. 
More generally, we don't have to be worried about converting between thinking about coherent sheaves on the formal scheme and thinking about them as compatible systems of coherent sheaves on actual schemes.
My question:
Is there a known example of a formal scheme for which that system of global sections does not satisfy the Mittag-Leffler condition? 
One thing to note is that it can't be affine (the maps are all surjective) or projective (finite dimensionality forces the images to stabilize). 
A subquestion is whether or not there is a general reason to believe such an example exists. People I talk to usually say things along the lines of: you definitely have to be careful here because in principle this could happen. But no one seems to have ever thought up an example.
Lastly (still related...I think), is there a known example where you can't think of coherent (or maybe invertible) sheaves as systems because the two aren't the same?
 A: It would take me too much effort to understand and write up the things below in algebraic geometry language because I am from analysis -- but this is where the Mittag-Leffler condition comes from and, originally, it is a broader condition than the one I have seen in books on homological algebra where it is required that the images of an inverse (or projective) spectrum stabilize in the sense that $f_m^n(X_m)=f_k^n(X_k)$ for all $k\ge m$ and $m=m(n)$ sufficiently large (here $f_m^n: X_m \to X_n$ are the linking maps of the inverse spectrum).
This condition is sufficient but not necessary for the vanishing of the derived inverse limit functor (and I suspect that this is very close to what you are interested in). Palamodov constructed this derivative by using injective resolutions but for spectra of abelian groups you can define it ad hoc as the cokernel of the map $\prod X_n \to \prod X_n$, $(x_n)_n \mapsto (x_n- f_{n+1}^n(x_{n+1}))_n$.
In Analysis, the $X_n$ are often complete metric groups and the sufficient condition we use is that $f_m^n(X_m)$ is contained in the closure of $f_k^n(X_k)$ (only for the discrete topologies this coincides with the "algebraic ML-condition). If $X_n$ are even locally convex Frechet spaces than we even have a characacterization for vanishing of the derived inverse limit functor: For every $n$ and every continuous seminorm $p$ on $X_n$ we have that $f_m^n(X_m)$ is contained in the closure of $f_k^n(X_k)$ with respect to $p$.
The situation where Mittag-Leffler originally used such ideas is for an exhaustion of an open set $\Omega\subseteq \mathbb C$ by open and relatively compact sets $\Omega_n$ 
 and $X_n=H(\Omega_n)$, the space of holomorphic functions on $\Omega$ with the topology of uniform convergence on compact sets. Runge's approximation theorem then implies that the "analytic ML-condition" is satisfied whereas the algebraic is not.
A: I construct below an example of a formal scheme where the ML condition is violated on the structure sheaf. In fact, the example is the formal completion of a (quasi-projective) $3$-fold along a Cartier divisor. It seems possible that there could also be a $2$-dimensional example.

Choose a smooth projective curve $C$ over a field $k$, an ample line bundle $A$ on $C$ that admits a non-zero global section $f \in H^0(C,A)$, and an anti-ample line bundle $L$ on $C$. Let $X := \underline{\mathrm{Spec}}(\oplus_{i,j \in \mathbb{Z}} L^i \otimes A^j)$ be the displayed $3$-fold, where the multiplicative structure is the obvious one. One may view $X$ as a $(\mathbf{G}_m \times \mathbf{G}_m)$-torsor over $C$. 
We record an elementary vanishing first.
Claim 1: The map $H^1(C,L^i \otimes A^j) \to H^1(C,L^i \otimes A^{j+n})$ induced by $f^n$ is surjective.
Proof: The map of sheaves $L^i \otimes A^j \to L^i \otimes A^{j+n}$ has a cokernel supported at a finite set of points, and thus has no $H^1$.
The chosen section $f$ also defines a section $f \in H^0(X,O_X)$ which is a non-zero divisor. Then:
Claim 2: Any $\alpha \in H^1(X,O_X)$ is annihilated by a power of $f$.
Proof: For fixed $i,j$ and $n \gg 0$, the map $H^1(C,L^i \otimes A^j) \to H^1(C,L^i \otimes A^{j+n})$ is $0$ as the target is $0$ by ampleness. The claim now follows from the identification $H^1(X,O_X) = \oplus_{i,j} H^1(C,L^i \otimes A^j)$.
Now we construct the formal scheme. Let $X_n \subset X$ be the Cartier divisor cut out by $f^{n+1}$, and let $\widehat{X}$ be the formal completion of $X$ along $X_0$. Then:
Claim 3: The projective system $\{ H^0(X_n,O_{X_n}) \}$ has a non-zero $R^1 \lim$. In particular, it fails the ML condition.
Proof: As $f$ is a non-zero divisor on $X$, there is an exact sequence
$1 \to H^0(X,O_X)/f^n \to H^0(X_n,O_{X_n}) \to H^1(X,O_X)[f^n] \to 1.$
As $n$ varies, this gives a projective system of exact sequences. The first term has surjective transition maps, so is acyclic for $\lim$. As $R\lim$ has cohomological dimension $1$, it is enough to show that $\lim_n H^1(X,O_X)[f^n] \neq 0$. For this, it is enough to demonstrate a single non-zero element $\alpha \in H^1(X,O_X)$ satisfying (a) $f^n \alpha = 0$ for some $n > 0$, and (b) there exist $\alpha_n \in H^1(X,O_X)$ such that $f \alpha_{n+1} = \alpha_n$ and $\alpha_0 = \alpha$. In fact, any non-zero $\alpha$ will do the job (and one checks easily that $H^1(X,O_X) \neq 0$ using the anti-ampleness of $L$). Indeed, (a) follows from Claim 2, and (b) follows from Claim 1. 
