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

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 (@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.

Equations

• TopCat.toSSet = CategoryTheory.Presheaf.restrictedULiftYoneda SimplexCategory.toTop.{?u.6}

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.

Equations

• X.toSSetObjEquiv n = Equiv.ulift.trans (CategoryTheory.ConcreteCategory.homEquiv.trans (Homeomorph.ulift.continuousMapCongr (Homeomorph.refl ↑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.

Equations

• SSet.toTop = CategoryTheory.Functor.leftKanExtension SSet.stdSimplex SimplexCategory.toTop.{?u.6}

noncomputable def sSetTopAdj : SSet.toTop ⊣ TopCat.toSSet

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

Equations

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

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.

Equations

• SSet.toTopSimplex = CategoryTheory.Presheaf.isExtensionAlongULiftYoneda SimplexCategory.toTop.{?u.14}

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.

Equations

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