Abstract simplicial complexes contribution

Stream: new members

[Denis Gorodkov]

Hi,
Having played around with Lean for a while, I wanted to try to start a Lean project with the goal of making it public. I would be happy to try to contribute to Mathlib if I am able to find a project that matches my ability.

One subject that I have professionally worked with a lot, but that does not seem to be formalized yet, is abstract simplicial complexes and the general approach to combinatorial topology (the toolset of simplicial complexes before geometric realization). My guess would be that, as soon as geometric realization happens, this is a tough task, but introducing the combinatorial toolset seems a reasonable exercise.

I have seen that simplicial sets have been realized in quite a bit of detail already. Would a more combinatorics-flavored theory from a topology/triangulation perspective be of any interest?

[Junyan Xu]

Looks like #33364 hasn't made it into mathlib yet. A compilation of previous threads:
#maths > Abstract Simplicial Complex @ 💬
#mathlib4 > AbstractSimplicialComplex @ 💬
#mathlib4 > simplicial complexes/PL manifolds @ 💬
#mathlib4 > Additions to the `SimplicialComplex` API @ 💬
#graph theory > Proof of the Kneser conjecture @ 💬
#new members > Isomorphisms of simplicial complexes @ 💬
#Is there code for X? > Abstract simplicial complex and the homology of S_n @ 💬
#mathlib4 > Simplicial Complex vs CW Complex for Topology? @ 💬
#Is there code for X? > Reasoning about abstract simplicial complexes @ 💬

[Denis Gorodkov]

Thank you, @Junyan Xu ! Searching through Mathlib didn’t return anything, and I underestimated how developed is this Zulip chat