Simplicial API

Stream: maths

[Robin Carlier]

Hi! Who's "in charge" of the simplicial API (simplex category and simplicial sets) in mathlib? I would be interested in working a bit on it (though I do not have much free time to do so) and I'd like to know what would be interesting "milestones" for it?
I have a file in which I proved a bunch of lemmas concerning epi and monos in the simplex category (namely that they're exactly the maps whose underlying functions are surjective/injective, how they behave with respect to length, existence and unificity of epi-mono factorization in the simplex category), I don't think my code is PR-able right now since the proofs are probably very poorly written (I'm still a lean begginer) but I'd like to know what I could work on anyway.

[Robin Carlier]

I was thinking about trying to prove the Eilenberg-Zilber lemma in simplicial sets (any simplex of a simplicial set is uniquely a degeneracy of a non-degenerate simplex)

[Eric Rodriguez]

there was some talk about it here!

[Eric Rodriguez]

its probably still worth at least posting it as a gist, then we can give you some general feedback ^^

[Robin Carlier]

Mmh, I'll try to have a mathlib fork on my github to post it then, rather than just sending a raw 400 lines of code here :P

[Robin Carlier]

Though I guess I could do a pastebin, but is there lean syntax coloring for it?

[Robin Carlier]

Aw nope.

[Eric Rodriguez]

that seems like a solid idea :b @mantainers can give you branch access too ^^

[Kevin Buzzard]

Usually the people mentioned in the copyright list are the people to talk to. Don't work if possible, CI is much better if you have push access to non master branches on the official mathlib repo -- post your github userid

[Robin Carlier]

I didn't understand what you meant by a gist! So here we go: https://gist.github.com/robin-carlier/4b4c19edcabf3be393d20e98aff44f5f
As you can see the proof are probably over-complicated due to me not being at ease with the library now, and relying to much on "have".
I don't think I'll just ask for push access right now, I don't feel like I should have access for now, but my (pretty empty) git account is https://github.com/robin-carlier.

[Robin Carlier]

Code is also completely undocumented, which is why I don't think it's worth anything yet.

[Robin Carlier]

I put some of the code in https://github.com/leanprover-community/mathlib/commit/1bf357f71a64386d605f650e34737cb546bf4124 after cleaning it up a bit, if anyone has general feedback (especially concerning style, I've been trying to follow the style guidelines but not sure I did everything right) that'd be nice. Does that amount of code seems too much/too little for a PR? Sorry if the questions feel silly but I'd rather not mess up.

[Ruben Van de Velde]

I think you probably should make the pull request - it's much easier to comment on anything there. The size seems fine; I wouldn't add too much to it.