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

The topological simplex associated to x : SimplexCategory. This is the object part of the functor SimplexCategory.toTop.

Instances For

    A morphism in SimplexCategory induces a map on the associated topological spaces.

    Instances For
      theorem SimplexCategory.coe_toTopMap {x : SimplexCategory} {y : SimplexCategory} (f : x y) (g : ↑(SimplexCategory.toTopObj x)) (i : (CategoryTheory.forget SimplexCategory).obj y) :
      ↑(SimplexCategory.toTopMap f g) i = Finset.sum (Finset.filter (fun k => f k = i) Finset.univ) fun j => g j

      The functor associating the topological n-simplex to [n] : SimplexCategory.

      Instances For