toSSet

Mathlib.AlgebraicTopology.SingularSet

URI: https://scilib.ai/kg/mathlib#TopCat.toSSet

Lean4

/-- 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} ⦋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. -/
noncomputable def toSSet : TopCat.{u} ⥤ SSet.{u} :=
  Presheaf.restrictedULiftYoneda.{0} SimplexCategory.toTop.{u}

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru