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?
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.