Three results about σ-spaces and ℵ-spaces

[Moniker1998]

The first theorem basically says that Moore space is a σ-spaces
The two other theorems are a corollary of O'Meara metrization theorem. (I read the proof and verified it, but you can double check)

This provides the much needed relationships between the two properties and all other properties (right now they are very poor).

[prabau]

Thanks to T788, the asserted trait P117 ($\sigma$-locally finite network) is now redundant for the spaces S57 and S74. This can be cleaned up.

[Moniker1998]

General cleanup can be done in another PR

[prabau]

It's making use of Kolmogorov quotient meta-properties for several properties that don't already have them. So that should be added.

[Moniker1998]

@prabau ready

[prabau]

I'll be ready on this very soon.

[Moniker1998]

@prabau 👍 I'm waiting for your response on this

[Moniker1998]

@prabau reminder that I'm waiting on this

[prabau]

I finished reading the paper a few days ago. I was thinking about the best way to express what I want to say.

Three theorems:

• (old T516) $\aleph_0$-space + first countable => metrizable
• (A) $\aleph$-space + first countable => metrizable
• (B) regular + first countable + $\sigma$-locally finite $k$-network => pseudometrizable

(A) is what is proved in the paper of O'Meara. I have read it in detail and did not see any problem with it.
(B) is what is proposed in this PR. It is equivalent to (A): (B) implies (A) directly, and the opposite implication follows by passing to the Kolmogorov quotient and back.

Note that the old T516 (with $\aleph_0$-spaces) could also have been given a slightly more general more formulation making use of the Kolmogorov quotient. That would be:

(variant for old T5156) regular + first countable + countable $k$-network => pseudometrizable.

The reason this was not done was a conscious decision on my part to not obscure that basic result from Michael's paper.

In a similar way, I really think it would be preferable to go with (A) instead of (B). People who work with $\aleph$ and $\aleph_0$ spaces make the assumption of T3 and don't try to see what would happen without T0. And for them, the theorem as stated as (A) is an important result that is quoted in many places (Encycl. of Gen. Top,, Handbook of set-theoretic topology, and many papers). If we replace it with (B), the (A) result gets hidden for users of pi-base, which is kind of a shame. (The same thing has happened with other well-known named theorems which were transformed before being integrated into pi-base, like Urysohn metrization theorem or Nagata-Smirnov metrization theorem, etc., and are now kind of hidden as a result.)

An additional argument in favor of (A) is that currently that are no spaces in pi-base where (B) would be needed to derive some traits when (A) did not do the job. And if one (unlikely) would appear in the future, we could always manually justify by saying "pass to the Kolmogorov quotient and use (A)".

But more importantly, the good news is that some work is being done to enhance the deduction system of pi-base so that meta-properties related to Kolmogorov quotient will be automatically integrated together with existing theorems to derive traits for non-T0 spaces. @danflapjax will be starting on #1198 and it would be awesome if he could get something going here.

[Moniker1998]

@prabau I'm not in favour of adding a weaker theorem until that system gets introduced

[prabau]

And I am not in favor of obscuring things when there is not a real need to.

We need to get opinions from more people about this.
@StevenClontz @ccaruvana @yhx-12243 @pzjp @plp127 @danflapjax

[Moniker1998]

Until that system comes, there is a need to

[pzjp]

I see the theorem list on $\pi$-Base as a very supporting element. The automated deduction for "standard facts" provides often a ridiculously twisted path. And unless we want to introduce huge redundancy it cannot be different. Many prominent results are not the most general (because too weak properties are often outside of common interest) but here we need the other ones too.

[StevenClontz]

the good news is that some work is being done to enhance the deduction system of pi-base so that meta-properties related to Kolmogorov quotient will be automatically integrated together with existing theorems

Less good news: while this isn't impossible (and is much better), I meant to say that we plan to make a standard PR to pi-base/data generated using a script, rather than enhancing pi-base/web. I'm hoping @jamesdabbs gets to sync up with me in the coming weeks to discuss how to make pi-base/web development become a bit more responsive.

[StevenClontz]

As for the PR at hand:

• I no longer believe we should edit theorems in-place to improve them, because I'd like for our IDs to be usable as permalinks to mathematical knowledge like other databases. Instead we should create a new theorem when one can be improved. Later, we should have a way to mark theorems that are deprecated or made redundant (it's not clear to me today whether those are different as a practical matter) by others. So I'd revert T516+T517 and create new theorems.
• I haven't dug into the mathematical content here, but I'm always keen on accepting contributions that answer queries. Right now https://topology.pi-base.org/spaces?q=Regular%2BFirst+countable%2BHas+a+%24%5Csigma%24-locally+finite+%24k%24-network%2B%7EPseudometrizable does not return the proof no such space exists, so if the proposed content of T516 is valid, and cannot be easily improved to a better result that works with our software today, then I'd like to see it added to the database.

[prabau]

About Steven's first bullet (@StevenClontz if you think this should be moved to a separate issue, feel free to move that so it does not clutter things here).

A general comment (not for this PR specifically): So you are saying, suppose we have a theorem (A + B + C => D) and then later on we realize the hypothesis B can be slightly weakened to B' and we would like to improve it to (A + B' + C => D),
we would have both theorems. Or suppose the hypothesis B is actually not needed. We would have both (A + B + C => D) and (A + C => D). This seems a little ridiculous?!?

In practical terms, how will it hurt people if they are looking for (A + B + C => D) and find the better result (A + C => D) ?

[StevenClontz]

I want to get some colleagues' input at #pi-base > improving theorems in pi-base (feel free to chime in there!)

