Equipments
Posted by Mike Shulman
I mentioned in my intro that as wonderful as -categories are, they’re really just one (important) part of the zoo of “higher categorical structures” out there. Today I want to tell you about another inhabitant of that zoo: a wonderful gadget called a proarrow equipment (or just an equipment), which lets us do what I call “formal category theory.” Equipments don’t seem to be very well-known, especially in the northern hemisphere (even though their inventor, R.J. Wood, is a Canadian at Dalhousie), but there are some indications that they’re gaining ground, so I’m doing my best to help them along.
This post will be a lightning-fast introduction to formal category theory in equipments. But I’m going to present the definition in a nonstandard way, because it turns out that an equipment is basically the same as what I’ve called a framed bicategory, and I find that way of thinking about it more natural—and also easier to generalize (but that’s another post). Some of it may go by a little quickly, but I think it’s the sort of thing that’s really quite fun to work out yourself once you’ve been pointed in the right direction.
What do I mean by formal category theory? This is an analogy to the way in which category theory can be called “formal mathematics.” That is, we see ourselves doing the same thing all the time in mathematics (limits, colimits, adjoints, universal constructions) and we write down category theory in order to do all those things formally, once and for all in abstract generality. But nowadays there are actually lots of kinds of category theory too: ordinary category theory, enriched category theory, internal category theory, fibered category theory, etc. After a while, one starts to get the feeling of “doing the same thing all the time” again: defining limits and colimits, proving adjoint functor and monadicity theorems, etc. So, can we “formalize” the essential aspects of category theory in an analogous way, and if so, how?
You might expect the answer to be “yes, with 2-categories.” Perhaps surprisingly, however, 2-categories don’t always suffice. We can do a lot of category theory in a 2-category: we can define adjunctions, construct Eilenberg-Moore and Kleisli objects for monads (the “formal theory of monads”), and talk about Kan extensions, comma objects, fibrations, and so on. But some things are missing, and some of the general notions are not always quite right. For instance, the most obvious 2-categorical analogue of a limit is a Kan extension, since in ordinary category theory limits can be identified with Kan extensions along functors to the terminal category. However, in enriched category theory this is insufficient; not all weighted limits arise in that way. Moreover, the “internal” notion of Kan extension in a 2-category gives the “weak” notion rather than the more important “pointwise” one.
The central observation is that what’s missing from the 2-category is hom-functors, and more generally profunctors. Recall that a profunctor (aka “distributor” or “(bi)module”) is a functor (or to , if and are -enriched). Including profunctors in our “structure for formal category theory” will allow us to talk about their representability, which is the essential ingredient for limits, pointwise Kan extensions, and all the other things that are missing from a 2-category.
So what kind of formal structure includes categories, functors, and profunctors? There are several different answers, but to me, the most obvious and natural-looking answer is a double category. Specifically, there’s a double category whose objects are small categories, whose vertical arrows (which we’ll just call “arrows”) are functors, whose horizontal arrows (which we’ll call “proarrows”) are profunctors, and whose squares are transformations natural in and . Composition of profunctors is by a coend: (note that I’m writing it in diagrammatic order) and the identity profunctor of is its hom-profunctor . The 2-categories and can be recovered from as its vertical and horizontal 2-categories, respectively, which I’ll write as and . (For , this is basically by definition; for , it’s a nice exercise in the Yoneda lemma.)
Similar double categories exist for all the other kinds of category theory (enriched, internal, fibered, etc.). Moreover, all these double categories have an additional very important property: given any “niche” there exists a “universal” or “cartesian” filler square with the property that any other square factors through the universal one uniquely: The profunctor is of course just . We say that a double category having this property equips the 2-category with proarrows, and speak of the whole double category as a proarrow equipment, or just an equipment.
Of particular importance in an equipment are the proarrows and , which exist for any arrow . By factoring the identity square through the universal fillers that define and , we obtain additional squares such that the composites are both equal to . And using the uniqueness of factorization through the universal squares, we can conclude moreover that the composites are equal to the identity squares of and respectively. In double-category lingo which I adopted from Dawson, Paré, and Pronk, this says that is a companion of and is a conjoint of . It follows, in particular, that and are adjoint in .
Now the central lemma about these companions and conjoints is the following: there is a natural bijection between squares of the form and squares of the form I like to think of this as saying that vertical arrows can be “slid around corners” to become horizontal arrows, turning them into the “representable proarrows” or (depending on whether you slid them “backwards” or “forwards” to get around the corner). The bijection is just given by composing with the four special squares defined above. In particular, by a Yoneda argument, for any , , and we have
so the companions and conjoints determine the rest of the cartesian squares. Note that this is an equipment-version of Yoneda reduction, aka the co-Yoneda lemma. Also, we have a bijection between 2-cells in and 2-cells in . It follows that the functor sending to is locally fully faithful.
Wood’s original definition of an equipment was a functor between (weak) 2-categories which is bijective on objects, locally fully faithful, and such that the image of each arrow of has a right adjoint in . Thus, our definition implies his. The converse is not too hard either, so the two are equivalent. However, I find that the double-category way of thinking makes the structure look much more natural; Wood’s definition looks very ad-hoc to me. The double-categorical approach also (a) automatically gives you a good 2- or 3-category of equipments, which is tricky to do with Wood’s definition (I believe this was first realized by Verity in his thesis), and (b) generalizes better to situations in which the coends that define profunctor composition may not exist. But those are for another day.
Now let me try to convince you that we do formal category theory in an equipment. Let’s start with this: two (vertical) arrows and are adjoint (in ) if and only if we have an isomorphism . Why? Well, an adjunction comes with a unit and a counit, which (expressed in ) are of the form Applying the bijection of the central lemma, we see that corresponds to a map , and likewise corresponds to a map . The triangle identities for and are then equivalent to saying that these two maps are inverse isomorphisms. So we’ve recovered the classical equivalence between the “diagrammatic” and isomorphism-of-hom-sets definitions of an adjunction, in a purely formal way.
Now let’s define limits. I’m not sure who first realized that limits can be defined in the following way, but Ross Street is a good guess. The notion of limit we end up with is actually more general than what you’re probably used to, but this extra generality turns out to be useful. Let be an arrow and let be a proarrow; we’re going to define what it means for an arrow to be the -weighted limit of . In the equipment of -enriched categories, if is the unit -category , then this will recover the usual notion of weighted limit. Of course, in a general equipment we may not have a “unit object,” so that extra generality is unavoidable; it’s like using generalized elements in ordinary category theory.
To make things easier, let’s assume that is closed, in the sense that composition of proarrows has adjoints in each variable The central lemma implies that analogously to (1), we have
In , the adjoints are given by the ends and Therefore, (2) is an abstract form of the Yoneda lemma, just as (1) is an abstract form of the co-Yoneda lemma.
Now recall that for -categories and , an object is a -weighted limit of if we have an isomorphism Thus it makes sense to define, in a closed equipment, an arrow to be the -weighted limit of if we have an isomorphism (If our equipment is not closed, we simply assert that has the universal property that would have if it existed.) In particular, when is the unit -category, this recovers the classical notion. But even in there are interesting examples for other values of . If we take for some functor , then (1) and (2) imply that so that is the -weighted limit of . That is, -weighted limits are just given by composition with . But more interestingly, one can show that if for some , then -weighted limits specialize to pointwise right Kan extensions along . That is, the extra data in an equipment lets us define the good notion of Kan extension (even in the enriched case) as a special case of a general notion of limit.
Amazingly, a huge amount of category theory can be done at this level of generality. I’ll give just one more example (for now): the theorem that right adjoints preserve limits. Suppose that is a -weighted limit of in the above sense, and let be an arrow with a left adjoint . We want to show that is a -weighted limit of . But we have which is what we want.
Finally, in the interests of full disclosure, I should say that equipments are not the only way to do formal category theory. A sort-of equivalent approach, due to Street and Walters, is a “Yoneda structure,” which equips a 2-category with “presheaf objects” so that profunctors can be recovered as functors . (It’s only “sort-of” equivalent due to differences in how size is dealt with.) Alternately, one can start from a well-behaved 2-category, such as a 2-topos, and construct an equipment or Yoneda structure, in one of several ways, and if one likes one can work only with those constructions without ever saying “equipment” or “Yoneda structure.” But I think that isolating the “proarrow structure” that enables us to do formal category theory is helpful, and can provide useful insights even if we only care about one particular kind of category theory—just like knowing some ordinary category theory can be helpful even if we only care about one particular category.
Re: Equipments
You know me, so I'm trying to understand equipments by first figuring out what they are a categorification of. Your introductory paragraphs imply that they're a categorification of categories, but I don't buy it. Let me decategorify paragraph 4 (where the first paragraph is paragraph 0):
So maybe an equipment is a categorification of something like an allegory?
Except that we usually don't think of relations as missing from ordinary category theory. We can define an internal relation in any category to be an object with morphisms and that satisfy a joint monicity condition. So why can't we define an internal profunctor in any -category to be an object with morphisms and equipped with a joint monicity structure?
Trying to write down that structure, I see that already this is not possible even when dealing with posets as categories enriched over . Of course, that means that there is an interesting decategorification of the notion of equipment which serves as a universe in which to do order theory. (This is an example of how categorification directly takes us from posets to categories or from categories to groupoids, while it is laxification that takes us from sets to posets or from groupoids to categories, and these are separate operations.) Has anybody studied that?
Conversely, I would hope that, as an unlaxified categorification of our ability to study relations internal to an arbitrary category, we can also study profunctors internal to an arbitrary -category. Do we have a theorem about that, that any locally groupoidal -category naturally has the structure of an equipment?
I think that I may have talked with you about this already on your personal web, Mike, but I can't check it now since the Ruby on Rails application is down. (In principle, I could check my backups, but that's not very convenient.) Sorry if you already explained all of this and it didn't stick the first time.