Topological manifold with boundary and related properties (part 1)

[prabau]

As proposed in #1736. Three new properties:

• (P235) locally a Euclidean half-space
• (P236) locally an $n$-Euclidean half-space
• (P237) topological $n$-manifold with boundary

This part 1 adds the new properties and some basic plumbing relating them to other properties. And one old result for locally contractible is generalized to P235.

Also added some mention of open nbhds for the previous locally Euclidean properties.

Part 2 will have more basic plumbing and generalizations of existing theorems. Followed by part 3 ...

[GeoffreySangston]

I'm ready to accept whenever those conversations are resolved.

[prabau]

@GeoffreySangston @felixpernegger
For the name, should we use "half-space", "halfspace" or "half space"?

We want to convey that a half space is a thing in itself. The first two versions tighten the two parts into a single concept and seem preferable. That is also what many sources seem to be using (wikipedia, Lee, ncatlab, etc) (with variations half-ball, half-plane, etc)

Personally I would have preferred "halfspace" because it's easier to type. But it seems more sources use "half-space", so I chose that one.

What do you think?

[felixpernegger]

Half-space seems fine
https://en.wikipedia.org/wiki/Half-space_(geometry)

[GeoffreySangston]

I like half-space just because that's what Lee uses in his trilogy of books, which is one of the sources I've spent the most time with. I don't have a real preference though.

[prabau]

Regarding "topological manifold" vs. "topological $n$-manifold":

The original version of manifold (P124) in pi-base was not completely precise and a little sloppy. It was called "topological manifold" and did allow variable dimension, although by accident of underspecification it seems.
We discussed improvements as part of #507 (not implemented), which were implemented in #539.
Look at #507 (comment), #507 (comment) and comments in between.

In particular, should a manifold have a dimension that can vary from point to point? A paragraph at the end of https://en.wikipedia.org/wiki/Manifold#Definition gives a few sources that allow that, but as you say, most sources do not.

In the end, we decided to not allow variable dimension either, and to use "topological $n$-manifold" to make it very clear that the dimension is a fixed number $n$ (also in comparison with the previous "topological manifold" in pi-base). This also has the advantage that it relates well to "locally $n$-Euclidean" (vs. "locally Euclidean").
(Note that Lee also uses the terminology $n$-manifold.)

Now we could decide to just use "topological manifold" if you think that's preferable. Please take a look at the links above and we can discuss further.

[prabau]

@StevenClontz FYI, since you were involved in the previous changes for manifolds.

[StevenClontz]

I have no strong opinions here so I'm good with whatever consensus y'all have (@ me back in if I need to break a tie or something)

[GeoffreySangston]

Okay I think we should stick with emphasizing Topological $n$-manifold since: (1) Some sources allow the dimension to vary. (2) Our usage isn't weird and agrees with standard texts like Lee's books. (3) Pi-base could eventually get some kind of other thing with "manifold" in the name so being more precise is probably a good idea for the future.

[prabau]

@GeoffreySangston I think the only remaining thing is #1744 (comment)