Splitting the arc connected property

[prabau]

This is a continuation of what was discussed in #552, as the need for this change is becoming more pressing.
First, discussion on the terminology. After coming to an agreement on this, I'll write the plan for deployment in another comment below and we can discuss further.

Global properties

To summarize, there are two notions of "arc" and of the corresponding "arc connectedness" property in the literature:

• (1) arc = injective path $f:[0,1]\to X$
• (2) arc = (homeomorphic) embedding of $[0,1]$ into $X$

(1) is used in S&S, and in nlab. In pi-base, it's P38 (arc connected).
(2) is used in Willard, Engelking, wikipedia, and many papers and is maybe more common?

It would be worth tracking these two properties separately. After input from @marswill and others, @ccaruvana and I discussed it one more time and came up with the following names:

(1) rename P38 to injectively path connected (and keep "arc connected" as an alias)
(2) new property, taking over the name arc connected

This will make the terminology more in line with what's used in the literature it seems.

Local properties

pi-base currently has "local" versions of some of the connectedness properties:

• connected vs. locally connected
• path connected vs. locally path connected
• arc connected vs. locally arc connected

Corresponding to two new global properties (1) and (2) above, we can have two local versions:

(1) locally injectively path connected (with "locally arc connected" as alias)
(2) locally arc connected

(1) used to be called P43 (locally arc connected). The new name is a mouthful, but it follow the usual naming pattern here. Furthermore, many of the theorems currently involving P43 will use property (2) when being upgraded, so the mouthful name won't be used everywhere.

Note: Mathematically speaking, the notion of arc connectedness, global or local, does not seem as important as path connectedness. Points being joined by a path gives rise to an equivalence relation, with the path components as equivalence classes. But there is no such equivalence relation for arcs. Having both (1) and (2) for the local versions is maybe overkill. But if we don't, people will wonder why not and will suggest to add them probably.

@StevenClontz @pzjp @yhx-12243 @ccaruvana and others interested:
Would appreciate if you can comment on the above, specifically on the list of properties and their names.

[pzjp]

Some alternative names for "injectively path connected":

• strongly path conn.
• weakly arc conn.
• weak-arc conn. (better one, for me; the shortest; also allows using a compact name weak arc for an injective path, emphasizing that they sometimes appear under the name "arc")

But I can imagine it could be somehow confusing compared to other weak/strong properties.
Also not sure if we need loc. inj. path conn.

What about "opposite" property: totally arc disconnected i.e. containing no homeomorphic image of $[0,1]$? The weak-arc analogue seems not appealing, though.

[Moniker1998]

Note: Mathematically speaking, the notion of arc connectedness, global or local, does not seem as important as path connectedness. Points being joined by a path gives rise to an equivalence relation, with the path components as equivalence classes. But there is no such equivalence relation for arcs. Having both (1) and (2) for the local versions is maybe overkill. But if we don't, people will wonder why not and will suggest to add them probably.

Especially given that in Hausdorff spaces the two coincide, which is majority of what one cares about in topology.

[prabau]

@StevenClontz @ccaruvana

Some alternative names for "injectively path connected":
- strongly path conn.
- weakly arc conn.
- weak-arc conn. (better one, for me; the shortest; also allows using a compact name weak arc for an injective path, emphasizing that they sometimes appear under the name "arc")

But I can imagine it could be somehow confusing compared to other weak/strong properties. Also not sure if we need loc. inj. path conn.

What about "opposite" property: totally arc disconnected i.e. containing no homeomorphic image of [ 0 , 1 ] ? The weak-arc analogue seems not appealing, though.

Strongly/weakly/weak-arc is not immediately clear without having to look up the definition every time. One advantage of "injectively path connected" is that, even though it is a little long, it is at least clear.

Also, in general we prefer not to invent new terminology in pi-base. Pi-base is meant to reflect the literature whenever possible. The various weak/strong versions you mention have probably not appeared in the literature. So it would seem to me preferable not to use these non-obvious terms.

As for the local version of (1) = P38 ("injectively path connected" or whatever other name we choose), we need to keep it because it's P43 in pi-base.

Not sure "totally arc disconnected" would be very useful, compared with "totally path disconnected". I would say we can start with the rest and then reevaluate if we want to add "totally arc disconnected" or not.

@StevenClontz @ccaruvana Can you comment on this?

[StevenClontz]

I immediately know what "injectively path connected" is meant to mean; my vote is for that name.

[pzjp]

So we are going to rename (both) current arc connectedness to injectively path connected (for backward compatibility) and introduce the real arc connectedness as a new property?

[prabau]

So we are going to rename (both) current arc connectedness to injectively path connected (for backward compatibility) and introduce the real arc connectedness as a new property?

Yes, exactly.

[prabau]

Now that we have agreed on the terminology, I think breaking things into multiple PRs as follows will make things manageable.

(Phase 1) PR introducing the new properties and renaming the old, together with changing all the theorems involving arc connected. And also adding any obvious new result to relate the properties (e.g., arc connected => injectively path connected, etc). But this PR will not add any deeper results like the generalization discussed in #1245 and #552 involving the US property; that can be done later. Also this PR will not fix any traits. But the property files will contain a WARNING indicating that this is work in progress and pi-base may temporarily not be completely accurate.

(Phase 2) One or more PRs to fix all the traits mentioning the word "arc" or referring to P38/P43. Keeping each of the PRs of manageable size will make it easier to review.

(Phase 3) PRs to add deeper results as desired.

I'll start working on (1). The review of that can take some time, it does not matter. But as soon as (1) is merged into pi-base, (2) should hopefully be written and reviewed quickly so that the disruption to users of pi-base will be kept to a minimum.