This is a writeup of some material developed mainly by James Dolan, with help from me.
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 -categories.
Definition: A doctrine is a -category with finite homotopy limits. Here we use homotopy limit as a synonym for bilimit.
Definition: Given doctrines and , a morphism of doctrines is a functor that preserves homotopy limits. Here a functor between -categories means a weak 2-functor, or what Benabou called a homomorphism of bicategories.
Definition: A theory of the doctrine is a morphism .
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 -category. (Fill in the details.)
Definition: An interpretation of the doctrine in the doctrine is a morphism
We often call the syntactic doctrine and the environment.
There is a -category whose objects are interpretations of in .
Claim: has finite homotopy limits, so it is again a doctrine.
We call the semantic doctrine associated to the syntactic doctrine . Categorified Gabriel–Ulmer duality is all about recovering the syntactic doctrine from the semantic doctrine.
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 and the latter .
Example: , the -category of
This is the primordial ‘environment’.
Example: Important in algebraic geometry is the doctrine of ‘dimensional theories’. A line object is an object in a symmetric monoidal category which is invertible (there exists an object such that ) and has . A dimensional theory over some commutative ring is a symmetric monoidal -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 .
We define the doctrine of dimensional theories, , to have
dimensional theories as objects,
symmetric monoidal -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 is a symmetric monoidal -linear category with finite colimits. The key example of an algebraic geometric theory is the category of coherent sheaves over some scheme over — or more generally, over some Artin stack over .
We define the doctrine of algebraic geometric theories, , to have
algebraic geometric theories as objects,
symmetric monoidal -linear functors preserving finite colimits as morphisms,
symmetric monoidal natural isomorphisms as 2-morphisms.
Example: the doctrine of finite limits theories?.
Example: Let be the opposite of the -category of finitely presented groupoids. This is the free doctrine on one object. We could roughly call the doctrine of ‘a thing’: since its ‘sketch’ consists of single object (the thing). Here , so we call the doctrine of groupoids.
Example: Let as a discrete -category. Here , the - category of essentially discrete groupoids. So, is the doctrine of essentially discrete groupoids.
To get the sketch here, we draw an object and its identity morphism; then we take the homotopy limit of this, say . comes with a projection to the original object , 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 , we can take the homotopy limit of its identity morphism, and the result is the groupoid of ‘objects of equipped with automorphism’, say . There’s a forgetful functor but also a map going back, . followed by is isomorphic to the identity. If followed by is also isomorphic to the identity, is an (essentially) discrete groupoid.
More generally, for any finite limits theory we can cook up a doctrine whose theories in are just models of in . To do this, we take the sketch for and add in, for each object in the sketch, an equation saying that is inverse to , where is the homotopy limit of . This is a way of asserting that is ‘essentially discrete’.
Puzzle: What is a model of in ? It’s an ‘essentially discrete object in ’. But what’s that like.
Example: Let 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, and , and morphisms , . But now we take the weak pullback and put in a morphism . Then we put in 2-morphisms called the associator and left/right unitors, and make these obey the usual laws.
Now consider a model . There are morphisms in the groupoid of objects but also objects in the groupoid of morphisms . 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, 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, , for which is equivalent to the -category .
What do we add? Above we have morphisms in the groupoid of objects — call them ‘old morphisms’ — which are automatically invertible. But we also have objects in the groupoid of morphisms — 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 and forming a certain weak pullback. This has a map to (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 -ary operations for each .
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 -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 by pointing to its category of interpretations in , namely , and the ‘finitely presentable’ objects in here would correspond to objects of (and thus ). Conversely, we expect .
Example: let be the doctrine of finitely presented algebraic geometric theories. Claim: is the doctrine of algebraic geometric theories.
Example: There is a finite limits theory , which is the embodiment of propositional logic. All finite sets can be formed from by products and equalizers, so this finite limits theory is the Cauchy completion of the Lawvere theory whose objects are powers of , which is the opposite of the category of finitely presented Boolean algebras. Note: is the opposite of the category of profinite sets. since 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 , the -category of finitely presented groupoids. Claim: theories of this doctrine are theories of first-order predicate logic. Conjecture: is the opposite of the category of profinite groupoids. . With luck this will explain the appearance of profinite groups in number theory.