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.

Yaël Dillies (Feb 09 2022 at 21:54):

What abstract simplicial stuff? We don't have abstract simplicial complexes, right?

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

https://leanprover-community.github.io/mathlib_docs/analysis/convex/simplicial_complex/basic.html

Yaël Dillies (Feb 09 2022 at 22:00):

Ah yeah, but those are not abstract!

Yaël Dillies (Feb 09 2022 at 22:00):

Shing wants to add the abstract ones, and it's literally a matter of removing that spatial condition.

Patrick Massot (Feb 09 2022 at 22:02):

And also https://leanprover-community.github.io/mathlib_docs/algebraic_topology/simplicial_object.html

Kevin Buzzard (Feb 09 2022 at 22:11):

I guess this is closer to CW complexes because you allow infinite combinatorial objects

Adam Topaz (Feb 09 2022 at 22:58):

Even better docs#category_theory.sSet (I think that's what it's called?)

Adam Topaz (Feb 09 2022 at 22:59):

Is it docs#sSet ?

Adam Topaz (Feb 09 2022 at 22:59):

Also docs#sSet.to_Top

Kevin Buzzard (Feb 09 2022 at 23:00):

Perfect! So indeed we do have abstract simplicial complexes

Reid Barton (Feb 09 2022 at 23:26):

Well, we have simplicial sets... but that's really the right framework anyways


Last updated: Dec 20 2023 at 11:08 UTC