Category Theory
Zulip Server
Archive

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.

Stream: theory: category theory

Topic: Proof that locales gives a separating family in topoi

Fernando Yamauti (Oct 29 2025 at 10:28):

Hi. Does anyone know perhaps a proof of the following fact without using any specific construction of a covering of effective descent given by a localic topos?

Statement. The functor $\mathbf{Topos} \to \widehat{\mathbf{Loc}}$ given by $\mathcal{X} \mapsto {h_{\mathcal{X}}}_{| \mathbf{Loc}}$, i.e., Yoneda and then restriction, is fully faithful.

Perhaps there's a tricky way using some property about models of geometric theories in locales...?

Jens Hemelaer (Oct 29 2025 at 18:49):

Some ideas:

You can decompose a topos into locale slices: for each object $X$ in the topos $\mathcal{E}$ you can write $L_X$ for the localic reflection of $\mathcal{E}/X$ (its opens correspond to the subobjects of $X$). There is a geometric morphism
$i_X : L_X \to \mathcal{E}$
for each $X$. The pullback $i_X^*$ restricts a sheaf to the frame of subobjects of $X$.

The family of the $i_X$'s is jointly surjective: if there are two objects $F$ and $G$ in $\mathcal{E}$ and $i_X^*F \cong i_X^*G$ for each $X$ then $F \cong G$.

