sober spaces

Stream: maths

[Johan Commelin]

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.

[Jeremy Avigad]

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.

[Reid Barton]

I think the Prop version is fine.

[Patrick Massot]

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

[Kevin Buzzard]

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

[Patrick Massot]

Do you mean he actually is continuing that thread?

[Patrick Massot]

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

[Kevin Buzzard]

Maybe he realised that nobody had answered yet :-)

[Patrick Massot]

I spend too much time translating.

[Johan Commelin]

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