Completed proof of the Brouwer Fixed Point Theorem

Stream: maths

[Brendan Seamas Murphy]

Hi everyone! I've mentioned a couple of times that I've been working on a proof of the brouwer fixed point theorem (via singular homology). As of 5 minutes ago it's complete! See "brouwer_fixed_point" at https://github.com/Shamrock-Frost/BrouwerFixedPoint/blob/master/src/brouwer_fixed_point.lean. This project involved formalizing a good amount of homological algebra, all of the eilenberg steenrod axioms, and some stuff about convex sets. I'll be working on merging this code into mathlib soon (after taking a break), but first I'd like to get the page at https://leanprover-community.github.io/100.html updated :)

[Adam Topaz]

If a theorem falls in a forest with no mathlib to hear, is it really proved?

[Brendan Seamas Murphy]

Absolutely, my tweet announcing this already has 10 likes :)

[Adam Topaz]

But seriously -- congrats! This is great!

[Adam Topaz]

I suppose you also calculated the homology of the sphere (the actual manifold) somewhere in your repo, right?

[Brendan Seamas Murphy]

Yep! See nth_homology_of_n_sphere in homology_of_spheres.lean

[Adam Topaz]

Very nice!

[Adam Topaz]

(link for others looking: https://github.com/Shamrock-Frost/BrouwerFixedPoint/blob/52f48d25068df0eadf3df5b2ede7bcb087d30527/src/homology_of_spheres.lean#L2043 )

[Adam Topaz]

What about $H_3(S^5)$?

[Brendan Seamas Murphy]

I gave a fairly explicit computation of Hₙ(Δⁿ, ∂ Δⁿ), and I think it would be relatively easy to show that the generating class is the identity. However my homeomorphism Sⁿ ≅ ∂Δⁿ⁺¹ is not explicit for silly reasons, because I was nearing the end of the project and just wanted to finish it up

[Brendan Seamas Murphy]

Adam Topaz said:

What about $H^3(S^5)$?

No, but combine sphere_homeo_topological_simplex_boundary and homology_of_boundary_is_zero :P

[Brendan Seamas Murphy]

After some refactoring passes I'll probably give a computation by Mayer Vietoris instead of what I'm doing here

[Yaël Dillies]

Very nice! But that means I have one less reason to finish up Sperner's lemma :grinning:

[Johan Commelin]

@Brendan Seamas Murphy This result is entry 36 on the following list https://www.cs.ru.nl/~freek/100/
Feel free to create a PR to update this entry https://github.com/leanprover-community/mathlib/blob/master/docs/100.yaml#L136 with a pointer to your work

[Brendan Seamas Murphy]

Ah I couldn't figure out the structure of the repo for the website/100 theorems, thanks for the reference!

[Brendan Seamas Murphy]

I'll add it tomorrow

[Johan Commelin]

This will only update our local copy https://leanprover-community.github.io/100.html but it will percolate through to Freek's website semi-automatically.

[Anne Baanen]

I noticed this hasn't been added to the 100 theorems list yet. So I went ahead and created a PR: #18372

[Michael Rothgang]

I recently came upon an application where Brouwer's fixed point theorem would be really useful (defining the boundary of a finite-dimensional manifold, showing that interior and boundary are disjoint and the interior is open). How far is this from hitting mathlib?

I'm aware this is/was waiting on a refactor of homology and the port being complete, but if I understand correctly this is almost immanent now.

No pressure, we're all volunteers! But I'd be excited to use this :-)

[Michael Rothgang]

(Funnily, my personal medium-term interest in defining boundary is for proving Sard's theorem with boundary - which could also be used to show Brouwer (though perhaps is not a simpler proof :smile: ).

[Kevin Buzzard]

Are we really talking about a refactor of singular homology, or are we talking about the refactor of homology of a complex as in kernel over image?

[Michael Rothgang]

Oops. The latter. Fixed.

[Scott Morrison]

Pinging @Brendan Seamas Murphy to make sure they see this! :-)

[Brendan Seamas Murphy]

Still pretty far, sorry. I made some headway refactoring and porting to lean 4 but didn't finish that. If anyone wanted to help the best thing to do would be to try and pr small chunks from my repo unrelated to the main theorem, it would be a lot more manageable if it was just the core logic that needed porting

[Brendan Seamas Murphy]

I'm also likely not going to merge the acyclic models stuff. It was interesting to work out but the direct argument with a prism for invariance of singular homology is much simpler

[Antoine Chambert-Loir]

I regret that. It is true that using the acyclic models theorem is often painful, and we might obey MacLane's diktat that it is worth being reproved every time, as if it were a kind of metatheorem, but I thought about it a years and I feel there is a way to make it useful.
Given a presentation of a category (using acyclic models), the proof of the theorem constructs a bunch of classes (I wish to call them an Eilenberg-Zilber datum) which, in turn, produces the desired morphisms of complexes. Now, there are cases where we know how to construct these classes — the case of prisms is such an example — and I believe it is interesting to frame it as such.

[Ruben Van de Velde]

Brendan Seamas Murphy said:

Still pretty far, sorry. I made some headway refactoring and porting to lean 4 but didn't finish that. If anyone wanted to help the best thing to do would be to try and pr small chunks from my repo unrelated to the main theorem, it would be a lot more manageable if it was just the core logic that needed porting

Is the work you've done towards porting to lean 4 available somewhere?