5
$\begingroup$

I've been trying to write down a proof of Di Liberti's Kan lemma fortissimo on the existence of left Kan extensions, given as Lemma 3.3 in the nLab entry on Kan extensions. Let $F : \mathcal{A} \to \mathcal{B}$ be a functor with $\mathcal{A}$ and $\mathcal{B}$ locally small, and $y : \mathcal{A} \to \widehat{\mathcal{A}}$ be the Yoneda embedding of $\mathcal{A}$ into its category of small presheaves. I'm having trouble with the implication:

If $\mathrm{Lan}_Fy$ exists (and is pointwise), then $\mathcal{B}(F-,b)$ is a small presheaf for every $b \in \mathcal{B}$.

My problem is that I don't know how large colimits in $\widehat{\mathcal{A}}$ are computed when they exist. Here is what I do know:

The density formula says that, for all $a \in \mathcal{A}$ and $G : \mathcal{A}^\mathrm{op} \to \mathbf{Set}$, we have an isomorphism of sets $$Ga \cong \int^{a' \in \mathcal{A}} \mathcal{A}(a,a') \times Ga'$$ natural in $a$ and $G$. Given a functor $D : \mathcal{I} \to [\mathcal{A}^\mathrm{op} ,\mathbf{Set}]$, if $\mathrm{ev}_a D : \mathcal{I} \to \mathbf{Set}$ has a colimit for each $a \in \mathcal{A}$, then these can be put together into functor $\mathcal{A}^\mathrm{op} \to \mathbf{Set}$ that is the colimit of $D$. This follows e.g. from Theorem 6.2.5 in Leinster's Basic Category Theory (the smallness hypotheses are not used in the proof, as far as I can tell). In our case, this means that we can promote the density formula to an isomorphism of functors $$G \cong \int^{a' \in \mathcal{A}} \mathcal{A}(-,a') \times Ga',$$ where the coend is taking place in $[\mathcal{A}^\mathrm{op} ,\mathbf{Set}]$.

If $G$ is a small presheaf, then this coend is reflected along the embedding $\widehat{\mathcal{A}} \hookrightarrow [\mathcal{A}^\mathrm{op} ,\mathbf{Set}]$, so we can see it as a coend in $\widehat{\mathcal{A}}$. In general, small colimits in $\widehat{\mathcal{A}}$ are computed pointwise, because a small colimit in $[\mathcal{A}^\mathrm{op} ,\mathbf{Set}]$ of small presheaves is a small presheaf.

However, if instead we are given that the (a priori) large coend $$\int^{a'\in\mathcal{A}} \mathcal{A}(-,a') \times Ga'$$ in $\widehat{\mathcal{A}}$ exists, can we conclude that it is isomorphic to $G$ and, thus, that $G$ is small?

If the answer is yes, then taking $G = \mathcal{B}(F-,b)$ proves the implication I quoted. Alternatively, is there a different approach to proving the implication that avoids this problem?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
4
$\begingroup$

I am happy to see that people are interested in this subject. Let me answer your question, and welcome you to the general topic of Yoneda structures :).

The main point is that by rebooting the proof of Prop. A.6 in the paper Codensity: Isbell duality, pro-objects, compactness and accessibility for the case of small presheaves, one sees that if $\mathrm{lan}_fy$ exists it has to coincide with $\mathcal{B}(f-,=).$ Then you are essentially done.

Improve this answer
$\endgroup$
3
  • 3
    $\begingroup$ It would be helpful to give an explicit proof in your answer, because the proof of Proposition A.6 makes use of the fact that $B$ is cocomplete, which is not assumed here. $\endgroup$
    – varkor
    Commented Sep 26 at 12:43
  • 2
    $\begingroup$ If $B$ is not complete, prolong the diagram with $A \to B \to P(B)$ with the small presheaf construction of B and observe that $P(B)(fy_B-,-) \circ y_B = B(f-,-)$. Now you are cocomplete and the argument runs for $P(B)(fy_B-,-)$. $\endgroup$
    – Ivan Di Liberti
    Commented Sep 26 at 13:54
  • $\begingroup$ Thanks! Through the argument in Prop A.6, I can see that if $\mathrm{lan}_y f$ has a right adjoint, then that must be $\mathcal{B}(f-,-)$. My problem is now showing that if $\mathrm{lan}_f y$ exists, it must be said right adjoint. I can see that $\mathrm{lan}_{\mathrm{lan}_y f} 1_{\widehat{\mathcal{A}}} = \mathrm{lan}_f y$, but how do we know that $\mathrm{lan}_y f$ preserves this extension? $\endgroup$
    – AdrianDoM
    Commented Sep 27 at 15:30

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .