# 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):

#### 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: May 16 2021 at 21:11 UTC