pi-base
Add the property Ordinal space and remove some redundant files
As mentioned in #640 . I have checked that all manually-deduced implications are still there (perhaps now being autometic).
T497 is redundant. We already know ordinal spaces are LOTS and scattered by the other theorems. Hence totally disconnected. And totally disconnected LOTS are zero-dimensional.
More comments later.
T497 is redundant. We already know ordinal spaces are LOTS and scattered by the other theorems. Hence totally disconnected. And totally disconnected LOTS are zero-dimensional.
More comments later.
Ah yes, thanks for the reminder!
(T490) [ordinal ==> locally relatively compact]:
Among the various variants of locally compact properties, a strong combination is [weakly locally compact + regular] (= condition (4) in https://en.wikipedia.org/wiki/Locally_compact_space). It is equivalent to every point having a local base of closed compact nbhds, and it implies both locally compact (by T224) and locally relatively compact (by T246).
Since we already know that ordinal space (or any LOTS) is regular, it seems to me it would be preferable (and more symmetrical) to change T490 to [ordinal ==> weakly locally compact]. Compare with the list of theorems we already have at https://topology.pi-base.org/properties/P000023/theorems.
(T495) [ordinal + perfectly normal ==> countable]:
The argument seems fine, but maybe a little too much for the justification without a reference. (The "General Reference Chart" does not really count, and should probably be removed?) I could not find a good reference for this in Engelking and other standard books though. And only mention of it, but no details on mathse. So we can probably keep your argument. But at least I think we should add an explicit mention of https://dantopology.wordpress.com/2009/10/11/the-first-uncountable-ordinal/ in the text (not in the refs: section).
@StevenClontz any specific opinion about this one?
(T490) [ordinal ==> locally relatively compact]:
Among the various variants of locally compact properties, a strong combination is [weakly locally compact + regular] (= condition (4) in https://en.wikipedia.org/wiki/Locally_compact_space). It is equivalent to every point having a local base of closed compact nbhds, and it implies both locally compact (by T224) and locally relatively compact (by T246).
Since we already know that ordinal space (or any LOTS) is regular, it seems to me it would be preferable (and more symmetrical) to change T490 to [ordinal ==> weakly locally compact]. Compare with the list of theorems we already have at https://topology.pi-base.org/properties/P000023/theorems.
Actually I do not understand the situation of weak local compactness and local relative compactness. Weakly Locally Compact: Every point has a compact neighborhood. Locally Relatively Compact: Every point has a closed and compact neighborhood. So by definition Weakly Locally Compact + KC => Locally Relatively Compact (should be added as a theorem), no? And it would be meaningful then to ask if Weakly Locally Compact + US => Locally Relatively Compact.
As for T490 itself, it follows directly that each $[0,\beta]$ is closed, so (unless you strongly oppose it) I would like to keep T490 as it is now.
(T495) [ordinal + perfectly normal ==> countable]:
The argument seems fine, but maybe a little too much for the justification without a reference. (The "General Reference Chart" does not really count, and should probably be removed?) I could not find a good reference for this in Engelking and other standard books though. And only mention of it, but no details on mathse. So we can probably keep your argument. But at least I think we should add an explicit mention of https://dantopology.wordpress.com/2009/10/11/the-first-uncountable-ordinal/ in the text (not in the
refs:section).@StevenClontz any specific opinion about this one?
I edited T495 :)
T490: Let me try to explain what my reasoning was.
Ordinal spaces are
- weakly locally compact (WLC) (P23)
- locally compact (P130)
- locally relatively compact (P24)
WLC is the weakest of the properties, implied by the other two. On the other hand, WLC in combination with T2 (which obviously holds for ordinal spaces) is the strongest of combinations, as it implies the other two (compare condition (5) in https://en.wikipedia.org/wiki/Locally_compact_space).
Now in general, there are spaces that are P130 and not P24, and others that are P24 and not P130. (Or course, that will not happen for Hausdorff spaces.) So in general, one cannot assume P24 (locally relatively compact) and deduce P130, or vice versa. But for ordinal spaces, it all works out because the space is Hausdoff. And in that case, it seems more basic and certainly more symmetrical to show WLC and deduce the other two from that, instead of priviledging one of P130/P24 over the other one.
And if you look at the page of theorems for WLC (https://topology.pi-base.org/properties/P000023), many of them assume WLC + T2, or WLC + regular (which is a consequence of WLC + T2), from which one can deduce the other two properties. But the page of theorems for the other two properties are more directed to results specific to these properties and not involving the other property.
Aside: good observation about [WLC + KC ==> locally relatively compact]. As far as I can see, it would not simplify any of the deductions or remove redundant trait files for the spaces currently in pi-base, but it could be added in a separate PR.
(T496) [ordinal + ccc ==> countable]:
This seems redundant by T495 combined with [LOTS + ccc ==> perfectly normal] (see https://topology.pi-base.org/spaces?q=lots%2Bccc%2B%7EPerfectly+normal).
T490: Let me try to explain what my reasoning was.
Ordinal spaces are
- weakly locally compact (WLC) (P23)
- locally compact (P130)
- locally relatively compact (P24)
WLC is the weakest of the properties, implied by the other two. On the other hand, WLC in combination with T2 (which obviously holds for ordinal spaces) is the strongest of combinations, as it implies the other two (compare condition (5) in https://en.wikipedia.org/wiki/Locally_compact_space).
Now in general, there are spaces that are P130 and not P24, and others that are P24 and not P130. (Or course, that will not happen for Hausdorff spaces.) So in general, one cannot assume P24 (locally relatively compact) and deduce P130, or vice versa. But for ordinal spaces, it all works out because the space is Hausdoff. And in that case, it seems more basic and certainly more symmetrical to show WLC and deduce the other two from that, instead of priviledging one of P130/P24 over the other one.
And if you look at the page of theorems for WLC (https://topology.pi-base.org/properties/P000023), many of them assume WLC + T2, or WLC + regular (which is a consequence of WLC + T2), from which one can deduce the other two properties. But the page of theorems for the other two properties are more directed to results specific to these properties and not involving the other property.
Aside: good observation about [WLC + KC ==> locally relatively compact]. As far as I can see, it would not simplify any of the deductions or remove redundant trait files for the spaces currently in pi-base, but it could be added in a separate PR.
I see your point. Thanks for the explanation.
Nice cleanup of the redundant traits.
Just one file S35|P31 should not have been removed.
Nice cleanup of the redundant traits.
Just one file S35|P31 should not have been removed.
Ah sorry! I have it restored.