AbstractSimplicialComplex

Stream: mathlib4

[Raylern]

Hi guys! We are a summer project group in Technion, Israel. Our group is writing an Abstract Simplicial Complex library in Lean 4. And we finished our first version of the library and we are ready to contribute to mathlib. Could anyone tell use what should we do?

Thanks in advance!

Raylern.

[Kevin Buzzard]

There are instructions on how to contribute in the README aren't there? You need to ask the maintainers for push access to the repo and give a GitHub username. Make small PRs at first (at most 150 lines) because the process is very exacting

[Yaël Dillies]

In that specific case, I would like to see the entire library, because @Shing Tak Lam, @Sophie Morel and myself already have written (abstract) simplicial complex material and it would be good to synthesize all approaches optimally.

[Patrick Massot]

Kevin, there are several webpages on the community webpage dedicated to this topic, but they are not yet rewritten for Lean 4, so the situation is currently not ideal.

[Raylern]

Kevin Buzzard said:

There are instructions on how to contribute in the README aren't there? You need to ask the maintainers for push access to the repo and give a GitHub username. Make small PRs at first (at most 150 lines) because the process is very exacting

Thank you for your reply. Indeed there are some instructions and the first one it said is to discuss it here :joy:

[Raylern]

Yaël Dillies said:

In that specific case, I would like to see the entire library, because Shing Tak Lam, Sophie Morel and myself already have written (abstract) simplicial complex material and it would be good to synthesize all approaches optimally.

Yes, sure. I will try to share the code and make it public after my supervisor's permission

[Raylern]

Patrick Massot said:

Kevin, there are several webpages on the community webpage dedicated to this topic, but they are not yet rewritten for Lean 4, so the situation is currently not ideal.

Thank you to inform us about the situation.

Actually, we saw some of the notes including Clara L¨oh's notes https://loeh.app.uni-regensburg.de/mapa/main.pdf and many others, but we found most of them are in Lean 3 and not yet imported to Lean 4. And also, we wrote somethings that we need for our further use in our library.

Please let us know if somebody is doing or has done this. Thanks again!

[Raylern]

Raylern said:

Patrick Massot said:

Kevin, there are several webpages on the community webpage dedicated to this topic, but they are not yet rewritten for Lean 4, so the situation is currently not ideal.

Thank you to inform us about the situation.

Actually, we saw some of the notes including Clara L¨oh's notes https://loeh.app.uni-regensburg.de/mapa/main.pdf and many others, but we found most of them are in Lean 3 and not yet imported to Lean 4. And also, we wrote somethings that we need for our further use in our library.

Please let us know if somebody is doing or has done this. Thanks again!

Actually we are also translating some of the notes (this part we are still doing) we saw to Lean 4. And of course, we respect the authors about whether to merge into the mathlib4 in lean 4, and will acknowledge the authors and make a reference to them and so on

[Raylern]

Raylern said:

Yaël Dillies said:

In that specific case, I would like to see the entire library, because Shing Tak Lam, Sophie Morel and myself already have written (abstract) simplicial complex material and it would be good to synthesize all approaches optimally.

Yes, sure. I will try to share the code and make it public after my supervisor's permission

Here is the link to our github respository: https://github.com/Raylern/Simplicial-Complexes

[Sophie Morel]

Is there a place in your project where I can see what you did (without reading all the Lean code) ? I have some stuff on abstract simplicial complexes in Lean4, but it's not in mathlib yet. It would be a good opportunity to merge what we did and add it to mathlib.

[Raylern]

Sophie Morel said:

Is there a place in your project where I can see what you did (without reading all the Lean code) ? I have some stuff on abstract simplicial complexes in Lean4, but it's not in mathlib yet. It would be a good opportunity to merge what we did and add it to mathlib.

OK, maybe I will try to write a list of the theorems and definitions we did tomorrow

[Sophie Morel]

Thanks !

[Raylern]

Sophie Morel said:

Thanks !

I added a list of things we already implemented in README.md file for you, here is the link: https://github.com/Raylern/Simplicial-Complexes/blob/main/README.md

[Raylern]

By the way, here is my supervisor @Suraj Krishna M S

[Sophie Morel]

Thank you ! I'll do the same in the next few days. (I have to sit in a bunch of 4th/5th year defenses next week and haven't read the students' papers yet, so I might be a little bit busy. :sweat_smile: )

[Sophie Morel]

Hi, sorry for taking so long, I also had trouble updating mathlib on my computer. Here is the repository with my code:
https://github.com/smorel394/AbstractSimplicialComplex
I also wrote a README file with a description of results. It seems that we had pretty separate goals, which is good, but we do not agree on the implementation of an abstract simplicial complex so we will need to make a choice.

[Sophie Morel]

Now I need to add way more comments in the files.

[Sophie Morel]

There, I cleaned stuff up a bit and added more comments to explain what I am doing. Except for Category.AbstractSimplicialComplex.lean, which is still a mess (this is where we define the category of abstract simplicial complexes, prove that it is equivalent to the category of concrete presheaves on the category of nonempty fintype, and construct the geometric realization).

[Suraj Krishna M S]

Thanks for sharing. Your file looks quite comprehensive! We will get back soon. The project ended last week and the students returned to China, but we plan to get back in touch soon.

[Jack McKoen]

Hi everyone. Did this ever go anywhere? I'd like to use ASC's in some of my current work in Lean, so I'd be interested to help get them in mathlib.

[Yaël Dillies]

I have detailed ideas for how it should be done but little time to do so.

[Jack McKoen]

I see :laughing: . In that case, I'll keep my eye on this! But if there's ever any grunt work to be done I wouldn't mind assisting.