yonedaEquiv_apply — Mathlib

English

Given f: J.yoneda.obj X ⟶ F, the Yoneda-equivalence sends f to its evaluation at X on the identity morphism.

Русский

Дано f: J.yoneda.obj X ⟶ F, отображение Канонической Эквивалентности отправляет f на его значение на X по единичному морфизму.

LaTeX

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

Lean4

theorem yonedaEquiv_apply {X : C} {F : Sheaf J (Type v)} (f : J.yoneda.obj X ⟶ F) :
    yonedaEquiv J f = f.val.app (op X) (𝟙 X) :=
  rfl

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