Property Suggestion: Semi-Locally Simply Connected

Edit: The suggestion of #818 is a much more comprehensive version of this. But I also understand that #818 had problems in its day because of needing experts to verify the algebraic topology stuff. Still, maybe it can happen?

Property Suggestion

A space is said to be semi-locally simply connected (also spelt semilocally) provided that every point x has a neighborhood U so that the inclusion map U -> X induces the zero map pi1(U, x) -> pi1(X, x).

Rationale

This property appears in Hatcher's Algebraic Topology.

It is crucial for the classification of covering spaces, as it is a necessary condition for having a simply connected covering space. It is also part of a standard sufficient condition: path-connected + locally path-connected + semi-locally simply connected implies that a simply connected covering space exists.

While we don't have the property of having a simply connected cover, adding SLSC as a property still provides interesting counterexamples: the Hawaiian earring is not SLSC and so has no simply connected covering space. If someone wanted to add "has a simply connected covering space" as a property, you could get further counterexamples: the Warsaw circle is path-connected and SLSC but not locally path-connected, but it still has a simply connected covering space (itself). Has a simply connected cover implies path connected and SLSC, but I'm not sure about the other direction.

Relationship to other properties

These spaces, and probably others, have a basis of contractible sets, which implies SLSC automatically.
Locally Euclidean -> SLSC
Alexandrov -> SLSC

These spaces may not have a basis of contractible sets but are SLSC.
Simply Connected -> SLSC

These three theorems would cover about 80 spaces.

Our current definition would also provide:
Totally path disconnected -> SLSC
which covers another 90 spaces.

In any case, I think the classification of covering spaces is a notable enough theorem that this deserves a property anyway. The most famous space that is not SLSC is the Hawaiian earring, which we already have.

Meta-Properties that I could find

This property is not hereditary with respect to closed sets. (The Hawaiian earring is compact and embeddable in R^2.)
X satisfies this property iff its Kolmogorov quotient Kol(X) does.
This property is preserved by arbitrary disjoint unions.
This property is preserved by finite products.
If each point has a neighborhood with the property, X also has the property.

Also, it seems like Explore links are much better than theorem links. If you change a theorem (maybe you want to generalize it), you're toast, but with an Explore link you always get what you ask for. I know theorem links get used, but I'm inclined to put Explore links here because if locally contractible or weakly contractible does get added, then the markdown would require adjustment if we use theorem links.

What do you think?

In this case it won't matter because an Explore link provides a slightly cleaner proof of your theorem, but in general.

Also, I think there is some limit to how much explore links should be relied on. For example, I could say that a path-connected GO space is a LO…

#1576
See the mathoverflow post in particular, this seems to be a delicate issue

#1576 See the mathoverflow post in particular, this seems to be a delicate issue

Unlike locally simply connected, semi-locally simply connected is pretty uncontroversial. The connection with universal covers appears to be the main critique in the mathoverflow post.

@mathmaster13

@mathmaster13 Apart from Hatcher, are there other good sources for this property?

Also, are there variants of the definition in the literature?

See #1576 instead of #818.

@mathmaster13 Apart from Hatcher, are there other good sources for this property?

Munkres 2nd edition page 494. Also Wikipedia https://en.wikipedia.org/wiki/Semi-locally_simply_connected
And most likely every source containing material about covering spaces.

Also, are there variants of the definition in the literature?

I've seen it defined multiple times and always the same way, so probably not.

Ok. Would have to see the best way to formulate it for pi-base, but I agree it's a good property to add.

The one truly ambiguous point is whether or not the empty set is SLSC or not.

A related oddity is whether the empty set is simply connected or not. Wikipedia uses the definition "any two paths between the same endpoints are path-homotopic". Hatcher uses the "trivial fundamental group" definition. Both sources then proceed to show the equivalence of the two definitions, making no mention of the possibility that the space is empty (which is when the two definitions disagree). As for what we do here, we state our property P200 Simply Connected as "trivial fundamental group" (thus the empty set should not be simply connected), but then we have a theorem Indiscrete -> Simply Connected, which is proven using Wikipedia's definition. If you ask pi base if the empty set is simply connected, it'll say yes. So we're inconsistent too.

But overall, SLSC is an important property with fun counterexamples to be had. If we wanted to add local contractibility or local simple connectedness (those are trickier to define), it would be good to do it before adding SLSC, since those two properties imply SLSC. But that would require justification from the literature.

I edited my original post to include relationships to other properties.

One does not need nonemptyness to define the fundamental group, see this, up to debate what "trivial" means then. But probably requiring nonemptyness is actually correct yeah.

I can't understand the Lean, but I do see:

The fundamental group is the automorphism group (vertex group) of the basepoint in the fundamental groupoid

What basepoint are they talking about?
And reading the first paragraph of that page they say "Given a topological space X and a basepoint x, the fundamental group is the automorphism group of x i.e. the group with elements being loops based at x (quotiented by homotopy equivalence)."
But maybe the Lean has another definition that I can't read.

It implicitly assumes nonempty in the docstring. Fundamental group is empty iff space is empty.
However, for simply connected they do in fact require nonempty: https://leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.html#IsSimplyConnected.nonempty
so we should probaly do the same.

You are right that the various characterizations of "simply connected" (P200) are not equivalent if $X$ is the empty space.

