Reasoning about abstract simplicial complexes

Stream: Is there code for X?

[Vikram Saraph]

Hey community,

I'm interested in writing proofs in Lean for some results about abstract simplicial complexes, for example showing that certain complexes are shellable. There doesn't appear to be a definition in mathlib for reasoning about abstract simplicial complexes directly, so if I wanted to do this, should I just write my own definition and go from there? eg:

structure AbstractSimplicialComplex (α : Type*) [DecidableEq α] where
    faces : Set (Finset α)
    empty_mem : (∅ : Finset α) ∈ faces
    downward_closed : ∀ {F G : Finset α}, F ∈ faces → G ⊆ F → G ∈ faces

I see there's a definition for geometric simplicial complexes but I'm not sure it's sufficient for what I want to do. I also saw that someone relatively recently asked about the geometric realization in another context. Having a function that lets me pass between a hypothetical AbstractSimplicialComplex structure and Geometry.SimplicialComplex would be helpful in proving certain results. For example, if I want to prove or work with the simplicial approximation theorem.

Is anyone aware of any existing ongoing effort to work with abstract simplicial complexes directly? If not, would it be reasonable to roll my own definition (as above) and start from there? Thoughts?

also, this is my first post, does it go in new members instead?

[Yaël Dillies]

@Sophie Morel has proved things about shellability. Maybe you can build on top of her work?

[Vikram Saraph]

Thanks! I’ll take a look at her work