Zulip Chat Archive

Stream: maths

Topic: sober spaces


view this post on Zulip Johan Commelin (Feb 05 2020 at 17:58):

https://en.wikipedia.org/wiki/Sober_space
A sober space is a topological space in which every irreducible (i.e. nonempty preirreducible) subset Z has a unique generic point: i.e. there is a unique x in Z such that Z is the closure of {x}.

I'm thinking of introducing sober_space as a class. Should it be a predicate, or should it carry a function that provides the generic point? I think in practice this function will never be computable, so I'm inclided to go for the predicate version.

view this post on Zulip Jeremy Avigad (Feb 06 2020 at 20:10):

The terminology gave rise to one of my favorite paper titles: https://link.springer.com/chapter/10.1007%2FBFb0089911. "Scott" here is Dana Scott, who first told me about it.

view this post on Zulip Reid Barton (May 03 2020 at 20:33):

I think the Prop version is fine.

view this post on Zulip Patrick Massot (May 03 2020 at 21:03):

Reid, did you really intend to post this message in that old thread?

view this post on Zulip Kevin Buzzard (May 03 2020 at 21:08):

Maybe he wants them too and realised we still don't have them :-)

view this post on Zulip Patrick Massot (May 03 2020 at 21:14):

Do you mean he actually is continuing that thread?

view this post on Zulip Patrick Massot (May 03 2020 at 21:14):

I didn't even read Johan's message, I assumed Reid messed up with Zulip.

view this post on Zulip Kevin Buzzard (May 03 2020 at 21:14):

Maybe he realised that nobody had answered yet :-)

view this post on Zulip Patrick Massot (May 03 2020 at 21:15):

I spend too much time translating.

view this post on Zulip Johan Commelin (May 04 2020 at 04:36):

I should return to sober spaces at some point. Thanks for reminding me!


Last updated: May 12 2021 at 07:17 UTC