# 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.

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.

## Instances For

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

## Instances For

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)

## Instances For

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