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.

source

instance SimplexCategory.instFintypeObjSimplexCategoryToQuiverToCategoryStructSmallCategoryTypeToQuiverToCategoryStructTypesToPrefunctorForget (x : SimplexCategory) :

Fintype (CategoryTheory.ConcreteCategory.forget.obj x)

source

def SimplexCategory.toTopObj (x : SimplexCategory) :

Set ((CategoryTheory.forget SimplexCategory).obj x → NNReal)

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

Instances For

source

instance SimplexCategory.instCoeFunElemForAllObjSimplexCategoryToQuiverToCategoryStructSmallCategoryTypeToQuiverToCategoryStructTypesToPrefunctorForgetInstConcreteCategorySimplexCategorySmallCategoryNNRealToTopObj (x : SimplexCategory) :

CoeFun ↑(SimplexCategory.toTopObj x) fun x => (CategoryTheory.forget SimplexCategory).obj x → NNReal

source

theorem SimplexCategory.toTopObj.ext {x : SimplexCategory} (f : ↑(SimplexCategory.toTopObj x)) (g : ↑(SimplexCategory.toTopObj x)) :

↑f = ↑g → f = g

source

def SimplexCategory.toTopMap {x : SimplexCategory} {y : SimplexCategory} (f : x ⟶ y) :

↑(SimplexCategory.toTopObj x) → ↑(SimplexCategory.toTopObj y)

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

Instances For

source

@[simp]

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

source

theorem SimplexCategory.continuous_toTopMap {x : SimplexCategory} {y : SimplexCategory} (f : x ⟶ y) :

Continuous (SimplexCategory.toTopMap f)

source

@[simp]

theorem SimplexCategory.toTop_obj (x : SimplexCategory) :

SimplexCategory.toTop.obj x = TopCat.of ↑(SimplexCategory.toTopObj x)

source

@[simp]

theorem SimplexCategory.toTop_map_apply :

∀ {X Y : SimplexCategory} (f : X ⟶ Y) (a : ↑(SimplexCategory.toTopObj X)), ↑(SimplexCategory.toTop.map f) a = SimplexCategory.toTopMap f a

source

def SimplexCategory.toTop :

CategoryTheory.Functor SimplexCategory TopCat

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

Instances For