stdSimplex

Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

URI: https://scilib.ai/kg/mathlib#SSet.stdSimplex

Lean4

/-- The functor `SimplexCategory ⥤ SSet` which sends `⦋n⦌` to the standard simplex `Δ[n]` is a
cosimplicial object in the category of simplicial sets. (This functor is essentially given by the
Yoneda embedding). -/
def stdSimplex : CosimplicialObject SSet.{u} :=
  uliftYoneda

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru