Pullback of modules is left adjoint to pushforward

Let $\alpha :f^{\ast }\mathcal{G}\to \mathcal{F}$ be an ${\mathcal{O}}_X$-linear morphism. By [F1] and [L3], $\alpha$ is equivalent to a morphism from the tensor-product presheaf $U⟼{\mathcal{O}}_X(U){\otimes }_{(f^{-1}{\mathcal{O}}_Y)(U)}(f^{-1}\mathcal{G})(U)$ into the sheaf $\mathcal{F}$.

Conversely, let $\beta :\mathcal{G}\to f_{\ast }\mathcal{F}$ be an ${\mathcal{O}}_Y$-linear morphism. By [L2], it corresponds to an $f^{-1}{\mathcal{O}}_Y$-linear morphism $\tilde{\beta }:f^{-1}\mathcal{G}\to \mathcal{F}$. Applying [L1] on each open set gives a morphism from the tensor-product presheaf of [F1] into $\mathcal{F}$, and then [L3] factors it uniquely through the sheafification $f^{\ast }\mathcal{G}$. This yields an ${\mathcal{O}}_X$-linear morphism $\alpha :f^{\ast }\mathcal{G}\to \mathcal{F}$.

Applying [L1] on each open set $U\subseteq X$ converts the map of step 1.1 into an $(f^{-1}{\mathcal{O}}_Y)(U)$-linear map $(f^{-1}\mathcal{G})(U)\to \mathcal{F}(U)$, compatible with restriction. Hence step 1.1 is equivalent to an $f^{-1}{\mathcal{O}}_Y$-linear sheaf morphism $\tilde{\alpha }:f^{-1}\mathcal{G}\to \mathcal{F}\mathrm{.}$

By [L2], the underlying sheaf morphism $\tilde{\alpha }$ corresponds to a sheaf morphism $\beta :\mathcal{G}\to f_{\ast }\mathcal{F}$. Because the maps in step 2.1 are $(f^{-1}{\mathcal{O}}_Y)(U)$-linear, the corresponding components ${\beta }_V$ are ${\mathcal{O}}_Y(V)$-linear. Thus $\beta$ is a morphism of ${\mathcal{O}}_Y$-modules.

The constructions in steps 3.1 and 1.2 are inverse because each stage is built from an adjunction with the standard mutually inverse formulas. Therefore ${\mathrm{Hom}}_{{\mathcal{O}}_X}(f^{\ast }\mathcal{G},\mathcal{F})\cong {\mathrm{Hom}}_{{\mathcal{O}}_Y}(\mathcal{G},f_{\ast }\mathcal{F})$ naturally in both variables.