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.

def Simplicial.«term|_|» : Lean.ParserDescr

The geometric realization of a simplicial set.

noncomputable def sSetTopAdj : SSet.toTop ⊣ TopCat.toSSet

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

instance instIsLeftAdjointSSetTopCatToTop : SSet.toTop.IsLeftAdjoint

instance instIsRightAdjointSSetTopCatToSSet : TopCat.toSSet.IsRightAdjoint

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.