Solution (source code)

= Solution

The <affine module sheaf> construction makes the remaining statements explicit. For $A=k[V]$ and an $A$-module $M$, define
$$
\widetilde M(D(f))=M_f
$$
on the <basis> of <principal open subsets>. Restrictions are the natural <localization> maps. Equivalently, a section on an arbitrary <open set> is a family $s_P\in M_{\mathfrak m_P}$ which near each point is represented by a single fraction $m/f^r$, with $f$ nonvanishing throughout that neighbourhood. This locally representable family construction gives a <sheaf>; the usual <localization> gluing verifies its <quasi-coherence>. Its <stalk> is $M_{\mathfrak m_P}$ and
$$
\boxed{\Gamma(V,\widetilde M)=M}.
$$
This last identification is precisely the standard module-localization gluing on the affine <basis>, not an assertion that arbitrary <sheaves> are determined by their global sections.

Now write $A=k[X]$, $B=k[Y]$ and $\alpha=\phi^\#:A\to B$. Let $\mathcal G=\widetilde M$, $\mathcal H=\widetilde N$ for $A$-modules $M,N$, and let $\mathcal F=\widetilde L$ for a $B$-module $L$. The affine versions of the three constructions are
$$
\boxed{\mathcal G\otimes_{\mathcal O_X}\mathcal H\cong\widetilde{M\otimes_A N},\qquad
\phi_*\mathcal F\cong\widetilde{{}_A L},\qquad
\phi^*\mathcal H\cong\widetilde{B\otimes_A N}}.
$$
Here ${}_A L$ denotes restriction of scalars along $\alpha$, whereas the last associated <sheaf> lives on $Y$. To verify the tensor-product assertion, localize at every prime: both <stalks> are $M_{\mathfrak m}\otimes_{A_{\mathfrak m}}N_{\mathfrak m}$. For the <direct image>, $\phi^{-1}D(a)=D(\alpha(a))$, and
$$
\Gamma(D(a),\phi_*\widetilde L)=L_{\alpha(a)}=({}_A L)_a.
$$
These equalities identify the <sheaves> on a <basis> and respect restrictions. For the <pullback of a sheaf of modules>, its <stalk> at $Q$ is $B_{\mathfrak m_Q}\otimes_A N$, exactly the <stalk> of $\widetilde{B\otimes_A N}$. The local tensor maps are compatible, so these <stalk> identifications come from an actual <sheaf> isomorphism. Thus all three constructions are <quasi-coherent> in the stated affine setting.

Finally construct the natural <projection formula for sheaves> map by sending a local tensor $m\otimes b$ to $b(1\otimes m)$ in the pulled-back <module>, followed by <direct image>. In the affine description, the target $\phi_*\phi^*\widetilde M$ is the <sheaf> associated with the $A$-module ${}_A(B\otimes_A M)$, while $\widetilde M\otimes_{\mathcal O_X}\phi_*\mathcal O_Y$ corresponds to $M\otimes_A B$. The maps
$$
m\otimes b\longmapsto b\otimes m,\qquad b\otimes m\longmapsto m\otimes b
$$
are inverse $A$-linear maps. Localizing them commutes with every restriction, proving
$$
\boxed{\phi_*\phi^*\widetilde M\cong
\widetilde M\otimes_{\mathcal O_X}\phi_*\mathcal O_Y}.
$$
No flatness assumption on $A\to B$ or finiteness assumption on $M$ is needed.