You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Fernando Yamauti (Jun 03 2025 at 02:42):Well. Equivariant homotopy theory is homotopy theory internal to presheaves on the orbit category. More generally, homotopy theory inside the topos of presheaves over a homotopy type is parametrized homotopy theory.
Fernando Yamauti (Jun 03 2025 at 02:53):As for the 1-cat case, one analogous of the first would be the topos of -sets. But I can't remember now any interesting theorem internal to this topos that would translate externally to something surprising. Perhaps people around here who have worked with -sets or representation theory of discrete groups might know some examples. Let's try tagging some @Morgan Rogers (he/him) @John Baez @Ryuya Hora
David Corfield (Jun 03 2025 at 06:42):I don't know if you've seen this already, but there's an MO question in this area which might provide some leads. E.g., the [[Bohr topos]] mentioned there is a presheaf topos.
Yiming Xu (Jun 03 2025 at 07:18):Many thanks!
Fernando Yamauti said:
Well. Equivariant homotopy theory is homotopy theory internal to presheaves on the orbit category. More generally, homotopy theory inside the topos of presheaves over a homotopy type is parametrized homotopy theory.
Many thanks! Both for providing this example and for pinging people around!
So I guess for homotopy theory, we are interested in the presheaves of abelian groups, right? Is there any concrete geometric formula that serves as minimal working example of what is going on there?
Yiming Xu (Jun 03 2025 at 07:19):David Corfield said:
I don't know if you've seen this already, but there's an MO question in this area which might provide some leads. E.g., the [[Bohr topos]] mentioned there is a presheaf topos.
Many thanks for the reference, I will check that as well.
Morgan Rogers (he/him) (Jun 03 2025 at 07:49):Beware that it sounds like you are conflating two logical aspects of toposes. Classifying toposes relate to geometric theories (the fragment of logic whose interpretation is preserved by geometric morphisms) while the "internal language of a topos" usually refers to the richer higher-order logic, which in typical accounts is written with notation resembling that of set theory. Only in the latter can one can talk about the Heyting operation on subobjects, notably including pseudocomplements, which are needed to state de Morgan's laws or the law of excluded middle.
Morgan Rogers (he/him) (Jun 03 2025 at 07:51):So if you've heard that a theorem is true "in any Boolean topos", that's typically a statement that the proof of the theorem is valid in the internal language of such toposes (typically meaning it uses LEM but nothing stronger)
Yiming Xu (Jun 03 2025 at 07:54):I see. My fault! Then I think I should edit the title of my question to only address interpreting geometric formulas. I intended to talk about Grothendieck topos stuff. The current piece of work relevant to this question does care about the preservation of formulas, which makes the negation operator unavailable for us since the subobject classifier is not necessarily preserved by geometric morphism.
But incidentally, what if we have a geometric morphism that luckily preserves the subobject classifier? Do we have an intuitive criteria that tell us when it happens?
Morgan Rogers (he/him) (Jun 03 2025 at 08:06):I should clarify that these things are interrelated, and produce surprising results. A classic example is the result that the universal local ring (which lives in the Zariski topos) is a field.
Morgan Rogers (he/him) (Jun 03 2025 at 08:10):To get back to answering your original question, the interpretation of a geometric formula in a presheaf topos (after fixing a signature/language and its interpretation in the topos over which to interpret the formula) tend to be not so surprising: everything is calculated "pointwise", so conjunctions and disjunctions are intersections and unions in the sets obtained by evaluating a presheaf, and similarly for existential quantification.
Yiming Xu (Jun 03 2025 at 08:14):Yes, the simplicity of presheaves, just as families of structures, makes it challenging to dig out something nontrivial. We would need a interesting presheaf topos, and I am not aware of any except for -sets (as hinted), and maybe the topos of trees (https://cs.au.dk/~birke/papers/sgdt-journal.pdf)
Yiming Xu (Jun 03 2025 at 08:16):Morgan Rogers (he/him) said:
I should clarify that these things are interrelated, and produce surprising results. A classic example is the result that the universal local ring (which lives in the Zariski topos) is a field.
Indeed surprising! Could you please elaborate a bit on why this example is a witness to the relevance?
daniel gratzer (Jun 03 2025 at 11:41):Yiming Xu said:
Yes, the simplicity of presheaves, just as families of structures, makes it challenging to dig out something nontrivial. We would need a interesting presheaf topos, and I am not aware of any except for -sets (as hinted), and maybe the topos of trees (https://cs.au.dk/~birke/papers/sgdt-journal.pdf)
While these two are certainly interesting, one can also find quite a lot of interesting structure in simplicial sets, cubical sets, or similar presheaf topoi. My collaborators and I have been extending some of the work by Riehl and Shulman using certain logical aspects of presheaves on the simplex category (these logical aspects are themselves closely related by the work by Blechschmidt and others on the logical properties of the Zariski topos). Also a lot of the work in dependent type theory on parametricity features various presheaf categories to structure things.
Fernando Yamauti (Jun 03 2025 at 13:10):Yiming Xu said:
So I guess for homotopy theory, we are interested in the presheaves of abelian groups, right? Is there any concrete geometric formula that serves as minimal working example of what is going on there?
It should be presheaves valued in homotopy types (aka anima and -groupoids). So I was referring to -topoi. Though a lot of people in homotopy theory tend to say simply "topoi" and drop the prefix.
In this case, anything that can be proven in HoTT should also be a theorem internally inside those things (e.g., Hurewicz theorem).
What tends to give more surprising theorems, even for -topoi, are statements about internal topoi. For instance, there are very simple characterizations of when a geometric morphism is, for instance, proper or locally connected in terms of the internal sites inside the codomain of the respective geometric morphism. Externalising those statements tends to be a hell even when the codomain is a presheaf topos.
Also, since you assumed that internal statements inside sheaves over top spaces are meaningful, perhaps it's relevant to notice that presheaves over preorders (finite preorders if we are talking about higher topoi) are sheaves over the respective Aleksandrov space. The Bohr topos mentioned by @David Corfield is such an example.
I would still, though, like to see some complicated statement about, say, representation theory of finite groups over some field turned into a simpler statement about -algebras inside the topoi of -sets.
Mike Shulman (Jun 03 2025 at 16:10):A nonzero number of classifying toposes turn out to be presheaf topoi, and they of course are defined by a generic interpretation of a specific geometric theory. For instance, the topos of simplicial sets is the classifying topos of a strict interval.
Yiming Xu (Jun 03 2025 at 17:04):Oh that's nice! Makes much sense! I will also think more in this direction of theories of presheaf types.