English
Let f,g: X → Y be morphisms in a category with HasEqualizer f g. The object underlying the subobject equalizerSubobject f g is isomorphic to the actual equalizer object; there exists a canonical isomorphism equalizerSubobject f g ≅ equalizer f g.
Русский
Пусть f,g: X → Y — морфизмы в категории, где задан эквалайзер. Объект подподобъекта equalizerSubobject f g изоморфен фактическому объекту эквалайзера равенств; существует канонические изоморфизм равенизера equalizerSubobject f g ≅ equalizer f g.
LaTeX
$$$$(equalizerSubobject f g : C) \\cong equalizer f g$$$$
Lean4
/-- The underlying object of `equalizerSubobject f g` is (up to isomorphism!)
the same as the chosen object `equalizer f g`. -/
def equalizerSubobjectIso : (equalizerSubobject f g : C) ≅ equalizer f g :=
Subobject.underlyingIso (equalizer.ι f g)
