Lemma 85.17.7. Let $S$ be a scheme. Let $P$ be a local property of morphisms of $\textit{WAdm}^{count}$ which is stable under base change. Let $f : X \to Y$ and $g : Z \to Y$ be morphisms of locally countably indexed formal algebraic spaces over $S$. If $f$ satisfies the equivalent conditions of Lemma 85.17.3 then so does $\text{pr}_2 : X \times _ Y Z \to Z$.

Proof. Choose a covering $\{ Y_ j \to Y\}$ as in Definition 85.7.1. For each $j$ choose a covering $\{ X_{ji} \to Y_ j \times _ Y X\}$ as in Definition 85.7.1. For each $j$ choose a covering $\{ Z_{jk} \to Y_ j \times _ Y Z\}$ as in Definition 85.7.1. Observe that $X_{ji} \times _{Y_ j} Z_{jk}$ is an affine formal algebraic space which is countably indexed, see Lemma 85.16.8. Then we see that

$\{ X_{ji} \times _{Y_ j} Z_{jk} \to X \times _ Y Z\}$

is a covering as in Definition 85.7.1. Moreover, the morphisms $X_{ji} \times _{Y_ j} Z_{jk} \to Z$ factor through $Z_{jk}$. By assumption we know that $X_{ji} \to Y_ j$ corresponds to a morphism $B_ j \to A_{ji}$ of $\text{WAdm}^{count}$ having property $P$. The morphisms $Z_{jk} \to Y_ j$ correspond to morphisms $B_ j \to C_{jk}$ in $\text{WAdm}^{count}$. Since $X_{ji} \times _{Y_ j} Z_{jk} = \text{Spf}(A_{ji} \widehat{\otimes }_{B_ j} C_{jk})$ by Lemma 85.12.4 we see that it suffices to show that $C_{jk} \to A_{ji} \widehat{\otimes }_{B_ j} C_{jk}$ has property $P$ which is exactly what the condition that $P$ is stable under base change guarantees. $\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).