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 (,1)(\infty,1)-categories.

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

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

Definition: A theory of the doctrine DD is a morphism F:DGpdF: D \to Gpd.

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)(3,2)-category. (Fill in the details.)

Definition: An interpretation of the doctrine CC in the doctrine DD is a morphism

F:CD.F : C \to D .

We often call CC the syntactic doctrine and DD the environment.

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

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

We call [C,Gpd][C,Gpd] the semantic doctrine associated to the syntactic doctrine CC. 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 CC and the latter DD.

Example: D=GpdD = Gpd, the (2,1)(2,1)-category of

  • groupoids,

  • 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 LL in a symmetric monoidal category which is invertible (there exists an object MM such that LM1L \otimes M \cong 1) and has S L,L=1 LLS_{L,L} = 1_{L \otimes L}. A dimensional theory over some commutative ring kk is a symmetric monoidal kk-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 kk.

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

  • dimensional theories as objects,

  • symmetric monoidal kk-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 kk is a symmetric monoidal kk-linear category with finite colimits. The key example of an algebraic geometric theory is the category of coherent sheaves over some scheme over kk — or more generally, over some Artin stack over kk.

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

  • algebraic geometric theories as objects,

  • symmetric monoidal kk-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 opC = FPGpd^{op} be the opposite of the (2,1)(2,1)-category of finitely presented groupoids. This is the free doctrine on one object. We could roughly call CC the doctrine of ‘a thing’: since its ‘sketch’ consists of single object (the thing). Here Mod(C,Gpd)=GpdMod(C,Gpd) = Gpd, so we call CC the doctrine of groupoids.

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

To get the sketch here, we draw an object XX and its identity morphism; then we take the homotopy limit of this, say YY. YY comes with a projection to the original object XX, 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 XX, we can take the homotopy limit of its identity morphism, and the result is the groupoid of ‘objects of XX equipped with automorphism’, say X˜\tilde{X}. There’s a forgetful functor p:X˜Xp: \tilde{X} \to X but also a map going back, i:XX˜i: X \to \tilde{X}. ii followed by pp is isomorphic to the identity. If pp followed by ii is also isomorphic to the identity, XX is an (essentially) discrete groupoid.

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

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

Example: Let CC 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, ObOb and MorMor, and morphisms i:ObMori: Ob \to Mor, s,t:MorObs,t: Mor \to Ob. But now we take the weak pullback Mor s× tMorMor {}_s \times_t Mor and put in a morphism :Mor s× tMorMor\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:CGpdF: C \to Gpd. There are morphisms in the groupoid of objects F(Ob)F(Ob) but also objects in the groupoid of morphisms F(Mor)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, CC 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, CC, for which Mod(C,Gpd)Mod(C,Gpd) is equivalent to the (2,1)(2,1)-category CatCat.

What do we add? Above we have morphisms in the groupoid of objects F(Ob)F(Ob) — call them ‘old morphisms’ — which are automatically invertible. But we also have objects in the groupoid of morphisms F(Mor)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×MorMor \times Mor and forming a certain weak pullback. This has a map to ObOb (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 nn-ary operations for each nn.

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 (,1)(\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 DD by pointing to its category of interpretations in GpdGpd, namely [D,Gpd][D,Gpd], and the ‘finitely presentable’ objects in here would correspond to objects of D opD^{op} (and thus DD). Conversely, we expect [D op,Gpd]D[D^{op}, Gpd] \simeq D.

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

Example: There is a finite limits theory FinSetFin\Set, which is the embodiment of propositional logic. All finite sets can be formed from 22 by products and equalizers, so this finite limits theory is the Cauchy completion of the Lawvere theory whose objects are powers of 22, which is the opposite of the category of finitely presented Boolean algebras. Note: [FinSet,Set]=BoolAlg[Fin\Set, Set] = \Bool\Alg is the opposite of the category of profinite sets. [FinSet op,Set]=Set[Fin\Set^{op}, Set] = Set since FinSet opFin\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 FPGpd\FP\Gpd, the (2,1)(2,1)-category of finitely presented groupoids. Claim: theories of this doctrine are theories of first-order predicate logic. Conjecture: [FPGpd,Gpd][\FP\Gpd, Gpd] is the opposite of the category of profinite groupoids. [FPGpd op,Gpd]=Gpd[\FP\Gpd^{op}, Gpd] = Gpd. With luck this will explain the appearance of profinite groups in number theory.

Revised on August 20, 2011 11:55:11 by Andrew Stacey? (129.241.15.200)