Trait Suggestion: Irrational slope topology S67 is Semimetrizable P102

[pzjp]

Trait Suggestion

The space Irrational slope topology S67 is Semimetrizable P102, but this fact is not known to pi-Base today: [link to pi-Base]

Proof

A semimetric $d:X^2\to[0,\infty)$ can be constructed as follows:

• $d((x,y),(z,0))=d((z,0),(x,y))=\min\{ |x-y/\theta-z|, |x+y/\theta -z| \}$ for $x,z,y\in \mathbb Q$, $y\geq0$,
• $d((x_1,y_1),(x_2,y_2))= 1$ if $x_1,x_2,y_1,y_2\in \mathbb Q$, $y_1,y_2>0$ and $(x_1,y_1)\neq (x_2,y_2)$,
• $d((x,y),(x,y)) =0$ for $x,y\in\mathbb Q$, $y> 0$.

The fact that $d$ is a symmetric follows from the fact that $\theta\notin \mathbb Q$ and hence in the first case attaining rational value $0$ requires $y=0$.

For $\epsilon<1$ and $z\in X$ it can be readily verified that $B_d(z,\epsilon):=\{w\in X: d(z,w)<\epsilon \} = N_\epsilon(z)$, for $z\in X$, where $N_\epsilon$ denotes a base neighborhood from the definition of S67.

Remark

I can imagine that semimetrizability of S67 follows from it being locally metrizable "and something" (e.g. separability). A potential theorem of this kind could resolve several traits. The only locally metrizable known to be not semimatrizable space (according to pi-Base) is the Long line S38.

[prabau]

Hi @pzjp . Thanks for all the great suggestions.

Before you create more issues with trait suggestions though, you may be interested to read the discussion at the end of #1055. See also #1065.

Would you be interested in contributing PRs yourself as well?

@StevenClontz

[StevenClontz]

I want to run a contributor tutorial next month: https://github.com/orgs/pi-base/discussions/1077

But in the meantime we also have this video: https://github.com/pi-base/data/wiki/Contributing

[pzjp]

@prabau What are the guidelines for such PR? I imagine many changes in "random" places wouldn't be nice to review. Should this be one space at a time or just some limit on the total number of added traits?

I have to get familiar with the workflow, anyway. I was not using git for several years and even back then I probably was not fluent.

I see more missing observations, indeed. Processing more of them at once would be convenient.

[prabau]

Thanks for the interest. It would be good to have you as a direct contributor.

Tomorrow I'll give you some general guidelines and recommendations on starting up with git, etc.

[prabau]

@pzjp Here are a few general guidelines for becoming a contributor. First is getting familiar with git and github.

It seems you have used git in the past, so you have some familiarity with it. No worry about not being fluent in git. All you need is a high-level conceptual understanding of git as a source code control system. In particular, the notion of commit and of branch. (We use the "topic branch" workflow for pi-base, https://git-scm.com/book/en/v2/Git-Branching-Branching-Workflows) I recommend reading some of the documentation in https://docs.github.com/en under "Get started" and going through the "Hello world" tutorial to create your first github repository. And then play with it, do edits, commits, create or modify one or multiple files, create separate branches, merge them into your main branch, etc.

So I don't have to repeat all of it here, please also look at all the comments in #933 regarding the onboarding process when @david20000813 started to become a contributor.

Once you feel comfortable with git/github, let us know and we can plan some really simple PRs to get the basic mechanics of a PR down. But I would really want you to go through the exercise of the Hello world tutorial first, make sure you can create and merge branches, and do commits involving one and multiple files in particular.

As for the scope of each PR, we can discuss more when we get to that stage. But please don't start an official PR in pi-base before discussing it first (we've had to block someone who jumped in enthusiastically without fully knowing what they were supposed to do).

So take your time. No rush on any of this. And feel free to ask anything at any time.

What editor do you use by the way?

[pzjp]

For pi-Base the online VSCode built in GitHub seems fine. Especially for the not-so-advanced work with editing traits. Recently I'm mostly using VSCode anyway but the online version minimizes the risk of being not synchronized, right?
In general I understood the video example.

[prabau]

