## 87.24 Morphisms of finite type

Due to how things are setup in the Stacks project, the following is really the correct thing to do and stronger notions should have a different name.

Definition 87.24.1. Let $S$ be a scheme. Let $f : Y \to X$ be a morphism of formal algebraic spaces over $S$.

1. We say $f$ is locally of finite type if $f$ is representable by algebraic spaces and is locally of finite type in the sense of Bootstrap, Definition 80.4.1.

2. We say $f$ is of finite type if $f$ is locally of finite type and quasi-compact (Definition 87.17.4).

We will discuss the relationship between finite type morphisms of certain formal algebraic spaces and continuous ring maps $A \to B$ which are topologically of finite type in Section 87.29.

Lemma 87.24.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 of finite type,

2. $f$ is representable by algebraic spaces and is of finite type in the sense of Bootstrap, Definition 80.4.1.

Proof. This follows from Bootstrap, Lemma 80.4.5, the implication “quasi-compact $+$ locally of finite type $\Rightarrow$ finite type” for morphisms of algebraic spaces, and Lemma 87.17.5. $\square$

Lemma 87.24.3. The composition of finite type morphisms is of finite type. The same holds for locally of finite type.

Proof. See Bootstrap, Lemma 80.4.3 and use Morphisms of Spaces, Lemma 67.23.2. $\square$

Lemma 87.24.4. A base change of a finite type morphism is finite type. The same holds for locally of finite type.

Proof. See Bootstrap, Lemma 80.4.2 and use Morphisms of Spaces, Lemma 67.23.3. $\square$

Lemma 87.24.5. Let $S$ be a scheme. Let $f : X \to Y$ and $g : Y \to Z$ be morphisms of formal algebraic spaces over $S$. If $g \circ f : X \to Z$ is locally of finite type, then $f : X \to Y$ is locally of finite type.

Proof. By Lemma 87.19.3 we see that $f$ is representable by algebraic spaces. Let $T$ be a scheme and let $T \to Z$ be a morphism. Then we can apply Morphisms of Spaces, Lemma 67.23.6 to the morphisms $T \times _ Z X \to T \times _ Z Y \to T$ of algebraic spaces to conclude. $\square$

Being locally of finite type is local on the source and the target.

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

1. the morphism $f$ is locally of finite type,

2. there exists a commutative diagram

$\xymatrix{ U \ar[d] \ar[r] & V \ar[d] \\ X \ar[r] & Y }$

where $U$, $V$ are formal algebraic spaces, the vertical arrows are representable by algebraic spaces and étale, $U \to X$ is surjective, and $U \to V$ is locally of finite type,

3. for any commutative diagram

$\xymatrix{ U \ar[d] \ar[r] & V \ar[d] \\ X \ar[r] & Y }$

where $U$, $V$ are formal algebraic spaces and vertical arrows representable by algebraic spaces and étale, the morphism $U \to V$ is locally of finite type,

4. there exists a covering $\{ Y_ j \to Y\}$ as in Definition 87.11.1 and for each $j$ a covering $\{ X_{ji} \to Y_ j \times _ Y X\}$ as in Definition 87.11.1 such that $X_{ji} \to Y_ j$ is locally of finite type for each $j$ and $i$,

5. there exist a covering $\{ X_ i \to X\}$ as in Definition 87.11.1 and for each $i$ a factorization $X_ i \to Y_ i \to Y$ where $Y_ i$ is an affine formal algebraic space, $Y_ i \to Y$ is representable by algebraic spaces and étale, such that $X_ i \to Y_ i$ is locally of finite type, and

Proof. In each of the 5 cases the morphism $f : X \to Y$ is representable by algebraic spaces, see Lemma 87.19.4. We will use this below without further mention.

It is clear that (1) implies (2) because we can take $U = X$ and $V = Y$. Conversely, assume given a diagram as in (2). Let $T$ be a scheme and let $T \to Y$ be a morphism. Then we can consider

