Beck-Chevalley via coend-calculus

283 Views Asked by At

Consider the following commutative square in $\bf Cat$; strictness can be removed from the initial assumptions, but let's proceed gradually.

enter image description here

Consider the induced diagram between presheaves

enter image description here

Beck-Chevalley isomorphism now says that the iso $$k^* f^* \cong h^* g^*$$ (induced by functoriality) induces another isomorphism $$h_! k^* \cong g^* f_!,$$ namely $$ \text{Lan}_f(P)\circ g \cong \text{Lan}_h(P\circ k) $$ for each $P\colon \mathbf{B}\to \bf Set$; I like to rephrase this isomorphism as the isomorphism of coends $$ \int^B \mathbf{A}(fB, gC)\times PB\cong \int^D \mathbf{C}(hD, C)\times P(kD) $$

Is there a way to prove this by coend-fu?

1

There are 1 best solutions below

3
On

As already mentioned in the comments, the Beck-Chevalley condition is not automatically satisfied; so you won't be able to show $g^* f_{!} \cong h_{!} k^*$. But you can construct a morphism $ h_{!} k^* \to g^* f_{!}$ using coends: For $P : \mathcal{B} \to \mathsf{Set}$, we have:

$$(h_{!} k^*)(P) = \int^{\mathcal{D}} \hom_\mathcal{C}(h(D),-) \times P(k(D))$$ $$(g^* f_{!})(P) = \int^{\mathcal{B}} \hom_\mathcal{A}(f(B),g(-)) \times P(B)$$

First, we have a canonical morphism of functors $$\hom_\mathcal{C}(h(D),-) \to \hom_{\mathcal{A}}(g(h(D)),g(-)) \cong \hom_\mathcal{A}(f(k(D)),g(-)),$$ which induces a morphism from $(h_{!} k^*)(P)$ to $$\int^{\mathcal{D}} \hom_\mathcal{A}(f(k(D)),g(-)) \times P(k(D)).$$ But this has an obvious "substitution" morphism to $$ \int^{\mathcal{B}} \hom_\mathcal{A}(f(B),g(-)) \times P(B),$$ that is, $(g^* f_{!})(P)$. A sufficient condition for $h_{!} k^* \cong g^* f_{!}$ is that $g$ and $k$ are fully faithful, as can be seen directly from the construction above.

By the way, $\mathsf{Set}$ can (should?) be replaced by any cocomplete category and $\mathcal{B},\mathcal{D}$ should be assumed to be small; otherwise $f_{!}$ and $h_{!}$ won't exist (even for $\mathsf{Set}$). Also, in order to construct a morphism of functors $h_{!} k^* \to g^* f_{!}$, we actually don't need $g h \cong f k$ (or even $gh=fk$); a morphism $fk \to gh$ suffices.