You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Given a functor and a category , assuming that a pointwise right extension functor exists (typically and are small and is complete), I think that full faithfulness of is equivalent to full faithfulness of right extension. Is this right? I've found proofs of the forward implication in the literature, but not of the converse. Does anyone know where to find one?
I do not think this is true, say you take to be the terminal category, then the right extension is the identity functor, which is fully-faithful, and this regardless of what is.
The fact that the extension is fully faithful is to say the counit of the adjunction restriction extension is a natural iso, so if you take to be , then if I didn't make any mistake, it tells you that for all copresheaf and all in , the collection of natural transformation is in bijection with the natural transformations , which does not seem to be to far from full faithfulness, but I don't know how to conclude
When the codomain is Set, the extension is fully faithful iff is: this follows from Remark 25 of Yoneda structures and KZ doctrines, for instance.
I'll talk about presheaves to avoid dualisation confrsion.
Given , the left Kan extension is the free extension by colimits of applied to representables. The right Kan extension is fully faithful iff the left Kan extension is (general result about adjoint triples!), iff is by full faithfulness of Yoneda.
It may be that the remark cited by Nathanael provides some general sufficient conditions for this argument to go through. As ClΓ©mence points out, I don't think you can expect the result to be true if there isn't an embedding of and into these diagram categories.
Ah, great, thanks to you all! I had your argument, @ClΓ©mence Chanavat, but didn't even notice it worked only with sets :upside_down: The developments of formal category theory look fascinating, but also intimidating. Is there a good entry point that you would advise?
At taltech, this semester, we are running a user friendly reading course on FCT. We started with the fundamentals of yoneda structures, and then explored a little bit Wood's proarrow equipments.
I believe nowadays most of the classical material (especially on equipments) is subsumed by virtual double categories (for which @Mike Shulman and @Geoff Cruttwell paper is the best introduction from scratch); for Yoneda structures, Street-Walters paper is still a good introduction; Weber's "2-topoi" paper has an introductory section in more modern language. A large chapter of the story is the role of internal fibrations for category theory, for which there is a lot of material scattered over different sources ("conspectus of variable categories" as well as Street's papers on fibrations).
The people I mentioned, and @Nathanael Arkor , can add more references :-) I am learning from them myself.
Thanks @fosco, this is helpful! (Although it doesn't quite make the whole thing less intimidating... :grinning_face_with_smiling_eyes:)
If you're asking in the context of Walker's paper, understanding the formal category theory is entirely unnecessary: the proof in Walker's paper just uses properties of left extensions, which can be unwound for the presheaf construction directly.
But for the "left extension is fully faithful implies the original functor was fully faithful" direction, you only need local full faithfulness of the presheaf construction, together with pseudonaturality of the Yoneda embedding (i.e. the first sentence of Walker's Remark 25).
I was asking for formal category theory as a whole, but thanks for the hints!
There's definitely a gap in the literature for a nice friendly and comprehensive treatment of formal category theory with modern techniques and language.
Dylan and I are working on it.
Tom Hirschowitz said:
I was asking for formal category theory as a whole, but thanks for the hints!
I'm going to give a biased response, but I think The formal theory of relative monads demonstrates many of the fundamentals of formal category theory in a modern setting, and spells out how everything specialises in a motivating example (namely, enriched category theory). It wasn't specifically written as an introduction to formal category theory, but in the interim, before such a text is ready, my hope is that it does serve as an entrypoint.