Trait Suggestion: Novak space S109 is extremally disconnected

[GeoffreySangston]

Trait Suggestion

The space Novak space S109 is extremally disconnected P49, but this fact is not known to pi-Base today: link to pi-Base.

(This issue began with the suggestion that Novak space is totally disconnected, hence the discussion below.)

Proof/References

See #1055 (comment)

[Moniker1998]

I would say to not aim for proving traits that could be resolved in a more efficient manner. That is, lets try to prove more about a space before doing a pull request/issue, and let the theorems resolve the rest. Of course, I get its not always possible.

But I think this is the mentality with which we have to handle pi-base.

[GeoffreySangston]

@Moniker1998 I certainly agree with you, but what's the more efficient manner? I raised the issue so we could discuss it.

If no easy strengthening is forthcoming, I can't see a legitimate reason not to include this, however.

[Moniker1998]

I'm saying this because we are already piling up in terms of raised issues (over 80 open ones). So lets try to be efficient.
I've mentioned this just to make sure that you are aware of this. I would try to avoid easier to prove traits for the ones that are actually less obvious, unless a trait couldn't be proven from other ones.

In this case we can say the space is extremally disconnected, since its a dense subspace of extremally disconnected space $\beta\mathbb{N}$.
This is what we should actually add.

[GeoffreySangston]

@Moniker1998 I disagree with the sentiment. Novak's space sat around for a long time without pi-base knowing if it is contractible or not. By raising the issue, now you point out it is extremally disconnected. (I want to point out that asking if someone knew if Novak space is extremally disconnected was an explicit part of the original post, and you can see the edits.) Had I not raised the issue, probably pi-base would not have known if it was contractible or not for quite a long time.

[Moniker1998]

I don't think that raising an issue for addition of a weaker property is a good place to determine if we can prove a stronger property or not.
Perhaps there should be a separate place for such questions, maybe in discussions. @StevenClontz

[GeoffreySangston]

@Moniker1998 I don't think that's a fair representation of this thread. A fair representation of this thread is twofold

1. To share information not known to pi-base (which did not even know if this space is not contractible). My long term goal is to fill out all of the information related to contractible + simply connected + a few other properties yet to be added.
2. To allow the community an opportunity to refine that information. In my view, it's not a problem if a trait gets added to pi-base which is eventually removed, if adding the trait in the first place did solve a problem and was not very difficult.

To me, item 2 is among the chief purposes of issues. Otherwise we should just make PR's directly. Edit: @StevenClontz Afterwards I realized I should probably explicitly ask you what you think about any normative claims like this.

I think if the position you advocate is adopted, then it gate keeps contribution to the website to only those members with strong knowledge of all 200 properties in pi-base. That seems like a clear bad outcome.

[Moniker1998]

To allow the community an opportunity to refine that information. In my view, it's not a problem if a trait gets added to pi-base which is eventually removed, if adding the trait in the first place did solve a problem and was not very difficult.

I do see this as a slight problem if it would keep to consistently occur. It creates unnecessary clutter, and as I said the issues keep on piling up as well.

[GeoffreySangston]

@Moniker1998 Do you have git PR privileges? I'm sure everyone would welcome your git contributions if not. That seems like a secondary issue @StevenClontz or @prabau might be able to address. Some of the issues you raised I had been intending to make PRs for, but since the academic year is ending I'm very busy with grading etc.. and it has to wait a bit.

[Moniker1998]

I think if the position you advocate is adopted, then it gate keeps contribution to the website to only those members with strong knowledge of all 200 properties in pi-base. That seems like a clear bad outcome.

I don't see how it is so. ideologically I am advocating for a more throughout approach towards issues, more research of a space and traits involved, current theorems on pi-base.
Practically, I am suggesting for there to be a place to ask if a stronger property can be proven, outside of 'issues' tab.

[GeoffreySangston]

I don't see how it is so. ideologically I am advocating for a more throughout approach towards issues, more research of a space and traits involved, current theorems on pi-base.

I can only speak for how this would affect me. This probably requires more investment in any particular Issue than I can currently afford to give. I was happy to notice that Novak's space was a subspace of $\beta \omega$, which knocks it off the list of '?Contractible' spaces. If the following suggestion is accepted, then that might solve the issue, but there are caveats:

Practically, I am suggesting for there to be a place to ask if a stronger property can be proven, outside of 'issues' tab.

I'm attracted to this idea. A counterpoint is that whatever goes in there may not be clearly distinguished from issue already. So the process turns from Issue -> PR -> Review into Less confident Issue -> More confident Issue -> PR -> Review, which may not actually be saving time or better organized.

[Moniker1998]

I'm attracted to this idea. A counterpoint is that whatever goes in there may not be clearly distinguished from issue already. So the process turns from Issue -> PR -> Review into Less confident Issue -> More confident Issue -> PR -> Review, which may not actually be saving time or better organized.

Yes. I am also against creating unnecessary bureaucracy. I suppose that was a bad idea

[GeoffreySangston]

To allow the community an opportunity to refine that information. In my view, it's not a problem if a trait gets added to pi-base which is eventually removed, if adding the trait in the first place did solve a problem and was not very difficult.

I do see this as a slight problem if it would keep to consistently occur. It creates unnecessary clutter, and as I said the issues keep on piling up as well.

Just wanted to add that I agree with you that this could lead to clutter. I think it's a matter of finding a balance though. Also, a few times now I've opened PR's to remove redundant traits from spaces, so I hope people are aware that I am aware of the potential issue.

[StevenClontz]

There's some good discussion here, and I think that as we (hopefully!) continue to grow, we need to have these discussions on community norms and expectations. Everything we've settled on during community calls is (or should be) in the https://github.com/pi-base/data/wiki

I'm always a fan of not letting the perfect be the enemy of the good. Furthermore, the more picky we are, the more friction we create for new community members to get involved.

So if an issue is opened that can be improved, I think we should focus on constructive feedback (e.g. suggest changing totally disconnected to extremally disconnected, or suggest that a theorem can be added instead of a single trait), and try to efficiently refine the issue to something that should be implemented, or determine that the issue can be closed or merged with another issue.

[prabau]

@StevenClontz @GeoffreySangston @Moniker1998
I would like to suggest an additional thing. The number of issues, especially for suggested traits, is becoming out of hand.

Some of these trait issues require a preliminary discussion, but probably most of them don't. For those that don't, it would be more efficient for the proposer to bypass writing an issue and directly write a PR instead. Some discussion is still possible in a PR itself.

That would serve two purposes: (1) more efficient overall process by going more quickly to implementation; (2) limit the rate at which the proposer generates issues/PRs. I.e., they would (or maybe should) wait until some of these PRs are merged before create new ones. I.e., should there be some form of (not enforced, but recommended) limit on the number of PRs currently pending from anyone? (Not even sure I agree about that one, but just writing this down for discussion.)

And like Steven, I don't really see a problem with adding a trait that later gets superseded by a stronger one or a theorem.

Anyway, these are possibilities to reduce buraucracy and improve overall efficiency.

Could be discussed in a community meeting.

[StevenClontz]

For those of us comfortable writing PRs, I definitely think that filling in trait gaps is best done directly. I'd rather have a dozen small one-file trait PRs than a dozen issues suggesting them. I'll update the issue template to suggest this.

[prabau]

@StevenClontz I had a few additional small suggestions for improving the new issue templates. Should I write an issue for discussion?

[StevenClontz]

@StevenClontz I had a few additional small suggestions for improving the new issue templates. Should I write an issue for discussion?

Find with me, or propose a PR directly if you think you have a solid improvement.