English
Two morphisms of presheaves f, g: P ⟶ Q are equal if their precompositions with all Yoneda morphisms yoneda.obj X ⟶ P agree; i.e., if for every X and p: yoneda.obj X ⟶ P one has p ≫ f = p ≫ g, then f = g.
Русский
Два морфизма прешпхеафов f, g: P ⟶ Q равны, если их предподобления по всем морфизмам Ёнеда yoneda.obj X ⟶ P совпадают; то есть если для каждого X и p: yoneda.obj X ⟶ P выполняется p ≫ f = p ≫ g, то f = g.
LaTeX
$$$\forall X, \forall p:\ yoneda.obj X ⟶ P,\ p \circ f = p \circ g \Rightarrow f = g$$$
Lean4
/-- Two morphisms of presheaves of types `P ⟶ Q` coincide if the precompositions
with morphisms `yoneda.obj X ⟶ P` agree. -/
theorem hom_ext_yoneda {P Q : Cᵒᵖ ⥤ Type v₁} {f g : P ⟶ Q} (h : ∀ (X : C) (p : 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 (yonedaEquiv) (h _ (yonedaEquiv.symm x))