Yes, github.dev (online vscode) works very well. As far as synchonization goes, we always do our work on a "topic branch", i.e., a new branch for each PR that is created from the main branch. After the branch is created, it may diverge from main because more changes are accumulated into main while the topic branch is being worked on. But that does not cause any problem because different people usually don't work on the same files at the same time. Eventually the topic branch gets merged back into main and gets deleted.

[pzjp]

@prabau I guess I'm more or less ready.
The one slightly confusing part in the video was the transition from 'private' branch to the actual pi-base branch. As I understand this is required in order to perform the check. And it looks like it can be done by just creating a new branch having a PR opened in the editor. It is spawning (?) a branch from one repository to another in a slightly implicit way (I would expect that creating branch is always an operation within one rep).

I've written some updates to S67 (P82, ~P89, ~P204) on my fork of pi-Base. link

[prabau]

@pzjp Okay. But please forget about pi-base for the moment and forget about the pi-base tutorial video.
I would like to see you comfortable with the github mechanisms first.

So can you please do the "Hello world" tutorial first? If you feel comfortable already, it should not take you much time.
https://docs.github.com/en/get-started/start-your-journey/hello-world

And after you go through the steps of that tutorial, you can also play further with your Hello world repository. Maybe it's already covered, but if it's not, make sure you can do the following:

• create a topic branch
• do commits that create or delete files
• modify more than one file at a time in the same commit
• merge the topic branch back into your main branch.

Sorry to insist on this, but we've had cases in the past where newcomers thought they knew what they were doing, but did not know some of the basic procedures.

(Then later, we'll talk in more detail about pi-base.)

[pzjp]

I did steps of this kind (the tutorial itself is not that precise).
I wrote about "pi-Base thing" because there begins a minor confusion.
My general doubts regarding the usage of version control systems are mostly "cosmetic". Llike: "how big the single commits should be" or "does their titles really matter" (e.g. I may randomly fix some spelling mistake in a different file. A pedantic approach would require a separate commit for that or messing with the title.) Luckily, the general approach on pi-Base seems to be indifferent to such doubts. And there are not likely to be conflicts while merging.

[prabau]

OK, let's discuss pi-base then. Don't confuse commits and PR (pull request). All our work is organized in logical units of work called PRs.

We follow the "topic branch" workflow for pi-base. I.e., it is recommended to have a separate branch (created off of the main branch of your repository) for each set of changes in a PR. That allows to have multiples independent changes going in parallel at the same time. Otherwise, if you do everything from the main branch (not recommended), it becomes very hard to disentangle both sets of changes and kind of a pain to wait for review of two PR at the same time, and if they don't get merged in the same order,... it becomes a mess. (Speaking of experience with some of the newcomers here in the past.)

The important thing is to keep each PR of manageable size. Gigantic PRs are bad. They are hard to review, may generate a lot of discussion for different parts of it, and take a long time to get approved and merged. It is always preferable to have several smaller PRs that can each be reviewed independently of others and more quickly. That way, we get steady incremental progress.

Each PR is typically some new theorem plus maybe associated trait cleanup, or some trait cleanup of some space, or some additional trait for a space, etc. You can sometimes put a little more things together if they are related, but if they are not related it's preferable to have a few smaller PRs. Again, please do not put too much in a single PR. We've had several cases in the past where the review took a very long time, and the PR never got completed and finally had to be closed and the work redone in smaller PRs.

[prabau]

So for your first PR, I suggest something small. Adding a single trait for a single space. Do you have any preference?

Preferably something easy, with not much mathematical content, that will not generate a lot of discussion.
It's just to make sure the mechanism of doing a PR works properly.

[pzjp]

I've listed 32 missing properties by now :)
For a trivial example let it be ~P180 for S86 link.
The proof is merely: The subspace $\mathbb R{\times}\{1\}$ is uncountable and discrete hence not separable.

[prabau]

Perfect. I see that you have cloned the official pi-base/data repository into you own piBase-copy repository.
So what you need to do is bring you pi-base repository up to date with the official one. Then create a topic branch for this PR based on your main branch. Then do a commit in that new branch, and create the PR.