Zulip Chat Archive

Stream: new members

Topic: Simplicial complexes?


view this post on Zulip 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?

view this post on Zulip Adam Topaz (Jan 19 2021 at 19:20):

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

view this post on Zulip Johan Commelin (Jan 19 2021 at 19:36):

branch#sset

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jan 19 2021 at 19:36):

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

view this post on Zulip Johan Commelin (Jan 19 2021 at 19:37):

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

view this post on Zulip Johan Commelin (Jan 19 2021 at 19:40):

@Pascal Wild also, welcome!

view this post on Zulip Pascal Wild (Jan 19 2021 at 19:51):

This is a great starting point! Thanks a lot!

view this post on Zulip 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: May 16 2021 at 21:11 UTC