Algebraic Topology

Stream: new members

[Jakub Rudzik]

Hi Lean Community!

My friends from university and I have recently started learning how to formalize mathematics in Lean, and we’ve decided to begin our own project. Our main interest lies in Algebraic Topology, and we had the idea to start formalizing parts of Hatcher’s Algebraic Topology. However, it seems that a lot of material up to the fundamental group of the circle and beyond has already been done in Mathlib4.

We would still like to contribute in some way, which leads to our question: which topics in Hatcher’s book would be good to work on? We’ve considered computing fundamental groups or homologies of specific spaces. Another possibility is some covering space theory, such as the existence of universal covers or deck transformations. There are also applications of the fact that the fundamental group of the circle is ℤ, like the Brouwer Fixed-Point Theorem or the Borsuk–Ulam Theorem.

Do you think these would be good topics to tackle? I'd love to here your opinion!

[Jack McCarthy]

Hi Jakub,

Great to hear that you're interested in Algebraic Topology, as there is still a lot of work to be done in that area. AFAIK, there is lots of content in Hatcher's book that is not currently in mathlib. For example, we do not currently have Van Kampen's Theorem, and this would be a great thing to get formalized (although perhaps not so great for a first project.) The code on Homology / Cohomology of a topological space is still very basic. If you take a look at AlgebraicTopology/SingularHomology, there is really only results about Totally Disconnect Spaces right now (which, of course, is not very useful for studying actual geometric spaces). Some results that would be nice to establish in this regard are:

• the Homology groups of spheres
• homology group is perserved by homotopy equivalence
• The relationship between the n'th homology group and K(pi, n) spaces
• The relationship between the singular chain complex of CW-complex and the homology groups of it's n-skeletons

There is also an ongoing project to formalize DeRham Cohomology which could always use more help. My suggestion would be to go to the Mathlib's currenly Open Issues and sort by the tag "good first issue". That will give you lots of relatively simply projects that would improve the state of the library. Find one that suits your interests/background, and then claim it.
https://github.com/leanprover-community/mathlib4/issues?q=is%3Aissue%20state%3Aopen%20label%3A%22good%20first%20issue%22

[Jakub Rudzik]

Hi Jack,

Thanks a lot for the advice!
We also considered Van Kampen's theorem, although I think you are right that it might not be great for the first project. I wasn’t aware, though, that singular homology has many open problems. In particular, the homology groups of spheres sound like a nice problem to tackle.

We will discuss it within our team and do our best to make some progress. That would be awesome!
Once again, thank you, and best regards!

[Michael Rothgang]

Hi and welcome! Can you move your message to a new topic, please? (It doesn't have anything to do with algebraic topology.) Also, please don't double-post.

[Michael Rothgang]

(Are you aware that there has been previous work on Ceva's theorem? It was never completed and merged into mathlib, though.)

[Jun Akita]

I'm sorry.
I understood. I discovered previous work on Ceva's theorem.
Thank you for telling.