Toronto spaces - roadmap #1549
Toronto spaces - roadmap #1549
Conversation
|
I like the branch name :-) |
|
This will possibly need a change in numeration of theorems, or some other PR will |
|
FYI I do think we should merge this eventually, but only after we find some theorems which automatically eliminate almost all spaces from being a Toronto space. |
|
To keep things tidy, the related #1395 that started this has been closed. |
|
I have not reviewed any of this (yet), but at a high level why do we have so many theorems here (14 and counting)? |
Because the paper |
|
There are some whihc can be deduced, I remove them now |
On the hindsight, by adding all these theorems, the explorer now only gives 5 more t2 spaces for which toronto is unknown |
|
@felixpernegger did you read the proofs of those theorems you are adding? |
|
not yet, will do tomorrow, I need to sleep now. |
|
A good news: T915 and T917 are in fact redundant, though the reasoning chain is very long. |
theorems/T000915.md
Outdated
There was a problem hiding this comment.
Redundant, can be removed.
theorems/T000917.md
Outdated
There was a problem hiding this comment.
Redundant, can be removed.
There was a problem hiding this comment.
Redundant after adding (Toronto + T₂ ⇒ Scattered) and #1562.
|
@felixpernegger My usual rant, after bad experiences in the past :-) And note it's irrelevant if for a new property most spaces have it as an unknown trait. Nothing forces us to "complete" spaces at the same time. That will happen eventually. |
Co-authored-by: yhx-12243 <yhx12243@gmail.com>
|
One serious question is that, the original paper assume |𝑋| = ℵ₁. So we need to double check whether this result still holds without this condition. At least I know some result (sequentially discrete, scattered) is holds for any T₂ Toronto space. |
|
@prabau if you prefer, I can split this up in 2-3 PR's
I think 1) is pretty much ready, 2) if we double check the proof of the paper and 3) still needs some work (see yhx's comment) |
|
@felixpernegger I think that would be useful. We can keep this as Draft for now to refer to, and then eventually close it. For comparison, see the comments we made for #1486. Not exactly the same situation, but somewhat similar. And unfortunately, that PR is not going anywhere soon due to these problems. |
|
Ok I will do that. But about that PR I want to add, that I think this was handed very poorly. The author is very talented but due to the response he got on the PR likely won't ever contribute again. |
felixpernegger
changed the title
Completely unrelated but this is the longest deduction chain i have ever seen haha
|
Yeah, it's unfortunate. We repeatedly told him not to do some things, but he kept going. Hope we'll be able to get back to his PR some day, once there is time to breathe with all the other PRs. |
|
I guess that S17 is Toronto will have to be added manually |
#1395 is meant to introduce Toronto spaces, however it is inactive (@StevenClontz).
Toronto spaces & the Toronto problem are relatively well documented in the literature, so I think it is reasonable to add them. All important known properties (as far as I can see) can be found in
https://wrbrian.wordpress.com/wp-content/uploads/2012/01/thetorontoproblem.pdf
also maybe see
https://en.wikipedia.org/wiki/Toronto_space
As stated in #1395 (and the link), under GCH we won't find T2 non-discrete Toronto spaces. Furthermore one can classify all non-T1 Toronto spaces (as some in the wordpress link). There might however still be interesting non-T2, T1 Toronto spaces.
I only added 3 trivial theorems so far. Adding the notion of upper and lower spaces would help eliminate many other spaces automatically, however I think this can be done at a later point. For now it would be nice to bring down the number of open, yet inactive PR's.
@Moniker1998