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