Theorems · Definition · category theory

CategoryTheory.Abelian.coimageIsoImage

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X Y : C} → (f : X ⟶ Y) → CategoryTheory.Abelian.coimage f ≅ CategoryTheory.Abelian.image f

There is a canonical isomorphism between the abelian coimage and the abelian image of a morphism.

Defined in

Mathlib.CategoryTheory.Abelian.Basic

Cited by

3 results in Mathlib

Foundations

Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian