Documentation

Mathlib.AlgebraicTopology.TopologicalSimplex

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.

instance SimplexCategory.instFintypeObjForget (x : SimplexCategory) :
Fintype (CategoryTheory.ConcreteCategory.forget.obj x)
Equations

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

Equations
Equations
  • x.instCoeFunElemForallObjForgetNNRealToTopObj = { coe := fun (f : x.toTopObj) => f }
theorem SimplexCategory.toTopObj.ext {x : SimplexCategory} (f g : x.toTopObj) :
f = gf = g
def SimplexCategory.toTopMap {x y : SimplexCategory} (f : x y) (g : x.toTopObj) :
y.toTopObj

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem SimplexCategory.coe_toTopMap {x y : SimplexCategory} (f : x y) (g : x.toTopObj) (i : (CategoryTheory.forget SimplexCategory).obj y) :
(SimplexCategory.toTopMap f g) i = jFinset.filter (fun (x_1 : (CategoryTheory.forget SimplexCategory).obj x) => f x_1 = i) Finset.univ, g j

The functor 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_map {X✝ Y✝ : SimplexCategory} (f : X✝ Y✝) :
SimplexCategory.toTop.map f = { toFun := SimplexCategory.toTopMap f, continuous_toFun := }