isLimitImage' — Mathlib

English

In an abelian category, exactness is equivalent to the equality image Subobject f = kernel Subobject g.

Русский

В абелевой категории точность эквивалентна равенству подобраза образа f и ядра g.

LaTeX

$$$S.Exact \\iff imageSubobject S.f = kernelSubobject S.g$$$

Lean4

/-- If `(f, g)` is exact, then `image.ι f` is a kernel of `g`. -/
def isLimitImage' (h : S.Exact) :
    IsLimit (KernelFork.ofι (Limits.image.ι S.f) (image_ι_comp_eq_zero S.zero) : KernelFork S.g) :=
  IsKernel.isoKernel _ _ h.isLimitImage (Abelian.imageIsoImage S.f).symm <| IsImage.lift_fac _ _

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