The Stacks project

Proof. Assumptions (2) and (3) imply that $X_{red} = X \times _ Y Y_{red} = Y_{red}$. We will use this without further mention.

If $Y' \to Y$ is an étale morphism of formal algebraic spaces over $S$, then the base change $f' : X \times _ Y Y' \to Y'$ satisfies conditions (1) – (4). Hence by Lemma 87.27.4 we may assume $Y$ is an affine formal algebraic space.

Say $Y = \mathop{\mathrm{colim}}\nolimits _{\lambda \in \Lambda } Y_\lambda$ as in Definition 87.9.1. Then $X_\lambda = X \times _ Y Y_\lambda$ is an algebraic space endowed with a monomorphism $f_\lambda : X_\lambda \to Y_\lambda$ which induces an isomorphism $X_{\lambda , red} \to Y_{\lambda , red}$. Thus $X_\lambda$ is an affine scheme by Limits of Spaces, Proposition 70.15.2 (as $X_{\lambda , red} \to X_\lambda$ is surjective and integral). To finish the proof it suffices to show that $X_\lambda \to Y_\lambda$ is a closed immersion which we will do in the next paragraph.

Let $X \to Y$ be a monomorphism of affine schemes such that $X_{red} = X \times _ Y Y_{red} = Y_{red}$. In general, this does not imply that $X \to Y$ is a closed immersion, see Examples, Section 110.36. However, under our assumption (4) we know that in the previous parapgrah either $X_\lambda \to Y_\lambda$ is of finite type or $Y_\lambda$ is Noetherian. This means that $X \to Y$ corresponds to a ring map $R \to A$ such that $R/I \to A/IA$ is an isomorphism where $I \subset R$ is the nil radical (ie., the maximal locally nilpotent ideal of $R$) and either $R \to A$ is of finite type or $R$ is Noetherian. In the first case $R \to A$ is surjective by Algebra, Lemma 10.126.9 and in the second case $I$ is finitely generated, hence nilpotent, hence $R \to A$ is surjective by Nakayama's lemma, see Algebra, Lemma 10.20.1 part (11). $\square$