hom_ext_yoneda — Mathlib

English

Two arrows between sheaves are equal if their precomposition with every Yoneda morphism is equal.

Русский

Две стрелки между оболочками равны, если их проскопирование по каждой Yoneda-стреле эквивалентно.

LaTeX

$$$\forall X\ p: J.yoneda.obj X ⟶ P,\ p ≫ f = p ≫ g \Rightarrow f = g$$$

Lean4

/-- Two morphisms of sheaves of types `P ⟶ Q` coincide if the precompositions with morphisms
`yoneda.obj X ⟶ P` agree.
-/
theorem hom_ext_yoneda {P Q : Sheaf J (Type v)} {f g : P ⟶ Q} (h : ∀ (X : C) (p : J.yoneda.obj X ⟶ P), p ≫ f = p ≫ g) :
    f = g := by
  ext X x
  simpa only [yonedaEquiv_comp, Equiv.apply_symm_apply] using congr_arg (J.yonedaEquiv) (h _ (J.yonedaEquiv.symm x))

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