mathlib documentation


Topological simplices #

We define the natural functor from simplex_category to Top sending [n] to the topological n-simplex. This is used to define Top.to_sSet in algebraic_topology.simpliciaL_set.

The topological simplex associated to x : simplex_category. This is the object part of the functor simplex_category.to_Top.

Instances for simplex_category.to_Top_obj
theorem simplex_category.to_Top_obj.ext {x : simplex_category} (f g : (x.to_Top_obj)) :
f = gf = g

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

theorem simplex_category.coe_to_Top_map {x y : simplex_category} (f : x y) (g : (x.to_Top_obj)) (i : y) :
(simplex_category.to_Top_map f g) i = (finset.filter (λ (k : x), f k = i) finset.univ).sum (λ (j : x), g j)

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