Lean4
/-- If `F : D ⥤ C` is a functor to an abelian category, `p : X ⟶ Y` is a morphisms
admitting a kernel such that `F` preserves this kernel and `F.map p` is an epi,
then `F.map Y` identifies to the cokernel of `F.map (kernel.ι p)`. -/
noncomputable def isColimitMapCoconeOfCokernelCoforkOfπ {X Y : D} (p : X ⟶ Y) [HasKernel p] (F : D ⥤ C)
[F.PreservesZeroMorphisms] [Epi (F.map p)] [PreservesLimit (parallelPair p 0) F] :
IsColimit (F.mapCocone (CokernelCofork.ofπ p (kernel.condition p))) :=
by
let e : parallelPair (kernel.ι p) 0 ⋙ F ≅ parallelPair (kernel.ι (F.map p)) 0 :=
parallelPair.ext (asIso (kernelComparison p F)) (Iso.refl _) (by simp) (by simp)
refine IsColimit.precomposeInvEquiv e _ ?_
let hp := Abelian.epiIsCokernelOfKernel _ (kernelIsKernel (F.map p))
refine IsColimit.ofIsoColimit hp (Cofork.ext (Iso.refl _) ?_)
change F.map p ≫ 𝟙 _ = 𝟙 _ ≫ F.map p
rw [Category.comp_id, Category.id_comp]
