Toward compact double categories: Part 1
The twisted Hom double functor
This post is cross-posted at the Topos Institute blog.
Lately I’ve been pursuing formal category theory using double categories. A first step in this program is to abstract from categories to category objects in a double category; for instance, internal categories are category objects in a double category of spans and enriched categories are category objects in a double category of matrices. The next step is to take structures defined on categories and generalize them to category objects in a double category. By the microcosm principle, that is possible when the double category possesses a categorified version of the very structure in question. The concepts from double category theory that I’ve used so far, like products and coproducts, indeed categorify familiar concepts from category theory. While there are interesting twists along the way,1 the one-dimensional story gives strong hints about how to generalize to double categories.
An operation on categories that has no direct analogue for sets is taking the opposite category. Though trivial to compute—simply turn the arrows around—the existence of a nontrivial symmetry on categories has the powerful consequence that every definition or result in the language of category theory has a dual. Ideas in category theory come at a two-for-the-price-of-one bargain. Opposites also occur constantly in everyday use of category theory, such as when taking a contravariant functor to be a (covariant) functor out of an opposite category.
An abstract account of categorical duality is thus essential for formal category theory: what structure must a double category possess for its category objects to admit a duality? Unfortunately, for all its apparent simplicity, categorical duality has resisted a satisfactory axiomatization. Ideally, we would find universal properties that determine the opposite category uniquely, at least up to equivalence. Let’s begin by seeing how a purely bicategorical approach founders.
The compact bicategory of profunctors
A basic property of the opposite category is that for any categories
Yet compact bicategories fall short of axiomatizing categorical duality via universal properties, in two ways.
First, a symmetric monoidal product is a structure on, not a universal property of, a bicategory. A purely bicategorical fix would be to use cartesian bicategories instead of monoidal bicategories, but as I have argued on this blog and in print (Patterson 2024), cartesian or finite-product double categories are more elegant solutions, being defined by simpler universal properties. So double categories already neatly solve this problem.
Second—and this is the problem that will occupy us—even once the symmetric monoidal structure on the bicategory is fixed, duals are defined by a bicategorical universal property, which is too loose in key examples. In the case of profunctors, the universal property gives equivalences of hom-categories
In particular, taking both
- the categories have equivalent categories of presheaves
- the categories are equivalent in the bicategory
- the Cauchy completions of the categories are equivalent (in
).
So, if I asked you for the dual of a category, you would be allowed to take its opposite and then also take its Cauchy completion. But wait, that’s not what I asked for! To make this more vivid, the nLab notes that the Cauchy completion of the category of open subsets of Euclidean spaces and smooth maps is the category of smooth manifolds. If those two categories were the same, differential geometry wouldn’t be a subject!
The second problem cannot be solved in the same way as the first. In the first case, the trouble is that the bicategory
Outline
With that preamble, our aim is to propose a definition of a compact double category.3 The definition will involve an adjunction in the loose direction of the double category, generalizing an adjunction in a bicategory. As far as I know, this notion of double adjunction has not yet been defined; the elegant theory of double adjunctions created by Grandis and Paré (1999) refers to the tight direction. To define such adjunctions, I will employ a version of the Hom double functor, but again, the Hom double functor from the Yoneda theory for double categories (Paré 2011) refers to the tight direction. Continuing to work backwards, to cook up this “twisted” Hom functor, which sends arrows to proarrows and vice versa, I will need similarly “twisted” notion of double functor.
So that’s where we will begin in the next section: defining a twisted lax functor between double categories. We then construct our motivating example, the twisted Hom functor on a double category. Only in the next post will get back to our original objective.
The upfront cost in machinery is admittedly high, but I find these ancillary ideas interesting in their own right and I believe they will find other uses. Still, everything explored here should be considered provisional.
Twisted double functors
The transpose of a strict double category
Definition 1 A twisted lax double functor
- each object
of to an object of , - each arrow
of to a proarrow of , - each proarrow
of to an arrow of , and - each cell of
to a cell of , as follows:
In addition, for composable arrows
Similarly, for composable proarrows
This data must satisfy the following axioms.
Naturality of composition comparisons, in both directions: for internally composable cells
and in ,and for externally composable cells
and in ,Naturality of unitality comparisons, in both directions: analogous.
Associativity and unitality of composition and identity comparisons, in both directions: two instances of the usual associativity and unitality axioms for a lax functor; cf. (Grandis 2019, Definition 3.5.1).
Notice that, when the domain
The rules for composing ordinary and twisted lax functors deserve more attention than I’ve given them. For now, I’ll just say that twisted lax functors can be precomposed with ordinary ones. Specifically, given a lax functor
The twisted Hom functor
In his “Yoneda theory for double categories,” Paré (2011) introduces the Hom double functor
in which
whose apex is the set of cells
Most parallel and economical would be to define a “twisted Hom functor” of the form
in which
Definition 2 The twisted Hom double functor on a double category
that maps
each pair of objects
and in to the hom-category comprising the proarrows and globular cells between them;each pair of arrows
and in to the profunctor between hom-categoriesin which the heteromorphisms from a proarrow
to another are just the cells in of formon which globular cells act by pre- and post-composition;
each pair of proarrows
and in to the functor between hom-categoriesthat sends a proarrow
to the composite proarrow and a globular cell to the composite cell ;each pair of cells in
as on the leftto the natural transformation on the right whose component
at a pair of proarrows and in is given by external composition:
The comparison cells of the twisted Hom functor are defined as follows. At pairs of composable arrows
The identity comparison
Finally, at pairs of composable proarrows
given by the associators of
given by the unitors of
This completes the construction of the twisted Hom functor. We crucially used that it is valued in profunctors, not spans, when defining the final comparison cells. The twisted Hom functor is, in fact, a twisted normal lax functor, meaning that the identity comparisons in both directions are isomorphisms. Like the ordinary Hom functor, the twisted Hom functor faithfully encodes all the operations of a double category, but now in a transposed fashion.
Next time, we put the twisted Hom functor to work, defining a compact double category using a twisted double adjunction.
References
Footnotes
There are at least two plausible and useful double-categorical analogues of cartesian categories: “cartesian double categories” (Aleiferi 2018) and “double categories with finite products” (Patterson 2024). Furthermore, the latter tend to exhibit a laxness with no 1-categorical counterpart.↩︎
A “compact bicategory” is sometimes taken to mean something different, namely a bicategory in which every morphism has a left and a right adjoint. In this series of posts we will only ever use “compact” to mean “compact closed.”↩︎
Compact double categories have been contemplated by various people over the years, but so far no entirely definite proposal has emerged. On the nLab, Shulman has sketched an interesting unbiased approach to compact double categories and compact virtual double categories. Further afield, Niefield (2024) studies cartesian closed double categories, which are closed in the tight direction, not the loose one.↩︎
I follow the convention that double categories and double functors are pseudo by default.↩︎
In the jargon of (Aleiferi 2018, Definition 4.3.7), the double category
is unit-pure: any cell between identity spans must itself be the external identity on a function. Thus, a twisted Hom functor valued in spans could only be defined for strict double categories. By contrast, the double category is not unit-pure: the cells bounded by identity profunctors are arbitrary natural transformations between functors.↩︎