During the course of trying to solve Vakil Exercise 13.1.F I decided I wanted to prove the following:
Suppose $X$ is a ringed space with structure sheaf $\mathscr{O}_X$. Suppose $\mathscr{F}, \mathscr{E}$ are $\mathscr{O}_X$-modules and $\mathscr{E}$ is locally free of finite rank. Then
$$
\mathscr{F} \otimes \mathscr{E}^\vee \cong \mathcal{Hom}(\mathscr{E}, \mathscr{F})
$$
Vakil 13.7.B has us prove this in less generality, but it also mentions that the result above should hold. This should follow from the corresponding fact for modules. I couldn't find this result on the Stacks Project or elsewhere online. How do you prove it?
(I am almost certain Vakil doesn't intend 13.1.F to be solved the way I am trying to solve it given the fact that he has us prove a less general version of the result later.)
EDIT: 13.1.F becomes 14.2.F in the December 2022 version of Vakil.
Best Answer
I am going to expalin how I think of giving very formal and organised proofs for these kind of results. There are two steps:
This "method" can be repeated on other proofs, for example if one tries to show that $\mathscr E^{\vee \, \vee} = \mathscr E$ for a locally free sheaf $\mathscr E$.
On the left you have a tensor product. Tensor products $\mathscr F \otimes \mathscr G$ are defined as sheafifications of some presheaf, which I will denote $\mathscr F \otimes_{pSh} \mathscr G$ so they are a little bit difficult to deal with. However, remember the universal property of sheafification:
$$\text{Hom}(\mathscr F^+, \mathscr G) = \text{Hom}(\mathscr F , \mathscr G)$$
which, in more down to earth words says that to give a morphism from the sheafification of a presheaf $\mathcal F$ to another sheaf $\mathcal G$ is the same as giving one from $\mathcal F$ to $\mathcal G$. Therefore, we have the task of defning a morphism $\varphi : \mathscr{F} \otimes_{psH} \mathscr{E}^\vee \to \mathcal{Hom}(\mathscr{E}, \mathscr{F})$. Note that we know the value of both presheaves on any open set (because we are now dealing with the presheaf tensor product), so we just need to define a natural $\mathcal O(U)$-linear map
$$\mathscr{F}(U) \otimes_{\mathcal O(U)} \text{Hom}_{\mathcal O_U}(\mathscr{E}_U, \mathcal O_U) \to \text{Hom}_{\mathcal O_U}(\mathscr{E}_U, \mathscr{F}_U)$$
Which is very natural:
$$ (*) \qquad s \otimes f \longmapsto \, (t \mapsto f(t) s) \in \text{Hom}_{\mathcal O_U}(\mathscr{E}_U, \mathscr{F}_U)$$
These maps clearly constitute a morphism of sheaves (they look so natural, its is clear that they commute with restrictions) and therefore putting everything together we obtain the desired morphism $\hat\varphi:\mathscr{F} \otimes \mathscr{E}^\vee \to \mathcal{Hom}(\mathscr{E}, \mathscr{F})$, corresponing to $\varphi$
Before the edit, I was going to prove that the map is an isomorphism on stalks, but one needs to prove first that $(\mathcal{Hom}(\mathscr{E}, \mathscr{F}))_p = \text{Hom}_{\mathcal O_p}(\mathscr{E}_p, \mathscr{F}_p)$ and this is not trivial. However, it is enough to show that $\varphi$ is an isomorphism on a covering of $X$. Since $\mathscr{E}$ is locally free, for the remainder of the proof it is enough to assume that $\mathscr{E}=\mathcal O_X^{\oplus n}$. In this case, we can factor $\varphi$ as
$$\mathscr{F} \otimes_{pSh} \mathscr{E} ^\vee \stackrel{\cong}{\longrightarrow} \left( \mathscr{F} \otimes_{pSh} \mathcal O_X ^\vee\right)^{\oplus n} \longrightarrow \left( \mathcal{Hom} (\mathcal O _X ,\mathscr F)\right)^{\otimes n} \stackrel{\cong}{\longrightarrow} \mathcal{Hom}(\mathscr{E}, \mathscr{F}),$$
where the left and right arrows are isomorphisms, so one reduces to the case $n=1$. In this case, the isomorphism can be checked on any open subset $V$, and using that
$$\mathcal{Hom}(\mathcal O_X , \mathscr F) (V) = \text{Hom}_{\mathcal O_X(V)}(\mathcal O_X(V) , \mathscr F (V))$$ $$\mathcal{Hom}(\mathcal O_X , \mathcal O_X) (V) = \text{Hom}_{\mathcal O_X(V)}(\mathcal O_X(V) , \mathcal O_X(V))$$
and the notation $M=\mathscr F(V)$, $R= \mathcal O_X(V)$, it is equivalent to checking that the $R$-module homomorphism
$$M \otimes_R \text{Hom}_R(R, R) \to \text{Hom}_R(R, M)$$
Given in a similar fashion as in $(*)$ is an isomorphism