The Stacks project

Proof. The notation using the subscript ${}_{/T}$ in the statement refers to the construction which to a morphism $f : X' \to X$ of algebraic spaces associates the morphism $f_{/T} : X'_{/f^{-1}T} \to X_{/T}$ of formal algebraic spaces, see Section 88.23. We will also use the notion $U \subset X$ and $U' \subset X'$ to denote the open subspaces with $|U| = |X| \setminus T$ and $U' = |X'| \setminus f^{-1}T$ introduced in Section 88.23.

After replacing $X'$ by $X' \amalg U$ we may and do assume the image of $X' \to X$ contains $U$. Let

be the pushout of $U' \to X'$ and the diagonal morphism $U' \to U' \times _ U U' = U' \times _ X U'$. Since $U' \to X$ is étale, this diagonal is an open immersion and we see that $R$ is an algebraic space (this follows for example from Spaces, Lemma 65.8.5). The two projections $U' \times _ U U' \to U'$ extend to $R$ and we obtain two étale morphisms $s, t : R \to X'$. Checking on each piece separatedly we find that $R$ is an étale equivalence relation on $X'$. Set $X'' = X'/R$ which is an algebraic space by Bootstrap, Theorem 80.10.1. By construction have the factorization as in the lemma and the morphism $X'' \to X$ is locally of finite type (as this can be checked étale locally, i.e., on $X'$). Since $U' \to U$ is a surjective étale morphism and since $s^{-1}(U') = t^{-1}(U') = U' \times _ U U'$ we see that $U'' = U \times _ X X'' \to U$ is an isomorphism. Finally, we have to show the morphism $X' \to X''$ induces an isomorphism $X'_{/T} \to X''_{/T}$. To see this, note that the formal completion of $R$ along the inverse image of $T$ is equal to the formal completion of $X'$ along the inverse image of $T$ by our choice of $R$! By our construction of the formal completion in Formal Spaces, Section 87.14 we have $X''_{/T} = (X'_{/T}) / (R_{/T})$ as sheaves. Since $X'_{/T} = R_{/T}$ we conclude that $X'_{/T} = X''_{/T}$ and this finishes the proof. $\square$