$\xymatrix{ U \times _ Y T \ar[d] \ar[r] & V \times _ Y T \ar[d] \\ X \times _ Y T \ar[r] & T }$

The vertical arrows are étale and the top horizontal arrow is locally of finite type as base changes of such morphisms. Hence by Morphisms of Spaces, Lemma 67.23.4 we conclude that $X \times _ Y T \to T$ is locally of finite type. In other words (1) holds.

Assume (1) is true and consider a diagram as in (3). Then $U \to Y$ is locally of finite type (as the composition $U \to X \to Y$, see Bootstrap, Lemma 80.4.3). Let $T$ be a scheme and let $T \to V$ be a morphism. Then the projection $T \times _ V U \to T$ factors as

$T \times _ V U = (T \times _ Y U) \times _{(V \times _ Y V)} V \to T \times _ Y U \to T$

The second arrow is locally of finite type (as a base change of the composition $U \to X \to Y$) and the first is the base change of the diagonal $V \to V \times _ Y V$ which is locally of finite type by Lemma 87.15.5.

It is clear that (3) implies (2). Thus now (1) – (3) are equivalent.

Observe that the condition in (4) makes sense as the fibre product $Y_ j \times _ Y X$ is a formal algebraic space by Lemma 87.15.3. It is clear that (4) implies (5).

Assume $X_ i \to Y_ i \to Y$ as in (5). Then we set $V = \coprod Y_ i$ and $U = \coprod X_ i$ to see that (5) implies (2).

Finally, assume (1) – (3) are true. Thus we can choose any covering $\{ Y_ j \to Y\}$ as in Definition 87.11.1 and for each $j$ any covering $\{ X_{ji} \to Y_ j \times _ Y X\}$ as in Definition 87.11.1. Then $X_{ij} \to Y_ j$ is locally of finite type by (3) and we see that (4) is true. This concludes the proof. $\square$

Example 87.24.7. Let $S$ be a scheme. Let $A$ be a weakly admissible topological ring over $S$. Let $A \to A'$ be a finite type ring map. Then

$(A')^\wedge = \mathop{\mathrm{lim}}\nolimits _{I \subset A\ w.i.d.} A'/IA'$

is a weakly admissible ring and the corresponding morphism $\text{Spf}((A')^\wedge ) \to \text{Spf}(A)$ is representable, see Example 87.19.11. If $T \to \text{Spf}(A)$ is a morphism where $T$ is a quasi-compact scheme, then this factors through $\mathop{\mathrm{Spec}}(A/I)$ for some weak ideal of definition $I \subset A$ (Lemma 87.9.4). Then $T \times _{\text{Spf}(A)} \text{Spf}((A')^\wedge )$ is equal to $T \times _{\mathop{\mathrm{Spec}}(A/I)} \mathop{\mathrm{Spec}}(A'/IA')$ and we see that $\text{Spf}((A')^\wedge ) \to \text{Spf}(A)$ is of finite type.

Lemma 87.24.8. Let $S$ be a scheme. Let $f : X \to Y$ be a morphism of formal algebraic spaces over $S$. If $Y$ is locally Noetherian and $f$ locally of finite type, then $X$ is locally Noetherian.

Proof. Pick $\{ Y_ j \to Y\}$ and $\{ X_{ij} \to Y_ j \times _ Y X\}$ as in Lemma 87.24.6. Then it follows from Lemma 87.19.9 that each $X_{ij}$ is Noetherian. This proves the lemma. $\square$

Lemma 87.24.9. Let $S$ be a scheme. Let $f : X \to Y$ and $Z \to Y$ be morphisms of formal algebraic spaces over $S$. If $Z$ is locally Noetherian and $f$ locally of finite type, then $Z \times _ Y X$ is locally Noetherian.

Proof. The morphism $Z \times _ Y X \to Z$ is locally of finite type by Lemma 87.24.4. Hence this follows from Lemma 87.24.8. $\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).