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