Category Theory
Zulip Server
Archive

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.


Stream: learning: questions

Topic: Full faithfulness of right extension functor


view this post on Zulip Tom Hirschowitz (Nov 27 2025 at 10:25):

Given a functor F:π’žβ†’π’ŸF: π’ž β†’π’Ÿ and a category Eβ„°, assuming that a pointwise right extension functor [π’ž,E]β†’[π’Ÿ,E][π’ž,β„°] β†’ [π’Ÿ,β„°] exists (typically π’žπ’ž and π’Ÿπ’Ÿ are small and Eβ„° is complete), I think that full faithfulness of FF 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?

view this post on Zulip ClΓ©mence Chanavat (Nov 27 2025 at 10:41):

I do not think this is true, say you take E \mathscr E to be the terminal category, then the right extension is the identity functor, which is fully-faithful, and this regardless of what F F is.

view this post on Zulip ClΓ©mence Chanavat (Nov 27 2025 at 11:06):

The fact that the extension is fully faithful is to say the counit of the adjunction restriction ⊣ \dashv extension is a natural iso, so if you take E \mathscr E to be Set Set , then if I didn't make any mistake, it tells you that for all copresheaf X ⁣:Cβ†’Set X \colon \mathscr C \to Set and all c c in C \mathscr C , the collection of natural transformation D(Fc,Fβˆ’)β‡’X \mathscr D(Fc, F-) \Rightarrow X is in bijection with the natural transformations C(c,βˆ’)β‡’X \mathscr C(c, -) \Rightarrow X , which does not seem to be to far from full faithfulness, but I don't know how to conclude

view this post on Zulip Nathanael Arkor (Nov 27 2025 at 12:58):

When the codomain is Set, the extension is fully faithful iff FF is: this follows from Remark 25 of Yoneda structures and KZ doctrines, for instance.

view this post on Zulip Morgan Rogers (he/him) (Nov 27 2025 at 14:09):

I'll talk about presheaves to avoid dualisation confrsion.
Given F:C→DF:C \to D, the left Kan extension [Cop,Set]→[Dop,Set][C^\mathrm{op},Set] \to [D^\mathrm{op},Set] is the free extension by colimits of FF applied to representables. The right Kan extension is fully faithful iff the left Kan extension is (general result about adjoint triples!), iff FF 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 CC and DD into these diagram categories.

view this post on Zulip Tom Hirschowitz (Nov 27 2025 at 20:26):

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?

view this post on Zulip fosco (Nov 27 2025 at 20:45):

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.

view this post on Zulip Tom Hirschowitz (Nov 27 2025 at 20:56):

Thanks @fosco, this is helpful! (Although it doesn't quite make the whole thing less intimidating... :grinning_face_with_smiling_eyes:)

view this post on Zulip Nathanael Arkor (Nov 27 2025 at 22:08):

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.

view this post on Zulip Nathanael Arkor (Nov 27 2025 at 22:10):

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).

view this post on Zulip Tom Hirschowitz (Dec 01 2025 at 16:47):

I was asking for formal category theory as a whole, but thanks for the hints!

view this post on Zulip Mike Shulman (Dec 01 2025 at 22:37):

There's definitely a gap in the literature for a nice friendly and comprehensive treatment of formal category theory with modern techniques and language.

view this post on Zulip Nathanael Arkor (Dec 02 2025 at 16:20):

Dylan and I are working on it.

view this post on Zulip Nathanael Arkor (Dec 02 2025 at 16:25):

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.