obj_map_id — Mathlib

English

For any objects X,Y in the category and any morphism f: op X ⟶ op Y, the action of the Yoneda functor on f composed with the identity at X equals the application of yoneda.map to f.unop at (op Y) on the identity at Y.

Русский

Для любых X,Y и любого морфизма f: op X ⟶ op Y выполнено равенство: (yoneda.obj X).map f (id X) = (yoneda.map f.unop).app (op Y) (id Y).

LaTeX

$$$ (\mathrm{yoneda.obj} X).\mathrm{map} f (\mathrm{id}_X) = (\mathrm{yoneda.map} f^{\mathrm{unop}}).\mathrm{app}(\mathrm{op} Y)(\mathrm{id}_Y) $$$

Lean4

theorem obj_map_id {X Y : C} (f : op X ⟶ op Y) : (yoneda.obj X).map f (𝟙 X) = (yoneda.map f.unop).app (op Y) (𝟙 Y) := by
  simp

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