The topological simplices and the singular simplices of a space

The topological n-simplex is a standard simplex on a finite nonempty type, up to a universe lift, hence contractible and in particular simply connected. This file also names its initial vertex, and the continuous map on the topological n-simplex that underlies a singular n-simplex of a space.

Main declarations

• SimplexCategory.toTopInitialVertex: the initial vertex of the topological n-simplex.
• TauCeti.TopCat.simplexMap: the continuous map underlying a singular simplex.

instance SimplexCategory.contractibleSpace (n : SimplexCategory) : ContractibleSpace ↑(toTop.{u}.obj n)

Every topological simplex is contractible, being a universe lift of a standard simplex on a finite nonempty type.

noncomputable def SimplexCategory.toTopInitialVertex (n : SimplexCategory) : ↑(toTop.{u}.obj n)

The initial vertex of the topological n-simplex: the universe lift of the standard-simplex vertex StdSimplex.single 0.

Equations

• n.toTopInitialVertex = { down := Convexity.StdSimplex.single 0 }

@[simp]

theorem SimplexCategory.toTopInitialVertex_down (n : SimplexCategory) : n.toTopInitialVertex.down = Convexity.StdSimplex.single 0

The initial vertex of the topological n-simplex lifts the standard-simplex vertex StdSimplex.single 0.

noncomputable def TauCeti.TopCat.simplexMap {X : TopCat} {n : SimplexCategoryᵒᵖ} (σ : (TopCat.toSSet.obj X).obj n) : C(↑(SimplexCategory.toTop.{u}.obj (Opposite.unop n)), ↑X)

The continuous map underlying a singular simplex, defined on the topological simplex SimplexCategory.toTop.obj n.unop rather than on the unlifted model used by TopCat.toSSetObjEquiv, so that it composes directly with the maps SimplexCategory.toTop.map.

Equations

• TauCeti.TopCat.simplexMap σ = TopCat.Hom.hom σ.down

@[simp]

theorem TauCeti.TopCat.simplexMap_map {X : TopCat} {m n : SimplexCategoryᵒᵖ} (α : m ⟶ n) (σ : (TopCat.toSSet.obj X).obj m) : simplexMap ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.obj X).map α)) σ) = (simplexMap σ).comp (TopCat.Hom.hom (SimplexCategory.toTop.{u}.map α.unop))

Reindexing a singular simplex precomposes the underlying continuous map with the induced map of topological simplices.

@[simp]

theorem TauCeti.TopCat.simplexMap_app {X Y : TopCat} {n : SimplexCategoryᵒᵖ} (f : X ⟶ Y) (σ : (TopCat.toSSet.obj X).obj n) : simplexMap ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map f).app n)) σ) = (TopCat.Hom.hom f).comp (simplexMap σ)

Pushing a singular simplex forward along a continuous map postcomposes the underlying continuous map with that map.