nLab doctrine

Redirected from "2-theories".
Doctrines

Doctrines

Idea

The concept of doctrine, as the word was originally used by Jon Beck, is a categorification of the concept of “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 cartesian double theories

In Lambert & Patterson, 2023, doctrines are treated as cartesian double categories. 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.

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.

As a class of limits

Especially in the theory of accessible categories and commutativity of limits and colimits, a “doctrine” is sometimes taken to be simply a class of shapes (or weights) for limits. For more about this, see sound doctrine.

References

William Lawvere, 23 Mar 2006:

The word “doctrine” itself is entirely due to Jon Beck and signifies something which is like a theory, except appropriate to be interpreted in the category of categories, rather than, for example, in the category of sets; of course, an important example of a doctrine is a 2-monad, and among 2-monads there are key examples whose category of “algebras” is actually a category of theories in the set-interpretable sense. Among such “theories of theories”, there is a special kind whose study I proposed in that paper. This kind has come to be known as “Kock-Zoeberlein” doctrine in honor of those who first worked out some of the basic properties and ramifications, but the recognition of its probable importance had emerged from those discussions with Jon.

The concept of doctrine is apparently first appears in print in

  • William Lawvere, Ordinal sums and equational doctrines, Lecture Notes in Math., Vol. 80 (Springer, Berlin, 1969).

General discussions of the “doctrine” concept:

Doctrines are treated as cartesian double categories in:

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

Last revised on May 7, 2024 at 09:47:01. See the history of this page for a list of all contributions to it.