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.

@[implicit_reducible]

noncomputable def SimplexCategory.toTop₀ : CategoryTheory.CosimplicialObject TopCat

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

Equations

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

@[simp]

theorem SimplexCategory.toTop₀_obj (n : SimplexCategory) : toTop₀.obj n = ↧(Convexity.StdSimplex ℝ (Fin (n.len + 1)))

@[simp]

theorem SimplexCategory.toTop₀_map {X✝ Y✝ : SimplexCategory} (f : X✝ ⟶ Y✝) : toTop₀.map f = TopCat.ofHom { toFun := Convexity.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.

Equations

• SimplexCategory.toTop.{?u.1} = CategoryTheory.Functor.comp SimplexCategory.toTop₀ TopCat.uliftFunctor

@[simp]

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

@[simp]

theorem SimplexCategory.toTop_obj (X : SimplexCategory) : toTop.{u}.obj X = TopCat.uliftFunctor.obj ↧(Convexity.StdSimplex ℝ (Fin (X.len + 1)))

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

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

@[instance_reducible]

noncomputable instance SimplexCategory.instUniqueCarrierObjTopCatToTop₀MkOfNatNat : Unique ↑(toTop₀.obj { len := 0 })

Equations

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

@[instance_reducible]

noncomputable instance SimplexCategory.instUniqueCarrierObjTopCatToTopMkOfNatNat : Unique ↑(toTop.{u}.obj { len := 0 })

Equations

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

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

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