Locally contractible initial PR

[GeoffreySangston]

Based on discussion from #1672 and the older thread #1150. Also see #1654 (on locally simply connected). There is a lot of work remaining to be added from those threads in future PRs; see for instance #1672 (comment) and #1672 (comment). Also, adding this was a blocking issue for the suggestion in #1671.

For this PR:

(1) I included two near-identical definitions of LC (maybe also see LC^1), but the second (or first) could be considered redundant. The first is slicker and nicely fits on the page with the big list of properties, but the second emphasizes that this property is pointwise defined.

(2) I have no references for "weakly locally contractible". Surely there must be some published theorem using this or its negation as a hypothesis or conclusion, but I don't know of any. I don't think it's great that the only reference on "weakly locally contractible" is to a source defining it with a different definition (this is done because of a suggestion in this comment #1672 (comment)).

(3) I include a reference to Fadell's paper for "weakly contractible", since I think that is the origin of his variant of the term, but since I also connect it to "semi-locally contractible", I also include a reference (Borges) to a paper which has both terms. Possibly this could be simplified or some other reference(s) could be used (maybe from my comment #1672 (comment)).

(4) I have no references for P223 ("locally contractible"), although that property does have some use in the literature. The issue was that I did not find any ideal source. (Edit: I remembered this is Hatcher's definition, though it's unfortunately buried in a proposition statement and the text seems slightly ambiguous since it could look like 'has an open basis of contractible sets' is stronger than whatever 'locally contractible' is supposed to mean.)

(5) This PR lacks counterexamples. Some of the converses have relatively easy counterexamples, but some are highly non-trivial. It felt burdensome to include counterexamples in this PR.

(6) There's a good chance I'm missing several of the basic theorems that could be added now.

[felixpernegger]

Nice, will take a look later

[prabau]

P223: mentioning the pi-base conventions does not seem helpful here.
Also, I can see Hatcher uses "locally contractible", but I can't see the definition of it anywhere. Was it another one of those informal things? I am wondering if there are maybe better refs for this.

[GeoffreySangston]

P223: mentioning the pi-base conventions does not seem helpful here. Also, I can see Hatcher uses "locally contractible", but I can't see the definition of it anywhere. Was it another one of those informal things? I am wondering if there are maybe better refs for this.

I felt inclined to mention it just because people online seemed annoyed about the wrong definition being used elsewhere (where the preference was for LC). It is implicit though since pi-base is posting pi-base's definition, so we can remove it.

Hatcher never defines it except vaguely in his proposition. Like I said before, I wasn't seeing any ideal source.

[prabau]

I felt inclined to mention it just because people online seemed annoyed about the wrong definition being used elsewhere (where the preference was for LC). It is implicit though since pi-base is posting pi-base's definition, so we can remove it.

I think we don't need to mention anything special for P223 in that respect. On the other hand, I definitely would mention it for P224, and even expand this further with a comparison with P223. Let me check the refs for P224 and then think of something for that.

[prabau]

Hatcher's (informal) def of "locally contractible" is on which page?

[GeoffreySangston]

Hatcher's (informal) def of "locally contractible" is on which page?

It's part of the statement of Proposition A.4 on page 522 (in the Appendix, after almost all the uses of it). The situation is pretty bad.

He says what it "usually means" to have a property 'locally' on page 61 though.

[GeoffreySangston]

I thought it was worth including Hatcher because it's a canonical text using this property in multiple places, even though the definition is not clearly presented.

[prabau]

P223: what would you think of using the following two paragraphs at the end explaining the terminology:
(Note: I am saying "very close" to the pi-base convention, because "locally P" in pi-base means the same with arbitrary nbhds, not necessarily open.) (Not sure if the part in parentheses below is really needed, but could be helpful. What do you think?)

"Locally contractible" is used in {{zb:1044.55001}}, where it is defined informally with the meaning above as part of the statement of Proposition A.4 on page 522. (As explained on page 61, that book follows the convention of a space being "locally P" for a property P to mean that every point has arbitrarily small open neighborhoods with the property; this is very close to the general convention used in pi-base.)

Other than that, the phrasing "locally contractible" does not seem to appear much in the literature.

[GeoffreySangston]

I think that paragraph is fine. I'm a bit confused though. Isn't pi-base saying 'locally P' means 'has an open basis of P sets' when it says

Use "locally P" when there's a basis of P neighborhoods

https://github.com/pi-base/data/wiki/Conventions-and-Style

Also, we could link to this when we write "conventions".

[prabau]

Just checked the wiki. There is indeed some sloppiness there. Let me fix it there, as nbhds in pi-base are not assumed to be open.

[GeoffreySangston]

@prabau I made a minor change to it which I hope you agree with.

I'll edit the PR now.

[prabau]

P223: You may be right that the second paragraph was not really needed.

As for linking to the pi-base conventions, specifically to the Local Properties section, we could do it:

the [general convention used in pi-base](https://github.com/pi-base/data/wiki/Conventions-and-Style#Local-Properties).

[GeoffreySangston]

P223: You may be right that the second paragraph was not really needed.

To be honest, I thought the last sentence was to me and that somehow the two paragraphs got merged into one.
Regardless, I'm not sure it should be added. I'd prefer to make it more objective sounding, but then it would make an objective claim which is not easily substantiated without more text than we'd want to devote. Plus it does appear in the literature in many dozen articles (i.e. 35 in this search), just not in anything specific to this or related properties, and in few canonical texts. I think we shouldn't mention this (though I did emphasize in LC that it's standard in ANRs, which is kind of an opinion, but could be well-justified; even LC is in competition with 2' from the old thread however.)

We do already have an alias of 'locally contractible' for LC, which does something to emphasize that 'locally contractible' might refer to LC. Maybe we should link to LC from P223?

[prabau]

I think what we have now for P223 is fine. But I haven't gotten to LC yet.

[prabau]

P224: just to confirm, we don't have the "semilocally contractible" property in pi-base at the moment, right? And we talked about adding it later at some point?

[GeoffreySangston]

P224: just to confirm, we don't have the "semilocally contractible" property in pi-base at the moment, right? And we talked about adding it later at some point?

Right. We have not added this yet, but we thought it was a good idea. Here is your first comment suggesting it #1672 (comment).

[prabau]

So later on we'll be able to replace "semilocally contractible" with a link to the new property.