Where do all these projection formulas come from? I have been intrigued for a long time by the formal similarity of results from different areas of mathematics. Here are some examples.
Set theory Given a map $f:X\to Y$ and subsets $X' \subset X, Y'\subset Y$, we have $$f(f^{-1}(Y')\cap X')=Y'\cap f(X')$$
Ringed spaces Given a morphism of ringed spaces $f:X\to Y$,  an $\mathcal O_X$-module $\mathcal F$ and a locally free module of finite type $\mathcal L$, we have
$$f_\ast(f^\ast{\mathcal L}\otimes_{\mathcal O_X} \mathcal F)=\mathcal L  \otimes_{\mathcal O_Y} f_{\ast}\mathcal F$$
Topology Consider a proper continuous map of connected oriented manifolds $f:X\to Y$, then for $x\in H^\ast _c(X,\mathbb Z)$ and $y\in H^\ast _c(Y ,\mathbb Z)$ we have (Dold, p.314)
$$ f_!(f^\ast y . x)=y. f_!(x)$$
Chow rings Given a proper map $f:X\to Y$ between nonsingular algebraic varieties and cycle classes $a\in CH^\ast(X), \beta \in  CH^\ast(Y)$ we have
$$ f_\ast(f^\ast \beta . \alpha)=\beta. f_\ast(\alpha) $$
K-theory  Given a proper morphism of finite Tor dimension $f:X\to Y$ between schemes (and assuming $X$ and $Y$ have suitable ample line bundles), Quillen proved in his fundamental article on higher K-theory  (Springer LNM 341, page 126) that for $x\in K_0(X)$ and $y\in K'_0(Y)$ 
$$f_\ast(f^\ast y . x)=y. f_\ast (x) $$
Derived categories Given a ring morphism $f:R\to S$, a bounded above complex $A$ of $R$-modules  and a complex $B$ of $S$-modules we obtain in $\mathbb D(R)$ (Weibel, p.404)
$$  f_\ast(\mathbb L f^\ast( A) \otimes_S^{\mathbb L} B)=A \otimes_R^{\mathbb L} (f_\ast B)$$
The question Of course I'm well aware that there are strong links between say K-theory and Chow rings and that the examples of projection formulas are not independent. What I would like to know is whether there is some general context of which these examples could be said to be illustrations, even if not particular cases in the strict sense. An analogy would be that Grothendieck's Galois theory explains the similarity between the traditional Galois theory of fields and the theory of covering spaces although it is not true that the general theory of topologiclal coverings is a special case of Grothendieck's results.
Edit After seeing several comments and an answer, I'd like to clarify my question. It is not principally to find a general formulation of which all those results would be a special case (although that certainly would be nice). But rather to know if there is a powerful, presumably tough,  result or theory  which would imply a good deal of the examples mentioned above. Perhaps a bit like K-theory used  for Riemann-Roch , Bott periodicity, classification of vector bundles...   
 A: Perhaps some of these formulae have allegory theory (or a generalization thereof) lurking in the background? In particular, recall Freyd's modularity law:
$$R(R^\dagger A \cap B) \supseteq A \cap RB$$
Now suppose that $f$ is a partial map, meaning that $ff^\dagger \subseteq \mathrm{id}_Y.$ Then
$$f(f^\dagger A \cap B) \subseteq ff^\dagger A \cap fB \subseteq A \cap fB$$
So, for $f$ a partial map between sets, we have:
$$f(f^\dagger A \cap B) = A \cap fB$$
for any relations $A$ and $B$ with appropriate domains and codomains. Taking the domains of these relations to be the set $1$ yields the desired result.
A: There is a very nice article by Peter May et al. which is all concerned with this question:


*

*H. Fausk, P. Hu, Peter May, Isomorphisms between left and right adjoints, Theory and Applications of Categories , Vol. 11, 2003, No. 4, pp 107-131. (http://www.tac.mta.ca/tac/volumes/11/4/11-04abs.html)


The article cleanly identifies three different flavors of Grothendieck's "yoga of six operations". One is the "Grothendieck context" which is governed by the projection formula for $f_\ast$ and another is the "Wirthmüller context" which all revolves around the projection formula involving $f_!$. I have extracted some aspects at: http://ncatlab.org/nlab/show/Wirthmueller+context 
The projection formula for $f_!$ is equivalent to the statement that the strong monoidal functor $f^\ast$ is also a strong closed functor. 
This setup, an adjoint triple $(f_! \dashv f^\ast \dashv f_\ast)$ between symmetric closed monoidal categories (or derived categories, $\infty$-categories) such that $f^\ast$ is strong monoidal and in addition the projection formula aka Frobenius reciprocity aka strong closedness holds turns out to be a fundamental notion way beyond the geometric context in which Grothendieck-Verdier duality was originally and is still traditionally considered. Indeed, this is precisely the setup that logicians/type theorists would call dependent linear type theory, it turns out. That may or may not seem illuminating to you (I don't know) but it shows in a way just how "foundational" this phenomenon is.
A: The first (set theory) formula is generalised in categorical logic to what is called "Frobenius reciprocity" there, and is then part of the handling of the existential quantifier (a natural way to go from "projection", in fact). It fits in with some category theory from the 1960s (Beck). Treating the existential quantifier axiomatically goes back to Halmos (classical logic though, and a bit earlier). See http://ncatlab.org/nlab/show/Frobenius+reciprocity for how it looks these days.
The "school of Eilenberg-Mac Lane" and "school of Grothendieck" tend to have different approaches to categorical heuristics; roughly speaking you seem to be asking in the spirit of Mac Lane's "functionalism" the standard question "if structure X occurs in many places in mathematics, shouldn't there be a general abstract theory?" 
