# Is one sheafification enough for the module inverse image?


My question is whether $$f^* \G$$ is equal to the sheafification of the presheaf $$f^+ \G \,\hat\otimes_{f^+ \O_Y} \O_X$$ (where $$\hat\otimes$$ denotes a tensor product without sheafification.

In particular I would be interested in some "high-level" argument which maybe applies to more general situations.

At this level, the argument would go roughly along the lines of: \begin{align*} \operatorname{Hom}_{\mathcal{O}_X}(f^* \mathcal{G}, \mathcal{F}) & \simeq \operatorname{Hom}_{\mathcal{O}_Y}(\mathcal{G}, f_* \mathcal{F}) \\ & \simeq \operatorname{Hom}_{\mathcal{O}_Y, psh}(\mathcal{G}, f_* \mathcal{F}) \\ & \simeq \operatorname{Hom}_{f^+ \mathcal{O}_Y, psh}(f^+ \mathcal{G}, \mathcal{F}) \\ & \simeq \operatorname{Hom}_{\mathcal{O}_X, psh}(f^+ \mathcal{G} \hat\otimes_{f^+ \mathcal{O}_Y} \mathcal{O}_X, \mathcal{F}) \\ & \simeq \operatorname{Hom}_{\mathcal{O}_x}([f^+ \mathcal{G} \hat\otimes_{f^+ \mathcal{O}_Y} \mathcal{O}_X]^+, \mathcal{F}). \end{align*} (Here for example, $$\operatorname{Hom}_{\mathcal{O}_Y, psh}(-, -)$$ represents the presheaf homomorphisms which are $$\mathcal{O}_Y$$-linear; and for a presheaf of $$\mathcal{O}_X$$-modules $$\mathcal{F}$$ then $$\mathcal{F}^+$$ is the sheafification as a sheaf of $$\mathcal{O}_X$$-modules.)
In this sequence, once you have established each isomorphism, and you have also verified that each is functorial in $$\mathcal{F}$$, then by Yoneda's lemma, it follows that the composite isomorphism of functors $$\mathcal{O}_X{-}\mathrm{Mod} \to \mathrm{Set}$$ is induced by a unique isomorphism of $$\mathcal{O}_X$$-modules $$f^* \mathcal{G} \simeq [f^+ \mathcal{G} \hat\otimes_{f^+ \mathcal{O}_Y} \mathcal{O}_X]^+$$.