The Stacks project

Theorem 98.27.17. Let $S$ be a locally Noetherian scheme such that $\mathcal{O}_{S, s}$ is a G-ring for all finite type points $s \in S$. Let $X'$ be an algebraic space locally of finite type over $S$. Let $T' \subset |X'|$ be a closed subset. Let $W$ be a locally Noetherian formal algebraic space over $S$ with $W_{red}$ locally of finite type over $S$. Finally, we let

be a formal modification, see Algebraization of Formal Spaces, Definition 88.24.1. If $X'$ and $W$ are separated¹ over $S$, then there exists a proper morphism $f : X' \to X$ of algebraic spaces over $S$, a closed subset $T \subset |X|$, and an isomorphism $a : X_{/T} \to W$ of formal algebraic spaces such that

1. $T'$ is the inverse image of $T$ by $|f| : |X'| \to |X|$,

2. $f : X' \to X$ maps $X' \setminus T'$ isomorphically to $X \setminus T$, and

3. $g = a \circ f_{/T}$ where $f_{/T} : X'_{/T'} \to X_{/T}$ is the induced morphism.

In other words, $(f : X' \to X, T, a)$ is a solution as defined earlier in this section.