doctrines 6

on the one hand, doctrines are to (weakly) groupoid-enriched categories what "finite limits theories" (aka "lex theories") are to ordinary categories. this lets us apply to the study of doctrines ideas coming from the study of finite limits theories, notably "gabriel-ulmer duality" and the method of constructing finite limits theories by "sketches". this makes doctrines fairly easy to work with.

on the other hand, the concept of doctrine arises naturally in trying to understand the foundations of algebraic geometry (the reasons for going beyond affine varieties to projective varieties and schemes, the importance of line bundles and vector bundles and coherent sheaves, classifying toposes and moduli stacks, and so forth), so doctrines aren't just easy to work with; there's also something worthwhile to be accomplished by working with them.

(in fact for us the necessity of working with and understanding doctrines much preceded the realization that doctrines can be seen as the groupoid-based analog of finite limits theories, and that ideas from the study of finite limits theories come ready-made to apply to the study of doctrines.)

first we'll set up a "dictionary" connecting concepts from the study of finite limits theories with concepts from the study of doctrines; then we'll set up a "catalog" of doctrines including some toy examples but also examples of actual relevance to algebraic geometry.

a "finite limits theory" t is a small category (sometimes called "the syntactic category of t" or "the category of formulas of t") with all finite limits. a "doctrine" d is a small groupoid-enriched category (sometimes called "the syntactic 2-category of d" or "the 2-category of theories of d") with all finite homotopy limits.

for a finite limits theory t, the category of finite-limit-preserving functors from the syntactic category of t to the category of sets is called "the category of models of t". it's a large category of a certain kind, from which the syntactic category of t can be recovered by certain means. for a doctrine d, the groupoid-enriched category of finite-homotopy-limit-preserving groupoid-enriched functors from the syntactic 2-category of d to the groupoid-enriched category of groupoids is called "the groupoid-enriched category of environments for d". it's a large 2-category of a certain kind, from which the syntactic 2-category of d can be recovered by certain means.


hmmm, what about the idea of trying to use "infinity-doctrines" and have the (infinity,1)-category of infinity-doctrines be the (infinity,1)-category of infinity-environments of an infinity-doctrine .... ?????or something like that .... ?????....

??is it really true that the concept of "finite homotopy limits" is a/the good concept in the same way that the concept of "finite limits" is?? .... or something like that...

??so the way that gabriel-ulmer duality (of the "classical" kind?? or something like that) works is that _no_ formula is a model, nor vice versa ... ??no wait a minute, i'm very confused here now.... i guess that i was thinking of something like how no small category of formulas is a large category of models (or something like that...) ... so some sort of level slip or something...

i suppose that i should also consider the finite limits theory of "categories with all finite limits" ... or something like that...