The Stacks project

Proof. In this proof we drop the subscript ${}_{small}$ from our pullback and pushforward functors. Denote $X_1 = X \times _ Y X$ and denote $f_1 : X_1 \to Y$ the morphism $f \circ \text{pr}_0 = f \circ \text{pr}_1$. Let $(\mathcal{F}, \varphi )$ be a descent datum for $\{ X \to Y\} $. Let us set $\mathcal{F}_1 = \text{pr}_0^{-1}\mathcal{F}$. We may think of $\varphi $ as defining an isomorphism $\mathcal{F}_1 \to \text{pr}_1^{-1}\mathcal{F}$. We claim that the rule which sends a descent datum $(\mathcal{F}, \varphi )$ to the sheaf

is a quasi-inverse to the functor in the statement of the lemma. The first of the two arrows comes from the map

and the second arrow comes from the map

where the arrow pointing left is invertible. To prove this works we have to show that the canonical map $f^{-1}\mathcal{G} \to \mathcal{F}$ is an isomorphism; details omitted. In order to prove this it suffices to check after pulling back by any collection of morphisms $\mathop{\mathrm{Spec}}(k) \to Y$ where $k$ is an algebraically closed field. Namely, the corresponding base changes $X_ k \to X$ are jointly surjective and we can check whether a map of sheaves on $X_{\acute{e}tale}$ is an isomorphism by looking at stalks on geometric points, see Theorem 59.29.10. By Lemma 59.55.4 the construction of $\mathcal{G}$ from the descent datum $(\mathcal{F}, \varphi )$ commutes with any base change. Thus we may assume $Y$ is the spectrum of an algebraically closed point (note that base change preserves the properties of the morphism $f$, see Morphisms, Lemma 29.9.4 and 29.44.6). In this case the morphism $X \to Y$ has a section, so we know that the functor is an equivalence by Lemma 59.104.1. However, the reader may show that the functor is an equivalence if and only if the construction above is a quasi-inverse; details omitted. This finishes the proof. $\square$