simplicial complexes/PL manifolds

Stream: mathlib4

[Justin Shaw]

Hello,
I'm currently learning geometric topology, and thought it would be fun to try and formalize the simplicial approximation theorem. I see that in mathlib there are definitions of simplicial sets, a basic definition of a topological n-simplex, and (apparently?) an upcoming PR by @Sophie Morel to implement abstract simplicial complexes. Would a mathlib implementation of simplicial complexes and/or PL manifolds have to depend on abstract simplicial complexes? If not, would it be unwise to try and implement them now?

[Yaël Dillies]

They already exist! docs#Geometry.SimplicialComplex

[Yaël Dillies]

I have more stuff in my repo LeanCamCombi. Feel free to PR whatever you need to mathlib

[Justin Shaw]

Yaël Dillies said:

They already exist! docs#Geometry.SimplicialComplex

I somehow did not see this, why thank you! This could probably be wrangled into a proof, but it seems like geometric topology would benefit from an embedding-invariant definition (i.e. based purely off of a finset with an associated topological space, a "default" metric, etc., also possibly the category of simplicial complexes as well?). On another note, out of curiosity, would this be classified under mathlib/AlgebraicTopology? It might be fun to eventually build up to a formalization of the generalized schoenflies theorem/dehn's lemma/loop theorem, but those feel like they might be a bit out of place folder-wise.