English
Let f,g: X → Y be morphisms. The canonical projection from the coequalizer of f and g, followed by the canonical isomorphism to the quotiented type, coincides with the universal coequalizing map. In other words, the composite π_f,g followed by the coequalizer isomorphism equals the universal quotient map mk_f,g.
Русский
Пусть f,g: X → Y — морфизмы. Каноническая проекция коэквалентa f,g, затем каноническое изоморфирование к фактору по отношению эквивалентности, совпадают с универсальной коэквалентной связью. Проще говоря, композиция π_f,g с изоморфизмом коэквалентности равна канонической факторной мапе mk_f,g.
LaTeX
$$$\\pi_{f,g} \\;\\circ\\; (\\mathrm{coequalizerInclusion}(f,g))\\_{{\\mathrm{hom}}} = \\mathrm{Function.Coequalizer.mk}\\ f\\ g$$
Lean4
@[elementwise (attr := simp)]
theorem coequalizerIso_π_comp_hom : coequalizer.π f g ≫ (coequalizerIso f g).hom = Function.Coequalizer.mk f g :=
colimit.isoColimitCocone_ι_hom (coequalizerColimit f g) WalkingParallelPair.one
