If the base change of a scheme to a limit is proper, then already the base change is proper at a finite level.

Lemma 32.13.1. Assumptions and notation as in Situation 32.8.1. If

1. $f$ is proper, and

2. $f_0$ is locally of finite type,

then there exists an $i$ such that $f_ i$ is proper.

Proof. By Lemma 32.8.6 we see that $f_ i$ is separated for some $i \geq 0$. Replacing $0$ by $i$ we may assume that $f_0$ is separated. Observe that $f_0$ is quasi-compact, see Schemes, Lemma 26.21.14. By Lemma 32.12.1 we can choose a diagram

$\xymatrix{ X_0 \ar[rd] & X_0' \ar[d] \ar[l]^\pi \ar[r] & \mathbf{P}^ n_{Y_0} \ar[dl] \\ & Y_0 & }$

where $X_0' \to \mathbf{P}^ n_{Y_0}$ is an immersion, and $\pi : X_0' \to X_0$ is proper and surjective. Introduce $X' = X_0' \times _{Y_0} Y$ and $X_ i' = X_0' \times _{Y_0} Y_ i$. By Morphisms, Lemmas 29.41.4 and 29.41.5 we see that $X' \to Y$ is proper. Hence $X' \to \mathbf{P}^ n_ Y$ is a closed immersion (Morphisms, Lemma 29.41.7). By Morphisms, Lemma 29.41.9 it suffices to prove that $X'_ i \to Y_ i$ is proper for some $i$. By Lemma 32.8.5 we find that $X'_ i \to \mathbf{P}^ n_{Y_ i}$ is a closed immersion for $i$ large enough. Then $X'_ i \to Y_ i$ is proper and we win. $\square$

Comment #896 by Kestutis Cesnavicius on

Suggested slogan: Limit formalism for proper morphisms of schemes

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