The Stacks project

Proof. By Lemma 61.12.2 any pro-étale covering is an fpqc covering. Hence the formula defines a sheaf on $X_{pro\text{-}\acute{e}tale}$ by Étale Cohomology, Lemma 59.39.2. Let $a : \mathop{\mathit{Sh}}\nolimits (X_{\acute{e}tale}) \to \mathop{\mathit{Sh}}\nolimits (X_{pro\text{-}\acute{e}tale})$ be the functor sending $\mathcal{F}$ to the sheaf given by the formula in the lemma. To show that $a = \epsilon ^{-1}$ it suffices to show that $a$ is a left adjoint to $\epsilon _*$.

Let $\mathcal{G}$ be an object of $\mathop{\mathit{Sh}}\nolimits (X_{pro\text{-}\acute{e}tale})$. Recall that $\epsilon _*\mathcal{G}$ is simply given by the restriction of $\mathcal{G}$ to the full subcategory $X_{\acute{e}tale}$. Let $f : Y \to X$ be an object of $X_{pro\text{-}\acute{e}tale}$. We view $Y_{\acute{e}tale}$ as a subcategory of $X_{pro\text{-}\acute{e}tale}$. The restriction maps of the sheaf $\mathcal{G}$ define a map

Namely, for $U$ in $X_{\acute{e}tale}$ the value of $f_{{\acute{e}tale}, *}(\mathcal{G}|_{Y_{\acute{e}tale}})$ on $U$ is $\mathcal{G}(Y \times _ X U)$ and there is a restriction map $\mathcal{G}(U) \to \mathcal{G}(Y \times _ X U)$. By adjunction this determines a map

Putting these together for all $f : Y \to X$ in $X_{pro\text{-}\acute{e}tale}$ we obtain a canonical map $a(\epsilon _*\mathcal{G}) \to \mathcal{G}$.

Let $\mathcal{F}$ be an object of $\mathop{\mathit{Sh}}\nolimits (X_{\acute{e}tale})$. It is immediately clear that $\mathcal{F} = \epsilon _*a(\mathcal{F})$.

We claim the maps $\mathcal{F} \to \epsilon _*a(\mathcal{F})$ and $a(\epsilon _*\mathcal{G}) \to \mathcal{G}$ are the unit and counit of the adjunction (see Categories, Section 4.24). To see this it suffices to show that the corresponding maps

and

are mutually inverse. We omit the detailed verification. $\square$