Documentation

Mathlib.AlgebraicTopology.SingularSet

The singular simplicial set of a topological space and geometric realization of a simplicial set #

The singular simplicial set TopCat.toSSet.obj X of a topological space X has as n-simplices the continuous maps [n].toTop → X. Here, [n].toTop is the standard topological n-simplex, defined as { f : Fin (n+1) → ℝ≥0 // ∑ i, f i = 1 } with its subspace topology.

The geometric realization functor SSet.toTop.obj is left adjoint to TopCat.toSSet. It is the left Kan extension of SimplexCategory.toTop along the Yoneda embedding.

Main definitions #

TODO #

The functor associating the singular simplicial set to a topological space.

Let X be a topological space. Then the singular simplicial set of X has as n-simplices the continuous maps [n].toTop → X. Here, [n].toTop is the standard topological n-simplex, defined as { f : Fin (n+1) → ℝ≥0 // ∑ i, f i = 1 } with its subspace topology.

Equations
Instances For

    The geometric realization functor is the left Kan extension of SimplexCategory.toTop along the Yoneda embedding.

    It is left adjoint to TopCat.toSSet, as witnessed by sSetTopAdj.

    Equations
    Instances For

      Geometric realization is left adjoint to the singular simplicial set construction.

      Equations
      Instances For
        noncomputable def SSet.toTopSimplex :
        CategoryTheory.yoneda.comp SSet.toTop SimplexCategory.toTop

        The geometric realization of the representable simplicial sets agree with the usual topological simplices.

        Equations
        Instances For