Skip to content

Scattered implies sober#1682

Merged
prabau merged 5 commits intomainfrom
artinianquasisober
Mar 18, 2026
Merged

Scattered implies sober#1682
prabau merged 5 commits intomainfrom
artinianquasisober

Conversation

@felixpernegger
Copy link
Collaborator

1 new trait.

If #1465 is ever implemented, this implies the very fun theorem Artinian + Noetherian => Finite.

Using hereditary and kolmogorov metaproperties I think one could make a bunch of theorems with sober, hyperconnected. For example there is also Artinian + Hyperconnected + ~Empty => Has a generic point (not in this PR).
But one would have to think in more detail how to make this systematic.

@prabau
Copy link
Collaborator

prabau commented Mar 18, 2026

T865: scattered implies T0. So it would be better to change the result to [scattered => sober].

@prabau
Copy link
Collaborator

prabau commented Mar 18, 2026

Consider also cleaning up https://topology.pi-base.org/spaces/S000046/properties/P000226, which becomes redundant.

@felixpernegger
Copy link
Collaborator Author

This also makes T169 redundant techinically

Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com>
@prabau
Copy link
Collaborator

prabau commented Mar 18, 2026

We should keep T169 (scattered => T0), which is not just "by definition". It's good to have it standalone.
I expanded the proof of T865 (scattered => sober) and it makes explicit use of T169.

Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com>
@prabau
Copy link
Collaborator

prabau commented Mar 18, 2026

It's good you noticed the cleanup for S44.
S46 can also have a cleanup of P226.

@prabau prabau changed the title Scattered implies quasi sober Scattered implies sober Mar 18, 2026
@prabau prabau merged commit 5397749 into main Mar 18, 2026
1 check passed
@prabau prabau deleted the artinianquasisober branch March 18, 2026 22:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants