Basic topological properties of manifolds

[grunweg]

Topological manifolds inherit properties from their model space, such as the following. Let $M$ be a topological manifold.

1. If $M$ is finite-dimensional, it is locally compact (if $M$ is modelled on e.g. the reals).
2. $M$ is locally connected.
3. $M$ is locally path-connected.
4. Deduce that $M$ is connected iff it is path-connected.
5. $M$ is locally simply connected.
6. $M$ is semi-locally simply connected.

Current status (October 2023):

• (1) is shown in [Merged by Bors] - feat: finite-dimensional manifolds are locally compact #7822, (3) in feat: real manifolds are locally path-connected #7877
• (3) implies (2), but mathlib doesn't have all the API for proving this yet. (If (5) were defined, this would also imply (3).)
• (5) and (6) are not defined in mathlib yet; mathlib has simply connected spaces, though

[grunweg]

Update. I've shown and PRed (3). I also have a branch working towards (2) and (4).

The implication (3) => (2) exposes some missing concepts and API (the remaining scaffolding is also on the branch): the definitions of locally connected and path-connected sets differ slightly, in that the former requires a basis of open connected neighbourhoods, whereas the latter doesn't require openness.
The gap is closed by showing that open subsets of locally path-connected sets are path-connected.
The core of this work is already in mathlib; what is missing is

• defining locally (path-)connected sets (mathlib only has such spaces)
• a bunch of API for them, including analogoes of pathConnectedSpace_iff_univ
• concluding that open subsets of locally path-connected sets are path-connected.

This branch also shows that locally path-connected implies locally connected.