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

• 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.Presheaf.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.yoneda.leftKanExtension SimplexCategory.toTop

noncomputable def sSetTopAdj : SSet.toTop ⊣ TopCat.toSSet

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

Equations

• sSetTopAdj = CategoryTheory.Presheaf.yonedaAdjunction (CategoryTheory.yoneda.leftKanExtension SimplexCategory.toTop) (CategoryTheory.yoneda.leftKanExtensionUnit SimplexCategory.toTop)

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

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

Equations

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

noncomputable def TopCat.toSSetIsoConst (X : TopCat) [TotallyDisconnectedSpace ↑X] : toSSet.obj X ≅ (CategoryTheory.Functor.const SimplexCategoryᵒᵖ).obj ↑X

The singular simplicial set of a totally disconnected space is the constant simplicial set.

Equations

• One or more equations did not get rendered due to their size.