yonedaEquiv_yoneda_map

Mathlib.CategoryTheory.Yoneda

URI: https://scilib.ai/kg/mathlib#CategoryTheory.yonedaEquiv_yoneda_map

English

Yoneda equivalence sends a Yoneda map to the underlying morphism.

Русский

Эквивалентность Ёнеды отправляет карту Ёнеды на исходный морфизм.

LaTeX

$$$ yonedaEquiv (yoneda.map f) = f $$$

Lean4

theorem yonedaEquiv_yoneda_map {X Y : C} (f : X ⟶ Y) : yonedaEquiv (yoneda.map f) = f :=
  by
  rw [yonedaEquiv_apply]
  simp

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

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

Разделы

Аффилиация

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