search

pi-base / data

A community database of topological counterexamples
https://topology.pi-base.org/
Creative Commons Attribution 4.0 International
72 stars 26 forks source link

Is Noetherian = Hereditarily compact missing? #849

Open GeoffreySangston opened 4 weeks ago

GeoffreySangston commented 4 weeks ago

The pi-Base has Hereditarily Lindelöf, but I don't see Noetherian = Hereditarily compact. Should I go ahead and add it?

StevenClontz commented 4 weeks ago

Looks like a fine addition to me!

prabau commented 4 weeks ago

The Stacks project has a good section about it: https://stacks.math.columbia.edu/tag/0050.

GeoffreySangston commented 3 weeks ago

I just saw that Hartshorne Exercise 3.17 defines the concept of a Zariski space, as a topological space which is Noetherian and such that every non-empty closed subset which is Irreducible (P000039) under the subspace topology has a unique generic point. Since I'm currently thinking about generic points in the PR #847, I thought it could be good to store this property here, possibly to add with a PR which adds Noetherian.

(There's some crossover between this comment and https://github.com/pi-base/data/pull/847#issuecomment-2453487482 because Hartshorne's Exercise also discusses the specialization preorder.)

prabau commented 3 weeks ago

Can we please add new properties separately instead of sticking them together with possibly unrelated things? Especially when there may be discussion about it. Having smaller PRs makes them easier to review and easier to get them merged. Multiple smaller PRs makes things move along better.

About your description of Zariski space, isn't it the same as [Noetherian + sober]?

GeoffreySangston commented 3 weeks ago

Can we please add new properties separately instead of sticking them together with possibly unrelated things? Especially when there may be discussion about it. Having smaller PRs makes them easier to review and easier to get them merged. Multiple smaller PRs makes things move along better.

I'll keep this in mind. For adding the properties from https://github.com/pi-base/data/pull/847#issuecomment-2452832521 ("Has a generic point" most immediately"), should I make a new pull request, or add them in that pull request? I think perhaps it's better to close that one and make new PR's for each property individually (especially since the first two commits of that one amount to nothing).

About your description of Zariski space, isn't it the same as [Noetherian + sober]?

Ah yes. I have now learned what sober means.

prabau commented 3 weeks ago

Yeah, maybe start from fresh. Close #847. Open a separate one with just "Has a generic point" and any associated theorems. And maybe traits asserting that a few space satisfy it, in particular the particular point topologies. (but don't mention the excluded point topologies here). So that can be reviewed and merged quickly.

The rest (to show the excluded point topologies are also contractible) can be done later.

As for "Zariski space", it's a synonym for [Noetherian + sober]. It's not even clear it's worth introducing. If the concept is used widely in the literature, then it would be a good idea to have it in pi-base for reference, as a convenience term. (For example we added "Polish" as a synonym for [separable + completely metrizable], as it is widely used.) But if it's only used in one of two sources, or with conflicting definitions, it's not clear there is a benefit to do so. One would have to research more into it first, but does not seem urgent at the moment.