Zulip Chat Archive

Stream: new members

Topic: Simplicial complexes?

Pascal Wild (Jan 19 2021 at 19:18):

Hi everyone!
I am new to Lean and would like to try whether I could prove some theorems related to my research. The mathematical objects I am mostly working with are simplicial complexes. Are they already defined in mathlib? If so, what about (co)homology groups of simplicial complexes?

Adam Topaz (Jan 19 2021 at 19:20):

@Johan Commelin has a branch of mathlib with some code about simplicial sets

Johan Commelin (Jan 19 2021 at 19:36):

branch#sset

Johan Commelin (Jan 19 2021 at 19:36):

Unfortunately there are too many things on my todo list. So I don't have much time to push this into mathlib.

Johan Commelin (Jan 19 2021 at 19:36):

But others should feel free to do with the code whatever they want.

Johan Commelin (Jan 19 2021 at 19:37):

That branch includes homology of topological spaces, in particular homology groups of simplicial complexes

Johan Commelin (Jan 19 2021 at 19:40):

@Pascal Wild also, welcome!

Pascal Wild (Jan 19 2021 at 19:51):

This is a great starting point! Thanks a lot!

Bhavik Mehta (May 04 2021 at 13:23):

@Yaël Dillies and I have a bunch of results about simplicial complexes, being actively worked on in branch#sperner-again

Last updated: Dec 20 2023 at 11:08 UTC