Theorems · Definition · category theory

CategoryTheory.Abelian.coimageImageComparison

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} →
        (f : P ⟶ Q) →
          [inst_2 : CategoryTheory.Limits.HasCokernel f] →
            [inst_3 : CategoryTheory.Limits.HasKernel f] →
              [inst_4 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] →
                [inst_5 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] →
                  CategoryTheory.Abelian.coimage f ⟶ CategoryTheory.Abelian.image f

The canonical map from the abelian coimage to the abelian image. In any abelian category this is an isomorphism. Conversely, any additive category with kernels and cokernels and in which this is always an isomorphism, is abelian.

Defined in

Mathlib.CategoryTheory.Abelian.Images

Cited by

18 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsCategoryTheory.Limits.HasCokernelCategoryTheory.Limits.HasKernelCategoryTheory.Limits.HasKernelCategoryTheory.Limits.HasCokernel