Lemma 88.27.3. In the situation above. Assume X is affine. Then the functor (88.27.0.1) is an equivalence.
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
Comments (0)