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: learning: questions

Topic: points of a topos

Leopold Schlicht (Aug 28 2021 at 18:19):

For which toposes is the category of its points small?

Mike Shulman (Aug 29 2021 at 01:19):

The category of points of a localic topos is always (essentially) small. Beyond that I don't know a general answer; e.g. I wouldn't expect there to be any clean criterion for which geometric theories have only a small number of isomorphism classes of models in Set.

Leopold Schlicht (Aug 29 2021 at 11:01):

Thank you very much!

Leopold Schlicht (Aug 29 2021 at 11:28):

My motivation for the question was that I wanted to find a left inverse of the inclusion of sober spaces into toposes. My idea was to send a topos $\mathcal E$ to the space given by the points of $\mathcal E$ and the open subtoposes of $\mathcal E$. But since the points of $\mathcal E$ need not form a set, this isn't well-defined.
So is it the cases that the inclusion of sober spaces into toposes does not have a left inverse?
But how, then, would one categorically express that a sober space can be reconstructed from its topos of sheaves by considering its points? (Of course one can say that the inclusion is fully faithful, but having something like a left inverse would be slightly better.)
Also, does the inclusion of sober spaces into locales have a left inverse?
(By "inverse", I always mean "inverse up to natural isomorphism".)

Zhen Lin Low (Aug 29 2021 at 11:33):

_If_ you have a topos that comes from a sober space then you can perform the reconstruction you suggest.

Leopold Schlicht (Aug 29 2021 at 11:34):

Also, I don't know if the assignment $\mathcal E\mapsto (\text{points of }\mathcal E\text{, subtoposes of }\mathcal E)$ is functorial, i.e., induces a continuous map for each topos morphism. Is it?

Zhen Lin Low (Aug 29 2021 at 12:26):

Yes, it is functorial, because you can pull back open subtoposes.

Mike Shulman (Aug 29 2021 at 14:42):

Any topos has a "localic reflection", obtained from the hyperconnected-localic factorization system. Thus, the inclusion of locales in toposes has a left inverse which is in fact a left adjoint. Similarly, the inclusion of sober spaces in locales has a left inverse that is a right adjoint, which takes the space of points. So combined, the inclusion of sober spaces in toposes also has a left inverse, though it is no longer an adjoint on either side.

Leopold Schlicht (Aug 31 2021 at 21:37):

Thanks!
@Mike Shulman Cool! How does this particular left inverse of the inclusion of sober spaces in toposes differ from $\mathcal E\mapsto (\text{points of }\mathcal E\text{, subtoposes of }\mathcal E)$?

Mike Shulman (Aug 31 2021 at 22:11):

I don't know offhand, sorry.

Zhen Lin Low (Aug 31 2021 at 22:53):

Well, for one thing, taking the localic reflection first ensures that you get a small set of points.

Jens Hemelaer (Sep 01 2021 at 08:54):

Hi @Leopold Schlicht, something close to
$\mathcal E\mapsto (\text{points of }\mathcal E\text{, open subtoposes of }\mathcal E)$
is described in this paper by Caramello, Section 2.1.

If you take a set of points $X$ of the topos $\mathcal{E}$, then the topology on $X$ given by the open subtoposes is called the subterminal topology. If $X$ is a separating set of points, then $\mathbf{Sh}(X)$ is the localic reflection of $\mathcal{E}$.

For a monoid $M$, points of $\mathbf{PSh}(M)$ are the same thing as flat left $M$-sets. The topos $\mathbf{PSh}(M)$ does not have any open subtoposes (other than the empty topos and the topos itself), so the subterminal topology will be the indiscrete topology. If you then turn this into a sober space, you get just one point.

Leopold Schlicht (Sep 01 2021 at 14:22):

Thanks!

Leopold Schlicht (Sep 11 2021 at 16:35):

Mike Shulman said:

I wouldn't expect there to be any clean criterion for which geometric theories have only a small number of isomorphism classes of models in Set.

At least for first-order theories $T$ over a finite signature the following conditions are equivalent:

1. $T$ has a small number of models up to isomorphism.
2. $T$ has finitely many models up to isomorphism.
3. $T$ has no infinite model.

(3) implies (2) follows from the compactness theorem and (1) implies (3) follows from Löwenheim–Skolem.

I wonder what's true in geometric logic.

Morgan Rogers (he/him) (Sep 11 2021 at 16:39):

There can surely be infinitely many finite models?

Leopold Schlicht (Sep 11 2021 at 16:41):

Example? Note that I require the signature to be finite.

Morgan Rogers (he/him) (Sep 11 2021 at 16:45):

Ah okay, I'd missed that. In that case I agree, assuming also that the relations and operations in the signature have finite arity (much as this consequence of the compactness theorem is still counterintuitive to me!)

Morgan Rogers (he/him) (Sep 11 2021 at 16:47):

