Day convolution and sheafification

Question

$\DeclareMathOperator\Psh{Psh}\DeclareMathOperator\Sh{Sh}\newcommand\copower{\mathrm{copower}}$I was looking through Bodil Biering's thesis On the Logic of Bunched Implications - and its relation to separation logic, and became confused by the following Day convolution argument in Lemma 4.3.1. The statement of the lemma includes the isomorphism in \eqref{462744_1} below.

Consider a site $C$ which is also monoidal, with tensor product $\cdot : C \times C \to C$. We have a geometric embedding $\mathbf{a} \dashv i : \Sh(C) \hookrightarrow \Psh(C)$, so $\mathbf{a}$ is the sheafification functor, and $i$ the inclusion of sheaves to presheaves. Also let $\mathbf{y}: C \to \Psh(C)$ be the Yoneda embedding. The proof of Lemma 4.3.1 has a chain of equations/isomorphisms: \begin{align} \mathbf{a}\left(i\mathbf{a} P \otimes Q\right) &= \mathbf{a} \left( \int^{n,n'}_{\text{Psh}(C)} i \mathbf{a} P(n) \times Q(n') \times \mathbf{y}(n \cdot n')\right) \\ &\cong \int^{n,n'}_{\text{Sh}(C)} \mathbf{a} i \mathbf{a} P(n) \times \mathbf{a}Q(n') \times \mathbf{a}\mathbf{y}(n \cdot n')\tag{1}\label{462744_1}\\ &\quad\vdots\\ &\cong\mathbf{a}(P \otimes Q). \end{align} Biering notes that this isomorphism is a consequence of the property that $\mathbf{a}$ preserves colimits and finite limits. It makes sense that the co-continuity of $\mathbf{a}$ allows it to be brought inside of the coend. I am struggling to understand where is the finite limit (which allows $\mathbf{a}$ to be applied to all factors?).

Here is my incomplete understanding of the coend. The Day convolution of two presheaves $F,G : C^\text{op} \to \mathbf{Set}$ is a coend $\int^{n,n' : C} H\left(\langle n,n' \rangle,\langle n,n' \rangle \right)$, where $H$ is the profunctor $(C \times C)^\text{op} \times (C \times C) \to \Psh(C)$ given by the composition $$ (C \times C)^\text{op} \times (C \times C) \xrightarrow{F \boxtimes G} \mathbf{Set} \times (C \times C) \xrightarrow{\mathbf{y} \circ \cdot} \mathbf{Set} \times \Psh(C) \xrightarrow{\copower} \Psh(C), $$ where $F \boxtimes G$ is the presheaf $(C \times C)^\text{op} \to \mathbf{Set}$ given by $(F \boxtimes G)\langle n , n' \rangle = F(n) \times G(n')$, and $\copower : \mathbf{Set} \times \Psh(C) \to \Psh(C)$ is the coproduct $$ \copower(A,F) = \coprod_{\_ \in A} F. $$ If we apply the functor $\mathbf{a}$ to the result, we are taking the coend of the profunctor: $$ (C \times C)^\text{op} \times (C \times C) \xrightarrow{F \boxtimes G} \mathbf{Set} \times (C \times C) \xrightarrow{\mathbf{y} \circ \cdot} \mathbf{Set} \times \Psh(C) \xrightarrow{\copower} \Psh(C) \xrightarrow{\mathbf{a}} \Sh(C), $$ which (I think), when setting $F = i \mathbf{a} P$ and $G = Q$, corresponds to the "integral" $$ \int^{n,n'}_{\Sh(C)} i\mathbf{a}P(n) \times Q(n') \times \mathbf{a}\mathbf{y}(n\cdot n').\tag{2}\label{462744_2} $$ It seems that the product in coend \eqref{462744_1} is not a product of presheaves (hence not a finite limit in $\Psh(C)$). Instead it is consequence of how the usual copowering over $\mathbf{Set}$ is a generalization of the Cartesian product.

Perhaps there is something wrong with the above paragraph, or perhaps there is an isomorphism from \eqref{462744_1} to \eqref{462744_2}?

Answer 1

$\require{AMScd}$I would say that the fact that $\bf a$ commutes with products is what allows you to apply it to all factors of the coend, but a more precise way to use its properties would be that $${\bf a}((Pn\times Qm)\cdot \hom(-,n\otimes m))\cong ({\bf a}Pn\times {\bf a}Qm)\cdot \hom(-,n\otimes m),$$ even if the copower operation in this specific case coincides with products.

Would you be interested in a different proof?

I'll give you two alternative proofs. Somehow I can't find totally satisfying the argument you're supposed to follow (but the statement is true, no doubt about it!)

Alternative proof 1 is based on cocontinuity of $\bf a$, plus the fact that ${\bf a}(P\times Q)\cong {\bf a}P \otimes Q$ where $P,Q$ are presheaves, $\bf a$ is sheafification, $\otimes$ is Day convolution (induced by a monoidal structure $\_\cdot\_$ on the domain of presheaves). Note that $P\otimes Q$ is a left Kan extension, precisely the left Kan extension of $P\times Q : C\times C \to Set \times Set \overset\times\to Set$ along $\_\cdot\_ : C\times C\to C$. But then, $${\bf a}(P \otimes Q) = {\bf a}(\text{Lan}_{(\_\cdot\_)}(P\times Q))\cong \text{Lan}_{(\_\cdot\_)}{\bf a}(P\times Q)\cong {\bf a}P\otimes Q$$ and now, clearly, also ${\bf a}(i{\bf a}P\otimes Q)$ is isomorphic to ${\bf a}P\otimes Q$ as well.

An alternative proof 2 relies, instead, on recognizing that the isomorphism you want is obtained applying sheafification $\bf a$ to a canonical morphism (this is mentioned in the thesis as well!). But given this, you can characterize completely the morphisms that sheafification sends to isomorphisms: given $f : A\to B$, the arrow ${\bf a}(f)$ is an iso if and only if, for every sheaf $R$, in the diagram $$\begin{CD} A @>q>> R \\ @VfVV @.\\ B \end{CD}$$ there is a unique $B\to R$ closing the triangle. Now, in your case $f = \eta_P\otimes Q : P\otimes Q \to i{\bf a}P\otimes Q$. You can easily prove that given a sheaf $R$, the condition above is satisfied.