Adds 'simply connected'

[GeoffreySangston]

Just wanted to go ahead and add this asap since Joe131 requested it. Discussed at #818 and #851.

Foreseeable issues:

1. Since path-connected is in the definition of simply connected ('simply connected => path connected' is added as T587), and 'contractible => simply connected' is added as T588, now 'contractible => path connected' (T583) might be considered redundant.

2. There's now both T584 (Indiscrete + ~Empty => Contractible) and T586 (Indiscrete => Simply connected). T586 is how pi-base knows the empty space is simply connected (which does follow from all of the equivalent definitions). This isn't really an issue I think, but maybe it looks odd.

3. There's quite a few other spaces to add, but I didn't want to add too much for the first PR.

I'll probably take some time to review the nlab proof of 'long line is not contractible'. I didn't immediately find any other complete proof. I'll look again later.

[prabau]

FYI, a full proof that the long line is not contractible: https://math.stackexchange.com/questions/1282097

[prabau]

FYI, when we quote some mathse post in the text, we have been using the notation {{mathse:4044399}} in combination with adding the post to the refs: section. If you want to deviate from that, I don't necessarily object, but we should discuss with @StevenClontz .

[prabau]

Would it be possible to renumber the theorems so they don't conflict with the pending #852 (meta-Lindelof property)?

[GeoffreySangston]

FYI, when we quote some mathse post in the text, we have been using the notation {{mathse:4044399}} in combination with adding the post to the refs: section. If you want to deviate from that, I don't necessarily object, but we should discuss with @StevenClontz .

Sorry about that! Just an oversight on my part.

[prabau]

Even though the PR is still in draft state, I thought I'd start giving some comments anyway.

"1-simply connected" as an alias: The usual terminology is "n-connected" (in this case, 1-connected). As one can check in zbmath for example, practically nobody uses "n-simply connected" or "1-simply connected".

As https://ncatlab.org/nlab/show/n-connected+space indicates:

The traditional terminology is ‘n-connected’, but this violates the rule that ‘1-foo’ should mean the same as ‘foo’. This can be fixed by saying ‘n-simply connected’ instead, which also has the advantage of stressing that we are extending the change from connected to simply connected spaces.

In other words, it's a pure invention of nlab, which is perfectly fine for their purpose of exploring things with the utmost generality and inventing terminology to fit their approach, but it does not reflect common usage, and does not need to be in pi-base.

[prabau]

P200:

I am not sure I like the phrasing "has trivial homotopy groups up to degree 1". Is that another nlab thing? In any case, it seems a little obscure, as $\pi_0(X)$ is not even a group. And one would have to look up the reference to see exactly what that means. How about something more direct:

$X$ is path-connected and has trivial fundamental group $\pi_1(X)$. Defined on page 28 of {{zb:1044.55001}}.

Also called $1$-connected. See n-connected space in nLab.

(rest of the stuff here)

(with pi-base link for "path-connected" and maybe wikipedia link for "fundamental group" ?)

[prabau]

As you noticed, T583 is now redundant, a consequence of the T588 and T590. As we want to avoid redundant theorems, what we usually do in this case is replace the previous T583 with one of the new results, the contents of T588 for example.

The proof for T588 would have to change slightly, I think. First refer to mathse:715720 from T583 to say it's path connected (no proof needed, really). Then the rest ... Please double check me on this: Spaces that are homotopically equivalent have isomorphic homotopy groups. So no need to do much at all. (maybe there is an easy reference to that fact somewhere)

[GeoffreySangston]

(with pi-base link for "path-connected" and maybe wikipedia link for "fundamental group" ?)

I didn't know how to get fundamental group to appear using the {{wikipedia: Fundamental_group}} method, so I just used [fundamental group](https://en.wikipedia.org/wiki/Fundamental_group). (A deeper issue is I haven't figured out how to use the preview window. Is the standard practice to make commits and then use the page https://topology.pi-base.org/dev to switch the active branch? I assume not. Otherwise I fear I'll be frequently bothering you all with broken commits.

I'll switch this from a draft commit tomorrow if I find time to review the two different proofs that the long line is not contractible. (That's not really necessary I know. I just like the idea of learning as I make these commits. I can go ahead and switch it to a regular pull request if that's annoying.)

[prabau]

(with pi-base link for "path-connected" and maybe wikipedia link for "fundamental group" ?)

