instIsIsoCoimageImageComparison — Mathlib

English

The coimage–image isomorphism exists for all morphisms, with explicit construction via image and coimage factorizations.

Русский

Сопоставление кообраза и образа существует для всех морфизмов; построение через факторизации образа и кообраза.

LaTeX

$$$$ \\text{IsIso}(\\operatorname{coimageImageComparison} f) $$$$

Lean4

/-- The coimage-image comparison morphism is always an isomorphism in an abelian category.
See `CategoryTheory.Abelian.ofCoimageImageComparisonIsIso` for the converse.
-/
instance : IsIso (coimageImageComparison f) :=
  by
  convert
    Iso.isIso_hom
      (IsImage.isoExt (coimageStrongEpiMonoFactorisation f).toMonoIsImage
        (imageStrongEpiMonoFactorisation f).toMonoIsImage)
  ext
  change _ = _ ≫ (imageStrongEpiMonoFactorisation f).m
  simp [-imageStrongEpiMonoFactorisation_m]

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