Brouwer's theorem

Stream: mathlib4

[metakuntyyy]

Hey guys, I have seen that Brouwer's fixed point theorem is proven in lean3 https://github.com/Shamrock-Frost/BrouwerFixedPoint/blob/master/src/brouwer_fixed_point.lean

I would like to port it and its result to mathlib4, since I might want to do some game theory, and for that I likely need either Brouwer or Kakutani.

Is this a good idea. It seems that the way to prove it is to calculate homology groups of spheres and balls. The idea is that if Brouwer is false then there exists a homotopy ball -> sphere. and homotopy equivalence implies that the homology groups are isomorphic. however the homology groups of the ball and sphere are not isomorphic.

Also there seems to be some work regarding simplicial homology and how it relates to singular homology.

Any ideas, suggestions?

[Joël Riou]

I am not aware of developments about homology of topological spaces or simplicial sets in mathlib, but it would be very good projects!

[metakuntyyy]

So as of right now I am trying to figure out how the port works. The lean3 repository doesn't even compile and it gives me weird oom or type errors. What would be the starting point even, would it be simplicial homology?

[Thomas Browning]

@Brendan Seamas Murphy @Brendan Seamas Murphy What's the status of Brouwer porting / inclusion into mathlib?

[Brendan Seamas Murphy]

Hi! I'm just confirming commit be49bf8 builds before I reply to the open issue. The short version is that the project was out of date with mathlib3 at the time of completion and broke when updated. I and I had planned to get it up to the latest version before running mathport but didn't finish. I'd love to see this ported and would be happy to help if you have questions @metakuntyyy. I believe be49bf8 should build and would be a good comparison to the latest commit but it might be a waste of work to restart from there

[Brendan Seamas Murphy]

@Yury G. Kudryashov might know about relevant PRs or changes in mathlib4 about the simplex stuff

[Johan Commelin]

I guess the whole homological algebra machinery in mathlib4 is quite different from what is used in your project, right?

[Brendan Seamas Murphy]

Hmm, probably the stuff copied from LTE can be removed

[metakuntyyy]

Yeah, that sounds great @Brendan Seamas Murphy

I've always to understand the connection between homology and topology and the construction of the homology groups in detail. I guess this should be a fine project for a beginner, given that the solution is already there.

[Yury G. Kudryashov]

I ported some simple lemmas that don't involve homologies some time ago. I'm ready to talk about the best way to fit this or that non-homological lemma (point topology, linear algebra) in Mathlib 4, but I have no experience with the implementation of homology in Mathlib.

[metakuntyyy]

Also as a bonus, if the proof is done I might try to port the results to metamath. It misses a lot of concepts and definitions.

[Yury G. Kudryashov]

It would be nice to have a version that builds against Mathlib 3 master branch, then run mathport and start going through the files.

[metakuntyyy]

Is there any documentation how the mathport works? Has anyone done it and what is the general idea behind it?

[Yury G. Kudryashov]

Mathlib was ported using mathport. Once we have a version that builds with the latest mathlib3, I can run mathport for you.

[metakuntyyy]

Ah great, so I assume most things remaining to be done is documentation of the ported lemmas?

[Yury G. Kudryashov]

No, a lot of code was not up to Mathlib standards. Also, homologies are done differently in Mathlib 4, so you'll need to rewrite parts of the proof using a different API.

[Yury G. Kudryashov]

But the first step is to make it compile.

[metakuntyyy]

Ah ok, I think I understand it. Because there are tons of ways to do the same thing in mathematics the goal is to use unified data structures. For example you can define two similar concepts in a slightly different way. The goal is to use the unified api of mathlib, where in the port a different api is used.

Did I understand that one correctly?

[Yury G. Kudryashov]

Yes, some of the mathematical facts in the repository was already added to Mathlib, sometimes under a slightly different name or using different API. If we want to merge it to Mathlib, then we need to port the code to Mathlib definitions.

[metakuntyyy]

Understood, thanks.

[Brendan Seamas Murphy]

The major place where this happens is that the project uses a different definition of standard topological simplices than mathlib. When I was planning to port this I was planning to change the definition in mathlib to the one used this project (which uses the existing machinery in other parts of mathlib for simplices defined as a convex hull, while the current definition is ad-hoc. Iirc)

[Johan Commelin]

@Brendan Seamas Murphy correct me if I'm wrong, but if the project depends on a fair amount of LTE, then I think trying to use mathport might be painful. Or is the dependency on LTE pretty light?

[Michael Rothgang]

AIUI (just an interested bystander), thia project depended on LTE - and then replaced this dependency by manually inlining the relevant parts (still ten thousand lines, but much less than LTE).

[Michael Rothgang]

@Brendan Seamas Murphy Did you get to confirming be49bf8 builds? How much effort would it be to makes this project build with the latest mathlib(3)?

Just today, I was reminded of some result which would really like to use homology groups of spheres. I understand this project won't be mathlib-PRable as-is, but porting it to Lean 4 still seems like a major step forward; I would be a shame to see this silently wither.

[Johan Commelin]

I fear that porting this to Lean 4 using mathport will be a lot of effort, and the end result would be something that is still quite far from mathlib compatibility (in the strict sense). After all, homological algebra went through a massive refactor.
So I think it might be better to use this repo as a very detailed blueprint, and just rewrite it in idiomatic mathlib4 homological algebra.

@Joël Riou what do you think?

[Joël Riou]

Yes, I would agree that it would be more interesting and efficient to use Brendan's repository as a blueprint/inspiration on how to proceed, and rewrite the code.