yonedaEquiv_symm_app_apply — Mathlib

English

For x in the sheaf at op X, the symmetric Yoneda equivalence yields the expected evaluation on X via the symmetrized map.

Русский

Для x из слоя в op X симметрическая эквивалентность Ёнеде возвращает искомую оценку на X через симметрированную карту.

LaTeX

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

Lean4

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

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