(Following the terminology in Hatcher) If $X$ is empty, one cannot choose a base point $x_0\in X$ and the notion of $\pi_1(X,x_0)$ does not make sense, even as a set (of homotopy classes of loops at the basepoint $x_0$). So $\pi_1(X)$ has no meaning either.

On the other hand, if $X$ is empty, there are no paths in $X$ and no loops in $X$ (since there are no functions from a nonempty set to an empty set). So the characterizations in the bullet list are all vacuously satisfied.

We could allow the empty set to be simply connected, or not. Would need to change either theorems or the definition. Whatever makes things easier overall would be the way to go. There is no right or wrong answer here, as it's a degenerate case.

Why does Lean require nonempty for simply connected?

Fundamental group is empty iff space is empty.

Groups are never empty. So how can one say that the "fundamental group" is empty?
I would say there is no fundamental group for an empty space.

You are right. The fundamental group is defined as a set but has no group structure...

Why does Lean require nonempty for simply connected?

I dont know exactly but probably to dont have to deal with exactly the issue here; not having to care whether basepoints exist or not.

In any case, the reason I think some version of locally simply connected (or maybe just locally contractible) should be added, is that it seems for some implication we write (properties) => SLSC although (some version of, maybe additionally with connected condition), (properties) => locally simply connected holds.

Munkres mentions it at page 495

Okay I see now. He calls it 'locally simple connected': "which would require that within each neighborhood of b there should exist a neighborhood U of b that is itself simply connected"
(Worth remembering now that Munkres imposes the convention that neighborhoods are open.)

It seems also worth mentioning that Munkres seems to give this definition off the cuff. It seems like the correct definition should be from a source which treats it formally, like Borsuk's.

@felixpernegger

@felixpernegger If we were to add one of the properties from Maurizio's list, would you prefer P_1 or P_10? He seems to suggest most authors prefer P_1, though P_10 seems to be equivalent to Borsuk's (I did not verify carefully), which it seems many also prefer.

Maybe you or someone else can start a discussion thread for this? (I would do it but I feel it should be started by someone more active than me.)

Also, what would pi-base contributors think about having two separate properties which have distinct names in the main definition title, but which share names in the 'Also known as' synonyms text? That could partially solve this. We choose a distinct name for the main definition, and reserve "Locally Simply Connected" for the 'Also known as text'. It doesn't solve the problem of deciding which definition to actually add first though.

I don't see why allowing us to make a stronger statement alone justifies a property's addition. If it has merit to be added on its own grounds, then that is another story. SLSC is a condition in a well known theorem, at least.

Am I mistaken in thinking that P_8 from Maurizio Barbato's list below is the same as pi-base's second definition of SLSC P229? He does write "P_7 and P_8 are usually taken as the definition of semilocally simply connected space (this notion seems to be by far the most relevant because of its applications in the theory of covering spaces)" so this is just to confirm with others.

https://mathoverflow.net/questions/487326/definition-of-locally-simply-connected-space

It's good that P_10 does imply P_8, according to this list.

I wonder if anybody thinks any of the equivalences of P_8 with P_5, P_6, or P_7 are worth mentioning on the page for P229?

Am I mistaken in thinking that

You are correct. P8 is just SLSC.

Important discussion. I agree we should start discussing this in a separate thread, and keep this one for SLSC if possible.

We'd like to eventually add one or more versions of "locally simply connected" and one or more versions of "locally contractible". And if I understand, you think we should tackle "locally simply connected" first. Is that right?

I don't see why allowing us to make a stronger statement alone justifies a property's addition. If it has merit to be added on its own grounds, then that is another story. SLSC is a condition in a well known theorem, at least.

locally simply connected is more well-known than many other properties we have
if we add locally contractible (which appears more well-known), it would be odd to leave this out

Important discussion. I agree we should start discussing this in a separate thread, and keep this one for SLSC if possible.

We'd like to eventually add one or more versions of "locally simply connected" and one or more versions of "locally contractible". And if I understand, you think we should tackle "locally simply connected" first. Is that right?

I think its the next logical step, but ill make a new issue, this here is getting bloated yeah

Great. Also note, one can "Reference in a new issue" from an existing comment. If it helps for editing.

I'd perhaps make a new issue for SLSC too—we're done with the trait and now just have a hit list of spaces, maybe theorems to add. So it's looking more like a project of adding algebraic traits to spaces than discussion about the SLSC property. I can make that issue if you think it makes sense.

Is this the thing GitHub discussions are good for or should it be an issue?

I'd perhaps make a new issue for SLSC too—we're done with the trait and now just have a hit list of spaces, maybe theorems to add. So it's looking more like a project of adding algebraic traits to spaces than discussion about the SLSC property. I can make that issue if you think it makes sense.

Is this the thing GitHub discussions are good for or should it be an issue?

Regarding SLSC, I don't think we need a new issue at the moment. For traits we can just write PRs directly. And if there is an additional theorem that would be useful, write a PR directly if it's not controversial, or open a new issue if a prior discussion would be beneficial.

For other algebraic topology properties to discuss, let's do it in separate issues as needed, not this one.

And as for Github discussions, we don't use them anymore. So "issues" is what we use for discussions.

starting to copy some of the comments here over to #1654

Done for now. Feel free to add more if needed.

I'm going to close this tomorrow.

Navigation Menu

Repository navigation

Property Suggestion: Semi-Locally Simply Connected #1634