presheafHom_map_app_op_mk_id — Mathlib

English

A compatibility lemma describing how the map along g in presheafHom behaves when evaluated at an identity on Y.

Русский

Лемма совместимости для поведения отображения вдоль g в presheafHom при вычислении на идентичности на Y.

LaTeX

$$$((presheafHom F G).map g.op \alpha).app( op( Over.mk(id_Y) ) ) = \alpha .app( op( Over.mk(g) ) )$$$

Lean4

@[simp]
theorem presheafHom_map_app_op_mk_id {X Y : C} (g : Y ⟶ X) (α : (presheafHom F G).obj (op X)) :
    ((presheafHom F G).map g.op α).app (op (Over.mk (𝟙 Y))) = α.app (op (Over.mk g)) :=
  presheafHom_map_app (𝟙 Y) g g (by simp) α

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