Topological simplices

We define the natural functor from SimplexCategory to TopCat sending ⦋n⦌ to the topological n-simplex. This is used to define TopCat.toSSet in AlgebraicTopology.SingularSet.

noncomputable def SimplexCategory.toTop₀ : CategoryTheory.CosimplicialObject TopCat

The functor SimplexCategory ⥤ TopCat.{0} associating the topological n-simplex to ⦋n⦌ : SimplexCategory.

@[simp]

theorem SimplexCategory.toTop₀_obj (n : SimplexCategory) : toTop₀.obj n = TopCat.of ↑(stdSimplex ℝ (Fin (n.len + 1)))

@[simp]

theorem SimplexCategory.toTop₀_map {X✝ Y✝ : SimplexCategory} (f : X✝ ⟶ Y✝) : toTop₀.map f = TopCat.ofHom { toFun := stdSimplex.map ⇑(CategoryTheory.ConcreteCategory.hom f), continuous_toFun := ⋯ }

noncomputable def SimplexCategory.toTop : CategoryTheory.Functor SimplexCategory TopCat

The functor SimplexCategory ⥤ TopCat.{u} associating the topological n-simplex to ⦋n⦌ : SimplexCategory.

@[simp]

theorem SimplexCategory.toTop_map {X✝ Y✝ : SimplexCategory} (f : X✝ ⟶ Y✝) : toTop.{u}.map f = TopCat.uliftFunctor.map (TopCat.ofHom { toFun := stdSimplex.map ⇑(CategoryTheory.ConcreteCategory.hom f), continuous_toFun := ⋯ })

@[simp]

theorem SimplexCategory.toTop_obj (X : SimplexCategory) : toTop.{u}.obj X = TopCat.uliftFunctor.obj (TopCat.of ↑(stdSimplex ℝ (Fin (X.len + 1))))

instance SimplexCategory.instNonemptyCarrierObjTopCatToTop₀ (n : SimplexCategory) : Nonempty ↑(toTop₀.obj n)

instance SimplexCategory.instNonemptyCarrierObjTopCatToTop (n : SimplexCategory) : Nonempty ↑(toTop.{u}.obj n)

@[implicit_reducible]

instance SimplexCategory.instUniqueCarrierObjTopCatToTop₀MkOfNatNat : Unique ↑(toTop₀.obj (mk 0))

@[implicit_reducible]

instance SimplexCategory.instUniqueCarrierObjTopCatToTopMkOfNatNat : Unique ↑(toTop.{u}.obj (mk 0))

instance SimplexCategory.instPathConnectedSpaceCarrierObjTopCatToTop₀ (n : SimplexCategory) : PathConnectedSpace ↑(toTop₀.obj n)

instance SimplexCategory.instPathConnectedSpaceCarrierObjTopCatToTop (n : SimplexCategory) : PathConnectedSpace ↑(toTop.{u}.obj n)