Locally Simply Connected Initial PR

[GeoffreySangston]

Based on extensive discussion from #1654.

I wanted to get this out so more eyes could look at T856. See #1654 (comment) and following comments. It is my intention to carefully study Frost's post tomorrow when I'm not so tired, but I assumed this will be the right argument anyway.

Other comments I jotted down while working on this:

• Currently omits locally 1-connected as an alias for LC^1 since Borsuk's book defines these as distinct concepts. However, some sources such as Sakai do seem to merge these, so maybe it should be an alias. I decided not to add it as an alias right now because I use locally 1-connected from Borsuk in the body.

• The way the second definition of P229 is written such that it quantifies over variables from the first definition is confusing.

• When we add locally contractible we'll upgrade T848 again.

[felixpernegger]

I just noticed that in theory we would also need to show a euclidean ball is path connected (we also dont mention this currently), but maybe its trivial enough to omit this.

[GeoffreySangston]

That's a good point. I can say instead that R^n is contractible then leave it at that.

[felixpernegger]

Alias "strongly locally simply connected"

[GeoffreySangston]

I'll refer to one of Armentrout's papers since he seems to have written a lot on this property and explicitly used that name.

This one's good because it uses it in the title: Armentrout, BING'S DOGBONE SPACE IS NOT STRONGLY LOCALLY SIMPLY CONNECTED

[felixpernegger]

Yes I agree, I meant add "strongly locally simply connected" as alias and keep this

[felixpernegger]

null-homotopic relatve what? Maybe it doesnt matter (not sure about conjugacy classes in higher homotopy groups)

[felixpernegger]

Doesnt this metaproperty also hold for the other 2 versions?

[felixpernegger]

Also metaproperties :

For all three:

• holds iff it holds for the kolmogorv quotient
• preserved by arbitrary disjoint union
• preserved by finite products (not 100% if it holds for LC^1)
• maybe hereditary wrt clopen?

For locally simply connected and lc1:

• hereditary wrt open subsets

[GeoffreySangston]

Here Moishe Kohan mentions that ANRs need not have P230. One of the ANRs he mentions is the one-point compactification of the Whitehead manifold, $W^+$, described by Melikhov here. Since $W^+ \times \mathbb{R} \approx S^3 \times \mathbb{R}$, it follows that $W^+ \times \mathbb{R}$ is a manifold, hence has all of these properties. Since $W^+$ is a retraction of $W^+ \times \mathbb{R}$, we want to argue that $W^+$ does not satisfy P230 or P231. Since it uses concepts unfamiliar to me, it's hard for me to tell from Melikhov's post if his argument applies without much modificaton to P230 and P231 however. I do know that the Whitehead manifold is famously not simply connected at infinity, but this property doesn't seem to correspond to P230 or P231.

There's also the other example shared by Melikhov here which I haven't tried to understand but which seems relevant. Most relevant actually is Theorem 3 on page 143 of Armentrout's paper which says "THEOREM 3. The space X is not strongly locally simply connected.", and Lemma 10, which says, "LEMMA 10. $X \times S^1$ is homeomorphic to $S^3 \times S^1$."

Summarizing, Armentrout's paper seems to directly show P230 is not preserved by retractions. I'll have to look more for a paper about P231, but I strongly suspect it is not either. Either way, the question seems likely to be highly non-trivial so let's not hold this up for that.

[felixpernegger]

nice. (very) non easy metaproperties are better added in a later PR anyways. :)