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: deprecated: topos theory

Topic: "topos" of condensed sets

David Michael Roberts (Dec 27 2021 at 22:56):

As much as I respect Peter S, I wish he'd stop calling the category of condensed sets a topos. It's not a set-theoretic subtlety, like using universes as a convenience, but it just isn't.

Zhen Lin Low (Dec 27 2021 at 23:06):

That sounds like a lost cause, though. He surely understands the difference and must think that it is not worth making a fuss over.

Reid Barton (Dec 28 2021 at 01:15):

Surely it's no worse than calling an elementary topos a topos.

John Baez (Dec 28 2021 at 01:37):

I don't know anything about the category of condensed sets - these days I avoid following modern trends in subjects I know I don't want to contribute to. But now I'm curious: why is it sort of like a topos, and why is it not a topos?

David Michael Roberts (Dec 28 2021 at 03:54):

@John Baez It's a cocomplete locally small pretopos that is the category of small sheaves on a large site. It has a filtration of subcategories indexed by the regular cardinals, each of which is a Grothendieck topos.

David Michael Roberts (Dec 28 2021 at 03:57):

I guess the best argument for Scholze's usage is that it satisfies the Giraud axioms, except the generating set, and the class that does this is somewhat controlled (so: not all the objects)

David Michael Roberts (Dec 28 2021 at 03:58):

@Zhen Lin Low until people are trying to make a formal proof in Lean, and are not sure whether they are formalising something about condensed sets or pyknotic sets relative to a universe.

Zhen Lin Low (Dec 28 2021 at 04:15):

David Michael Roberts said:

I guess the best argument for Scholze's usage is that it satisfies the Giraud axioms, except the generating set, and the class that does this is somewhat controlled (so: not all the objects)

Yes, exactly. I think for many purposes the exactness properties are enough, but there isn't a snappy name for such categories. "Cocomplete locally small pretopos" is rather a mouthful.

John Baez (Dec 28 2021 at 04:28):

Thanks, David!

John Baez (Dec 28 2021 at 04:30):

I've been forced to think a bit about the category of small presheaves on a large site, so this is interesting.

David Michael Roberts (Dec 28 2021 at 07:24):

In case it's interesting, categories of small sheaves appear in set theory when people do class forcing, which generalises ordinary forcing as sheaves on certain small sites. I must write this up, one day.

Fawzi Hreiki (Dec 28 2021 at 08:16):

So such a category does not have exponentials or a subobject classifier?

Zhen Lin Low (Dec 28 2021 at 08:32):

It is, at least, non-obvious whether it has exponentials or a subobject classifier. In a sense, the reason why a Grothendieck topos has those things (and many other kinds of classifying objects besides) is because the small generating set lets you construct representations/adjoints.

David Michael Roberts (Dec 28 2021 at 12:22):

It's much easier for such a category to have a subobject classifier than exponentials, in my experience

Todd Trimble (Dec 28 2021 at 13:55):

The category of small sheaves on a large category doesn't even have to have a terminal object. Take $X$ to be large and discrete, for instance. The support of a small colimit of representables is always a small set.

Mike Shulman (Dec 28 2021 at 18:46):

However, there are reasonable conditions on a large site that ensure its category of small sheaves has finite limits. In the case of a trivial topology this is in Day-Street Limits of small functors, while for nontrivial topologies it's in my Exact completions and small sheaves. It seems not outside the realm of possibility that there are similar conditions for exponentials and subobject classifiers.

Mike Shulman (Dec 28 2021 at 18:47):

re: terminology, it's too bad that "pretopos" and "quasitopos" are already taken...

Jens Hemelaer (Dec 28 2021 at 19:32):

David Michael Roberts said:

I guess the best argument for Scholze's usage is that it satisfies the Giraud axioms, except the generating set, and the class that does this is somewhat controlled (so: not all the objects)

Another reason could be that intuitively you are working with $\kappa$-condensed sets (which is a topos), but with $\kappa$ a "variable". It seems that within a proof often $\kappa$ is fixed, so then all properties of a Grothendieck topos are available.

David Michael Roberts (Dec 28 2021 at 21:47):

I think that's why Barwick and Haine invented "macrotopos", which, if not exactly right, is close. But then you have a neologism to deal with.

Mike Shulman (Dec 28 2021 at 21:49):

Jens Hemelaer said:

Another reason could be that intuitively you are working with $\kappa$-condensed sets (which is a topos), but with $\kappa$ a "variable". It seems that within a proof often $\kappa$ is fixed, so then all properties of a Grothendieck topos are available.

But presumably the inclusion from $\kappa$-condensed sets to $\lambda$-presented sets, for $\kappa<\lambda$, is not a logical functor. So while you can use this structure inside an "irrelevant" proof , you can't use it in a definition or a construction.

Mike Shulman (Dec 28 2021 at 21:50):

By the way, this conversation hasn't been off-topic for some time, has it? Maybe it should be moved to a different stream.

David Michael Roberts (Dec 29 2021 at 00:15):

David Michael Roberts said:

I think that's why Barwick and Haine invented "macrotopos", which, if not exactly right, is close. But then you have a neologism to deal with.

