My question has two parts, one specifically about sheafification, and the second one is whether there is an "abstract-nonsensification" of it.
Let $X$ be a fixed topological space, $(-)^a : \mathbf{Psh}(X)\to \mathbf{Sh}(X)$ denotes sheafification (I will stick to sheaves of abelian groups). Let $\mathbb Z$ denote the constant presheaf, and $\underline{\mathbb Z}$ the constant sheaf.
$\otimes$ denotes tensor product over $\mathbb Z$ (the naive one) and $\otimes^a$ tensor product over $\underline{\mathbb Z}$
Now a presheaf of rings $A$ is just a monoid in the monoidal category $(\mathbf{Psh}(X),\otimes)$ and same for a sheaf of rings with $\otimes^a$ (I think).
If $A$ is a presheaf of rings and $M$ and $A$-module, then it is well-known that $M^a$ is a sheaf of $A^a$-modules. My first question is : is it obvious; in the following sense :
Is $(-)^a$ monoidal with respect to the afore-mentioned monoidal structures ?
Now the answer to this (if it is indeed yes, which I suspect it is) seems highly-related to our very definition of $\otimes^a$, which is: given sheaves $\mathcal{F,G}$, $\mathcal{F}\otimes^a \mathcal{G} := (\mathcal{F}\otimes \mathcal{G})^a$. Therefore, it seems reasonable to ask if there is an abstract nonsense version of it. Therefore, I ask the following question :
Let $(C,\otimes_C, I_C), (D,\otimes_D, I_D)$ be two monoidal categories [I'm not including the data of associators and unitors, but it's there, and I'm not assuming that they're strict monoidal], and let $F\dashv G: C\to D$ [to be sure, $F:C\to D$] be an adjunction between the underlying categories. Are there nice conditions -that are satisfied in the above test case- we can impose on this data for it to follow that $F$ is monoidal ? For instance, are a natural isomorphism $A\otimes_D B \to F(G(A)\otimes_C G(B))$ and an isomorphism $I_D\to F(I_C)$ enough (satisfying certain compatibility conditions with associators and unitors) ? What if we also require that $G$ is faithful ? Full and faithful ?
EDIT: here's one step forward. If we require that $C,D$ be monoidal closed with internal homs $\hom_C, \hom_D$ respectively, and if we require that $F,G$ be an "internal adjunction" in the sense that $G\hom_D(FA,B) \simeq \hom_C(A,GB)$ (naturally - which I think holds in the sheaf case) then we easily get a natural isomorphism $F(A\otimes_C B)\to F(A)\otimes_D F(B)$ via Yoneda, and I suspect this isomorphism should be such that $F$ is actually monoidal. So I'm willing to assume that $C,D$ are monoidal closed if that helps in any way (though if there are reasonable constraints without this addition, then I'm all ears)
The answer is yes. The point is that $\mathbf{Sh}(X)$ is a (reflexive) localization of $\mathbf{Psh}(X)$, and this induces a universally defined symmetric monoidal structure on $\mathbf{Sh}(X)$ for which the localization (sheafification) functor is symmetric monoidal.
This in particular implies that the structure so-defined on $\mathbf{Sh}(X)$ is the usual one, and that the sheafification functor is symmetric monoidal.
Suppose $W$ is a class of arrows in a symmetric monoidal category $C$ such that for any $f\in W, A\in C, A\otimes f\in W$. Then there is an essentially unique symmetric monoidal structure on $C[W^{-1}]$ such that the functor $C\to C[W^{-1}]$ is (strong) symmetric monoidal.
This criterion is particularly applicable when $C$ is presentable and $\otimes$ commutes with colimits in each variable. Then, oftentimes, $W$ will be "generated" by a set of arrows $S$ ($W$ is then the class of $S$-local equivalences), and it suffices to check that $A\otimes f\in W$ for each $f\in S$.
In that situation, the localization is what's called a reflexive localization, and $C\to C[W^{-1}]$ has a (fully faithful) right adjoint which exhibits $C[W^{-1}]$ as a full reflexive subcategory of $C$ (the $S$-local objects), and not only is $C\to C[W^{-1}]$ symmetric monoidal, the inclusion $C[W^{-1}]\to C$ is lax symmetric monoidal.
In our situation, $C= \mathbf{Psh}(X)$, $S= \{\mathbb Z[\mathrm{coeq}(\coprod_{i,j}\mathbb h_{U_{i,j}}\rightrightarrows \coprod_i h_{U_i})\to h_U] \mid (U_i)_{i\in I}$ open cover of $U\subset X\}$ (this is not quite well written, as we need $S$ to be a set - to solve that, either use covering sieves rather than covering families, or put restraints on $I$), where $h_U$ denotes the representable sheaf associated to an open $U\subset X$.
Then, clearly the $S$-local objects are exactly the sheaves (of abelian groups), and therefore we get a localization $\mathbf{Psh}(X)\to\mathbf{Sh}(X)$ at the $S$-local equivalences. Now to prove the compatibility condition, since $\otimes$ commutes with colimits, and since any sheaf of abelian groups is an iterated colimit of sheaves of the form $\mathbb Z[h_U]$, it suffices to check that $\mathbb Z[h_U]\otimes f \in W$ for each $f\in S$, but this follows by the fact that $\mathbb Z[h_U]\otimes \mathbb Z[h_V]\cong \mathbb Z[h_{U\cap V}]$, so in fact for $f\in S, \mathbb Z[h_U]\otimes f\in S$ up to isomorphism.
Therefore we get a unique symmetric monoidal structure on $\mathbf{Sh}(X)$ such that the localization ( = sheafification) functor $\mathbf{Psh}(X)\to \mathbf{Sh}(X)$ is symmetric monoidal. In particular, we get $(F\otimes G)^a \cong F\otimes^a G$ and so this new symmetric monoidal structure is exactly the one described in the post.
There is also a framework for adjunctions which compares lax and oplax monoidal structures on adjoints.
All of this goes through in $\infty$-categories as well, which can be particularly useful.