Proof.
Let $(I_\lambda )$ be a fundamental system of weakly admissible ideals of definition in $A$. Consider $Y$ as in (2). Then $Y \times _ X \mathop{\mathrm{Spec}}(A/I_\lambda )$ is affine (Definition 87.24.1 and Lemma 87.19.7). Say $Y \times _ X \mathop{\mathrm{Spec}}(A/I_\lambda ) = \mathop{\mathrm{Spec}}(B_\lambda )$. The ring map $A/I_\lambda \to B_\lambda $ is of finite type because $\mathop{\mathrm{Spec}}(B_\lambda ) \to \mathop{\mathrm{Spec}}(A/I_\lambda )$ is of finite type (by Definition 87.24.1). Then $(B_\lambda )$ is an object of $\mathcal{C}$.
Conversely, given an object $(B_\lambda )$ of $\mathcal{C}$ we can set $Y = \mathop{\mathrm{colim}}\nolimits \mathop{\mathrm{Spec}}(B_\lambda )$. This is an affine formal algebraic space. We claim that
\[ Y \times _ X \mathop{\mathrm{Spec}}(A/I_\lambda ) = \left(\mathop{\mathrm{colim}}\nolimits _\mu \mathop{\mathrm{Spec}}(B_\mu )\right) \times _ X \mathop{\mathrm{Spec}}(A/I_\lambda ) = \mathop{\mathrm{Spec}}(B_\lambda ) \]
To show this it suffices we get the same values if we evaluate on a quasi-compact scheme $U$. A morphism $U \to \left(\mathop{\mathrm{colim}}\nolimits _\mu \mathop{\mathrm{Spec}}(B_\mu )\right) \times _ X \mathop{\mathrm{Spec}}(A/I_\lambda )$ comes from a morphism $U \to \mathop{\mathrm{Spec}}(B_\mu ) \times _{\mathop{\mathrm{Spec}}(A/I_\mu )} \mathop{\mathrm{Spec}}(A/I_\lambda )$ for some $\mu \geq \lambda $ (use Lemma 87.9.4 two times). Since $\mathop{\mathrm{Spec}}(B_\mu ) \times _{\mathop{\mathrm{Spec}}(A/I_\mu )} \mathop{\mathrm{Spec}}(A/I_\lambda ) = \mathop{\mathrm{Spec}}(B_\lambda )$ by our second assumption on objects of $\mathcal{C}$ this proves what we want. Using this we can show the morphism $Y \to X$ is of finite type. Namely, we note that for any morphism $U \to X$ with $U$ a quasi-compact scheme, we get a factorization $U \to \mathop{\mathrm{Spec}}(A/I_\lambda ) \to X$ for some $\lambda $ (see lemma cited above). Hence
\[ Y \times _ X U = Y \times _ X \mathop{\mathrm{Spec}}(A/I_\lambda )) \times _{\mathop{\mathrm{Spec}}(A/I_\lambda )} U = \mathop{\mathrm{Spec}}(B_\lambda ) \times _{\mathop{\mathrm{Spec}}(A/I_\lambda )} U \]
is a scheme of finite type over $U$ as desired. Thus the construction $(B_\lambda ) \mapsto \mathop{\mathrm{colim}}\nolimits \mathop{\mathrm{Spec}}(B_\lambda )$ does give a functor from category (1) to category (2).
To finish the proof we show that the above constructions define quasi-inverse functors between the categories (1) and (2). In one direction you have to show that
\[ \left(\mathop{\mathrm{colim}}\nolimits _\mu \mathop{\mathrm{Spec}}(B_\mu )\right) \times _ X \mathop{\mathrm{Spec}}(A/I_\lambda ) = \mathop{\mathrm{Spec}}(B_\lambda ) \]
for any object $(B_\lambda )$ in the category $\mathcal{C}$. This we proved above. For the other direction you have to show that
\[ Y = \mathop{\mathrm{colim}}\nolimits (Y \times _ X \mathop{\mathrm{Spec}}(A/I_\lambda )) \]
given $Y$ in the category (2). Again this is true by evaluating on quasi-compact test objects and because $X = \mathop{\mathrm{colim}}\nolimits \mathop{\mathrm{Spec}}(A/I_\lambda )$.
$\square$
Comments (4)
Comment #1970 by Brian Conrad on
Comment #1979 by Johan on
Comment #1980 by jojo on
Comment #2022 by Johan on