presheaf_map_apply_coe — Mathlib

English

The underlying function of the presheaf map equals the action map on sections: the coe of the presheaf map evaluated at x coincides with M.map f x.

Русский

Функция отображения прешефа совпадает с отображением на секциях: коэффициент отображения на x равен M.map f x.

LaTeX

$$$\mathrm{coe}\ ((M.presheaf.map\ f)\hom\ x) = M.map\ f\ x.$$$

Lean4

@[simp]
theorem presheaf_map_apply_coe {X Y : Cᵒᵖ} (f : X ⟶ Y) (x : M.obj X) :
    DFunLike.coe (α := M.obj X) (β := fun _ ↦ M.obj Y) (M.presheaf.map f).hom x = M.map f x :=
  rfl

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