John Baez Doctrines

Preface

This is a writeup of some material developed mainly by James Dolan, with help from me.

The idea

For us, a doctrine is a categorified version of an essentially algebraic theory, meaning a category with finite limits. But rather than working with general weak 2-categories, we prefer to work with (2,1)-categories, meaning (weak) 2-categories for which every 2-morphism is invertible. We can regard this as a step towards working with $(\infty,1)$-categories.

Definition: A doctrine is a $(2,1)$-category with finite homotopy limits. Here we use homotopy limit as a synonym for bilimit.

Definition: Given doctrines $C$ and $D$, a morphism of doctrines $F: C \to D$ is a functor that preserves homotopy limits. Here a functor between $(2,1)$-categories means a weak 2-functor, or what Benabou called a homomorphism of bicategories.

Definition: A theory of the doctrine $D$ is a morphism $F: D \to Cat$, where $Cat$ stands for the 2-category of

• categories,

• functors, and

• natural isomorphisms

We can also define 2-morphisms and 3-morphisms of doctrines, and they form a tricategory where all 3-morphisms are invertible: that is, a $(3,2)$-category. (Fill in the details.)

Definition: An interpretation of the doctrine $C$ in the doctrine $D$ is a morphism

$$F : C \to D .$$

We often call $C$ the syntactic doctrine and $D$ the environment.

There is a $(2,1)$-category $[C,D]$ whose objects are interpretations of $C$ in $D$.

Claim: $[C,D]$ has finite homotopy limits, so it is again a doctrine.

We call $[C,Gpd]$ the semantic doctrine associated to the syntactic doctrine $C$. Categorified Gabriel–Ulmer duality is all about recovering the syntactic doctrine from the semantic doctrine.

Examples

Here are some examples of doctrines. Some of these tend to show up as syntactic doctrines while others tend to show up as environments, though there is no clear-cut distinction. We call the former $C$ and the latter $D$.

Example: $D = Cat$, the $(2,1)$-category of

• categories,

• functors, and

• natural isomorphisms

This is the primordial ‘environment’.

Example: Important in algebraic geometry is the doctrine of ‘dimensional theories’. A line object is an object $L$ in a symmetric monoidal category which is invertible (there exists an object $M$ such that $L \otimes M \cong 1$) and has $S_{L,L} = 1_{L \otimes L}$. A dimensional theory over some commutative ring $k$ is a symmetric monoidal $k$-linear category where every object is a line object. The key example of a dimensional theory is the category of line bundles over some projective variety over some field $k$.

We define the doctrine of dimensional theories, $D = Dim$, to have

• dimensional theories as objects,

• symmetric monoidal $k$-linear functors as morphisms,

• symmetric monoidal natural isomorphisms as 2-morphisms.

Example: Also important in algebraic geometry is the doctrine of algebraic geometric theories. An algebraic geometric theory over some commutative ring $k$ is a symmetric monoidal $k$-linear category with finite colimits. The key example of an algebraic geometric theory is the category of coherent sheaves over some scheme over $k$ — or more generally, over some Artin stack over $k$.

We define the doctrine of algebraic geometric theories, $D = \Alg\Geom$, to have

• algebraic geometric theories as objects,

• symmetric monoidal $k$-linear functors preserving finite colimits as morphisms,

• symmetric monoidal natural isomorphisms as 2-morphisms.

Example: the doctrine of finite limits theories?.

Example: Let $C = FPGpd^{op}$ be the opposite of the $(2,1)$-category of finitely presented groupoids. This is the free doctrine on one object. We could roughly call $C$ the doctrine of ‘a thing’: since its ‘sketch’ consists of single object (the thing). Here $Mod(C,Gpd) = Gpd$, so we call $C$ the doctrine of groupoids.

Example: Let $C = Fin\Set^{op}$ as a discrete $(2,1)$-category. Here $Mod(C,Gpd) = Set$, the $(2,1)$- category of essentially discrete groupoids. So, $C$ is the doctrine of essentially discrete groupoids.

To get the sketch here, we draw an object $X$ and its identity morphism; then we take the homotopy limit of this, say $Y$. $Y$ comes with a projection to the original object $X$, and there is also a map going back. So, we just need a bit of extra stuff to make this an equivalence.

The point here is that for any groupoid $X$, we can take the homotopy limit of its identity morphism, and the result is the groupoid of ‘objects of $X$ equipped with automorphism’, say $\tilde{X}$. There’s a forgetful functor $p: \tilde{X} \to X$ but also a map going back, $i: X \to \tilde{X}$. $i$ followed by $p$ is isomorphic to the identity. If $p$ followed by $i$ is also isomorphic to the identity, $X$ is an (essentially) discrete groupoid.

