Lemma 96.27.5. In Situation 96.27.1 if there exists a solution $(f : X' \to X, T, a)$ then there is a functorial bijection $F(V) = \mathop{\mathrm{Mor}}\nolimits _ S(V, X)$ on the category of locally Noetherian schemes $V$ over $S$.

Proof. Let $V$ be a locally Noetherian scheme over $S$. Let $x : V \to X$ be a morphism over $S$. Then we get an element $(Z, u', \hat x)$ in $F(V)$ as follows

1. $Z \subset V$ is the inverse image of $T$ by $x$,

2. $u' : V \setminus Z \to U' = U$ is the restriction of $x$ to $V \setminus Z$,

3. $\hat x : V_{/Z} \to W$ is the composition of $x_{/Z} : V_{/Z} \to X_{/T}$ with the isomorphism $a : X_{/T} \to W$.

This triple satisfies the compatibility condition because we can take $V' = V \times _{x, X} X'$, we can take $\hat x'$ the completion of the projection $x' : V' \to X'$.

Conversely, suppose given an element $(Z, u', \hat x)$ of $F(V)$. We claim there is a unique morphism $x : V \to X$ compatible with $u'$ and $\hat x$. Namely, let $V' \to V$, $\hat x'$, and $x'$ witness the compatibility between $u'$ and $\hat x$. Then Algebraization of Formal Spaces, Proposition 86.26.1 is exactly the result we need to find a unique morphism $x : V \to X$ agreeing with $\hat x$ over $V_{/Z}$ and with $x'$ over $V'$ (and a fortiori agreeing with $u'$ over $V \setminus Z$).

We omit the verification that the two constructions above define inverse bijections between their respective domains. $\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).