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
.
instance
SimplexCategory.instFintypeObjSimplexCategoryToQuiverToCategoryStructSmallCategoryTypeToQuiverToCategoryStructTypesToPrefunctorForget
(x : SimplexCategory)
:
Fintype (CategoryTheory.ConcreteCategory.forget.obj x)
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
instance
SimplexCategory.instCoeFunElemForAllObjSimplexCategoryToQuiverToCategoryStructSmallCategoryTypeToQuiverToCategoryStructTypesToPrefunctorForgetInstConcreteCategorySimplexCategorySmallCategoryNNRealToTopObj
(x : SimplexCategory)
:
CoeFun ↑(SimplexCategory.toTopObj x) fun x => (CategoryTheory.forget SimplexCategory).obj x → NNReal
theorem
SimplexCategory.toTopObj.ext
{x : SimplexCategory}
(f : ↑(SimplexCategory.toTopObj x))
(g : ↑(SimplexCategory.toTopObj x))
:
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
@[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
theorem
SimplexCategory.continuous_toTopMap
{x : SimplexCategory}
{y : SimplexCategory}
(f : x ⟶ y)
:
@[simp]
theorem
SimplexCategory.toTop_obj
(x : SimplexCategory)
:
SimplexCategory.toTop.obj x = TopCat.of ↑(SimplexCategory.toTopObj x)
@[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
The functor associating the topological n
-simplex to [n] : SimplexCategory
.