toPresheaf_map_app_apply — Mathlib

English

Two morphisms between presheaves of modules are equal if their components agree; Extensionality principle for presheaf morphisms

Русский

Два морфизма между прешефами модулей равны, если их компоненты совпадают; принцип экстенсивности для морфизмов прешефов.

LaTeX

$$$\text{If } f.app X = g.app X \text{ for all } X, \text{ then } f = g.$$$

Lean4

@[simp]
theorem toPresheaf_map_app_apply (f : M₁ ⟶ M₂) (X : Cᵒᵖ) (x : M₁.obj X) :
    DFunLike.coe (α := M₁.obj X) (β := fun _ ↦ M₂.obj X) (((toPresheaf R).map f).app X).hom x = f.app X x :=
  rfl

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