If I were the one promoting condensed sets, I'd say something like "they form a category so close to being a topos that in practice you can ignore the distinction".

Jens Hemelaer (Dec 29 2021 at 08:23):

David Michael Roberts said:

I think that's why Barwick and Haine invented "macrotopos", which, if not exactly right, is close. But then you have a neologism to deal with.

Thanks for the reference!

David Michael Roberts (Dec 29 2021 at 09:36):

Actually, if I were to invent a name, I'd call it a "near-topos". It's closer to being a Grothendieck topos than a general pretopos, and "macrotopos" sounds to me like a special kind of topos

David Michael Roberts (Dec 29 2021 at 09:47):

The only name clash I can think of is with a near-ring, but that is sufficiently far from commutative algebra that algebraic geometers won't get confused.

Notification Bot (Dec 29 2021 at 12:09):

This topic was moved here from #general: off-topic > "Topos" of condensed sets by Morgan Rogers (he/him)

Todd Trimble (Dec 29 2021 at 12:19):

The Greek counterpart of quasi- is pseudo-; how does pseudotopos sound?

Mateo Carmona (Dec 29 2021 at 14:49):

Todd Trimble said:

The Greek counterpart of quasi- is pseudo-; how does pseudotopos sound?

Pseudotopos is already used, see Pursuing stacks (section 104 A)).

Todd Trimble (Dec 29 2021 at 15:01):

Wow, thanks very much for that link! I've never read it.

Mike Shulman (Dec 29 2021 at 18:04):

Also "pseudotopos" sounds to me like a pseudoalgebra for a 2-monad whose strict algebras are toposes.

Amar Hadzihasanovic (Dec 29 2021 at 19:22):

An imposter topos... a “toposter”.

John Baez (Dec 29 2021 at 20:14):

I would suggest "tapas".

Matteo Capucci (he/him) (Dec 30 2021 at 11:36):

typos

Zhen Lin Low (Dec 30 2021 at 12:26):

I believe a typos is a model of unintentional type theory.

Jon Sterling (Dec 30 2021 at 15:45):

Let's call it Toupée. It has a nice French ring to it.

Ivan Di Liberti (Dec 30 2021 at 16:01):

A cocomplete infinitary pretopos is really just a 2-locale.

Fawzi Hreiki (Dec 30 2021 at 17:52):

I think most people would say that a 2-locale is a sheaf topos

Ivan Di Liberti (Dec 30 2021 at 17:54):

Fawzi Hreiki said:

I think most people would say that a 2-locale is a sheaf topos

You are right, but we need some kind of new standard, right? I think this could be a solution. I understand that it implicitly assumes that a 1-locale should really be a poclass (as opposed to poset), but I think it is a "fair proposal".

We could agree that an n-locale is a cocomplete infinitary n-pretopos, and an n-topos is an n(+1) locale with a generator. This is a very Giraud-like point of view.

Jon Sterling (Dec 30 2021 at 18:38):

I don't mind "n-topos is an (n+1)-XXX with a generator", but I don't think I like using locale for XXX here. haha

Jon Sterling (Dec 30 2021 at 18:44):

But maybe I could be won over. lol

Mike Shulman (Dec 30 2021 at 19:07):

"Giraud category"? [[infinitary pretopos]]?

Fawzi Hreiki (Dec 30 2021 at 19:11):

Well, a locale is a lex reflective subposet or a power set. Likewise, a 2-locale is a lex reflective subcategory of a presheaf category.

Mike Shulman (Dec 30 2021 at 19:16):

I don't think a locally small category satisfying the Giraud axioms, but without a generating set, is necessarily a lex reflective subcategory of a presheaf category.

Ivan Di Liberti (Dec 30 2021 at 19:16):

Mike Shulman said:

I don't think a locally small category satisfying the Giraud axioms, but without a generating set, is necessarily a lex reflective subcategory of a presheaf category.

But a cocomplete locally small infinitary pretopos is lex reflective in its small presheaves. This is its canonical (re)presentation.

Mike Shulman (Dec 30 2021 at 19:17):

I think it would be a very bad idea to define a notion of "n-locale" such that a "1-locale" would not be the same as the accepted notion of locale.

Ivan Di Liberti (Dec 30 2021 at 19:18):

Mike Shulman said:

I think it would be a very bad idea to define a notion of "n-locale" such that a "1-locale" would not be the same as the accepted notion of locale.

I agree, but I think if you want a unified notation, which is also effective and does not introduce strange terminology, some notational clash will be needed.

Mike Shulman (Dec 30 2021 at 19:20):

Ivan Di Liberti said:

But a cocomplete locally small infinitary pretopos is lex reflective in its small presheaves. This is its canonical (re)presentation.

Well, that's a different thing than being lex reflective in a presheaf category. And "being lex reflective in a category of small presheaves" is not a sufficient characterization, because as Todd pointed out, in general a category of small presheaves need not even have finite limits.

Mike Shulman (Dec 30 2021 at 19:21):

Ivan Di Liberti said:

I agree, but I think if you want a unified notation, which is also effective and does not introduce strange terminology, some notational clash will be needed.

