Weakly contractible definition + trivial theorems

[felixpernegger]

Updating #1761.
Note this still misses whitehead theorem.

This PR has high priority!

[prabau]

If $f:X\to Y$ is a weak homotopy equivalence between two spaces (i.e., induces isomorphisms between all homotopy groups). does there necessarily exist an "inverse" i.e. a weak homotopy equivalence going the other way $Y\to X$?
I.e., is the relation of "weak homotopy equivalence" between spaces symmetric? (it's obviously reflexive and transitive).

[prabau]

The definition is kind of ok, although it could be slightly more precise. I'll suggest an edit.

[prabau]

Need to mention a specific definition/page where this is defined, in Hatcher for example, or some other AT book.

[prabau]

No need to add https://en.wikipedia.org/wiki/Homotopy_group in the refs: section, as it's only an accessory concept. It's good that it's linked to directly from the text.

On the other hand, need to add a direct link to something for "weakly homotopy equivalent".

[felixpernegger]

If f : X → Y is a weak homotopy equivalence between two spaces (i.e., induces isomorphisms between all homotopy groups). does there necessarily exist an "inverse" i.e. a weak homotopy equivalence going the other way Y → X ? I.e., is the relation of "weak homotopy equivalence" between spaces symmetric? (it's obviously reflexive and transitive).

according to this no
https://math.stackexchange.com/questions/80217/existence-of-weak-homotopy-equivalence-not-a-symmetric-relation
(very good question)

[felixpernegger]

No need to add https://en.wikipedia.org/wiki/Homotopy_group in the refs: section, as it's only an accessory concept. It's good that it's linked to directly from the text.

On the other hand, need to add a direct link to something for "weakly homotopy equivalent".

I thought we usually link it in the refs section as well even if we link directly in text?
In any case, there is also https://en.wikipedia.org/wiki/Weak_equivalence_(homotopy_theory) (which I actually dont like so much, but we should link it anyways)

[felixpernegger]

Need to mention a specific definition/page where this is defined, in Hatcher for example, or some other AT book.

I for the sake of it cant find a textbook containing either of the names (even though the term appears a lot)
A paper with over 70 citations by a reputable author defining the term is for example
https://zbmath.org/0979.55010
maybe we can use this?

[prabau]

If f : X → Y is a weak homotopy equivalence between two spaces (i.e., induces isomorphisms between all homotopy groups). does there necessarily exist an "inverse" i.e. a weak homotopy equivalence going the other way Y → X ? I.e., is the relation of "weak homotopy equivalence" between spaces symmetric? (it's obviously reflexive and transitive).

according to this no https://math.stackexchange.com/questions/80217/existence-of-weak-homotopy-equivalence-not-a-symmetric-relation (very good question)

Good to know.

Of course, for the case of a weakly contractible space, it does not matter: if there is a weak homotopy equivalence from $X$ to a singleton (by the unique map possible), any map from the singleton to $X$ will also be a weak homotopy equivalence, and vice versa. And it's equivalent to all homotopy groups being trivial.

[prabau]

The Lück,-Meintrup paper does not seem easily accessible. We should replace it with something else. I'll keep looking.

We need one ref using the name "weakly contractible" (maybe even Hatcher), and another one using "homotopically trivial".

[felixpernegger]

We need one ref using the name "weakly contractible" (maybe even Hatcher), and another one using "homotopically trivial".

Hatcher doesnt have this. I disagree we need sources for both

[felixpernegger]

The Lück,-Meintrup paper does not seem easily accessible. We should replace it with something else. I'll keep looking.

Typing it to google scholar immediately gives a pdf, so it is easily accessible

https://scholar.google.com/scholar?hl=de&as_sdt=0%2C5&q=On+the+Universal+Space+for+Group+Actions+with+Compact+Isotropy&btnG=

[prabau]

It's good that one can access it. We then need to add that as a link for the benefit of pi-base users.

As a general guideline, we also need to add a reference for the aliases that we use. That shows that we don't make things up and anyone interested can follow up if desired. I have found a good reference for "homotopically trivial".

If you allow me, I can add a commit with these changes.

[felixpernegger]

yes just commit directly :)

[prabau]

I added some references and did some minor tidying up.

About the meta-property for products, Hatcher prop. 4.2 seems to prove it for arbitrary products. What do you think?

[prabau]

Another pending issue: should the empty space be weakly contractible or not?
See P200 (simply connected) for comparison.

See #1634 (comment). I just reread the long discussion we had as part of #1634. Either way would have been acceptable, but eventually the consensus was to not do a special case for the empty space. (See how things were eventually formulated in P200.)

Now for P242 (weakly contractible), what would be the pros and cons of having the empty set be or not be P242?
(I know you like things to match Lean, but apart from that).

[felixpernegger]

I added some references and did some minor tidying up.

About the meta-property for products, Hatcher prop. 4.2 seems to prove it for arbitrary products. What do you think?

Looks good.

Nice it holds for arbitrary.

[felixpernegger]

Another pending issue: should the empty space be weakly contractible or not? See P200 (simply connected) for comparison.

See #1634 (comment). I just reread the long discussion we had as part of #1634. Either way would have been acceptable, but eventually the consensus was to not do a special case for the empty space. (See how things were eventually formulated in P200.)

Now for P242 (weakly contractible), what would be the pros and cons of having the empty set be or not be P242? (I know you like things to match Lean, but apart from that).

The upside is that it then better matches simply connected.

Downsides are that we currently have 3 definitions in the file and one of them just dooesnt work for the empty space (so we would have no add "X is empty or ....".

Additionally (the reason why I added this property in the first place), the theorem CW complex + weakly contractible => contractible becomes uglier.

Additionally, "Weakly Contractible" should probably be analogue to "Contractible" which is always nonempty.

---

So I do think it is easier this way. (and once again, simply connected should be nonempty as well, but I really dont wanna bring that up again right now)

[prabau]

Ok, let's go with requiring nonempty for now. If it becomes too ugly, we can change it later.

(Note that many papers don't even mention the empty space one way or the other. They ignore it completely, as it is a degenerate case that is not interesting.)

Then, can you change the first paragraph and add "nonempty" in there?

[felixpernegger]

Another thing I just noticed, T890 is redundant factors over simply connected), but maybe its good to display it anyways for clarity?

[prabau]

Good point. Path connected is $n=0$ and simply connected is $n=0$ and $1$. Since it's so simple, I think we don't lose clarity without T890 and we should remove it.

[felixpernegger]

I removed it directly now (without redoing UID's), we can put CW complex + weakly contractible => contractbile there later

[prabau]

When I look at the list of theorems for a given property, I find it easier if the list starts with the basic result and the non-trivial theorems come afterwards.
Can you for example move T893 to T890?

[prabau]

or I can do the move if you want

[felixpernegger]

makes sense

[prabau]

one last remark for myself. Higher homotopy groups are defined in terms of basepoint-preserving homotopies. On the other hand, the null-homotopies for the maps $S^n\to X$ in the first definition don't have any basepoint to preserve. That does not cause any problem, as already explained when discussing P200 (simply connected).

[felixpernegger]

Yess, additionally higher homotopy are abelian, so conjugates cancel out