yonedaEquiv_apply

Mathlib.CategoryTheory.Yoneda

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

English

For any f, yonedaEquiv f equals the evaluation at (op X) of f on the identity morphism.

Русский

Для любого f, yonedaEquiv f равно применению f к (op X) на единичный морфизм.

LaTeX

$$$ yonedaEquiv f = f.(op X)(\\mathrm{id}_X) $$$

Lean4

theorem yonedaEquiv_apply {X : C} {F : Cᵒᵖ ⥤ Type v₁} (f : yoneda.obj X ⟶ F) : yonedaEquiv f = f.app (op X) (𝟙 X) :=
  rfl

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

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

Разделы

Аффилиация

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