abelianImageToKernelIsKernel — Mathlib

Lean4

/-- `Abelian.image S.f` is the kernel of `kernel.ι S.g ≫ cokernel.π S.f` -/
noncomputable def abelianImageToKernelIsKernel :
    IsLimit (KernelFork.ofι S.abelianImageToKernel S.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π) :=
  KernelFork.IsLimit.ofι _ _ (fun k hk => kernel.lift _ (k ≫ kernel.ι S.g) (by rw [assoc, hk]))
    (fun k hk => by simp only [← cancel_mono (kernel.ι S.g), assoc, abelianImageToKernel_comp_kernel_ι, kernel.lift_ι])
    (fun k hk b hb => by
      simp only [← cancel_mono S.abelianImageToKernel, ← cancel_mono (kernel.ι S.g), hb, assoc,
        abelianImageToKernel_comp_kernel_ι, kernel.lift_ι])

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