More generally, for any finite limits theory $T$ we can cook up a doctrine whose theories in $Gpd$ are just models of $T$ in $Set$. To do this, we take the sketch for $T$ and add in, for each object $X$ in the sketch, an equation saying that $i: X \to \tilde{X}$ is inverse to $\tilde{X} \to X$, where $\tilde{X}$ is the homotopy limit of $1: X \to X$. This is a way of asserting that $X$ is ‘essentially discrete’.

Puzzle: What is a model of $\Fin\Set^{op}$ in $Gpd^{op}$? It’s an ‘essentially discrete object in $Gpd^{op}$’. But what’s that like.

Example: Let $C$ be defined by the following sketch. We roughly copy the usual sketch for a ‘category object’ which we would use to construct the finite limits theory of categories. So, we start with two objects, $Ob$ and $Mor$, and morphisms $i: Ob \to Mor$, $s,t: Mor \to Ob$. But now we take the weak pullback $Mor {}_s \times_t Mor$ and put in a morphism $\circ : Mor {}_s \times_t Mor \to Mor$. Then we put in 2-morphisms called the associator and left/right unitors, and make these obey the usual laws.

Now consider a model $F: C \to Gpd$. There are morphisms in the groupoid of objects $F(Ob)$ but also objects in the groupoid of morphisms $F(Mor)$. So, we seem to be getting a pseudo double category in the sense of Grandis, but where the morphisms in one direction (morphisms in the groupoid of objects) are all invertible.

So, $C$ is the doctrine of pseudo double categories with vertical morphisms invertible.

Example: By adding more to the sketch above, we get the doctrine of categories, $C$, for which $Mod(C,Gpd)$ is equivalent to the $(2,1)$-category $Cat$.

What do we add? Above we have morphisms in the groupoid of objects $F(Ob)$ — call them ‘old morphisms’ — which are automatically invertible. But we also have objects in the groupoid of morphisms $F(Mor)$ — call them ‘new morphisms’ which are not. Every old morphism gives a new morphism, thanks to how composition is defined on a weak pullback. (Fill in the details here!) We want to add stuff to our sketch that makes the new morphisms the same as the old ones.

We take the thing of ‘inverse pairs of new morphisms’ by starting with $Mor \times Mor$ and forming a certain weak pullback. This has a map to $Ob$ (in fact two, but pick either one). We then insert 2-morphisms into our sketch which say that this map is an equivalence. This should make the new morphisms be (essentially) the same as the old ones.

Example: We would similarly like the doctrine of operads, which has an object of objects, or types, and an object of $n$-ary operations for each $n$.

Sketches

We would like a theory of sketches that allows us to ‘present’ doctrines, much as the usual theory of sketches (explained for example in Barr and Wells’ Toposes, Triples and Theories) allows us to present finite limits theories. But fully formalizing the usual theory of sketches takes some work, and presumably this will be even worse for doctrines or eventually $(\infty,1)$-categories with finite limits.

This could be relieved if we had a Gabriel–Ulmer duality theorem for doctrines, since then we could specify a doctrine $D$ by pointing to its category of interpretations in $Gpd$, namely $[D,Gpd]$, and the ‘finitely presentable’ objects in here would correspond to objects of $D^{op}$ (and thus $D$). Conversely, we expect $[D^{op}, Gpd] \simeq D$.

Example: let $FP\Alg\Geom$ be the doctrine of finitely presented algebraic geometric theories. Claim: $[FP\Alg\Geom^{op}, Gpd]$ is the doctrine of algebraic geometric theories.

Example: There is a finite limits theory $Fin\Set$, which is the embodiment of propositional logic. All finite sets can be formed from $2$ by products and equalizers, so this finite limits theory is the Cauchy completion of the Lawvere theory whose objects are powers of $2$, which is the opposite of the category of finitely presented Boolean algebras. Note: $[Fin\Set, Set] = \Bool\Alg$ is the opposite of the category of profinite sets. $[Fin\Set^{op}, Set] = Set$ since $Fin\Set^{op}$ is the free finite limits theory on one object.

Categorifying this example, we should get an interesting doctrine which is the embodiment of predicate logic. Namely, let $\FP\Gpd$, the $(2,1)$-category of finitely presented groupoids. Claim: theories of this doctrine are theories of first-order predicate logic. Conjecture: $[\FP\Gpd, Gpd]$ is the opposite of the category of profinite groupoids. $[\FP\Gpd^{op}, Gpd] = Gpd$. With luck this will explain the appearance of profinite groups in number theory.