English
Let C be an Abelian category. For any two parallel morphisms f,g: X → Y there exists an equalizer e: E → X with f ∘ e = g ∘ e, and this equalizer is universal: for any z: Z → X with f ∘ z = g ∘ z there exists a unique u: Z → E such that z = e ∘ u.
Русский
Пусть C — абелева категория. Для любых двух параллельных морфизмов f,g: X → Y существует равнитель e: E → X с условием f ∘ e = g ∘ e, причем для любого z: Z → X с f ∘ z = g ∘ z существует единственный u: Z → E такой, что z = e ∘ u.
LaTeX
$$$\\\\forall X,Y \\\\in \\\\mathrm{Obj}(C), \\\\forall f,g: X \\\\to Y, \\\\exists E, e: E \\\\to X, \\\\ f \\\\circ e = g \\\\circ e \\\\land \\\\forall Z, z: Z \\\\to X, \\\\ f \\\\circ z = g \\\\circ z \\\\Rightarrow \\\\exists! u: Z \\\\to E, \\\\ z = e \\\\circ u.$$$
Lean4
instance (priority := 100) hasEqualizers : HasEqualizers C :=
Preadditive.hasEqualizers_of_hasKernels
