nLab
doctrine

Doctrines

Idea

A doctrine, as the word was originally used by Jon Beck, is a categorification of a “theory”. Thus, a doctrine could also reasonably be called a “2-theory.”

Here we are using the word “theory” in a vague non-precise sense. For instance, there is a theory of groups, a theory of abelian groups, a theory of commutative rings, and so on. Likewise, there is a doctrine of monoidal categories, a doctrine of categories with finite products, a doctrine of rig categories, and so on.

Moreover, just as categories are objects of a 2-category (the categorification of a category), ordinary theories are objects of some doctrine. The doctrine in which a theory lives specifies the structure on categories in which models of that theory can be internalized. For instance, the theory of groups lives naturally in the doctrine of categories with finite products, since a group object can be defined in any such category. Likewise, the theory of monoids lives in the doctrine of monoidal categories, and so on.

Moreover, in general there is a “free” category containing a model (the “walking model”) of some given theory: for instance there is a category with finite products freely generated by a group object (namely, the Lawvere theory of a group), and a monoidal category freely generated by a monoid object (namely, the augmented simplex category). In this way, a theory whose models are categories in some doctrine can itself be regarded as a category in that doctrine, with the property that the category of models of a theory TT in a category KK is the hom-category hom(T,K)hom(T,K) in the relevant doctrine. In fact, we can fruitfully think of a doctrine as the collection of all theories in that doctrine, since (for example) any category with finite products can be regarded as a “theory” that can be interpreted in any other such category, via finite-product-preserving functors.

For this to make sense, whatever a doctrine is, it must in particular induce a 2-category of its models. Or, at least, of its models in Cat, which is so far all that we have talked about. But one can also imagine considering 2-theories as objects of some 3-theory, and so on. (Unfortunately this approach involves us in an infinite regress when we look for a formal definition!)

Definitions

As 2-monads

A number of people, starting with Lawvere, have defined “doctrine” to mean 2-monad (particularly a 2-monad on CatCat). This may seem reasonable, since all the examples of doctrines we considered above are, in fact, (the algebras for) some 2-monad on CatCat. However, it is not really correct.

At a lower level, the “theories” considered above of which a doctrine is supposed to be a categorification are also not the same as monads. In particular, the morphisms between such theories are not all representable by morphisms of monads. For instance, there is a morphism of theories from the theory of commutative rings to the theory of abelian groups which sends a ring to its multiplicative group of units, but this is not induced by any morphism of monads because it does not preserve the underlying set.

Likewise, not all “morphisms of doctrines” are representable by morphisms of 2-monads.

As 2-categories

Another possible definition of “doctrine” is just “a 2-category”. In this approach, we identify a doctrine with its category of models (in Cat). This has the advantage of simplicity. Moreover, we can say easily what a model of a theory in a doctrine is: it is just a morphism in the 2-category (of models of that doctrine). It is also easy to generalize to Higher doctrines (given a notion of higher category).

However, while useful, this approach has the disadvantage of being too broad: there are many 2-categories that we would not really want to consider as being the category of models of some doctrine.

See also at 2-algebraic theory.

As logics

The word “doctrine” can also be used to design a particular setting for categorical logic (e.g., categories with finite products, geometric logic etc…; see internal logic). This can also be formalized in a more general way using weak higher categories. This generalization is necessary to treat complicated algebraic structures like symmetric operads or higher operads in a categorical logical way.

References

General discussions of the “doctrine” concept:

A pedadogically aimed study of higher doctrines, using the simple definition of doctrines as (weak) n-categories described by generators and relations:

Revised on June 27, 2014 16:58:44 by Colin Zwanziger (174.63.87.107)