Well, I suppose that's tautologically true for a sufficently wide definition of "strange"...

Ivan Di Liberti (Dec 30 2021 at 19:21):

Mike Shulman said:

Ivan Di Liberti said:

But a cocomplete locally small infinitary pretopos is lex reflective in its small presheaves. This is its canonical (re)presentation.

Well, that's a different thing than being lex reflective in a presheaf category. And "being lex reflective in a category of small presheaves" is not a sufficient characterization, because as Todd pointed out, in general a category of small presheaves need not even have finite limits.

The category of small presheaves is very likely to have finite limits, Rosicky and Adamek discuss this in their paper on the topic. That said, one can replace lex with flat, it does not make a conceptual difference. Also, if we think of descent, as a form of lexity of colimits, this is clearly the correct point of view on Giraud Axioms.

Mike Shulman (Dec 30 2021 at 19:40):

Replacing lex with flat doesn't help, since the identity functor is always flat, so a category of small presheaves is always a flat-reflective subcategory of itself, yet it may not have finite limits.

Mike Shulman (Dec 30 2021 at 19:41):

I believe it is true that a locally small category is an infinitary-pretopos if and only if it has finite limits and is a left-exact reflective subcategory of its small-presheaf category (which, as mentioned, has finite limits whenever the original category does). For instance, I think this is part of the general Garner-Lack theory of "lex colimits".

Mike Shulman (Dec 30 2021 at 19:43):

However, this doesn't solve the problem of size, since in the case of posets we can equally well talk about powerclasses of poclasses.

Ivan Di Liberti (Dec 30 2021 at 20:10):

Mike Shulman said:

I believe it is true that a locally small category is an infinitary-pretopos if and only if it has finite limits and is a left-exact reflective subcategory of its small-presheaf category (which, as mentioned, has finite limits whenever the original category does). For instance, I think this is part of the general Garner-Lack theory of "lex colimits".

Oh, there was a misunderstanding. Finite limits are included in my definition of infinitary pretopos.

Ivan Di Liberti (Dec 30 2021 at 20:11):

Mike Shulman said:

However, this doesn't solve the problem of size, since in the case of posets we can equally well talk about powerclasses of poclasses.

I think I am lost with "what's the problem" here. I really do not belong to this forum-like debates, sorry.

Mike Shulman (Dec 30 2021 at 21:10):

Ivan Di Liberti said:

Oh, there was a misunderstanding. Finite limits are included in my definition of infinitary pretopos.

Yes, mine too. The point is that "being a lex/flat reflective subcategory of a small-presheaf category" does not include finite limits, so it's not equivalent to being an infinitary pretopos.

Fawzi Hreiki (Dec 30 2021 at 21:22):

@Mike Shulman Yeah that was my point. A 2-locale should be a sheaf topos since they’re the lex reflective subcategories of presheaf categories.

Mike Shulman (Dec 30 2021 at 22:19):

Oh, sorry, I misunderstood what side you were taking.

Zhen Lin Low (Dec 30 2021 at 22:44):

I am puzzled by the statement that a cocomplete locally small infinitary pretopos is lex-reflective in a category of small presheaves. I think I can agree that this is so if we take presheaves on the pretopos itself, but that sounds tautological. Or is it known that small sheaves are automatically small presheaves?

Mike Shulman (Dec 31 2021 at 01:00):

Why is it tautological? There's a theorem to prove about how the Giraud axioms imply left-exactness of the reflector.

Zhen Lin Low (Dec 31 2021 at 01:38):

There's something unsatisfactory about using the pretopos itself as the site. Here's how I think about it. Given a site (C, J), we have the category of small presheaves on C and the category of small J-sheaves on C; assuming J is subcanonical, we get a colimit-preserving functor from presheaves to sheaves. Is it always a localisation? Does it always have a right adjoint? I know there are combinatorial hypotheses that ensure the functor is lex.

Mike Shulman (Dec 31 2021 at 02:31):

I don't think it always has a right adjoint, but I think it should always be a coinverter; this is more or less the conclusion of section 8 of Exact completions and small sheaves. I don't see what's unsatisfactory about it; if the category doesn't have a small generating set, then there's no reason there would be any other possibility, and in any case the pretopos itself is certainly a more canonical choice of site than anything smaller.

Zhen Lin Low (Dec 31 2021 at 04:48):

Choosing the pretopos itself as the site makes the existence of the right adjoint almost tautological, however. It would be much more interesting if there were a combinatorial condition on (C, J) ensuring that small J-sheaves on C are also small presheaves on C.

Mike Shulman (Dec 31 2021 at 05:31):

Ah, yes, I agree about the right adjoint being easier in that case. But I would regard that as a good thing, since in the situation we're trying to generalize (toposes) the right adjoint also exists for trivial reasons. Sure, it would also be interesting to have a combinatorial condition as you suggest, but that would be icing on the cake. (-:

🇺🇦 unmuamua 🇺🇦 (Mar 05 2022 at 19:39):

Zhen Lin Low said:

I believe a typos is a model of unintentional type theory.

many thanks for the reference (sorry for offtopic). it made me laughing first time after last ten days of shellings and other circumstances.