Cartesian Bicategories
Posted by John Baez
guest post by Daniel Cicala and Jules Hedges
We continue the Applied Category Theory Seminar with a discussion of Carboni and Walters’ paper Cartesian Bicategories I. The star of this paper is the notion of ‘bicategories of relations’. This is an abstraction of relations internal to a category. As such, this paper provides excellent, if technical, examples of internal relations and other internal category theory concepts. In this post, we discuss bicategories of relations while occasionally pausing to enjoy some internal category theory such as relations, adjoints, monads, and the Kleisli construction.
We’d like to thank Brendan Fong and Nina Otter for running such a great seminar. We’d also like to thank Paweł Sobociński and John Baez for helpful discussions.
Shortly after Bénabou introduced bicategories, a program was initiated to study these through profunctor bicategories. Carboni and Walters, however, decided to study bicategories with a more relational flavor. This is not quite as far a departure as one might think. Indeed, relations and profunctors are connected. Let’s recall two facts:
a profunctor from to is a functor from to , and
a relation between sets and can be described with a -valued matrix of size .
Heuristically, profunctors can be thought of as a generalization of relations when considering profunctors as “-valued matrix of size ”. As such, a line between profunctors and relations appears. In Cartesian Bicategories I, authors Carboni and Walters walk this line and continue a study of bicategories from a relational viewpoint.
The primary accomplishment of this paper is to characterize ‘bicategories of internal relations’ and of ‘ordered objects’ in a regular category . To do this, the authors begin by introducing the notion of Cartesian bicategory, an early example of a bicategory with a monoidal product. They then explore bicategories of relations, which are Cartesian bicategories whose objects are Frobenius monoids. The name “bicategories of relations” indicates their close relationship with classical relations .
We begin by defining the two most important examples of a bicategory of relations: and . Knowing these bicategories will ground us as we wade through the theory of Cartesian bicategories. We finish by characterizing and in terms of the developed theory.
Internal relations
In set theory, a relation from to is a subset of . In category theory, things become more subtle. A relation from to internal to a category is a ‘jointly monic’ -span That is, for any arrows such that and hold, then . In a category with products, this definition simplifies substantially; it is merely a monic arrow .
Given a span and the relation from above, we say that is -related to if there is an so that
commutes. We will write when is -related to .
While we can talk about relations internal to category, we cannot generally assemble them into another category. However, if we start with a regular category , then there is a bicategory of relations internal to . The objects are those of . The arrows are the relations internal to with composition given by pullback:
Additionally, we have a unique 2-cell, written , whenever . Diagrammatically, if there exists a commuting diagram
Internal ordered objects
We are quite used to the idea of having an order on a set. But what about an order on a category? This is captured by the bicategory of ordered objects and ideals in a regular category .
The objects of are ordered objects in . An ordered object is a pair consisting of an -object and a reflexive and transitive relation internal to .
(Puzzle: is a monic of type . Both reflexivity and transitivity can be defined using morphisms. What are the domains and codomains? What properties should be satisfied?)
The arrows of are a sort of ‘order preserving relation’ called an ideal. Precisely, an ideal between ordered objects is a relation such that given
morphisms with a common domain , and
relations , , and
then .
In , an ordered object is a preordered set and an ideal is a directed subset of with the property that if it contains and , then it contains .
There is at most a single 2-cell between parallel arrows in . Given , write whenever .
Cartesian Bicategories
Now that we know what bicategories we have the pleasure of working with, we can move forward with the theoretical aspects. As we work through the upcoming definitions, it is helpful to recall our motivating examples and .
As mentioned above, in the early days of bicategory theory, mathematicians would study bicategories as -enriched profunctor bicategories for some suitable . A shrewd observation was made that when is Cartesian, a -profunctor bicategory has several important commonalities with and . Namely, there is the existence of a Cartesian product , plus for each object , a diagonal arrow and terminal object . With this insight, Carboni and Walters decided to take this structure as primitive.
To simplify coherence, we only look at locally posetal bicategories (i.e. -enriched categories). This renders 2-dimensional coherences redundant as all parallel 2-cells manifestly commute. This assumption also endows each hom-poset with 2-cells and, as we will see, local meets . For the remainder of this article, all bicategories will be locally posetal unless otherwise stated.
Definition. A locally posetal bicategory is Cartesian when equipped with
a symmetric tensor product ,
a cocommutative comonoid structure, , and , on every -object
such that
- every 1-arrow is a lax comonoid homomorphism, i.e.
- for all objects , both and have right adjoints and .
Moreover, is the only cocommutative comonoid structure on admitting right adjoints.
(Question: This definition contains a slight ambiguity in the authors use of the term “moreover”. Is the uniqueness property of the cocommutative comonoid structure an additional axiom or does it follow from the other axioms?)
If you’re not accustomed to thinking about adjoints internal to a general bicategory, place yourself for a moment in . Recall that adjoint functors are merely a pair of arrows (adjoint functors) together with a pair of 2-cells (unit and counit) obeying certain equations. But this sort of data can exist in any bicategory, not just . It is worth spending a minute to feel comfortable with this concept because, in what follows, adjoints play an important role.
Observe that the right adjoints and turn into a commutative monoid object, hence a bimonoid. The (co)commutative (co)monoid structure on an object extend to a tensor product on as seen in this string diagram:
Ultimately, we want to think of arrows in a Cartesian bicategory as generalized relations. What other considerations are required to do this? To answer this, it is helpful to first think about what a generalized function should be.
For the moment, let’s use our based intuition. For a relation to be a function, we ask that every element of the domain is related to an element of the codomain (entireness) and that the relationship is unique (determinism). How do we encode these requirements into this new, general situation? Again, let’s use intuition from relations in . Let be a relation and be the relation defined by whenever . To say that is entire is equivalent to saying that the composite relation contains the identity relation on (puzzle). To say that is deterministic is to say that the composite relation is contained by the identity (another puzzle). These two containments are concisely expressed by writing and . Hence and form an adjoint pair! This leads us to the following definition.
Definition. An arrow of a Cartesian bicategory is a map when it has a right adjoint. Maps are closed under identity and composition. Hence, for any Cartesian bicategory , there is the full subbicategory whose arrows are the maps in .
(Puzzle: There is an equivalences of categories for a regular category . What does this say for ?)
We can now state what appears as Theorem 1.6 of the paper. Recall that refers to the right adjoint.
Theorem. Let be a locally posetal bicategory. If is Cartesian, then
has finite bicategorical products ,
the hom-posets have finite meets (i.e. categorical products) and the identity arrow in is maximal (i.e. a terminal object), and
bicategorical products and biterminal object in may be chosen so that ,where denotes the appropriate projection.
Conversely, if the first two properties are satisfied and the third defines a tensor product, then is Cartesian.
This theorem gives a nice characterisation of Cartesian bicategories. The first two axioms are straightforward enough, but what is the significance of the above tensor product equation?
It’s actually quite painless when you break it down. Note, every bicategorical product comes with projections and inclusions . Now, let and which gives . One canonical arrow of type is which first projects to , arrives at via , which then includes into . The other arrow is similar, except we first project to . The above theorem says that by combining these two arrows with a meet , the only available operation, we get our tensor product.
Characterizing bicategories of internal relations
The next stage is to add to Cartesian bicategories the property that each object is a Frobenius monoid. In this section we will study such bicategories and see that Cartesian plus Frobenius provides a reasonable axiomatization of relations.
Recall that an object with monoid and comonoid structures is called a Frobenius monoid if the equation
holds. If you’re not familiar with this equation, it has an interesting history as outlined by Walters. Now, if every object in a Cartesian bicategory is a Frobenius monoid, we call it a bicategory of relations. This term is a bit overworked as it commonly refers to . Therefore, we will be careful to call the latter a “bicategory of internal relations”.
Why are bicatgories of relations better than simply Cartesian bicategories? For one, they admit a compact closed structure! This appears as Theorem 2.4 in the paper.
Theorem. A bicategory of relations has a compact closed structure. Objects are self-dual via the unit
and counit
Moreover, the dual of any arrow satisfies
and
Or if you prefer string diagrams, the above inequalities are respectively
and
Because a bicategory of relations is Cartesian, maps are still present. In fact, they have a very nice characterization here.
Lemma. In a bicategory of relations, an arrow is a map iff it is a (strict) comonoid homomorphism iff .
As one would hope, the adjoint of a map corresponds with the involution coming from the compact closed structure. The following corollary provides further evidence that maps are well-behaved.
Corollary. In a bicategory of relations:
is a map implies . In particular, multiplication is adjoint to comultiplication and the unit is adjoint to the counit.
for maps and , if then .
But maps don’t merely behave in a nice way. They also contain a lot of the information about a Cartesian bicategory and, when working with bicategories of relations, the local information is quite fruitful too. This is made precise in the following corollary.
Corollary. Let be a pseudofunctor between bicategories of relations. The following are equivalent:
strictly preserves the Frobenius structure.
The restriction strictly preserves the comonoid structure.
preserves local meets and .
Characterizing bicategories of internal relations
The entire point of the theory developed above is to be able to prove things about certain classes of bicategories. In this section, we provide a characterization theorem for bicategories of internal relations. Freyd had already given this characterization using allegories. However, he relied on a proof by contradiction whereas using bicategories of relations allows for a constructive proof.
A bicategory of relations is meant to generalize bicategories of internal relations. Given a bicategory of relations, we’d like to know when an arrow is “like an internal relation”.
Definition. An arrow is a tabulation if there exists maps and such that and .
This definition seems bizarre on its face, but it really is analogous to the jointly monic span-definition of an internal relation. That is saying that is like a span . The equation implies that this span is jointly monic (puzzle).
A bicategory of relations is called functionally complete if every arrow has a tabulation and . One can show that the existence of these tabulations together with compact closedness is sufficient to obtain a unique (up to isomorphism) tabulation for every arrow. We now provide the characterization, presented as Theorem 3.5.
Theorem. Let be a functionally complete bicategory of relations. Then:
is a regular category (all 2-arrows are trivial by an above corollary)
There is a biequivalence of bicategories obtained by sending the relation of to the arrow of .
So all functionally complete bicategories of relations are bicategories of internal relations. An interesting quesion is whether any regular category can be realized as for some functionally complete bicategory of relations. Perhaps a knowledgeable passerby will gift us with an answer in the comments!
From this theorem, we can classify some important types of categories. For instance, bicategories of relations internal to a Heyting category are exactly the functionally complete bicategory of relations having all right Kan extensions. Bicategories of relations internal to an elementary topos are exactly the functionally complete bicategories of relations such that is representable in for all objects .
Characterizing ordered object bicategories
The goal of this section is to characterize the bicategory of ordered objects and ideals. We already introduced earlier, but that definition isn’t quite abstract enough for our purposes. An equivalent way of defining an ordered object in is as an -object together with a relation on such that and . Does this data look familiar? An ordered object in is simply a monad in !
(Puzzle: What is a monad in a general bicategory? Hint: how are adjoints defined in a general bicategory?)
Quite a bit is known about monads, and we can now apply that knowledge to our study of .
Recall that any monad in gives rise to a category of adjunctions. The initial object of this category is the Kleisli category. Since the Kleisli category can be defined using a universal property, we can define a Kleisli object in any bicategory. In general, a Kleisli object for a monad need not exist but when it does, it is defined as an arrow plus a 2-arrow such that, given any arrow and 2-arrow , there exists a unique arrow such that . The pasting diagrams involved also commute:
As in the case of working inside , we would expect for to be on the left of an adjoint pair, and indeed it is. We get a right adjoint such that the composite is our original monad . The benefit of working in the locally posetal case is we also have that . This realizes as an idempotent:
It follows that the Kleisli object construction is exactly an idempotent splitting of ! This means we can start with an exact category and construct by splitting the idempotents of . With this in mind, we move on to the characterization, presented as Theorem 4.6.
Theorem. A bicategory is biequivalent to a bicategory if and only if
is Cartesian,
every monad in has a Kleisli object,
for each object , there is a monad on and a Frobenius monoid that is isomorphic to the monad’s Kleisli object,
given a Frobenius monoid x and with , splits.
Final words
The authors go on to look closer at bicategories of relations inside Grothendieck topoi and abelian categories. Both of these are regular categories, and so fit into the picture we’ve just painted. However, each have additional properties and structure that compels further study.
Much of what we have done can be done in greater generality. For instance, we can drop the local posetal requirement. However, this would greatly complicate matters by requiring non-trivial coherence conditions.
Re: Cartesian Bicategories
A very nice and comprehensive post! I have just a few comments/questions.
I presume that by “biproduct” you mean “bicategorical product”. Unfortunately it’s better not to do this, because “biproduct” also means something else. (Which is also related to cartesian bicategories: the third property in Theorem 1.6 is a sort of categorified version of this other notion of biproduct.)
Your definition of Frobenius monoid doesn’t seem right to me; at least, your additional axiom doesn’t coincide with the usual one (the last of the string diagram pictures here). Is it equivalent?
I didn’t know that Freyd used a proof by contradiction in characterizing allegories of internal relations. I would be surprised if that use were essential; have you looked at it? In particular, the theory of allegories is also exposited in chapter A3 of Sketches of an Elephant, and I don’t recall any use of excluded middle there; the Elephant is generally quite careful about noting such uses.
You asked whether any regular category can be realized as for some functionally complete bicategory of relations . Am I missing something? Can’t we just take ?