∞-Atomic Geometric Morphisms
Posted by Mike Shulman
Today’s installment in the ongoing project to sketch the -elephant: atomic geometric morphisms.
Chapter C3 of Sketches of an Elephant studies various classes of geometric morphisms between toposes. Pretty much all of this chapter has been categorified, except for section C3.5 about atomic geometric morphisms. To briefly summarize the picture:
Sections C3.1 (open geometric morphisms) and C3.3 (locally connected geometric morphisms) are steps and on an infinite ladder of locally n-connected geometric morphisms, for . A geometric morphism between -toposes is locally -connected if its inverse image functor is locally cartesian closed and has a left adjoint. More generally, a geometric morphism between -toposes is locally -connected, for , if it is “locally” locally -connected on -truncated maps.
Sections C3.2 (proper geometric morphisms) and C3.4 (tidy geometric morphisms) are likewise steps and on an infinite ladder of n-proper geometric morphisms.
Section C3.6 (local geometric morphisms) is also step on an infinite ladder: a geometric morphism between -toposes is -local if its direct image functor has an indexed right adjoint. Cohesive toposes, which have attracted a lot of attention around here, are both locally -connected and -local. (Curiously, the case of locality doesn’t seem to be mentioned in the 1-Elephant; has anyone seen it before?)
So what about C3.5? An atomic geometric morphism between elementary 1-toposes is usually defined as one whose inverse image functor is logical. This is an intriguing prospect to categorify, because it appears to mix the “elementary” and “Grothendieck” aspects of topos theory: a geometric morphisms are arguably the natural morphisms between Grothendieck toposes, while logical functors are more natural for the elementary sort (where “natural” means “preserves all the structure in the definition”). So now that we’re starting to see some progress on elementary higher toposes (my post last year has now been followed by a preprint by Rasekh), we might hope be able to make some progress on it.
Unfortunately, the definitions of elementary -topos currently under consideration have a problem when it comes to defining logical functors. A logical functor between 1-toposes can be defined as a cartesian closed functor that preserves the subobject classifier, i.e. . The higher analogue of the subobject classifier is an object classifier — but note the switch from definite to indefinite article! For Russellian size reasons, we can’t expect to have one object classifer that classifies all objects, only a tower of “universes” each of which classifies some subcollection of “small” objects.
What does it mean for a functor to “preserve” the tower of object classifiers? If an -topos came equipped with a specified tower of object classifiers (indexed by , say, or maybe by the ordinal numbers), then we could ask a logical functor to preserve them one by one. This would probably be the relevant kind of “logical functor” when discussing categorical semantics of homotopy type theory: since type theory does have a specified tower of universe types , the initiality conjecture for HoTT should probably say that the syntactic category is an elementary -topos that’s initial among logical functors of this sort.
However, Grothendieck -topoi don’t really come equipped with such a tower. And even if they did, preserving it level by level doesn’t seem like the right sort of “logical functor” to use in defining atomic geometric morphisms; there’s no reason to expect such a functor to “preserve size” exactly.
What do we want of a logical functor? Well, glancing through some of the theorems about logical functors in the 1-Elephant, one result that stands out to me is the following: if is a logical functor with a left adjoint , then induces isomorphisms of subobject lattices . This is easy to prove using the adjointness and the fact that preserves the subobject classifier:
What would be the analogue for -topoi? Well, if we imagine hypothetically that we had a classifier for all objects, then the same argument would show that induces an equivalence between entire slice categories . (Actually, I’m glossing over something here: the direct arguments with and show only an equivalence between sets of subobjects and cores of slice categories. The rest comes from the fact that preserves local cartesian closure as well as the (sub)object classifier, so that we can enhance to an internal poset and to an internal full subcategory and both of these are preserved by as well.)
In fact, the converse is true too: reversing the above argument shows that preserves if and only if induces isomorphisms of subobject lattices, and similarly preserves if and only if induces equivalences of slice categories. The latter condition, however, is something that can be said without reference to the nonexistent . So if we have a functor between -toposes that has a left adjoint , then I think it’s reasonable to define to be logical if it is locally cartesian closed and induces equivalences .
Furthermore, a logical functor between 1-toposes has a left adjoint if and only if it has a right adjoint. (This follows from the monadicity of the powerset functor for 1-toposes, which we don’t have an analogue of (yet) in the -case.) In particular, if the inverse image functor in a geometric morphism is logical, then it automatically has a left adjoint, so that the above characterization of logical-ness applies. And since a logical functor is locally cartesian closed, this geometric morphism is automatically locally connected as well. This suggests the following:
Definition: A geometric morphism between -topoi is -atomic if
- It is locally -connected, i.e. is locally cartesian closed and has a left adjoint , and
- induces equivalences of slice categories for all .
This seems natural to me, but it’s very strong! In particular, taking we get an equivalence , so that is equivalent to a slice category of . In other words, -atomic geometric morphisms coincide with local homeomorphisms!
Is that really reasonable? Actually, I think it is. Consider the simplest example of an atomic geometric morphism of 1-topoi that is not a local homeomorphism: for a group . The corresponding geometric morphism of -topoi is a local homeomorphism! Specifically, we have . So in a sense, the difference between atomic and locally-homeomorphic vanishes in the limit .
To be sure, there are other atomic geometric morphisms of 1-topoi that do not extend to local homeomorphisms of -topoi, such as for a topological group . But it seems reasonable to me to regard these as “1-atomic morphisms that are not -atomic” — a thing which we should certainly expect to exist, just as there are locally 0-connected morphisms that are not locally -connected, and 0-proper morphisms that are not -proper.
We can also “see” how the difference gets “pushed off to ” to vanish, in terms of sites of definition. In C3.5.8 of the 1-Elephant it is shown that every atomic Grothendieck topos has a site of definition in which (among other properties) all morphisms are effective epimorphisms. If we trace through the proof, we see that this effective-epi condition comes about as the “dual” class to the monomorphisms that the left adjoint of a logical functor induces an equivalence on. Since an -topos has classifiers for -truncated objects, we would expect an atomic one to have a site of definition in which all morphisms belong to the dual class of the -truncated morphisms, i.e. the -connected morphisms. So as , we get stronger and stronger conditions on the morphisms in our site, until in the limit we have a classifier for all morphisms, and the morphisms in our site are all required to be equivalences. In other words, the site is itself an -groupoid, and thus the topos of (pre)sheaves on it is a slice of .
However, it could be that I’m missing something and this is not the best categorification of atomic geometric morphisms. Any thoughts from readers?
Re: ∞-Atomic Geometric Morphisms
So you’ve made advances on this in under six weeks:
The original motivation for my question was modal logic. Now we know that modal homotopy type theory is all about mapping between -toposes, does your suggestion point us anywhere interesting?
We’re also in the territory of my MO question that Jacob Lurie kindly answered.