yonedaEquiv_symm_app_apply

Mathlib.CategoryTheory.Yoneda

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

← MathLib Explorer

English

The symmetric side evaluates to F.map on the given morphism.

Русский

Симметричная сторона вычисляется как F.map на данного морфизма.

LaTeX

$$$ (yonedaEquiv.symm x).app Y f = F.map f.op x $$$

Lean4

@[simp]
theorem yonedaEquiv_symm_app_apply {X : C} {F : Cᵒᵖ ⥤ Type v₁} (x : F.obj (op X)) (Y : Cᵒᵖ) (f : Y.unop ⟶ X) :
    (yonedaEquiv.symm x).app Y f = F.map f.op x :=
  rfl

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

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

Разделы

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

Аффилиация

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