Zulip Chat Archive

Stream: new members

Topic: Brouwer's fixed point theorem?

Mark Lavrentyev (Feb 09 2022 at 20:22):

I see there is recent activity on the fundamental groupoid for topological spaces front - are people looking for help? Particularly interested in making progress towards proving Brouwer's fixed point theorem.

Yaël Dillies (Feb 09 2022 at 20:23):

cc @Shing Tak Lam

Yaël Dillies (Feb 09 2022 at 20:25):

Bhavik and I have a completely different approach to Brouwer's fixed point theorem, namely to go through Sperner's lemma and subdivisions. It's over at branch#sperner-again and I'm planning to get back to it once the prerequisites have hit mathlib (starting with #11308)

Shing Tak Lam (Feb 09 2022 at 20:30):

I don't have much (if any) time for Lean in the near future, so really anything about the fundamental groupoid (or higher homotopy groups in general) would be useful. I haven't looked much at sperner-again, but I think we'll be able to get Brouwer for higher dimensions than 2 using Sperner right? Since with the fundamental group(oid) I think you can only get the dimension 2 case?

Eric Rodriguez (Feb 09 2022 at 20:31):

(this should be in a different thread)

Yaël Dillies (Feb 09 2022 at 20:33):

For the Sperner part, that's right, Shing. I don't know about the fundamental groupoid part (is it that the generalization is higher order homotopy theory?).

Mark Lavrentyev (Feb 09 2022 at 21:32):

I only really know of the homology way about doing > 2 dim Brouwer via homology - and I'm not really sure about how developed (singular/simplicial) homology is in mathlib, but happy to help develop fundamental groupoids if that'd be helpful either way. I'm just looking not to duplicate someone else's efforts :)

Patrick Massot (Feb 09 2022 at 21:49):

We need homology for higher dimensional Brouwer. But it should be much easier now that we have a lot of abstract homological algebra and abstract simplicial stuff.