## 87.31 Proper morphisms

Here is the definition we will use.

Definition 87.31.1. Let $S$ be a scheme. Let $f : Y \to X$ be a morphism of formal algebraic spaces over $S$. We say $f$ is proper if $f$ is representable by algebraic spaces and is proper in the sense of Bootstrap, Definition 80.4.1.

It follows from the definitions that a proper morphism is of finite type.

Lemma 87.31.2. Let $S$ be a scheme. Let $f : X \to Y$ be a morphism of formal algebraic spaces over $S$. The following are equivalent

1. $f$ is proper,

2. for every scheme $Z$ and morphism $Z \to Y$ the base change $Z \times _ Y X \to Z$ of $f$ is proper,

3. for every affine scheme $Z$ and every morphism $Z \to Y$ the base change $Z \times _ Y X \to Z$ of $f$ is proper,

4. for every affine scheme $Z$ and every morphism $Z \to Y$ the formal algebraic space $Z \times _ Y X$ is an algebraic space proper over $Z$,

5. there exists a covering $\{ Y_ j \to Y\}$ as in Definition 87.11.1 such that the base change $Y_ j \times _ Y X \to Y_ j$ is proper for all $j$.

Proof. Omitted. $\square$

Lemma 87.31.3. Proper morphisms of formal algebraic spaces are preserved by base change.

Proof. This is an immediate consequence of Lemma 87.31.2 and transitivity of base change. $\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).