search

pi-base / data

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

Delete T340: Topological n-manifold => second countable? #810

Open Jianing-Song opened 1 week ago

Jianing-Song commented 1 week ago

We already have T461: Topological n-manifold => Embeddable into Euclidean space, and T459: Embeddable into Euclidean space => Second countable. And unlike the $T_2\Rightarrow T_1$ theorem, this T340 does not simplify any proof because it follows merely from the definition.

Any comments?

StevenClontz commented 1 week ago

Sounds fine to me.

prabau commented 1 week ago

Technically, it is true that T340 (top. n-manifold ==> second countable) is deducible from T461 and T459. But T461 a highly non-trivial result, while the fact that top. n-manifolds are second countable is an immediate consequence of the definition. (And T461 makes use of second countability in its proof.)

@StevenClontz, in light of this, if you still think we can remove T340, I would be fine with it. Just wanted both of you to consider if there would be a better way to approach this?

StevenClontz commented 1 week ago

T461 a highly non-trivial result

TBH I didn't think carefully about this; I suppose I haven't tried proving this myself and underestimated how intricate the result might be. I was coming from the perspective that this result felt "well-known".

Jianing-Song commented 1 week ago

Technically, it is true that T340 (top. n-manifold ==> second countable) is deducible from T461 and T459. But T461 a highly non-trivial result, while the fact that top. n-manifolds are second countable is an immediate consequence of the definition. (And T461 makes use of second countability in its proof.)

@StevenClontz, in light of this, if you still think we can remove T340, I would be fine with it. Just wanted both of you to consider if there would be a better way to approach this?

I think there is a difference between T340 and $T_2\Rightarrow T_1$. Although $T_2\Rightarrow T_1$ is deduced automatically, a person who wants to know the proof can consult this theorem directly, without having to know all these intermediate terms. However, the case of T340 is different. I mean, no one would need to have a proof of "topological manifolds are second countable", because that is merely what the definition says, so T340 really only serves for automatic deduction. That's why I think it can be replaced by T459 and T461. Of course, it is up to you to decide ultimately :)