Locally orderable and GO spaces are SLSC

[mathmaster13]

Thanks @prabau for the theorems. (This won't be the last SLSC PR.)

This PR is ready as soon as somebody (probably me) finds a reference for "a connected subspace of a LOTS is a LOTS", and puts it either as a metaproperty for LOTS ("This property is hereditary with respect to connected sets") with a reference, or as part of the proof of T851. Or we just decide that it doesn't need a reference, which I disagree with.

In any case, whoever does that first can un-draft this PR.

I used an explore link to show "path connected LOTS is simply connected" or something like that, because if we add other algebraic properties (locally contractible or weakly contractible) then the theorem would change and so the text in that file would have to be changed too.

Here's a proof of connected implies order convex, and then we'd need one for order convex implies LOTS (I'd spell that out, even if it's easy to see, because who thinks about that outside of pi base? Unless somebody does.). I don't have access to Munkres right now.

#1634 (comment)

[prabau]

Great. I'll look at this later today.

[prabau]

Munkres Theorem 16.4 on p. 91

[mathmaster13]

Munkres Theorem 16.4 on p. 91

thanks, will do
do we want to have it as a metaproperty in the LOTS file? (hereditary WRT connected sets)

[prabau]

I wanted to give more details for T850.
But look at the list of path connected LOTS and why they are simply connected:
https://topology.pi-base.org/spaces?q=LOTS%2BPath+connected%2BSimply+connected
Compare main branch and new branch.

In the new branch, the reason for S25 (reals), S158 ([0,1]), ... are simply connected becomes a list of implications using T850 itself. That circular dependency is bad.

Also, I was going to suggest to also remove the "redundant traits" that follow from the new theorems. But unfortunately that would introduce logical circular dependencies in some cases.

As an example: S38 (long ray) is simply connected, with an explicit justification. And it is path connected (derived from simply connected). So we cannot remove simply connected as a trait. And no matter what, we need the explicit justification in this case for establishing T850.

I'll make a suggestion for a slightly different justification below.

---

Side remark: That illustrates also why we cannot blindly uses "Explore" links in general.

[mathmaster13]

Munkres Theorem 16.4 on p. 91

This one? {{zb:0951.54001}}

I don't know what edition you have.

[prabau]

You can edit T851 and I'll take a look tomorrow.

Note: if we had a property like "locally suborderable" = "locally GO-space", we could subsume T851 and T852 into a single result. But nobody seems to be using that, so it does not seem worth introducing. For now, we have a few other pairs of results like that. No biggie.

[mathmaster13]

You can edit T851 and I'll take a look tomorrow.

Note: if we had a property like "locally suborderable" = "locally GO-space", we could subsume T851 and T852 into a single result. But nobody seems to be using that, so it does not seem worth introducing. For now, we have a few other pairs of results like that. No biggie.

I put the T851 justification as hereditariness properties of P133. Thus T851 doesn't need to be edited.

[mathmaster13]

I used an explore link for T851 because I know that theorem will be edited (a path connected LOTS is locally contractible and thus locally simply connected for basically any definition of the term). But I don't think I like that. I suppose we can just modify T851 when T850 inevitably needs to change?

[prabau]

It would be good if you could also check if any of the asserted traits for SLSC can be removed as redundant.

[mathmaster13]

It would be good if you could also check if any of the asserted traits for SLSC can be removed as redundant.

S39 Closed Long Ray: Uh?? deducible because it's a LOTS -> locally orderable -> SLSC, which I suppose is fine because the Explore link in the theorem "locally orderable -> SLSC" shows that any path connected LOTS is simply connected, using T850, which is self-justifying. (We may want to change the explore link to a regular theorem link and just edit it when we add new properties.) Let me know if you'd like this one kept in.

S40: Can go. Locally orderable and not a path connected LOTS.

S41: LOTS -> locally orderable. Can go.

S56: Locally orderable.

S206: Locally orderable.

[felixpernegger]

It would be good if you could also check if any of the asserted traits for SLSC can be removed as redundant.

S39 Closed Long Ray: Uh?? deducible because it's a LOTS -> locally orderable -> SLSC, which I suppose is fine because the Explore link in the theorem "locally orderable -> SLSC" shows that any path connected LOTS is simply connected, using T850, which is self-justifying. (We may want to change the explore link to a regular theorem link and just edit it when we add new properties.) Let me know if you'd like this one kept in.

S40: Can go. Locally orderable and not a path connected LOTS.

S41: LOTS -> locally orderable. Can go.

S56: Locally orderable.

S206: Locally orderable.

You dont have to check this manually so carefully, just go advanced tab on pibase, change it to our branch, and then click on manually added SLSC traits (click on the proofs). If they are redundant there is a yellow box on top saying so

[felixpernegger]

You can almost always remove redundant traits without thinking too much about it.

[mathmaster13]

You dont have to check this manually so carefully, just go advanced tab on pibase, change it to our branch, and then click on manually added SLSC traits (click on the proofs). If they are redundant there is a yellow box on top saying so

This is exactly what I did, haha
I will make less fanfare of it next time

[prabau]

Regarding the metaproperties you added for LOTS (P133):

The fact that a connected subspace $A\subseteq X$ is also LOTS can be shown in a more direct way: $A$ is a GO-space, and connected GO-spaces are LOTS (T131). I don't have a problem if you want to keep it as a metaproperty, but it's simple enough that we don't need an explicit justification.

About the order-convex one: that does not really fit the other meta-properties, which are strictly of a topological nature. This is given in terms of some extraneous characterization (note that a LOTS does not determine a total order - i.e., there could be multiple total orders compatible with the topology, so again it's not intrinsic to the topology). Furthermore, the metaproperties were not meant to collect all possibly useful facts about properties. So I would'd like to remove that particular metaprop. If you want to have a wider discussion on what is or is not fitting for metaproperties, we can open an issue and discuss there.

[mathmaster13]

Regarding the metaproperties you added for LOTS (P133):

No worries. I know that we don't actually have "hereditary WRT connected sets" as a metaproperty right now. So I am leaning towards removing it for that reason and removed it in this current commit; it seems a little out of place (unless you suggest to keep it). I've never worked with GO-spaces and so would never find "connected GO-space is a LOTS" on my own (which, by the way, is literally saying that a connected subspace of a LOTS is a LOTS). But if someone's clever and cares enough I suppose they can look it up. (though I had a hard time finding it)

[prabau]

That's fine. We don't really need to have it now.

Can you also remove the added reference, not needed anymore for P133.

[prabau]

@mathmaster13 leaving it to you to merge, so you can practice wiping out the "Extended description" before clicking on "Confirm squash and merge".