Lean4
/-- If `F : D ⥤ C` is a functor to an abelian category, `i : X ⟶ Y` is a morphism
admitting a cokernel such that `F` preserves this cokernel and `F.map i` is a mono,
then `F.map X` identifies to the kernel of `F.map (cokernel.π i)`. -/
noncomputable def isLimitMapConeOfKernelForkOfι {X Y : D} (i : X ⟶ Y) [HasCokernel i] (F : D ⥤ C)
[F.PreservesZeroMorphisms] [Mono (F.map i)] [PreservesColimit (parallelPair i 0) F] :
IsLimit (F.mapCone (KernelFork.ofι i (cokernel.condition i))) :=
by
let e : parallelPair (cokernel.π (F.map i)) 0 ≅ parallelPair (cokernel.π i) 0 ⋙ F :=
parallelPair.ext (Iso.refl _) (asIso (cokernelComparison i F)) (by simp) (by simp)
refine IsLimit.postcomposeInvEquiv e _ ?_
let hi := Abelian.monoIsKernelOfCokernel _ (cokernelIsCokernel (F.map i))
refine IsLimit.ofIsoLimit hi (Fork.ext (Iso.refl _) ?_)
change 𝟙 _ ≫ F.map i ≫ 𝟙 _ = F.map i
rw [Category.comp_id, Category.id_comp]
