The Stacks project

Proof. We first prove that $F$ is continuous. Let $\{ x_ i \to x\} _{i \in I}$ be a covering of $\mathcal{X}$. By Categories, Definition 4.33.9 the functor $F$ transforms strongly cartesian morphisms into strongly cartesian morphisms, hence $\{ F(x_ i) \to F(x)\} _{i \in I}$ is a covering of $\mathcal{Y}$. This proves part (1) of Sites, Definition 7.13.1. Moreover, let $x' \to x$ be a morphism of $\mathcal{X}$. By Categories, Lemma 4.33.13 the fibre product $x_ i \times _ x x'$ exists and $x_ i \times _ x x' \to x'$ is strongly cartesian. Hence $F(x_ i \times _ x x') \to F(x')$ is strongly cartesian. By Categories, Lemma 4.33.13 applied to $\mathcal{Y}$ this means that $F(x_ i \times _ x x') = F(x_ i) \times _{F(x)} F(x')$. This proves part (2) of Sites, Definition 7.13.1 and we conclude that $F$ is continuous.

Next we prove that $F$ is cocontinuous. Let $x \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{X})$ and let $\{ y_ i \to F(x)\} _{i \in I}$ be a covering in $\mathcal{Y}$. Denote $\{ U_ i \to U\} _{i \in I}$ the corresponding covering of $\mathcal{C}$. For each $i$ choose a strongly cartesian morphism $x_ i \to x$ in $\mathcal{X}$ lying over $U_ i \to U$. Then $F(x_ i) \to F(x)$ and $y_ i \to F(x)$ are both a strongly cartesian morphisms in $\mathcal{Y}$ lying over $U_ i \to U$. Hence there exists a unique isomorphism $F(x_ i) \to y_ i$ in $\mathcal{Y}_{U_ i}$ compatible with the maps to $F(x)$. Thus $\{ x_ i \to x\} _{i \in I}$ is a covering of $\mathcal{X}$ such that $\{ F(x_ i) \to F(x)\} _{i \in I}$ is isomorphic to $\{ y_ i \to F(x)\} _{i \in I}$. Hence $F$ is cocontinuous, see Sites, Definition 7.20.1.

The final assertion follows from the first two, see Sites, Lemmas 7.21.1, 7.20.2, and 7.21.5. $\square$