But restricting to finite signatures is rather unrepresentative for studying theories classified by toposes. After all, any infinite space has infinitely many points, and hence so does the topos of sheaves on that space, but not a large collection of points!

Mike Shulman (Sep 11 2021 at 17:16):

I believe there's a geometric theory of finite sets. It has one axiom
$\vdash \bigvee_{n\in\mathbb{N}} \exists x_1 \cdots \exists x_n \bigwedge_{i\neq j} x_i \neq x_j \wedge \forall x (x=x_1 \vee \cdots \vee x=x_n).$
The signature is finite (one sort, no relations or operations), but it should have infinitely many finite models and no infinite models.

Jacques Carette (Sep 12 2021 at 13:17):

What's the meta-theory in which you write down that axiom? $\cdots$ is surprisingly hard to axiomatize properly. [It's generated some nice papers for people who have tried.]

Mike Shulman (Sep 12 2021 at 14:50):

Any theory with a natural numbers object?

Mike Shulman (Sep 12 2021 at 14:50):

What's the problem with it?

Nathanael Arkor (Sep 12 2021 at 14:57):

I think @Jacques Carette's point is that … is typically used as ad hoc notation for some form of iteration, but with unclear formal semantics.

Mike Shulman (Sep 12 2021 at 14:58):

Do you seriously think there is any ambiguity in what I wrote?

Mike Shulman (Sep 12 2021 at 14:58):

Of course if I were going to formalize it in a proof assistant I would have to define something formal by recursion, but in mathematics we write things like that all the time and no one objects.

Nathanael Arkor (Sep 12 2021 at 14:59):

I don't think there is any ambiguity; in geometric logic, you are able to express infinitary axioms, and it is clear what the axiom you wrote expands to.

Jacques Carette (Sep 12 2021 at 14:59):

@Nathanael Arkor Exactly. @Mike Shulman Mathematically? Most definitely not.

Nathanael Arkor (Sep 12 2021 at 14:59):

It's a different question about expressing these kinds of axioms in a finitary language.

Mike Shulman (Sep 12 2021 at 14:59):

But geometric logic is not a finitary language. That's the point.

Mike Shulman (Sep 12 2021 at 15:01):

The question, as I understood it, was whether a theory in geometric logic over a finite signature can have infinitely many models that are all finite. I think this theory shows that the answer to that question is yes. Are you wondering about a different question? Or objecting to that somehow?

Jacques Carette (Sep 12 2021 at 15:02):

My main point was to remark that to 'say' your one axiom formally assumes quite a lot of power in your ambient theory, even though it's mathematically obvious what it meant. A further point is that, if one scours the literature for occurrences of such 'mathematically obvious' notation, it turns out that the actual interpretation can often be significantly more subtle than it appears.

Jacques Carette (Sep 12 2021 at 15:03):

I possibly erred in attaching my comment to this particular thread, as the context (geometric logic) does indeed have enough power to say this, and thus I was being confusing.

Mike Shulman (Sep 12 2021 at 15:04):

Ok. I agree that infinitary language are quite powerful and subtle in general!

Jacques Carette (Sep 12 2021 at 15:06):

For example, when people use $\cdots$ notation, it's not always clear if the $n=0$ case is allowed or not. In practice, both occur.

Mike Shulman (Sep 12 2021 at 15:06):

Well, that's just sloppy. (-:

Jacques Carette (Sep 12 2021 at 15:08):

Much more interesting is that there are cases where in $\cdots$ notation, when there are multiple uses of $\cdots$ in the same formula, there are cases where one can actually take $n$ to be negative and the result ends up being meaningful! This is the case for a number of block-matrix identities, for examples, but also other generalizations to situations with sums and its continuous counterpart, integrals.

Mike Shulman (Sep 12 2021 at 15:10):

This is getting quite far off from the subject of this thread.

Jacques Carette (Sep 12 2021 at 15:10):

Agreed.

Leopold Schlicht (Sep 13 2021 at 13:10):

Morgan Rogers (he/him) said:

But restricting to finite signatures is rather unrepresentative for studying theories classified by toposes.

Which toposes are classified by a geometric theory over a finite signature?

Leopold Schlicht (Sep 13 2021 at 13:20):

Mike Shulman said:

I believe there's a geometric theory of finite sets. It has one axiom
$\vdash \bigvee_{n\in\mathbb{N}} \exists x_1 \cdots \exists x_n \bigwedge_{i\neq j} x_i \neq x_j \wedge \forall x (x=x_1 \vee \cdots \vee x=x_n).$
The signature is finite (one sort, no relations or operations), but it should have infinitely many finite models and no infinite models.

Alright. Probably Löwenheim–Skolem fails too for geometric logic.

Leopold Schlicht (Sep 13 2021 at 13:23):

@Jacques Carette Thanks for the comments. Interesting!