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 n-simplices which identify to continuous maps stdSimplex ℝ (Fin (n + 1)) → X, where stdSimplex ℝ (Fin (n + 1)) is the standard topological n-simplex, defined as the subtype of Fin (n + 1) → ℝ consisting of functions f such that 0 ≤ f i for all i and ∑ i, f i = 1.

The geometric realization functor SSet.toTop 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 (@joelriou)

• Show that the singular simplicial set is a Kan complex.
• Show the adjunction sSetTopAdj is a Quillen equivalence.

noncomputable def TopCat.toSSet : CategoryTheory.Functor TopCat SSet

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

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

noncomputable def TopCat.toSSetObjEquiv (X : TopCat) (n : SimplexCategoryᵒᵖ) : (toSSet.obj X).obj n ≃ C(↑(stdSimplex ℝ (Fin ((Opposite.unop n).len + 1))), ↑X)

If X : TopCat.{u} and n : SimplexCategoryᵒᵖ, then (toSSet.obj X).obj n identifies to the type of continuous maps from the standard simplex stdSimplex ℝ (Fin (n.unop.len + 1)) to X.

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.

noncomputable def sSetTopAdj : SSet.toTop ⊣ TopCat.toSSet

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

noncomputable def SSet.toTopSimplex : CategoryTheory.Functor.comp stdSimplex toTop ≅ SimplexCategory.toTop.{u}

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

instance instIsLeftKanExtensionSimplexCategoryTopCatSSetToTopInvFunctorToTopSimplex : SSet.toTop.IsLeftKanExtension SSet.toTopSimplex.inv

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.