Taking module sheaf commutes with tensor product I'm trying to prove proposition II.5.2.b in Algebraic Geometry by Hartshorne. The proposition states that for $ A $-modules $ M $ and $ N $ and $X=\text{Spec}\ A$ there is an isomorphism $ (M\otimes_{A}N)^\tilde{}\cong \tilde{M}\otimes_{\mathcal{O}_{X}}\tilde{N} $.
I think I have a proof using category theory. I defined a "bilinear" morphism of sheaves and showed that both sheaves satisfy a universal property similar to that of the tensor product of modules. I'm curious as to whether this is a common proof. The proof in the book is very brief. It says this follows since localisation commutes with tensor products.
I'm also interested in a more constructive proof. Vakil's notes contain a hint saying we can define an isomorphism on distinguished open subsets and on such subsets no need for sheafification. This is page 372. The book by Wedhorn and Görtz appears to follow the same approach but it's missing details. This is page 185. Can someone help me fill in the details of such a proof?
 A: I would say that your proof is not particularly common, certainly I've never seen it before (admittedly this doesn't mean much). The proof in Hartshorne is brief because it is one of those scenarios where doing the "obvious" thing works. Here is the proof that I think Hartshorne had in mind (which is entirely constructive):
Let $T$ be the tensor pre-sheaf of $\tilde{M}\otimes_{\mathcal{O}_X}\tilde{N}$ and $\theta : T \rightarrow \tilde{M}\otimes_{\mathcal{O}_X}\tilde{N}$ be the canonical morphism. We may define the "obvious" morphism $\varphi: T \rightarrow \tilde{(M\otimes_A N)}$ that over each open set sends $f\otimes g$ to $f\cdot g$. 
Explicitly, for each $P \in \operatorname{Spec}(A)$, $(f\cdot g)(P) :=f(P)\cdot g(P) \in (M\otimes_A N)_P$ where we are implicitly using the canonical isomorphism from $M_P\otimes_{A_P} N_P$ to $(M\otimes_A N)_P$. This is where we are using that localisation commutes with tensor products.
You should check that on the stalk at $P$, $\varphi_P$ gives the canonical isomorphism $M_P\otimes_{A_P} N_P \rightarrow (M\otimes_A N)_P$.
Finally, by the universal property of sheafification, $\varphi$ factors through some morphism $\bar\varphi:\tilde{M}\otimes_{\mathcal{O}_X}\tilde{N}\rightarrow \tilde{(M\otimes_A N)}$, i.e. $\varphi = \bar\varphi\circ\theta$ and since $\varphi$ is an isomorphism on stalks, $\bar\varphi$ is an isomorphism.
As frequently happens in Hartshorne, a lot of algebraic detail is left out,and you can see why. If he included all of the details like this every time this kind of problem arose, the book would be $2-3$ times as long!
For the construction Vakil/Wedhorn and Görtz use, this is simply using the fact that you know what the sections of $\mathcal{O}_X, \tilde{M}$ and $\tilde{N}$ look like over the distinguished open affine pieces $D(f)$ of $X$. Since these form a basis for the topology on $X$ you can define the morphism $\varphi$ explicitly on these open pieces as the isomorphism $M_f\otimes_{A_f} N_f\rightarrow (M\otimes_A N)_f$ (this is again using the fact that tensor product commutes with localisations) and then "glue" this to get a morphism defined on any open set, which is an isomorphism on stalks since it is an isomorphism on the sections of a basis for the topology. You then still need to produce $\bar\varphi$ in the same way.
Which proof you prefer is entirely a matter of choice, they're essentially the same. The second one is probably cleaner, in some sense. The actual morphism looks nicer on each affine piece, but the price you pay is having to work slightly harder to show that the morphisms commute with restriction, depending on how happy you are to say it is "obvious".
A: Yes, there is a "categorial" proof. We formulate the following
Universal Property. Let $\mathscr{F} \times \mathscr{G}$ be the presheaf of sets $U \mapsto \mathscr{F}(U) \times \mathscr{G}(U)$. Let $f\colon \mathscr{F} \times \mathscr{G} \to \mathscr{H}$ be a map of preheaves that is $\mathcal{O}_X$-bilinear, that is, for $s \in \mathscr{F}(U)$, the map taking $t \in \mathscr{G}(U)$ to $f(U)(s,t)$ is $\mathcal{O}_X(U)$-linear, and symmetrically in $t$.
Then, we define $\mathscr{F} \otimes_{\mathcal{O}_X} \mathscr{G}$ to be the (unique) $\mathcal{O}_X$-module such that $f$ uniquely factors through $\mathscr{F} \otimes_{\mathcal{O}_X} \mathscr{G}$.
Remark. All my usual sources don't really explore this; EGAI just cites Godement (II, 2.8), who asks the reader to state the universal property, and the Stacks Project Tag 01CA doesn't precisely define what an $\mathcal{O}_X$-bilinear map of $\mathcal{O}_X$-modules is (there are probably some permutations of restrictions that I missed but I think the idea is clear).
The point is that taking global sections on an affine scheme $\operatorname{Spec}(A)$ gives you back the universal property for the tensor product of $A$-modules. You can obtain the tensor product for an arbitrary scheme by glueing as in Exercise 1.22, and the uniqueness of the factorization above.
