Circles and rationals are not Toronto

[artemetra]

First time contributing, two easy traits. These spaces are not Toronto:

• S000170 Circle S^1
• S000027 Rational numbers Q

Let me know if something is wrong here, I'll gladly fix it.

[prabau]

Hi @artemetra Thanks for your interest in pi-base. Regarding the Toronto property, PR #1549 has been proposed in the past to add various theorems that would allow to deduce more traits automatically. But that PR is on hold and pieces of it need to be broken off into their own little PR. You can read the whole discussion about it.
So the two traits you are proposing would most probably become redundant and we would rather focus on some of the pending theorems instead.

@felixpernegger Is there anything you'd like to add?

[prabau]

I have not looked in detail at the proposed theorems in #1549, but here is one simple theorem that would cover your two spaces:
[ T2 + no isolated point => not Toronto ]

Maybe @felixpernegger has a better one that covers even more.

[felixpernegger]

I dont really have anything to add. The PR is fine as it is; yes most likely the traits are covered by some theorem, but I highly doubt someone will really work on this anytime soon, so why not add them now.

In hindsight, I think maybe adding Toronto wasnt the smartest decision, but whatever.

[prabau]

@felixpernegger approved this. But I am not approving this PR.

@artemetra The theorem I suggested would be more valuable, as it would allow to derive that 48 more spaces are not Toronto, including the two you covered:
https://topology.pi-base.org/spaces?q=T2%2B%7EHas+an+isolated+point%2B%3FToronto

Would you be interested in working on adding this theorem instead?
If yes, let me know and I'll close this PR. We can then talk about how to add the new theorem.

[felixpernegger]

I have not looked in detail at the proposed theorems in #1549, but here is one simple theorem that would cover your two spaces: [ T2 + no isolated point => not Toronto ]

Maybe @felixpernegger has a better one that covers even more.

I thought about this briefly and came up with the following:

Assume $X$ is infinite, Toronto with no isolated points. If there is a nonempty open set $U$ with $|X\setminus U|=|X|$. So if $x \in U$ is arbitrary, remove all points from $U$ except $x$. The resulting subspace has same card. as $X$, but has an isolated point. Contradiction with Toronto.

---

So what we have to ask us, is what properties imply the existence of a large closed set.
One solution (though there may be others as well):
If a space is not hyperconnected, there are two nonempty disjoint open sets, by set theory one of those must have the desired property from above.
So we have: Toronto + ~Hyperconnected + ~Has An Isolated Point => Finite

This in particular covers the T2 case (according to pibase search this covers 3 more spaces than t2)

[felixpernegger]

This covers 51 out of 96 unknown toronto traits, so this would actually be a very good theorem to have (I changed my mind). The total number of unknown traits would be reduced by about 2% by this theorem, definitely one of the most effective theorems still missing.

(there are only 5 hyperconnected t1 spaces with an isolated point, which are all pretty obscure, so for practical purposes the above proposed theorem is enough)

[artemetra]

Thank you for your replies! I agree that if this is covered by simple theorems then of course there is no need to add this trait manually. So perhaps this PR should be closed.

this would actually be a very good theorem to have

@felixpernegger which theorem are you referring to here, since several got mentioned? Is it [ T2 + no isolated point => not Toronto ] or [ Toronto + ~Hyperconnected + ~Has An Isolated Point => Finite ] ? I also want to note that while I don't have the best understanding of the discussion in #1549, the two spaces I talked about already covered by theorems from canada: S27 and S170. So I am not sure how redundant we want to be assuming the theorems in #1549 are all correct.

[felixpernegger]

Thank you for your replies! I agree that if this is covered by simple theorems then of course there is no need to add this trait manually. So perhaps this PR should be closed.

this would actually be a very good theorem to have

@felixpernegger which theorem are you referring to here, since several got mentioned? Is it [ T2 + no isolated point => not Toronto ] or [ Toronto + ~Hyperconnected + ~Has An Isolated Point => Finite ] ? I also want to note that while I don't have the best understanding of the discussion in #1549, the two spaces I talked about already covered by theorems from canada: S27 and S170. So I am not sure how redundant we want to be assuming the theorems in #1549 are all correct.

We want Toronto + ~Hyperconnected + ~Has An Isolated Point => Finite. This is more general, since T2 + has Multiple points => ~Hyperconnected.

Iirc that PR has the major issue of (most of) the theorems only working if we assume P114, so I recommend to just ignore whats written there; its not so relevant anymore.

[artemetra]

I see, I'll work on that then and open a new pull request once the proof is done. I'll close this now.

[prabau]

@artemetra There are multiple logically equivalent ways to phrase a theorem. The following seems rather natural to me, as far as applying it:
~Hyperconnected + ~Has An Isolated Point + ~finite => ~Toronto

But if we like "positive conditions" better, I think I would prefer:
Toronto + ~Has An Isolated Point + ~finite => Hyperconnected