yonedaEquiv_symm_map — Mathlib

English

The symmetric variant of YonedaEquiv map: symm maps commute with application of mapped morphisms on Y.

Русский

Симметричный вариант карты Yoneda: симм-коммутирует с применением отображений.

LaTeX

$$$J.yonedaEquiv.symm\ x \\circ f = J.yonedaEquiv.symm (f.\val.app { unop := X } x)$$$

Lean4

theorem yonedaEquiv_symm_map {X Y : Cᵒᵖ} (f : X ⟶ Y) {F : Sheaf J (Type v)} (t : F.val.obj X) :
    J.yonedaEquiv.symm (F.val.map f t) = J.yoneda.map f.unop ≫ J.yonedaEquiv.symm t :=
  by
  obtain ⟨u, rfl⟩ := J.yonedaEquiv.surjective t
  rw [yonedaEquiv_naturality', Equiv.symm_apply_apply, Equiv.symm_apply_apply]

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