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.
John Onstead (Apr 23 2024 at 14:45):On the nlab page for proarrow equipments, it states that the reason why some V-Cat need proarrow equipments to fully do category theory within is because they may lack comma objects. Specifically it states that in Cat, "hom-functors can be recovered by looking at comma categories... in some sense this is what all the above internalizations are secretly doing" with the "above internalizations" referring to concepts like limits, fully faithful morphisms, and pointwise kan extensions. My first question is: how is it that you can recover hom functors and related internalizations in Cat from the comma categories? Is it really as simple as finding the comma category (a/b) for C (with a and b functors from the terminal category picking out the objects a and b in C), or is something else at work?
Secondly, not all categories V-Cat have all comma objects. However, any category can be "upgraded" easily into one with all limits, including comma objects, by taking the Yoneda embedding into the presheaf category. In this case, we can find the 2-category [V-Cat^op, Cat] and the Yoneda embedding y: V-Cat -> [V-Cat^op, Cat]. This does have all comma objects. So why do we need proarrow equipments when we could just do this operation to "uncover" the "hidden" comma objects of any V-Cat, and then we can do all internalizations with that?
Nathanael Arkor (Apr 23 2024 at 15:34):The basic issue is that many aspects of category theory rely on being able to talk about hom-sets, e.g. full faithfulness, the hom-set isomorphism characterisation of adjunctions, etc. In formal category, we therefore need some way to talk about these aspects without being able to "look inside" our objects and see that they contain a notion of morphism in them (just like how we don't want to look inside the objects of the category of sets to see that they contain elements).
For instance, if we want to talk about full faithfulness, we need to represent in some way a collection of morphisms . How can we do this? Well, it depends on what we understand to represent. One obvious candidate is the comma category . This seems reasonable, because we know, following Lawvere, that many aspects of category theory that rely upon hom-sets can be reformulated in terms of comma categories. However, there is a problem with this approach when we do enriched category theory. The problem is not about the existence of comma objects: rather, it is that comma objects do not suffice to faithfully capture the aspects of enriched category theory that involve hom-objects. Intuitively, this is because comma objects capture structure described by individual morphisms in a category, but individual morphisms in an enriched category (meaning morphisms of the form in the base of enrichment) do not suffice to capture all of the structure of the hom-objects in general. For instance, it is not true that we can capture enriched full faithfulness using (enriched) comma categories.
Another candidate for capturing these aspects is the notion of distributor/profunctor, which is the approach taken for proarrow equipments. In contrast to comma objects, it turns out that these do suffice to capture the structure of hom-objects in enriched category theory. (Alternatively, presheaf categories also suffice, essentially because they represent distributors, and this is the approach taken by Yoneda structures.)
Nathanael Arkor (Apr 23 2024 at 15:37):John Onstead said:
My first question is: how is it that you can recover hom functors and related internalizations in Cat from the comma categories? Is it really as simple as finding the comma category (a/b) for C (with a and b functors from the terminal category picking out the objects a and b in C), or is something else at work?
Essentially yes, though you usually want to work with [[generalised elements]] rather than [[global elements]]. For instance, Lawvere proved that if and only if and this isomorphism is concrete over the product category. So the hom-set formulation of an ordinary adjunction can be captured 2-categorically. However, this technique does not work for enriched adjunctions for the reasons explained above.
Nathanael Arkor (Apr 23 2024 at 15:44):Unfortunately, although it was already realised in the late 1970s – mid 1980s that 2-categories and property-like structure does not suffice for formal category theory (at least if intended to capture enriched category theory), you can find a lot of subsequent 2-categorical literature that ignores this, and therefore establishes theorems at a weaker level of generality than would be natural with proarrow equipments or related structures.
John Onstead (Apr 23 2024 at 19:42):Ah thanks for all the help!
Nathanael Arkor said:
Unfortunately, although it was already realised in the late 1970s – mid 1980s that 2-categories and property-like structure does not suffice for formal category theory (at least if intended to capture enriched category theory), you can find a lot of subsequent 2-categorical literature that ignores this, and therefore establishes theorems at a weaker level of generality than would be natural with proarrow equipments or related structures.
I guess this explains why extra "structure" or "stuff" is needed to do this, like in a Yoneda Structure or Proarrow Equipment!