Is Noetherian = Hereditarily compact missing?

[GeoffreySangston]

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

[StevenClontz]

Looks like a fine addition to me!

[prabau]

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

[GeoffreySangston]

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 #847 (comment) because Hartshorne's Exercise also discusses the specialization preorder.)

[prabau]

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]

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 #847 (comment) ("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]

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.