The Stacks project

Proof. Recall that $f_{big}$ is the morphism of topoi associated to the continuous and cocontinuous functor $u : (\mathit{Sch}/X)_\tau \to (\mathit{Sch}/Y)_\tau$, $U/X \mapsto U/Y$. Moreover, we have $f_{big}^{-1}\mathcal{O} = \mathcal{O}$. Hence the existence of $f_{big!}$ follows from Modules on Sites, Lemma 18.16.2, respectively Modules on Sites, Lemma 18.41.1. Note that if $U$ is an object of $(\mathit{Sch}/X)_\tau$ then the functor $u$ induces an equivalence of categories

because both sides of the arrow are equal to $(\mathit{Sch}/U)_\tau$. Hence the agreement of $f_{big!}$ on underlying abelian sheaves follows from the discussion in Modules on Sites, Remark 18.41.2. The exactness of $f_{big!}$ follows from Modules on Sites, Lemma 18.16.3 as the functor $u$ above which commutes with fibre products and equalizers. $\square$