pi-base
Adding properties to S198 and add Locally Euclidean where dimensionality can vary
This PR includes two changes. One is that it adds properties to S198 "Disjoint union of the reals and a singleton" so that values for all but 7 properties are known or derived. The other is that it makes P123 be simply "locally Euclidean" and explicitly allowing the dimensionality to vary across the space. This second part deserves more explanation. While working to improve S198 I came to the conclusion that, despite having no qualms about it at the time, it was a mistake to have P123 be "locally $n$-Euclidean", a change enacted in PR #539. The biggest motivation is that this way the disjoint union of any two locally Euclidean spaces is also locally Euclidean. Furthermore, only the single theorem T438 relies on the assumption that the dimension is the same everywhere. It's not even fundamentally related to Euclideanness, but rather a more general property about local similarity everywhere that could unify it with T209. I will share thoughts on what exactly that property could be in a separate issue.
It would have been nice to discuss this as an "issue" first instead of a PR, but at least we have a proof of concept here to make things more concrete. Hope to study this and comment in the coming days. In the mean time, I'll change this to draft so that various people can voice their opinion in a discussion.
I originally planned to open an issue, but since I had the work done, I decided to just open a PR instead. I figured it would be somewhat controversial, but thankfully only a few spaces are affected: just Deleted Dieudonné plank and Bing's discrete extension space would no longer be deduced as not locally Euclidean.
Yes, no harm in opening a PR when the work is done. Sometimes I find doing so a useful exercise when I'm not sure if this kind of idea is half-baked or not myself. :-)
I like modeling things to maximize the expressiveness and automated deduction of the database. I'm slammed with prepping for MathFest later this week though. Probably this is something to add to our next community meeting next week. https://github.com/orgs/pi-base/discussions/690
A few comments after taking a closer look. Independently of what's in pi-base, there are two related properties:
- (1) (P123) Locally $n$-Euclidean (= locally Euclidean of dimension $n$), where $n$ is globally constant
- (2) Locally Euclidean, where $n$ can vary from point to point
with corresponding "topological $n$-manifold" and "topological manifold" (where $n$ can vary).
Property (1) is stronger, (2) is weaker. But mathematically if one understands the stronger one, one automatically understand the weaker one, as any locally Euclidean space is the topological sum (disjoint union) of open subspaces, each of them locally $n$-Euclidean for some $n$. If pi-base had a more comprehensive system of deduction, one could deduce most of the properties of S198 just from the fact it's a certain disjoint union ... But we don't have this at the moment.
So your proposal for S198 is to replace Locally $n$-Euclidean with Locally Euclidean, as all the theorems involving Locally $n$-Euclidean remain valid (with the exception of T438). This then provides an economical way to deduce many of the properties of S198.
Here are some counterarguments though. First (but we should confirm this in the next discussion meeting), pi-base has been operating under the principle that we prefer to reflect terminology and notions commonly used in the literature, unless there is a compelling reason to deviate from that. It seems that most definitions of "topological manifold" (and the corresponding locally Euclidean notion) assume $n$ does not vary from point to point. That is the case in particular in Munkres, Lee (Intro to Topological Manifolds), Willard, and many books about differential geometry.
Also, we lose something by just asserting a certain space is locally Euclidean when it is know that the dimension $n$ was constant.
So I'd like to present an alternative proposal to achieve the same goal:
- keep P123 and P124 as before
- don't delete T438
- introduce a new property "Locally Euclidean", where $n$ can vary from point to point.
- replace P123 with this new property for many of the theorems having P123 as a hypothesis (but not T438 for example)
- it seems to me it would be preferable to not introduce "topological manifold" where $n$ can vary. But that can be debated.
Added some clarifications. Please take a look.
I am curious why you removed the blank lines between the metadata portion and the rest. It does not make a difference to the final layout on the web page, but I was following @StevenClontz 's custom in this.
One remaining thing. The argument for T536 [locally Euclidean + connected ==> locally $n$-Euclidean] seems to be lacking something. Can you explain to me some details? Specifically, how to get to the point that we could deduce that some $\mathbb R^n$ is homeomorphic to some $\mathbb R^m$? Would be good also to reference something for invariance of domain...
I have commited a change for T536. The problem with the previous version is that it was not clear one could conclude that $\mathbb R^n$ was homeomorphic to $\mathbb R^m$. It was only clear that an open set of one was homeomorphic to an open set of the other. But it's also a consequence of invariance of domain that this is impossible unless $n=m$.
As far as I am concerned, this PR is ready to merge. @danflapjax @StevenClontz Can you take a look?
@StevenClontz If you eventually merge this, it would be really helpful for the "squash and merge" part if you could blank out the description section before clicking the "squash and merge" button. The list of individual commits is irrelevant and would even be misleading in this case. Compare: https://github.com/pi-base/data/pull/779#issuecomment-2366952604 Just my 2c.
I'll do a proper review once I have confirmation from @danflapjax that this is ready.
@prabau Sorry, I had somehow missed that you had committed that change. It looks good to me, and I'm good with merging now.