Abstract simplicial complex and the homology of S_n

Stream: Is there code for X?

[Sehun Kim]

Should I ask whether there is a direct notion for an abstract simplicial complex and their geometric realization

I know that there is a notion for the simplicial object in Mathlib but I could not find its geometric realization or the relation between the abstract simplicial complex

I also want to know that there is a computation result of the homology (or homotopy) of the specific geometric structure like $H_n(S_n)= \mathbb{Z}$.

When I wrote a code like Jordan Curve Theorem, I needed a result of $H_n(S_n)= \mathbb{Z}$, but I could not find the direct computation of it in the mathlib. If there is no result of it, can I contribute the code for it? This may include the general result like [Freudenthal Suspension Theorem] (https://en.wikipedia.org/wiki/Freudenthal_suspension_theorem)

[Joël Riou]

We have the topological realization functor https://leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicTopology/SingularSet.html but not the computation of the homology of spheres.

[Sehun Kim]

If I write a code for the computation of some typical geometric objects like sphere, torus,Klein bottle... etc. then is there a room for contribution to Mathlib library? I think this results could be used in many other theorems.

[Joël Riou]

Of course. But in order to do that, I think you basically need to prove a few general theorems regarding singular homology! (Currently, we basically only have the definition.)