The n-Category Café

If what you really want is to be talking about $\mathbf{H}/W$ and $\mathbf{H}$, why don’t you just make that explicit? Work in the dependent type theory of $\mathbf{H}$ with a type called $W$ and use the $\Sigma$ and $\Pi$ types.

Sure, but I was just wondering if there was a process in reverse where because of how we think about some modalities we see we want an $\infty$-atomic morphism, and that leads us to the slice picture.

I think I’d need to know the intuition behind a morphism being described as ‘atomic’. How much of nLab: atomic topos would carry over to the $\infty$ case?

I can’t think offhand of a way to categorify the descriptions of 1-atomic topoi in terms of complete atomic Boolean algebras or generating sets of atoms. Johnstone remarks already in the 1-Elephant that these characterizations don’t even relativize to arbitrary 1-atomic geometric morphisms, so that the name “atomic” is arguably not really appropriate for geometric morphisms with codomain other than $Set$.

I think I mentioned this case in the antepenultimate paragraph of the post?

Yes you did! Sorry about that, I slipped right past it.

Thanks for the explanation, this helps.

I agree that it would be quite nice to have an $\infty$-version of Pare’s monadicity theorem for 1-toposes. I thought about this a little last year (and even talked to Mathieu Anel about it when he visited CMU), but in the end I didn’t make much progress. My hope was that having an impredicative universe might help – and that such a theorem would then help to better understand the impredicative encodings of colimits.

Interesting stuff! So to get an actual endofunctor it seems you need to be using an object classifier of the same size as the objects you’re mapping into it. For instance, for large spaces $X$ you’re considering the space of maps from $X$ into the large space of small spaces. I’m concerned these could all be essentially constant for appropriate $X$, which would blow up conservativity.

For instance, suppose $X$ is some $BG$, so that we’re looking at the space of spaces $Y$ with a homotopy coherent $G$-action. But it seems that if $G$ is, say, a large discrete simple group, we shouldn’t expect any maps from $G$ into a small group like the homotopy automorphisms of $Y$. If we assumed the $G$-action were strict, instead of homotopy coherent, this would be immediate, though I’m not sure how to reconcile the strictification process with the point set assumptions I made on $G$.

Of course, size issues mean that there is no hope of getting an actual monadicity theorem. I put “monadic on $U$-small objects” in scare quotes because I didn’t mean it literally, since as you say the operation $U^{(-)}$ is not an endofunctor of $U$-small objects. I didn’t have any precise meaning in mind, but I was thinking of something like “this operation that is not an endofunctor satisfies properties X, Y, and Z that monadic functors also satisfy, and which are sufficient for drawing various conclusions that we would like to draw from monadicity, such as the existence of colimits or the existence of adjoints”. There some paper that I can’t recall right now that does something like this for the presheaf-category “monad” on $Cat$. I don’t know for sure whether something like it would work here, but it seems fairly likely to me that it would if we could deal with the other problems. Hence, why I decided to ignore size issues for now and focus on the issues of categorification, which seem more serious to me.

the operation $(−)U^{(-)}$ is not an endofunctor of $U$-small objects

Don’t forget, there is the paper Monads need not be endofunctors.

If you’re looking for examples of non-hypercomplete $\infty$-topoi, look no further than the $\infty$-topos of parameterized spectra, or more generally the $\infty$-topos of (finitary) $n$-excisive, unpointed functors $Top \to Top$ for fixed $n$. To me, this has become one of the most fundamental examples of an $\infty$-topos out there! Similarly, I think the tangent $\infty$-topos of an arbitrary $\infty$-topos is rarely hypercomplete.

Actually, given that the topos of $n$-excisive functors can be defined using a site of finite sets and surjections, maybe non-hypercompleteness is something important to consider when it comes to atomic geometric morphisms.

How about this: should the forgetful functor from paramterized spectra to spaces be an atomic geometric morphism?

Okay, so that forgetful functor is certainly locally $\infty$-connected (indeed, it’s cohesive). But is it even $(-1)$-atomic, i.e. does its inverse image functor preserve the subobject classifier?

I think it is.

Note that a stable $\infty$-category has no non-equivalence monomorphisms.

Let $S$ denote the $\infty$-category of spaces, and let $TS$ denote the $\infty$-category of parameterized spectra. The forgetful functor $U: TS \to S$ preserves limits, and in particular monomorphisms. Any morphism $f: (E,X) \to (F,Y)$ in $TS$ factors as a fiberwise morphism $f_0$ in $T_X S$ (the category of $X$-parameterized spectra) followed by $f_1$, a cartesian lift of $Uf$. Now, if $f$ is mono, then $Uf$ is mono, and so $f_1$ is mono. Then by pasting properties of pullback squares, $f_0$ is mono in $TS$, and hence also in the stable category $T_X S$. So $f_0$ is an equivalence. So $f$ is cartesian over a monomorphism in $S$. Thus the forgetful functor $Mono(TS)/(F,Y) \to Mono(S)/Y$ is an equivalence.

Hmm. And maybe a similar argument would work to show that it’s $n$-atomic for all finite $n$.

I think the main reason I’m skeptical of this “intermediate notion of atomic” is that for other classes of geometric morphisms, like locally connected, proper, local, etc., it seems clear that the “important” notion for $\infty$-toposes is the one that refers to the whole $(\infty,1)$-topos rather than playing games with $\infty$-truncatedness. There might be intermediate notions in those cases too, but we haven’t dignified them with names like “locally $\infty$-connected” or “$\infty$-proper”; if I had to talk about them, I might invent a name like “$(\infty-1)$-proper”. I suppose we could consider renaming everything and using something like “$(\infty+1)$-proper” for the stronger versions, but it seems more natural to me for the condition that refers to the whole $\infty$-topos to be the one with the prefix $\infty$.

I guess my inclination would be to use the unadorned term (e.g. “proper geometric morphism”) for the notion referring to the whole topos. But maybe this clashes too much with existing usage.

Alternatively, one could use the prefix $\omega$ – e.g. “$\omega$-proper geometric morphism” would mean “$n$-proper geometric morphism for all $n$”, and save $\infty$ for the notion referring to the whole topos. Actually, I kind of like that – $\omega$ connotes the notion of infinity meaning that says “bigger than all finite things”, while $\infty$ connotes a more absolute,”bigger” notion of infinity.

I want to defend keeping the prefix $\omega$- to refer to actual $\omega$-categories, i.e. the things that nowadays some people call $(\infty,\infty)$-categories because they started abusing “$\infty$-category” to mean $(\infty,1)$-category.

It would certainly make sense that when the objects under consideration are $n$-topoi for some $0\le n\le \infty$, the default meaning of “proper” would be “$n$-proper”. That does clash with existing usage for 1-toposes: a “proper geometric morphism” between 1-toposes is actually a $(-1)$-proper one (a 0-proper one being called ‘tidy’), while a “locally connected geometric morphism” between 1-toposes is actually a locally $0$-connected one (a locally $(-1)$-connected one being called ‘open’). True, in the $\infty$-case there’s less room for ambiguity, but I think there should always be the option of adding the prefix for disambiguation, and the prefix $\infty$- ought to refer to the “most natural” notion for $\infty$-toposes.