This entry is about the theorem in topos theory. For the theorem in logic that often goes by the same name, see at Diaconescu-Goodman–Myhill theorem.
Diaconescu’s theorem asserts that any presheaf topos is the classifying topos for internally flat functors on its site.
Often a special case of this is considered, which asserts that for every topological space and discrete group there is an equivalence of categories
between the geometric morphisms from the sheaf topos over to the category of permutation representations of and the category of -torsors on .
For a category, write
for its presheaf topos.
For any topos, write
for the full subcategory of the functor category on the internally flat functors.
(Diaconescu’s theorem)
There is an equivalence of categories
between the category of geometric morphisms and the category of internally flat functors .
This equivalence takes to the composite
where is the Yoneda embedding and is the inverse image of .
See for instance (Johnstone, theorem B3.2.7).
If is a finitely complete category we may think of it as the syntactic category and in fact the syntactic site of an essentially algebraic theory . An internally flat functor is then precisely a finite limit preserving functor, hence is precisely a -model in .
Therefore the above theorem says in this case that there is an equivalence of categories
between the geometric morphisms and the -models in .
This says that is the classifying topos for .
If is a discrete group and is its delooping groupoid, is the category of permutation representations of , also called the classifying topos of .
In this case an internally flat functor may be identified with a -torsor object in .
For this reason one sees in the literature sometimes the term “torsor” for internally flat functors out of any category . It is however not so clear in which sense this terminology is helpful in cases where is not a delooping groupoid or at least some groupoid.
A standard reference is section B3.2 in
The first proof of this result can be found in:
Another proof is in
Last revised on June 6, 2019 at 17:18:53. See the history of this page for a list of all contributions to it.