The Stacks project

Proof. We already know the functor is fully faithful, see Lemma 88.27.2. Essential surjectivity. Let $g : W \to X_{/T}$ be a morphism of formal algebraic spaces with $W$ locally Noetherian and $g$ rig-étale. We will prove $W$ is in the essential image in a number of steps.

Step 1: $W$ is an affine formal algebraic space. Then we can find $U \to X$ of finite type and étale over $X \setminus T$ such that $U_{/T}$ is isomorphic to $W$, see Lemma 88.25.1. Thus we see that $W$ is in the essential image by Lemma 88.25.7.

Step 2: $W$ is separated. Choose $\{ W_ i \to W\}$ as in Formal Spaces, Definition 87.11.1. By Step 1 the formal algebraic spaces $W_ i$ and $W_ i \times _ W W_ j$ are in the essential image. Say $W_ i = (X'_ i)_{/T}$ and $W_ i \times _ W W_ j = (X'_{ij})_{/T}$. By fully faithfulness we obtain morphisms $t_{ij} : X'_{ij} \to X'_ i$ and $s_{ij} : X'_{ij} \to X'_ j$ matching the projections $W_ i \times _ W W_ j \to W_ i$ and $W_ i \times _ W W_ j \to W_ j$. Consider the structure

(We can't use the letter $U$ as it has already been used.) Applying Lemma 88.25.6 we find that $(t, s) : R \to V \times _ X V$ defines an étale equivalence relation on $V$ over $X$. Thus we can take the quotient $X' = V/R$ and it is an algebraic space, see Bootstrap, Theorem 80.10.1. Since completion commutes with fibre products and taking quotient sheaves, we find that $X'_{/T} \cong W$ as formal algebraic spaces over $X_{/T}$.

Step 3: $W$ is general. Choose $\{ W_ i \to W\}$ as in Formal Spaces, Definition 87.11.1. The formal algebraic spaces $W_ i$ and $W_ i \times _ W W_ j$ are separated. Hence by Step 2 the formal algebraic spaces $W_ i$ and $W_ i \times _ W W_ j$ are in the essential image. Then we argue exactly as in the previous paragraph to see that $W$ is in the essential image as well. This concludes the proof. $\square$