Now for two geometric morphisms $\phi,\psi: \mathcal{E} \to \mathcal{E'}$ you can similarly show that $\phi \cong \psi$ as soon as $\phi\circ i_X \cong \psi\circ i_X$ for all objects $X$.

Jens Hemelaer (Oct 29 2025 at 19:30):

Ok, this doesn't seem to work... there is no geometric morphism $i_X$ in general the way I described it.

Ivan Di Liberti (Oct 30 2025 at 18:47):

Errol Yuksel gave a talk at CT last year where he claimed to have proven this theorem.

Fernando Yamauti (Oct 30 2025 at 22:24):

Ivan Di Liberti said:

Errol Yuksel gave a talk at CT last year where he claimed to have proven this theorem.

Do you mean this talk https://xabier.garcia.martinez.webs.uvigo.gal/CT2024/files/Slides/Yuksel_Slides.pdf ?

If so, that seems the same proof as usual, where one has to find some localic topos with a map of effective descent to the classifying topos of the one object theory. That’s exactly what I'm trying to avoid.

Btw, I briefly talked to him last year at the topos conference about a sketch of a proof I had of a higher version of Joyal-Tierney. I recall he was trying to prove some version of JT for ionads.

Fernando Yamauti (Oct 30 2025 at 22:31):

What I'm after could be something along the lines of what @Jens Hemelaer was suggesting: some canonically defined maximal atlas instead of a specific atlas constructed in a somewhat intrincate way.

Ivan Di Liberti (Oct 31 2025 at 10:26):

No, I do not mean that. I meant this one: https://archive.math.muni.cz/conference/ct2025/data/uploads/abstracts/yuksel.pdf

Fernando Yamauti (Oct 31 2025 at 19:27):

Ivan Di Liberti said:

No, I do not mean that. I meant this one: https://archive.math.muni.cz/conference/ct2025/data/uploads/abstracts/yuksel.pdf

Ah! So not last year's CT! Admittedly almost though!

Here are the slides if anyone is interested

Thanks for the pointer. He still relies on JT's covering though to prove that the maximal covering does the job. The improvement of Moerdijk-Vermeulen (which I was unaware of) is that open surjections are also lax effective epis (so we get a $(2, 2)$-sheaf besides a $(2, 1)$-sheaf).

Btw, MW's result on the slides (I have yet to check the original paper though), then, imply that the topos associated to a specific localic category coincides with the topos associated to the groupoid completion of such localic cat.

Christopher Townsend (Nov 01 2025 at 07:39):

Fernando Yamauti said:

Ivan Di Liberti said:

No, I do not mean that. I meant this one: https://archive.math.muni.cz/conference/ct2025/data/uploads/abstracts/yuksel.pdf

Ah! So not last year's CT! Admittedly almost though!

Here are the slides if anyone is interested

Thanks for the pointer. He still relies on JT's covering though to prove that the maximal covering does the job. The improvement of Moerdijk-Vermeulen (which I was unaware of) is that open surjections are also lax effective epis (so we get a $(2, 2)$-sheaf besides a $(2, 1)$-sheaf).

Btw, MW's result on the slides (I have yet to check the original paper though), then, imply that the topos associated to a specific localic category coincides with the topos associated to the groupoid completion of such localic cat.

Yes, I think this was perhaps what I was alluding to during my QA at Octoberfest. We can 'get' the localic category of a bounded topos via the 2-structure of the 2-category of toposes.

As to the main question: can we avoid the standard `localic cover + descent' argument and still get full & faithful representation of geometric morphisms ? I think this results needs the toposes to be bounded (would we really expect it for elementary toposes?).

Once we have the bound in our topos F, then we have a localic effective descent morphism: W->>1 where W=[N->>B], i.e. surjections from the naturals to the bound (in F). This is enough to get that Loc_F = [G,Loc] (+) so you can get the result without topos-theoretic descent, but obviously at the cost of needing localic descent - so I don't think we can avoid some sort of descent argument to get there.

(+) http://www.christophertownsend.org/Documents/LOCALIC_PROOF_LOCALIC_GROUPOID_GROTH_20111018.pdf

Errol Yuksel (Nov 03 2025 at 14:27):

Hi. I am not aware of any proofs of this fact that don’t rely in some way on localic covers or descent.

However, it might be possible to adapt to the pointfree setting the recent work of Hamad, Marquès-Tarantino-van Gool, and Saadia, which generalise ultracategories.
On one level, the representation theorem they each showed can be understood as showing that topological spaces are dense in the category of toposes with enough points. The three proofs are different and make different uses of localic/topological covers.
In particular the proof of Marquès-Tarantino-van Gool does not seem to rely on those at all, and adapting it might yield a proof which relies only on properties of models of geometric theories in locales as you were hinting at.

Fernando Yamauti (Nov 04 2025 at 07:29):

Christopher Townsend said:

As to the main question: can we avoid the standard `localic cover + descent' argument and still get full & faithful representation of geometric morphisms ? I think this results needs the toposes to be bounded (would we really expect it for elementary toposes?).

Yes. "Topos" for me means always "Grothendieck topos", so everything is bounded.

Once we have the bound in our topos F, then we have a localic effective descent morphism: W->>1 where W=[N->>B], i.e. surjections from the naturals to the bound (in F). This is enough to get that Loc_F = [G,Loc] (+) so you can get the result without topos-theoretic descent, but obviously at the cost of needing localic descent - so I don't think we can avoid some sort of descent argument to get there.

I don't mind descent. I just don't want a proof relying on JT's covering and its variations (surjections or partial surjections potentially satisfying some property from some infinite cardinal to the bound).

I still think JT's covering and also Barr's and Diaconescu's are somewhat artificial. But that’s perhaps mainly a cosmetically aversion I have. Perhaps I'm just stupid and those specific atlases are actually universal in some sense I cannot yet apprehend.

Btw, since you mentioned your QA at the Octoberfest, can you refresh my memory on what you said about the localic category presenting a topos? Was it just that statement I'd mentioned from MW? It was too late that day and I was very sleepy...

Fernando Yamauti (Nov 04 2025 at 09:02):

Errol Yuksel said:

However, it might be possible to adapt to the pointfree setting the recent work of Hamad, Marquès-Tarantino-van Gool, and Saadia, which generalise ultracategories.
On one level, the representation theorem they each showed can be understood as showing that topological spaces are dense in the category of toposes with enough points. The three proofs are different and make different uses of localic/topological covers.
In particular the proof of Marquès-Tarantino-van Gool does not seem to rely on those at all, and adapting it might yield a proof which relies only on properties of models of geometric theories in locales as you were hinting at.

Hi. I think I've never seen you around here. Thanks for chiming in!

Cool! I was not aware of Marquès-Tarantino-van Gool paper.

There are, then, two points to be addressed based on their construction.

1. In the enough points case, however, I think there's always a canonical covering present, namely, a disjoint union of the terminal topos indexed by a separating family of points. So an almost atlas is already given (not of effective descent in general, only surjective)

2. It's also not clear how to construct an atlas of made of topological spaces for each ultraconvergence space. Perhaps that doesn't even exist for arbitrary ultraconvergence spaces (for instance, one such that étales spaces over it doesn't form a topos)?

I don't know if covering by a surjection is easier than covering by an open surjection. If it's not, 1 seems hopeless for now.

Jens Hemelaer (Nov 04 2025 at 21:59):

I like the idea of this surjection from a disjoint union of points to a topos with enough points. I would be interested in having something similar for any Grothendieck topos. Maybe following this kind of ideas will lead to rediscovering the construction from Barr's theorem?

This surjection from disjoint union of points to topos with enough points also shows that just surjection is indeed not enough to answer the original question, you need something more (open surjection if I understand you correctly).

Fernando Yamauti (Nov 05 2025 at 07:08):

Jens Hemelaer said:

I like the idea of this surjection from a disjoint union of points to a topos with enough points. I would be interested in having something similar for any Grothendieck topos. Maybe following this kind of ideas will lead to rediscovering the construction from Barr's theorem?

Yes. But the usual proofs I remember construct first an open surjection by a locale and, then, cover that locale by a Boolean one. That's why I said it's perhaps as difficult as finding a real atlas.

But now I'm starting to remember I've seen a proof in some notes of Cisinski that doesn't rely on a real atlas. I will search that later.

This surjection from disjoint union of points to topos with enough points also shows that just surjection is indeed not enough to answer the original question, you need something more (open surjection if I understand you correctly).

That's point 2: finding out if it's possible and how to cover (as a jointly effective epi) an ultraconvergent space by topological spaces.

For coherent topoi, it's true that the associated left ultracategory is completely determined by its values on compacta (left ultracats embed fully faithfully into condensed cats). But I don't know the analogous statement for those ultraconv spaces.

Errol Yuksel (Nov 05 2025 at 15:57):

1. If what you are after is a surjective geometric morphism, then yes toposes with enough points come with a canonical covering. However, if you’re interested in groupoidal representations or density I think you need to ask more of this covering. For instance, the cover which comes out of the representation theorem of Butz-Moerdijk is more involved than just a separating family of points, and the paper of Wrigley really shows that more structure than just the points is needed.

2. I thought you wanted to avoid atlases and that’s why I mentioned the Marquès-Tarantino-van Gool paper over the other two. But regarding your question about atlases for ultraconv. spaces, I recommend Saadia’s paper whose proof goes through coverings of ultraconv. spaces/toposes with enough points.

My main point is that the representation of toposes with enough points in terms of ultraconv. spaces is closely linked to the density of topological spaces in toposes with enough points. Indeed, I believe Hamad actually proves the latter and only then deduces the former. That the former implies the latter follows directly if we know that topological spaces are dense in ultraconv. spaces, which should be easier to show than for toposes.
As you mention, the case of ultracategories and compacta is already in Lurie (and does not really rely on atlases iirc). Also, the posetal ultraconv. spaces are relational beta-modules which are known to be equivalent to topological spaces, so in a sense it boils down to showing that “beta-“posets are dense in “beta-“categories.

Of course, my first answer was quite speculative: assuming we had a pointfree version of ultraconv. spaces, a proof of reprensation of toposes therein which did not rely on covers (e.g. a pointfree version of the Marquès-Tarantino-van Gool proof), and that locales were dense in these pointfree ultraconv. spaces, then I think we could deduce a proof of the fact that you were after without covers/atlases. But that’s a lot of ifs.

Fernando Yamauti (Nov 05 2025 at 21:53):

Errol Yuksel said:

1. If what you are after is a surjective geometric morphism, then yes toposes with enough points come with a canonical covering. However, if you’re interested in groupoidal representations or density I think you need to ask more of this covering. [...]
2. I thought you wanted to avoid atlases and that’s why I mentioned the Marquès-Tarantino-van Gool paper over the other two.

Yes. Surjective geom morphisms are, in general, not of effective descent. Perhaps I should clarify what I'm after and also some sloppy language I've been using.

To avoid further confusion, from now on, I will use the word "atlas" when the covering is an effective epi with a Cech nerve that is levelwise affine (locale or top space depending on the context). The word "covering" will always mean a morphism or a family of morphisms with the same target.

Best proof: density without using any covering whatsoever. Notice though that implicitly the maximal covering ($Loc_{/{\mathcal{X}}}$ for a fixed topos $\mathcal{X}$) is being used (since density means such covering is an epi in the cat of topoi).

2nd best proof: proving that the maximal covering is an effective epi in the cat of topoi without using any smaller atlas (such as JT's).

3rd best proof: proving that some covering satisfying some universal property is an epimorphism or an effective epimorphism.

But regarding your question about atlases for ultraconv. spaces, I recommend Saadia’s paper whose proof goes through coverings of ultraconv. spaces/toposes with enough points.

I couldn't find anything like an atlas for arbitrary ultraconvergent spaces in this paper. Is it proven somewhere there? I don't even know whether that's true in general.

Lurie (Thm.4.4.7) proves only for ultragroupoids that those can be presented by an atlas of compacta, but the statement for ultracats is missing though. He proves density in Thm.4.3.3.

My main point is that the representation of toposes with enough points in terms of ultraconv. spaces is closely linked to the density of topological spaces in toposes with enough points. Indeed, I believe Hamad actually proves the latter and only then deduces the former. That the former implies the latter follows directly if we know that topological spaces are dense in ultraconv. spaces, which should be easier to show than for toposes.

Hmm... I'm not finding that also. The statement is Lemma 7.6, but the proof requires Moerdijk-Butz's atlas (which is not much different from JT's)

As you mention, the case of ultracategories and compacta is already in Lurie (and does not really rely on atlases iirc). Also, the posetal ultraconv. spaces are relational beta-modules which are known to be equivalent to topological spaces, so in a sense it boils down to showing that “beta-“posets are dense in “beta-“categories.

Yes. Lurie doesn't explicitly use an atlas in order to prove $Fun^{LUlt} (Pt(-), Set)$ recovers the topos. He proves instead that for a pretopos $\mathcal{C}$ some sheaves on $\text{Pro} (\mathcal{C})$ can be seen as sheaves on the cat of elements of the representable functor associating each compactum $X$ to $X$-valued models of $C$.

But, anyways, a proof that $Mod (\mathcal{C})$ has an atlas is missing and I don't think the core of $Mod (\mathcal{C})$ is enough to recover sheaves over $\mathcal{C}$.

Of course, my first answer was quite speculative: assuming we had a pointfree version of ultraconv. spaces, a proof of reprensation of toposes therein which did not rely on covers (e.g. a pointfree version of the Marquès-Tarantino-van Gool proof), and that locales were dense in these pointfree ultraconv. spaces, then I think we could deduce a proof of the fact that you were after without covers/atlases. But that’s a lot of ifs.

My 2 points were addressing that. More precisely, 1 was addressing what should substitute the functor points and 2 was addressing how to prove that locales are dense in (the conjectural) pointfree ultraconv spaces.

Errol Yuksel (Nov 07 2025 at 15:07):

Ah thank you for clarifying the difference between atlas and covering, I had been using them somewhat interchangeably thus far.

Best proof: density without using any covering whatsoever. Notice though that implicitly the maximal covering ($Loc/X$ for a fixed topos $X$) is being used (since density means such covering is an epi in the cat of topoi).

2nd best proof: proving that the maximal covering is an effective epi in the cat of topoi without using any smaller atlas (such as JT’s).

3rd best proof: proving that some covering satisfying some universal property is an epimorphism or an effective epimorphism.

Indeed, a proof which does not mention any covering (not even the maximal one about which the theorem is making a statement) would be very cool to have but I have no idea what it could look like.
The second best case scenario is what I took your initial question to be, and could only offer a speculative answer. As for the third best proof, I think the one sketched in my talk roughly fits that description: density follows from the existence of one single-morphism (2,2)-atlas (effective epi. in the (2,2) sense) which is stable under pullbacks (such as the JT atlas).

But regarding your question about atlases for ultraconv. spaces, I recommend Saadia’s paper whose proof goes through coverings of ultraconv. spaces/toposes with enough points. 

I couldn't find anything like an atlas for arbitrary ultraconvergent spaces in this paper. Is it proven somewhere there? I don't even know whether that's true in general.

I was a bit vague. In section 7, for every ultraconv. space coming from a topos, the author constructs a cover which is both an atlas in ultraconv. spaces and in toposes with enough points (based on the Butz-Moerdijk atlas but different from it). And actually, the category of sheaves/étale spaces over an ultraconv. space which admits an atlas will necessarily be a Grothendieck topos.

This is because the sheaves functor from ultraconv. space to CAT sends colimits to limits since it is representable. So if an ultraconv. space is a colimit of topological spaces, then the corresponding category of sheaves will be a limit in CAT of a diagram of Grothendieck toposes and inverse image functors, hence a Grothendieck topos itself.

Lurie (Thm.4.4.7) proves only for ultragroupoids that those can be presented by an atlas of compacta, but the statement for ultracats is missing though. He proves density in Thm.4.3.3.

Yes I was only referring to 4.3.3, the density of compacta in ultracategories, to motivate the density of topological spaces in ultraconvergence spaces/virtual ultracategories. I’m not aware of any analogues of 4.4.7 for ultraconv. spaces. And the main ingredient in the proof of 4.3.3 seems to be that spaces of the form $\beta(S)$ are compacta.

My main point is that the representation of toposes with enough points in terms of ultraconv. spaces is closely linked to the density of topological spaces in toposes with enough points. Indeed, I believe Hamad actually proves the latter and only then deduces the former. That the former implies the latter follows directly if we know that topological spaces are dense in ultraconv. spaces, which should be easier to show than for toposes.

Hmm... I'm not finding that also. The statement is Lemma 7.6, but the proof requires Moerdijk-Butz's atlas (which is not much different from JT's)

I haven’t checked through every detail of Hamad’s proof but my understanding is that section 7.3 is a proof of density of topological spaces in toposes with enough points (thm 7.5) based on the idea that the subatlas of Butz-Moerdijk-like groupoids is final in the maximal atlas, which feels somewhere between your 2nd and 3rd best types of proofs.

Christopher Townsend (Nov 08 2025 at 09:44):

@Fernando Yamauti - hey I'm trying to reply to your comment, but not sure if this is going to put it in the right place in the thread...

I think the coverings are artificial in the sense that they are not canonical - but this is part of the (non-artificial) fact that the groupoids are only defined up to Morita equivalence. We can abstract the issue away: an adjunction of cartesian categories (say, D 'over a base' C) is the connected components adjunction of an internal groupoid in the base C iff there exists some W in D such 'xyz'. So, at some point, you need to say 'there exists some W' (I outlined how D=[N->>B] in the usual case above).

For the localic category of a topos, this is explicit in Moerdijk's early work on extending JT to morphisms. [Def 3.1 of IEKE MOERDIJK: The classifying topos of a continuous groupoid. II. Cahiers de topologie et géométrie différentielle catégoriques, tome 31, no 2 (1990), p. 137-168http://www.numdam.org/item?id=CTGDC_1990__31_2_137_0]. You can also think about it as the locale of morphism of the generic model once lifted to the localic cover. I think what I was trying to say was that it was this construction that I was really interested in.

[For completeness 'xyz' is 'C/LW equivalent D/W via the slice of the adjunction; and W->1 is of effective descent'. (There are a couple of other characterisations that also work at the generality of adjunctions between cartesian (=finite limit) categories.)]

Joshua Wrigley (Nov 12 2025 at 10:55):

@Fernando Yamauti You've already received the answer I would have given to your question (that is a link to Errol Yuksel's talk). Seeing as my paper came up in the context of effective descent morphisms of topoi, I am just going to add a few thoughts here which may or may not be apparent when reading the paper (they were not completely apparent to me when I was writing it).

We know from Joyal-Tierney that open surjections are effective descent in the bicategory of Grothendieck topoi. However, open surjections (alone) are not effective descent in the bicategory of Grothendieck topoi with enough points. The content of the characterisation theorem in the paper can be understood as specifying what else is needed of an open surjection for it to be effective descent for topoi with enough points.

For a counterexample, see Example 57. It describes a point of a connected atomic topos (and hence an open surjection) which is not of topological effective descent. Because this particular counterexample concerns connected atomic topoi, it was possible to deduce it already using the techniques of Caramello's topological Galois theory.