Lemma 86.24.4. With assumptions and notation as in Theorem 86.23.4 let $f : X' \to X$ correspond to $g : W \to X_{/T}$. Then $f$ is proper if and only if $g$ is a formal modification (Definition 86.21.1).

Proof. If $f$ is proper, then $g$ is a formal modification by Lemma 86.21.3. Assume $g$ is a formal modification. By Lemmas 86.24.1 and 86.24.3 we see that $f$ is quasi-compact and separated.

By Cohomology of Spaces, Lemma 67.19.2 and Remark 67.19.3 it suffices to show that given any commutative diagram

$\xymatrix{ \mathop{\mathrm{Spec}}(K) \ar[r] \ar[d] & X' \ar[d]^ f \\ \mathop{\mathrm{Spec}}(R) \ar[r]^ p \ar@{-->}[ru] & X }$

where $R$ is a complete discrete valuation ring with fraction field $K$, there is a dotted arrow making the diagram commute. There are three cases: Case I: $p(\mathop{\mathrm{Spec}}(R)) \subset U$. This case is trivial because $U' \to U$ is an isomorphism. Case II: $p$ maps $\mathop{\mathrm{Spec}}(R)$ into $T$. This case follows from our assumption that $g : W \to X_{/T}$ is proper. Namely, if $Z$ denotes the reduced induced closed subspace structure on $T$, then $p$ factors through $Z$ and

$W \times _{X_{/T}} Z = X' \times _ X Z \longrightarrow Z$

is proper by assumption which implies we get the lifting property by Cohomology of Spaces, Lemma 67.19.2 applied to the displayed arrow. Case III: $p(\mathop{\mathrm{Spec}}(K))$ is not in $T$ but $p$ maps the closed point of $\mathop{\mathrm{Spec}}(R)$ into $T$. In this case the corresponding morphism

$p_{/T} : \text{Spf}(R) \longrightarrow X'_{/T} = W$

is an adic morphism (by Formal Spaces, Lemma 85.10.4 and Definition 85.19.3). Hence our assumption that $g : W \to X_{/T}$ be rig-surjective implies we can lift $g_{/T}$ to a morphism $\text{Spf}(R') \to W = X'_{/T}$ for some extension of complete discrete valuation rings $R \subset R'$. Algebraizing the composition $\text{Spf}(R') \to X'$ using Formal Spaces, Lemma 85.28.3 we find a morphism $\mathop{\mathrm{Spec}}(R') \to X'$ lifting $p$ as desired. $\square$

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).