Three properties around fundamental groups

[felixpernegger]

See #818.

For my final PR of the year, I want to add the most important properties which are not in pi-base. Typically (?) semilocally simply connected and universal covers are covered in a first course in topology.

I add :

• Semilocally simply connected
• Locally simply connected
• Has a universal cover (= semilocally simply connected + connected + locally path connected)

So far I only added the definitions and no theorems, I want to make sure my definitions are alright (can add theorems in later commit).
And while adding 3 properties at once is admittedly a bit much, they are all very closely related, so I think this is appropriate.

[Moniker1998]

@prabau

[Moniker1998]

We should definitely be careful when adding properties, much more when adding three of them.

[prabau]

Hmm, I think this requires serious discussion (which would maybe have been more appropriate in an "issue"). Discussion about possible alternative terminologies, related theorems, etc, etc.

Adding all these different properties at the same time also seems not appropriate. Can we do it one property at a time instead? Starting with one, with some basic accompanying theorems and in other PRs some distinguishing example spaces as necessary.

@felixpernegger FYI, in the past we used to have a bunch of property definitions that someone had added over the years. they did not have connections with any other properties. We decided to delete them all, and then only accept new properties if someone took the work to provide related theorems and related sample spaces. That's really the preferred way to go.

[prabau]

If you want to put this as draft and discuss this in an issue, that would be fine too.

Added later: Just saw that @Moniker1998 already marked this as draft.

[felixpernegger]

Hmm, I think this requires serious discussion (which would maybe have been more appropriate in an "issue"). Discussion about possible alternative terminologies, related theorems, etc, etc.

Adding all these different properties at the same time also seems not appropriate. Can we do it one property at a time instead? Starting with one, with some basic accompanying theorems and in other PRs some distinguishing example spaces as necessary.

@felixpernegger FYI, in the past we used to have a bunch of property definitions that someone had added over the years. they did not have connections with any other properties. We decided to delete them all, and then only accept new properties if someone took the work to provide related theorems and related sample spaces. That's really the preferred way to go.

Well I can write more on this tomorrow, but the point really is that especiall semilocally simply connected is a basic property in algebraic topology we need to calculate fundamental groups (typically taught in a first course). It is quite odd for a topological database not to contain this in my opinion.There are a few connections as well (i.e. with locally path connected and simply connected)

[felixpernegger]

A classical counterexample (but embeddable in R^2) for non semilocally simply connected is the Haiwaiian earrings for example

[Moniker1998]

It is quite odd for a topological database not to contain this in my opinion.

I don't think its odd since this database focuses on properties important to general topology, more so than algebraic topology.

[prabau]

I think it's perfectly fine to add these properties, just that it needs to be discussed and done one at a time, in a series of PR adding theorems and examples for each, before moving on to the next. That would be the preferred approach.

As to why it's not in pi-base yet, it's because of what @Moniker1998 said. Pi-base started as an online version of the book Counterexamples in topology, which was focused on general topology and did not contain anything related to algebraic topology. Other properties were added later, again mainly for general topology, because that's what the people involved in pi-base were interested in. It's a historical reason.