# Is one sheafification enough for the module inverse image?

Let $$\newcommand{\G}{\mathcal{G}}\newcommand{\O}{\mathcal{O}} f: (X, \O_X) \to (Y, \O_Y)$$ be a morphism of locally ringed spaces and $$\G$$ a sheaf of $$\O_Y$$ modules. The module inverse image of $$\G$$ is defined as $$f^* \G = f^{-1} \G \otimes_{f^{-1} \O_Y} \O_X$$ There are three sheafifications involved here: one for the tensor product one for $$f^{-1} \G$$ and finally one for $$f^{-1} O_Y$$, since the inverse image $$f^{-1} \G$$ is defined as the sheafification of $$f^+ \G$$, where $$f^+ \G (U) = \varinjlim_{V \supset f(U)} \G(V)$$

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]^+$$.