yonedaEquiv_map

Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

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

← MathLib Explorer

English

The map sending stdSimplex.obj n to X and back via yonedaEquiv commutes with stdSimplex.map.

Русский

Отображение, связанное с yonedaEquiv, commute с stdSimplex.map.

LaTeX

$$$\yonedaEquiv\_map(f) = \text{..., identity ...}$$$

Lean4

theorem yonedaEquiv_map {n m : SimplexCategory} (f : n ⟶ m) : yonedaEquiv.{u} (stdSimplex.map f) = objEquiv.symm f :=
  yonedaEquiv.symm.injective rfl

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

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

Разделы

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

Аффилиация

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