This is a follow-up to this question:
[Reduction to graph subgroups for Bredon homology when the $G\_1\times G\_2$ is $G\_2$-free](https://mathoverflow.net/questions/395183/reduction-to-graph-subgroups-for-bredon-homology-when-the-g-1-times-g-2-is-g/395285#395285)


In his (very nice) answer Gregory Arone stated the following fact. Let $Q:\mathcal{C}\_0\to\mathcal{C}$ be a functor between locally small categories. Then there is adjunction between functor categories
$$
Q\_!\colon[\mathcal{C}\_0,\mathcal{D}]\leftrightarrows[\mathcal{C},\mathcal{D}]\colon Q^\ast,
$$
where $Q^\ast$ is a precomposition with $Q$ and $Q\_!$ is the left Kan extension (I hope I have the correct notation). Now if we have functors $F\colon\mathcal{C}\_0\to\mathcal D$ and $G\colon\mathcal{C}^{op}\to\mathcal{D}$, then there is an isomorphism of coends:
$$
F\otimes\_{\mathcal{C\_0}}Q^\ast G\cong Q\_!F\otimes\_{\mathcal{C}}G.
$$


So my question is: how to prove this isomorphism? And is it something coming from having just an djoint pair of functors, or it applies only to this particular setting - i.e., we have a functor and its left Kan extension?


P.S. If this is a simple fact, reference will also do.



Isomorphism of coends
Knowing that $Q\_!F : y\mapsto \int^z \hom(Qz,y)\otimes Fz$ (this is often called "pointwise formula" for Kan extensions) it is easy to derive the isomorphism in question:
$$
\begin{align}
Q\_!F\;\otimes\_{\cal C\_0} G& := \int^y Q\_!F(y)\otimes Gy \\ 
&\cong \int^y \int^z \hom(Qz,y)\otimes Fz \otimes Gy \\ 
&\cong \int^z Fz\otimes \left( \int^y \hom(Qz,y)\otimes Gy\right)\\ 
&\cong \int^z Fz\otimes GQ(z) \\ 
& = F \;\otimes\_{\cal C\_0} GQ = F \;\otimes\_{\cal C\_0} Q^\*G
\end{align}
$$


