English
The map on cokernels respects the iso on hom, i.e., G.map (cokernel.π f) followed by the iso hom component equals cokernel.π (G.map f).
Русский
Отображение G коэквалайзера в сочетании с хамом изоморфизма равно cokernel.π для отображенного f.
LaTeX
$$$G\\ maps\\ (cokernel.\\pi\\; f) \\;\\circ\\; (\\mathrm{PreservesCokernel.iso}\\; G f).hom = cokernel.\\pi (G.map f)$$$
Lean4
/-- The map of a cokernel cofork is a colimit iff
the cokernel cofork consisting of the mapped morphisms is a colimit.
This essentially lets us commute `CokernelCofork.ofπ` with `Functor.mapCocone`.
This is a variant of `isColimitMapCoconeCoforkEquiv` for equalizers,
which we can't use directly between `G.map 0 = 0` does not hold definitionally.
-/
def isColimitMapCoconeCoforkEquiv' :
IsColimit (G.mapCocone (CokernelCofork.ofπ h w)) ≃
IsColimit
(CokernelCofork.ofπ (G.map h) (by simp only [← G.map_comp, w, Functor.map_zero]) : Cofork (G.map f) 0) :=
CokernelCofork.isColimitMapCoconeEquiv _ _
