monoIsKernelOfCokernel — Mathlib

Lean4

/-- In a `NonPreadditiveAbelian` category, a mono is the kernel of its cokernel. More precisely:
If `f` is a monomorphism and `s` is some colimit cokernel cocone on `f`, then `f` is a kernel
of `Cofork.π s`. -/
def monoIsKernelOfCokernel [Mono f] (s : Cofork f 0) (h : IsColimit s) :
    IsLimit (KernelFork.ofι f (CokernelCofork.condition s)) :=
  IsKernel.isoKernel _ _
    (kernel.ofCompIso _ _ (Limits.IsColimit.coconePointUniqueUpToIso h (colimit.isColimit _))
      (CoconeMorphism.w (Limits.IsColimit.uniqueUpToIso h <| colimit.isColimit _).hom _))
    (asIso <| Abelian.factorThruImage f) (Abelian.image.fac f)

Похожие утверждения