English
From the universal property of a coequalizer, two arrows k,l: coequalizer f g → W are equal if and only if their compositions with the coequalizer projection π f g are equal; i.e., π f g ≫ k = π f g ≫ l implies k = l.
Русский
Из универсального свойства коэквалайзера следует, что две стрелки k,l: коэквалайзер f g → W равны тогда и только тогда, когда их композиции с проекцией коэквалайзера π f g равны; то есть π f g ≫ k = π f g ≫ l → k = l.
LaTeX
$$$ (\\operatorname{coequalizer}.\\pi f g) \\circ k = (\\operatorname{coequalizer}.\\pi f g) \\circ l \\; \\Rightarrow\\; k = l $$$
Lean4
/-- Two maps from a coequalizer are equal if they are equal when composed with the coequalizer
map -/
@[ext]
theorem hom_ext {W : C} {k l : coequalizer f g ⟶ W} (h : coequalizer.π f g ≫ k = coequalizer.π f g ≫ l) : k = l :=
Cofork.IsColimit.hom_ext (colimit.isColimit _) h
