[Theorem 3.1, ArtinII]

Theorem 97.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

$g : X'_{/T'} \longrightarrow W$

be a formal modification, see Algebraization of Formal Spaces, Definition 87.24.1. If $X'$ and $W$ are separated1 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.

Proof. Let $F$ be the functor constructed using $X'$, $T'$, $W$, $g$ in this section. By Lemma 97.27.6 it suffices to show that $F$ corresponds to an algebraic space $X$ locally of finite type over $S$. In order to do this, we will apply Proposition 97.26.1. Namely, by Lemma 97.27.9 the diagonal of $F$ is representable by closed immersions and by Lemmas 97.27.10, 97.27.11, 97.27.12, 97.27.13, 97.27.14, and 97.27.16 we have axioms [0], [1], [2], [3], [4], and [5]. $\square$

[1] See Remark 97.27.18.

In your comment you can use Markdown and LaTeX style mathematics (enclose it like $\pi$). A preview option is available if you wish to see how it works out (just click on the eye in the toolbar).