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.

[Sophie Morel]

I created a branch of mathlib where I started putting my abstract simplicial complex stuff.

[Sophie Morel]

@Yaël Dillies, if there is a way to give you editing rights on that branch I'll do it, but I can't figure out how to do it right now.

[Johan Commelin]

@Sophie Morel Everyone with write access to non-master branches of mathlib4 has write access to all non-master branches of mathlib4

...

...

Yes, that means that anybody can totally mess up other peoples work if they're sufficiently malicious.

[Sophie Morel]

Oh cool, then I don't have to do anything. I'm not too worried, because I also keep my own copies of my work.

[Adam Topaz]

I've started prefixing my branch names with AT so it's less likely that there's a clash with someone else's branch.

[Sophie Morel]

Ah, that's a good idea, I didn't think of the risk of accidentally messing up someone else's branch because you chose the same name.

[Sophie Morel]

(Also, this way I get to call all my branches "SM + something"... :grinning_face_with_smiling_eyes: )

[Ruben Van de Velde]

You'd only be able to mess up things if you use git push -f without paying attention, fwiw

[Yaël Dillies]

FYI term starts tomorrow for me so I'll have very little time to look into this!

[Sophie Morel]

No pressure, I'm just working on putting all this in PR-able shape, and I suppose I'll PR it eventually. Moved the branch so its name starts with "SM", now it's there.

[Berber]

Sophie Morel said:

I created a branch of mathlib where I started putting my abstract simplicial complex stuff.

How usable is this branch? Is there some movement here? I would love to have something working, and have it be in mathlib.

[Kevin Buzzard]

It seems to add 3000 lines of code so it's not suitable as a PR (which typically adds under 200) but it might be highly suitable as a guide for how one might want to set things up.

[Kevin Buzzard]

If you get Sophie's blessing and want to take it on, you could do worse than getting the first 221 lines of Mathlib/Combinatorics/AbstractSimplicialComplex/Basic.lean compiling (if it doesn't compile any more) and then opening a PR. The work will need reviewing and if you're prepared to take on the role of the person making the changes then this might be a good way to proceed.

[Berber]

nice, i'll take a look, thank you!

[Sophie Morel]

You guys have my blessing to do whatever you want with the code, I will be happy if it is useful to somebody. I unfortunately don't have time now to make it PR-able.