map_yonedaEquiv — Mathlib

English

Variant expressing how YonedaEquiv interacts with strict maps: F.map g^op (yonedaEquiv f) equals f.val.app (op Y) g for f : J.yoneda.obj X ⟶ F and g: Y ⟶ X.

Русский

Вариант, выражающий взаимодействие YonedaEquiv с отображениями: F.map g^op (yonedaEquiv f) = f.app (op Y) g.

LaTeX

$$$F.map\ g^{op}\ (J.yonedaEquiv\ f) = f.app\ (op\ Y)\ g$$$

Lean4

/-- See also `map_yonedaEquiv'` for a more general version. -/
theorem map_yonedaEquiv {X Y : C} {F : Sheaf J (Type v)} (f : J.yoneda.obj X ⟶ F) (g : Y ⟶ X) :
    F.val.map g.op (J.yonedaEquiv f) = f.val.app (op Y) g := by
  rw [yonedaEquiv_naturality, yonedaEquiv_comp, yonedaEquiv_yoneda_map]

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