[Moniker1998]

As for the PR at hand:

* I no longer believe we should edit theorems in-place to improve them, because I'd like for our IDs to be usable as permalinks to mathematical knowledge like other databases. Instead we should create a new theorem when one can be improved. Later, we should have a way to mark theorems that are deprecated or made redundant (it's not clear to me today whether those are different as a practical matter) by others. So I'd revert T516+T517 and create new theorems.

* I haven't dug into the mathematical content here, but I'm always keen on accepting contributions that answer queries. Right now  https://topology.pi-base.org/spaces?q=Regular%2BFirst+countable%2BHas+a+%24%5Csigma%24-locally+finite+%24k%24-network%2B%7EPseudometrizable does not return the proof no such space exists, so if the proposed content of T516 is valid, and cannot be easily improved to a better result that works with our software today, then I'd like to see it added to the database.

Just to be clear, are you saying I should add 4 different theorems instead of 2? @StevenClontz

[prabau]

@Moniker1998 Apart from the discussion above, for the locally compact case the first thing that O'Meara does is prove a lemma that reduces it to the first countable case.

One can in fact replace the proposed T517 with an even more general building block than this lemma. It's a result that was essentially already known to pi-base:
[ sigma-space + weakly locally compact => first countable ]
π-Base, Search for $\sigma$-space + WLC + ~First countable
In combination with the old T516 this would already prove the old T517.

In this case, by passing to the Kolmogorov quotient, we can state the more general version that does not assume T0, namely:
[ regular + weakly locally compact + $\sigma$-locally finite network => first countable ]

[prabau]

And since [ $\sigma$-locally finite network + regular => $G_\delta$ space ], one could maybe generalize the building block even more with $G_\delta$ in the hypotheses (or just "Has point $G_\delta$" ?) plus some suitable separation axiom?

[yhx-12243]

Yes. In fact if we use “ℵ-space + first countable => metrizable” (i.e., just leave the non-T₀ spaces alone), only T516 suffices and the whole T517 is redundant.

However, if we want to dive into non-T₀ case, we should reconsider T503 (this theorem is T₁-only), so the Kolmogorov coreflection is not directly available, and maybe we should weaken it to “R₁ + WLC + Gδ-space ⇒ First Countable”, seems wasty.

[Moniker1998]

I presume everything should go as it is, but with @prabau suggestion then?

[StevenClontz]

As for the PR at hand:

* I no longer believe we should edit theorems in-place to improve them, because I'd like for our IDs to be usable as permalinks to mathematical knowledge like other databases. Instead we should create a new theorem when one can be improved. Later, we should have a way to mark theorems that are deprecated or made redundant (it's not clear to me today whether those are different as a practical matter) by others. So I'd revert T516+T517 and create new theorems.

* I haven't dug into the mathematical content here, but I'm always keen on accepting contributions that answer queries. Right now  https://topology.pi-base.org/spaces?q=Regular%2BFirst+countable%2BHas+a+%24%5Csigma%24-locally+finite+%24k%24-network%2B%7EPseudometrizable does not return the proof no such space exists, so if the proposed content of T516 is valid, and cannot be easily improved to a better result that works with our software today, then I'd like to see it added to the database.

Just to be clear, are you saying I should add 4 different theorems instead of 2? @StevenClontz

Per discussion at #1442 I'm not longer suggesting 4 different theorems instead of 2.

[prabau]

@yhx-12243 Yes, I was thinking the same thing.

T503 (WLC + T2 + points G_delta => first countable)
Generalizing this to some hypotheses that become T503 is not so obvious because "points G_delta" is inherently T1.
So for example one could take a space $X$ that has points G_delta and is not a G_delta space, like S35 (ordinal space $\omega_1$) or S41 (lexicographic unit square) and take the "double pointed" version of it. The result would lose the points G_delta property.

The corresponding property would be something like: "a space such that its Kolmogorov quotient has points G_delta". But that property is too artificial. So the best we can do is weaken the result to what you suggest:
(**) [ WLC + R1 + $G_\delta$-space => first countable ]

That would not cover the double pointed examples above. Still, (**) would be more than enough for the current purpose of the non-T0 generalization of ($\aleph$-space + WLC => metrizable).

This illustrates again that all this discussion is a little bit artificial. If we had an enhanced deduction system taking into account Kolmogorov quotients automatically, none of this extra stuff would be necessary. (@StevenClontz FYI)

[prabau]

@StevenClontz After the discussion above, we still need your input on one thing for T516 ($\aleph_0$-space + first countable => metrizable).

Option 1:
replace T516 with (regular + first countable + $\sigma$-locally finite k-network => pseudometrizable)

• Advantage: avoid redundancy
• Disadvantage: ($\aleph$-space + first countable => metrizable) is the result usually quoted in the literature, as O'Meara's metrization theorem. (For example, it is in two places in Encyclopedia of General Topology (Hart, Nagata, Vaughan).) That result become hidden to users of pi-base.

---

Option 2:
replace T516 with ($\aleph$-space + first countable => metrizable)
and separately add (regular + first countable + $\sigma$-locally finite k-network => pseudometrizable)

• Advantage: O'Meara's metrization theorem is not obscured
• Disadvantage: redundancy

[prabau]

@StevenClontz FYI we need your input on the above to be able to continue with this PR

[StevenClontz]

I'm leaning towards allowing the redundancy. Every new theorem is a liability (it might be wrong). But if we have the chance to reflect a famous, named theorem, we should probably do so. One day the software will allow us to mark theorems which are redundant with others, and handle them in deductions as appropriate.

So I vote Option 2.