I didn't know how to get fundamental group to appear using the {{wikipedia: Fundamental_group}} method, so I just used fundamental group. (A deeper issue is I haven't figured out how to use the preview window. Is the standard practice to make commits and then use the page https://topology.pi-base.org/dev to switch the active branch? I assume not. Otherwise I fear I'll be frequently bothering you all with broken commits.

There are two levels of preview. The first one is while editing in vscode (github.dev). While editing a file, at the upper right of the editor pane there are a bunch of icons. One of them is for opening a preview window. Pretty handy while editing.

The other level of preview is to see the full resulting web page after a commit. After each commit, a build is triggered. If the build is successful, the commit in the list of commits gets a green checkmark. This can also be checked in the Actions pane at the top of the page (https://github.com/pi-base/data/actions). Anyway, after a commit is built succesfully, one can check the result in the pi-base web site by going to the Advanced page (https://topology.pi-base.org/dev) and entering the specific branch name. (Sometimes it does not work. But first clicking Reset, then trying the new branch name usually works.)

Regarding the fundamental group link, you did the right thing. Maybe we don't even need that one in the refs: list, as it is just an auxiliary link. But either way, it's fine.

[prabau]

I'll switch this from a draft commit tomorrow if I find time to review the two different proofs that the long line is not contractible. (That's not really necessary I know. I just like the idea of learning as I make these commits. I can go ahead and switch it to a regular pull request if that's annoying.)

Nothing annoying here. Feel free to switch to Open when you prefer. I have also found that editing pi-base is great way to learn. It forces one to dig deeper into things.

[GeoffreySangston]

Does pi-base have a style preference for line lengths? I've been representing each idea/idea chunk/proof/definition with its own line, and I'm just using the online editor so it doesn't bother me, but I know terminal users may prefer to restrict to certain character limits (traditionally 80 characters max).

Is there a unified style guide sitting around that I've missed?

[GeoffreySangston]

The fact 'every map to a contractible space is homotopic to a constant map' is one of the equivalent characterizations of 'contractible' on Wikipedia, but does not appear on pi-base's Contractible

[prabau]

The fact 'every map to a contractible space is homotopic to a constant map' is one of the equivalent characterizations of 'contractible' on Wikipedia, but does not appear on pi-base's Contractible

I think you are right. We should add that characterization (no proof needed, it's pretty obvious). That will allow to use a shorter argument for T583. And also change to a shorter argument for S38|P200.

BTW, should be something like "For every nonempty space $Y$, every map $X\to Y$ is ..." (I added the missing "nonempty" to wikipedia).

[StevenClontz]

Does pi-base have a style preference for line lengths? I've been representing each idea/idea chunk/proof/definition with its own line, and I'm just using the online editor so it doesn't bother me, but I know terminal users may prefer to restrict to certain character limits (traditionally 80 characters max).

Is there a unified style guide sitting around that I've missed?

https://github.com/pi-base/data/wiki/Conventions-and-Style and the wiki in general is what we have. I'm not too picky with styling Markdown source; if we want to start doing so, I'd also want to rig up a VS Code plugin and GitHub Action to enforce this linting.

[GeoffreySangston]

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

Oh I didn't even see there was a Wiki! Thank you.

[GeoffreySangston]

There's probably some things to fix here, but I don't want to hold this up forever either.

[prabau]

P200: remove "Defined on page 28 of ..." from the last paragraph, as it's now in the first paragraph.

T583: Some of the double braces should be single braces: {P37}, etc. For some reason, I can't do the preview on that theorem. Maybe that's why.

S38|P199: (long ray is not contractible) The mathse proof seems very organized and clear to me. The nlab is hard to read, at the least because of its formatting. Not sure I even want to try to parse all that. Is there anything that the nlab adds to the understanding of this? If not, how about removing the nlab reference?

Same for the other two spaces. Note that for the other two spaces, we could just say something like
Similar to the proof that {S38|P199}.
which will expand to "Similar to the proof that Long ray is not Contractible" with an appropriate link.

S38|P200: (long ray is simply connected) Would there be a detailed proof somewhere that we can refer to? mathse or book?
https://math.stackexchange.com/questions/1352181 for inspiration? Need to check for other posts.

I need to check this proof further.

In the mean time, it seems we should mention also that the space is path connected. That actually follows from the fact that it is arc connected: https://topology.pi-base.org/spaces/S000038/properties/P000038. But that in turn is a consequence of simply connected. So we can remove redundancies by adding the contents of that last file to this one and removing the P38 trait file. (and arc connected will follow from path connected + T2)

[GeoffreySangston]

Is there anything that the nlab adds to the understanding of this?

You're right. I'm not sure why I didn't swap it out completely.

[GeoffreySangston]

S38|P200: (long ray is simply connected) Would there be a detailed proof somewhere that we can refer to? mathse or book? https://math.stackexchange.com/questions/1352181 for inspiration? Need to check for other posts.

I need to check this proof further.

I think the part of Eric Wofsey's post concerning this:

This is locally connected and simply connected (any path must be contained in $[0,\alpha]$ for some $\alpha<\omega_1$, and $[0,\alpha]$ is homeomorphic to $[0,1]$ and hence contractible).

is the same proof as what we've currently got in S38|P200. 'll look around.

(Edit: Somehow I overlooked this part "In the mean time, it seems we should mention also that the space is path connected.")

Probably not a good page to link to, but this page also more or less has the same thing, and is more focused on the particular question: http://at.yorku.ca/b/ask-an-algebraic-topologist/2020/2977.htm

[GeoffreySangston]

I think {S153|P200} can refer to {S153|P38}. Though maybe instead we should write the proof (so long as we don't find a reference) in {S153|P39} and refer both to that one. I believe {S153|P39} has one extra detail.

[prabau]

S39 (closed long ray) is actually not path connected (already known in pi-base). So it is not simply connected and not contractible either. No need to assert anything extra.

[prabau]

For S153 (open long ray), it's very sparsely populated. Most of the basic traits are unknown because nobody ever took the time to look at it in detail. There should be a separate PR to remedy this. So it does not really matter if you want to add something now or leave it out. We can clean it up later on with the rest.

[StevenClontz]

FYI, when we quote some mathse post in the text, we have been using the notation {{mathse:4044399}} in combination with adding the post to the refs: section. If you want to deviate from that, I don't necessarily object, but we should discuss with @StevenClontz .

{{mathse:4044399}} is best for referencing Mathematics Stack Exchange

[GeoffreySangston]

I think that's everything?

[prabau]

Seems a comment above from your comment to S38|P200 got overlooked. Repeating it here. What do you think?

The fact 'every map to a contractible space is homotopic to a constant map' is one of the equivalent characterizations of 'contractible' on Wikipedia, but does not appear on pi-base's Contractible

I think you are right. We should add that characterization (no proof needed, it's pretty obvious). That will allow to use a shorter argument for T583. And also change to a shorter argument for S38|P200.

BTW, should be something like "For every nonempty space $Y$, every map $Y\to X$ is ..." (I added the missing "nonempty" to wikipedia).

[prabau]

P199: I think we also need that $X$ is nonempty for the additional characterization.

S38|P200 (long ray is simply connected):
I know why compact connected sets in $X$ are homeomorphic to what you said. But not sure it's completely clear to everyone. Anyway, I was thinking of something simpler like this maybe:

"The image of $F$ is compact, hence bounded in $X$ as an ordered set. So $F(X)$ is contained in some interval homeomorphic to the interval $[0,1]\subseteq\mathbb R$. Since {S158|P199}, the map $F$ is homotopic to a constant map."

(I think the argument above is correct. It does not need that the image of $F$ is contractible, only that it is contained in some contractible subset of $X$.)

This would also depend on adding that S158 (Unit interval) is contractible.

What do you think?

[GeoffreySangston]

What do you think?

I think it's clearly a strict improvement, because it uses the basic elements of the space to explain more in fewer words. I'll go ahead and change it.

And I see that by asserting we're a subset of an interval, we can ignore managing the two cases.

I didn't see how to improve it, so I copied it in more or less verbatim. I did however write '{S158}' instead of $[0, 1] \subset \mathbb{R}$.

[GeoffreySangston]

This would also depend on adding that S158 (Unit interval) is contractible.

I think danflapjax's comment #818 (comment) should be considered, perhaps for a future pull request though.

I will go ahead and add 'S158 (Unit interval) is contractible'.

[GeoffreySangston]

P199: I think we also need that X is nonempty for the additional characterization.

Yes I agree, because previously that form was vacuously satisfied by $X = \emptyset$.

[prabau]

Looks good!