Theorem Suggestion: A characterization of Finite T0 spaces

[plp127]

Theorem Suggestion

If a space is:

• sober P73
• alexandrov P90
• noetherian P208

then it is finite P78.

Rationale

This theorem would give a characterization of topological spaces with finite Kolmogorov quotient as the Alexandrov Quasi-sober Noetherian spaces.

Proof

Let X be alexandrov sober and noetherian. Equip X with the specialization preorder (x le y iff x in closure {y}).

Since X is T0 (Sober ⇒ T0), X is a partial order.
Since X is Noetherian, its closed sets are well founded. Since it is Alexandrov, every lower set is closed. Therefore, the lower sets are well founded, so X is a well-quasi-order, meaning it has no infinite strictly decreasing sequences and no infinite antichains.
Since X is sober, it has no infinite strictly increasing sequences. For suppose it did have such a sequence a_i, then S := { x in X | exists i, x < a_i } would be a nonempty closed irreducible subset without generic point.

Then, since X is a partial order and has no infinite strictly increasing sequences and no infinite strictly decreasing sequences, X has no infinite chains (see for example answer on math stachexchange).
Since X has no infinite chains and no infinite antichains, it is finite (see for example answer on math stackexchange).

[felixpernegger]

Very cool, should I make stackexchange question, so you can post it there?