Add three new theorems regarding countable pi-character

[JSMassmann]

Following up from #1712, particularly @felixpernegger's advice to just PR the theorems I know.

[felixpernegger]

Can you add the metaproperies in this PR which we discussed in the last?

[prabau]

Did you check the proof of the theorems quoted from the Handbook?

They make the assumption that spaces are T2.
But for T905 (T2 + compact + countably tight => countable pi-character) for example:
It seems to me that X has countable pi-character iff Kol(X) does (please double check that meta-property).
And on the other hand, compact and countably tight also have the same metaprop.
So by passing to the Kol quotient, one can immediately improve the theorem by replace T2 with R1.

And more than that: where is exactly the T2 assumption used in the proof? Often a blanket assumption of separation axiom in a paper is not used in some of the results. It would be great if you could check this. Maybe we can generalize things even more.

Same comments for T903.

[prabau]

T904: it's okay. But it can really be written in a simpler (and shorter) way. (use notation $U\cdot U^{-1}$, given O, find W s.t. $W\cdot W^{-1}\subseteq O$ by continuity of the group operations, etc, etc. And all this indexing is not really necessary.)
The basic idea is that if $U$ is a nonempty open set, $U\cdot U^{-1}$ is a nbhd of the identity element.

[JSMassmann]

Did you check the proof of the theorems quoted from the Handbook?

Yes. But not to the extent of knowing for certain where they use separation axioms.

Same comments for T903.

In that case they explicitly state the $T_3$ hypothesis, rather than having it as a blanket, so I don't know if it could be weakened.

And all this indexing is not really necessary.

Sorry - set theorist by trade!

[prabau]

Counterexample for P243 not being hereditary:

• $\pi w(\beta\omega)=\omega$
• $\pi w(\beta\omega\setminus\omega)=2^\omega$ (mentioned on p. 14 of the Handbook, I did not check it)

(should say $\aleph_0$ and $2^{\aleph_0}$ but using $\omega$ seems common here)

[prabau]

@JSMassmann After doing a few commits, you should check the result on the pi-base site itself, to see if there are any formatting problems among other things.
(go the Advanced tab and enter the branch name for the PR)

Look at T904 in particular.

[JSMassmann]

Yeah. $\beta \omega \setminus \omega$ is closed, hence why you can't get hereditary-ness for more than open or dense sets in general. (I usually see $\aleph_0$ used instead of $\omega$ when talking about cardinality - an advantage is that $2^\omega$ really has three different meanings, while $2^{\aleph_0}$ doesn't.)

Oops. I see the formatting issue now.

[felixpernegger]

a few small more comments, then we should be good to go

[felixpernegger]

Suggested change

	- P000011: true
	- P000005: true

This stays closed to the source; this doesnt weaken the assumption since regular + has point g delta => t3 anyways

[prabau]

@JSMassmann Please change P5 to P11. It is equivalent since (points G_delta) implies T1. If you compare the theorem pages for each of the properties (https://topology.pi-base.org/properties/P000011 vs. https://topology.pi-base.org/properties/P000005), when we can phrase a theorem with just regular in the hypotheses, we do so, as it is a formally weaker property. In the general case, technically it's very very slightly easier to check the hypotheses, and the theorem has wider applicability. (of course equivalent in this case) But, more that that, using regular here allows to have the theorem side by side with other theorems that also use "regular + points G_delta" in the hypotheses, like T508.

[felixpernegger]

The source explicitly write T3 and not regular. Writing anything else complicates this for no reason.

I am strongly against this.

[felixpernegger]

In the general case, technically it's very very slightly easier to check the hypotheses and the theorem thus has wider applicability. (of course equivalent in this case) But, more that that, using regular here allows to have the theorem side by side with other theorems that also use "regular + points G_delta" in the hypotheses, like T508.

Most (or at least a lot of) theorems in pibase are essentially unusable directly anyways
(For example we do not have urysohn metrization theorem lol).

Instead deduction engine works very well

[prabau]

@felixpernegger You keep insisting about following the source. You did the same in other PRs. This is misguided. Often we modify things to best fit what we want to present in pi-base. It does not really matter what one source says. It's just one tool in the justification of a result. (For another example, many sources make blanket assumptions of some separation axioms. Engelking for example in many places. But we don't add the same assumption if it's not needed.)

[felixpernegger]

We obviously should have theorems in their most general form, but dont abuse sources.
A good example/practise of this is https://topology.pi-base.org/theorems/T000845

[felixpernegger]

@felixpernegger Since things are equivalent, and like you said, the deduction engine works very well, you should not have a problem with either choice. And since for some people it is helpful to have things presented in a certain way, it should hopefully not matter to you.

The individual need to be perfectly clear. It is fine to just use outside sources obv, but if we say something is Corollary XY and then the result is actually not, we need to clarify this. A more glarring example is the other suggestion I made to the pr

[prabau]

A more glarring example is the other suggestion I made to the pr

I totally agree about that one. I thought yesterday about making a suggestion along these lines and you beat me to it. (Actually I wanted to suggest something a little more explicit. Will write it up.)

[JSMassmann]

So... what should it be? P5 or P11? I personally don't mind, I see the arguments for both.

[felixpernegger]

So... what should it be? P5 or P11? I personally don't mind, I see the arguments for both.

I think its best if you decide.

[prabau]

@felixpernegger This time, please don't approve and merge before I have had the chance to give all my comments. I would really appreciate it. In the same way, I will give you all the opportunity to give all your comments.

[prabau]

@felixpernegger Completely off topic, but I have also long thought it would be nice to add the Urysohn metrization thm in its usual form to pi-base. Would you have an objection if I do so?

[felixpernegger]

@felixpernegger Completely off topic, but I have also long thought it would be nice to add the Urysohn metrization thm in its usual form to pi-base. Would you have an objection if I do so?

Yes this is a good idea. https://topology.pi-base.org/theorems/T000302 is using it in its proof actually.

[prabau]

You can add a metaproperty for open sets as suggested by Felix: #1791 (comment)

[JSMassmann]

Okay.

[prabau]

@JSMassmann I am satisfied with what there is right now. Leaving it up to you about P5 vs P11.

[JSMassmann]

Okay. I think keeping it as P11 is good.