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

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 = ∑ (j : x) in finset.filter (λ (k : x), f k = i) finset.univ, g j

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

Equations