mathlib documentation

algebraic_topology.topological_simplex

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.

Equations
Instances for simplex_category.to_Top_obj
@[ext]

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

Equations
@[simp]
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.

Equations