pi-base / data

A community database of topological counterexamples
https://topology.pi-base.org/
Creative Commons Attribution 4.0 International
69 stars 24 forks source link

T6 definition #677

Closed Almanzoris closed 2 weeks ago

Almanzoris commented 3 weeks ago

The current definition here is: a space that is both T1 and Perfectly normal.

But every Perfectly normal space is G delta and every G delta space is R0. Therefore, every Perfectly normal space is R0. As a space is T1 if, and only if, it is T0 and R0, then it is sufficient to define a T6 space as a space that is both T0 and Perfectly normal.

prabau commented 3 weeks ago

Good observation.

Note that [T0 + perfectly normal ==> T6] is already deducible from pi-base, as you can see from the Explore page: https://topology.pi-base.org/spaces?q=T_0%2Bperfectly+normal%2B%7ET_6

But we can definitely add the equivalent characterization you suggest. This is similar to T_3, which is defined as regular + T1, but that is equivalent to regular +T0. (Could also be defined as regular + T2).

Would you like to try your hand at writing a PR for this?

Almanzoris commented 3 weeks ago

Thank you, and yeah, certainly.

And, for sure, I would like to.

prabau commented 2 weeks ago

Awesome! Not sure how much experience you have with github/git. But if you don't, I strongly suggest to learn about git/github first. A good starting point is all the comments made when @Jianing-Song was onboarded, specifically https://github.com/pi-base/data/issues/593#issuecomment-2009313831 and other comments in the same thread. (specifically, you should become familiar with the high level git workflow, the notion of "topic branch", which is what we use, pull requests, etc. And need to become familliar with the use of github.dev = the vscode editor. The github help and the "hello world" tutorial are worth going through). See the various links in the comments mentioned above.

And just to be clear, the change involved here don't involved anything more than adding one sentence to the property file P000067.md: "Equivalently, a space that is {P1} and {P15}." No changes needed to any theorem or anything else.

The change is trivial, but it serves as an opportunity for you to become familiar with git/github and the mechanics of making contributions. So take all the time you need for this, explore github, etc. Please ask as many questions as you need and we'll happily help out.

Almanzoris commented 2 weeks ago

Yeah, I have no experience with github/git. Thank you very much for your information, your time and your patience. I am going to try to get familiar with this, starting by learning these basics.

And my bad, right, I will just add that sentence.

prabau commented 2 weeks ago

Later on, if you have the inclination, there are lots of little improvements that could be made to pi-base. For example, if you are interested in a particular space, remove redundant traits and add some missing ones. Or if you are studying a particular theorem, pi-base often does not point to a good justification. It only has a assertion from Steen & Seebach, and that could be replaced by a reference to a theorem in Willard or Engelking, or possibly with something in mathse. Anyway, we welcome you as a contributor.

prabau commented 2 weeks ago

Feel free to close this issue as it has been resolved.

Almanzoris commented 2 weeks ago

Thank you! I surely will if I notice any.