Semilocally Contractible Initial PR

[GeoffreySangston]

Suggested in the comment #1672 (comment). There are some references to it in this comment #1672 (comment). We planned to modify weakly locally contractible upon adding this here #1672 (comment).

For this PR:

• I changed the reference from Borges to Sakai because Borges's definition is actually slightly different (though equivalent), and this subtlety seems distracting.

• This MSE post shows that Semilocally contractible + Has a group topology implies LC. This theorem could be included now or in a future PR.

• Note that, unlike SLSC, this property does not satisfy the meta-property "X satisfies this property iff each of its path components does." I.e. a totally path disconnected + semilocally contractible space is discrete, so $\mathbb{Q}$ is not semilocally contractible. SLSC (which is standard terminology) does not include semilocally 0-connected (= has open path components); maybe it's better to read semilocally simply connected as semilocally 1-connected to remember this. On the other hand, semilocally contractible does imply semilocally 0-connected.

[felixpernegger]

• Note that, unlike SLSC, this property does not satisfy the meta-property "X satisfies this property iff each of its path components does." I.e. a totally path disconnected + semilocally contractible space is discrete, so

      Q
    
   is not semilocally contractible. SLSC (which is standard terminology) does not include semilocally 0-connected (= has open path components); maybe it's better to read semilocally simply connected as semilocally 1-connected to remember this. On the other hand, semilocally contractible does imply semilocally 0-connected.
  

Does Semilocally Contractible + Has Open Path components => Semilocally simply connecte?

[GeoffreySangston]

Does Semilocally Contractible + Has Open Path components => Semilocally simply connecte?

Semilocally contractible implies both Semilocally simply connected (=semi-locally 1-connected)and Has Open Path components (=semi-locally 0-connected). I.e., the first is because an inclusion map being null-homotopic implies
the pushforward on fundamental groups is trivial: For $\sigma$ representing an element of $\pi_1(U)$ and $\iota : U \hookrightarrow X$,
$\iota_\ast \sigma := \iota \circ \sigma : S^1 \to X$ is null-homotopic via $H(s, t) = F(\sigma(s), t)$, where $F : U \times [0, 1] \to X$ is the given null-homotopy of the inclusion map $\iota$.

So we could change the current file to any of:

• "Since $\iota : U \hookrightarrow X$ is null-homotopic, the pushforward $\iota_\ast : \pi_1(U, x) \hookrightarrow \pi_1(X, x)$ is trivial for every $x \in X$."
• More fully spelling this out
• Keep it is as "Immediate from the definitions"

I prefer the last one because the definitions are set up to make this an "unwrapping the definitions" theorem.

Semilocally simply connected does not imply Has Open Path components (semi-locally 0-connected), whereas
the LOCALLY simply connected (=LC^1 + LC^0 or =locally 1-connected + locally 0-connected) properties do imply locally 0-connected (=locally path connected).

[prabau]

will try to get to it this weekend

[prabau]

For the definition, if $U$ is a nbhd of $x$ such that the inclusion of $U$ into $X$ is null-homotopic, the same is true of any nbhd $V\subseteq U$. (we get a nbhd base of those in a way). I am wondering if it could be useful to mention that, as sometimes this is used in proofs?

Then also there would be no real need to mention the bit about open nbhds. What was your thinking for mentioning the open nbhds here?

I am thinking it could be useful to make a similar remark for P229 (SLSC). Thoughts?

[prabau]

Regarding the proposed theorem in the second bullet in #1745 (comment), I think it can be done later in a separate PR. That way, we already have P239 out there and we can experiment with it.

[GeoffreySangston]

For the definition, if U is a nbhd of x such that the inclusion of U into X is null-homotopic, the same is true of any nbhd V ⊆ U . (we get a nbhd base of those in a way). I am wondering if it could be useful to mention that, as sometimes this is used in proofs?

Then also there would be no real need to mention the bit about open nbhds. What was your thinking for mentioning the open nbhds here?
I am thinking it could be useful to make a similar remark for P229 (SLSC). Thoughts?

@prabau I think I was probably looking at the $LC$ file while writing this, which includes "(equivalently, an open neighborhood)". Incidentally, it's interesting that $LC$ is the localization of semilocally contractible (i.e., $LC$ = Locally semilocally contractible...), so I'm wondering if the same aesthetic to include it or not include it should apply in both cases? I think for $LC$ we were probably partially motivated by the way these are presented in locally path connected P42 (where I think the equivalence is less trivial?).

It does seem a bit trivial though. I'm not sure it's worth mentioning. Maybe if we saw it used in a trait I'd be more supportive of including it.

[prabau]

will read #1745 (comment) tomorrow