Let us say that a geometric theory T is of presheaf type if its classifying topos
is (equivalent to) a presheaf topos. (We adhere to the convention that geometric logic allows arbitrary disjunctions, while coherent logic means geometric and finitary.) Write Mod(T) for the category of Set-models and homomorphisms of T. The next proposition is well known; see, for example, MacLane–Moerdijk [13], pp. 381-386, and the textbook of Adámek–Rosický [1] for additional information:
Proposition 0.1. For a category
, the following properties are equivalent:
(i)
is a finitely accessible category in the sense of Makkai–Paré [14], i.e., it has filtered colimits and a small dense subcategory
of finitely presentable objects
ii)
is equivalent to Pts
, the category of points of some presheaf topos
(iii)
is equivalent to the free filtered cocompletion (also known as Ind-
) of a small category
.
(iv)
is equivalent to Mod(T) for some geometric theory of presheaf type.
Moreover, if these are satisfied for a given
, then the
—in any of (i), (ii) and (iii)—can be taken to be the full subcategory of
consisting of finitely presentable objects. (There may be inequivalent choices of
, as it is in general only determined up to idempotent completion; this will not concern us.)
This seems to completely solve the problem of identifying when T is of presheaf type: check whether Mod(T) is finitely accessible and if so, recover the presheaf topos as Set-functors on the full subcategory of finitely presentable models. There is a subtlety here, however, as pointed out (probably for the first time) by Johnstone [10].