Reference Cartesian double theories: A double-categorical framework for categorical doctrines [patterson-lambert-dbltheory]

Abstract

  • May , 2024
  • Michael Lambert, Evan Patterson

The categorified theories known as doctrines specify a category equipped with extra structure, analogous to how ordinary theories specify a set with extra structure. We introduce a new framework for doctrines based on double category theory. A cartesian double theory is defined to be a small double category with finite products and a model of a cartesian double theory to be a finite product-preserving lax functor out of it. Many familiar categorical structures are models of cartesian double theories, including categories, presheaves, monoidal categories, braided and symmetric monoidal categories, 2-groups, multicategories, and cartesian and cocartesian categories. We show that every cartesian double theory has a unital virtual double category of models, with lax maps between models given by cartesian lax natural transformations, bimodules between models given by cartesian modules, and multicells given by multimodulations. In many cases, the virtual double category of models is representable, hence is a genuine double category. Moreover, when restricted to pseudo maps, every cartesian double theory has a virtual equipment of models, hence an equipment of models in the representable case. Compared with 2-monads, double theories have the advantage of being straightforwardly presentable by generators and relations, as we illustrate through a large number of examples. 

 @article
{patterson-lambert-dbltheory, title={Cartesian double theories: A double-categorical framework for categorical doctrines}, volume={444}, ISSN={00018708}, DOI={10.1016/j.aim.2024.109630}, url={https://arxiv.org/abs/2310.05384}, journal={Advances in Mathematics}, author={Lambert, Michael and Patterson, Evan}, year={2024}, month={May}, pages={109630} }

Backlinks

Double Categories [efr-NC0R]

Definition Double Category [efr-RXP4]

A (strict) double category is a category internal to the category \mathsf {Cat} of categories. Concretely, it consists of:

  1. A set of objects \operatorname {\mathbf {ob}} \mathbb {C}
  2. A collection of vertical morphisms forming a category \mathbb {C}_v with \operatorname {\mathbf {ob}} \mathbb {C}_v = \operatorname {\mathbf {ob}} \mathbb {C}
  3. A collection of horizontal morphisms forming a category \mathbb {C}_h with \operatorname {\mathbf {ob}} \mathbb {C}_h = \operatorname {\mathbf {ob}} \mathbb {C}
  4. An a collection of squares. Each square has a left and right boundary given by vertical morphisms l,r, and top and bottom boundary given by horizontal morphisms t,b so that \operatorname {\mathrm {dom}} t = \operatorname {\mathrm {dom}} l, \operatorname {\mathrm {cod}} t = \operatorname {\mathrm {dom}} r and so on:
    The squares compose horizontally and vertically in the obvious way, each of which form a category (in particular, there are identity squares for each vertical and horizontal map).

A double functor is a mapping on objects, vertical and horizontal morphisms, and squares, which preserves all the identities and composition.

There is also a notion of pseudo double category, which weakens the horizontal composition to only be associative and unital up to a coherent system of squares. We will not go into the details here, see § [efr-000D] for more on this.

Example [efr-BEJ6]

There is a pseudo double category \mathsf {\mathbb Cat} where the objects are categories, the vertical maps are functors, the horizontal maps are profunctors (functors \mathcal {C} \times \mathcal {D}^\mathrm {op} \to \mathsf {Set}, sometimes called bimodules), and the squares are natural transformations.

For any category with pullbacks \mathcal {C}, there is a pseudo double category \mathsf {\mathbb Span}(\mathcal {C}) with \mathcal {C} as the vertical category, spans as the horizontal morphisms, and commutative diagrams as the squares.

There is a double category \mathsf {\mathbb Rel} of sets, functions, and relations.

For any Markov category \mathcal {C}, there is a double category with \mathbb {C}_v = \mathcal {C}_\mathrm {det} and \mathbb {C}_h = \mathcal {C}.

For any category at all, there is a double category \operatorname {Sq}(\mathcal {C}) with \operatorname {Sq}(\mathcal {C})_v = \operatorname {Sq}(\mathcal {C})_h = \mathcal {C} and commutative squares as the pullback squares.

Definition [efr-Y1S5]

A double category is thin if, for each compatible square of vertical and horizontal morphisms, there is at most one square filling it. In other words, such a square either commutes or doesn't.

Sometimes the two classes of morphism are instead called loose and tight, especially in cases where the composition of the loose class is not associative, or if the loose class is a superset of the tight class.

Although the explicit description above is probably the best way to think about the data of a double category, on a technical level it is often useful to think in terms of internal categories. An internal category in a category \mathcal {C} is a pair of objects C_0, C_1, maps d,c: C_1 \to C_0, i: C_0 \to C_1 (the domain, codomain and identity), and a map m: C_1 \times _{C_0} C_1 \to C_1 (the multiplication), satisfying the usual laws of a category. A double category in the above sense is then an internal category in the category of categories.

In the terms of Definition [efr-RXP4], C_0 is \mathbb {C}_v, and C_1 is the category whose objects are horizontal arrows, and whose morphisms are squares (composed vertically). Obviously, we could just as easily have oriented things horizontally, but this is the convention usually adopted.

Given a double category \mathbb {C}, there is another double category \mathbb {C}^T called the transpose of \mathbb {C}, which has the same objects but exchanges the horizontal and vertical morphisms. In many cases it is not clear which of \mathbb {C} and \mathbb {C}^T is the "correct" one to work with, and we may have to pass back and forth between them. We try to stick to the convention that the horizontal morphisms are the "loose" ones. To avoid confusion, we will also simply specify the classes of morphisms directly, speaking for example of "the lenses" or "the charts" when working with the double category \mathsf {\mathbb Arena}(\mathcal {A}) (Definition [efr-0025]).

The concept of double category goes back to Reference [ehresmann-dblcats]. See Reference [johnson-yau-2dim-categories], section 12.3 for a textbook treatment. They have been widely used in applied category theory. An early application is in Reference [baez-courser-structured-cospans], which constructed a "structured" version of the double category of cospans. Here the philosophy is that the horizontal morphisms are the "systems" (in a general sense) which are being wired together by horizontal composition, while the vertical morphisms (and squares) are "structure-preserving maps between systems". This is similar to the our double category of "bisystems" (§ [efr-MWCE]). Recent work by Lambert and Patterson Reference [patterson-lambert-dbltheory] applies double categories to categorical algebra, with many applications to systems modeling, see Reference [catcolab-introducing] (as well as to classical category theory). In the next section we'll see their application to categorical systems theory, and later see them applied to parametrized morphisms.