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

The singular simplicial set TopCat.to_SSet.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

• TopCat.toSSet : TopCat ⥤ SSet is the functor assigning the singular simplicial set to a topological space.
• SSet.toTop : SSet ⥤ TopCat is the functor assigning the geometric realization to a simplicial set.
• sSetTopAdj : SSet.toTop ⊣ TopCat.toSSet is the adjunction between these two functors.

TODO

• Generalize to an adjunction between SSet.{u} and TopCat.{u} for any universe u
• Show that the singular simplicial set is a Kan complex.
• Show the adjunction sSetTopAdj is a Quillen adjunction.

noncomputable def TopCat.toSSet : CategoryTheory.Functor TopCat SSet

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

• TopCat.toSSet = CategoryTheory.ColimitAdj.restrictedYoneda SimplexCategory.toTop

noncomputable def SSet.toTop : CategoryTheory.Functor SSet TopCat

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

• SSet.toTop = CategoryTheory.ColimitAdj.extendAlongYoneda SimplexCategory.toTop

noncomputable def sSetTopAdj : SSet.toTop ⊣ TopCat.toSSet

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

Equations

• sSetTopAdj = CategoryTheory.ColimitAdj.yonedaAdjunction SimplexCategory.toTop

noncomputable def SSet.toTopSimplex : CategoryTheory.Functor.comp CategoryTheory.yoneda SSet.toTop ≅ SimplexCategory.toTop

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

Equations

• SSet.toTopSimplex = CategoryTheory.ColimitAdj.isExtensionAlongYoneda SimplexCategory.toTop