The abelian image and coimage.

In an abelian category we usually want the image of a morphism f to be defined as kernel (cokernel.π f), and the coimage to be defined as cokernel (kernel.ι f).

We make these definitions here, as Abelian.image f and Abelian.coimage f (without assuming the category is actually abelian), and later relate these to the usual categorical notions when in an abelian category.

There is a canonical morphism coimageImageComparison : Abelian.coimage f ⟶ Abelian.image f. Later we show that this is always an isomorphism in an abelian category, and conversely a category with (co)kernels and finite products in which this morphism is always an isomorphism is an abelian category.

@[inline, reducible]

abbrev CategoryTheory.Abelian.image {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] {P : C} {Q : C} (f : P ⟶ Q) : C

The kernel of the cokernel of f is called the (abelian) image of f.

@[inline, reducible]

abbrev CategoryTheory.Abelian.image.ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] {P : C} {Q : C} (f : P ⟶ Q) : CategoryTheory.Abelian.image f ⟶ Q

The inclusion of the image into the codomain.

@[inline, reducible]

abbrev CategoryTheory.Abelian.factorThruImage {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] {P : C} {Q : C} (f : P ⟶ Q) : P ⟶ CategoryTheory.Abelian.image f

There is a canonical epimorphism p : P ⟶ image f for every f.

theorem CategoryTheory.Abelian.image.fac {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] {P : C} {Q : C} (f : P ⟶ Q) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.factorThruImage f) (CategoryTheory.Abelian.image.ι f) = f

f factors through its image via the canonical morphism p.

instance CategoryTheory.Abelian.mono_factorThruImage {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] {P : C} {Q : C} (f : P ⟶ Q) [CategoryTheory.Mono f] : CategoryTheory.Mono (CategoryTheory.Abelian.factorThruImage f)

@[inline, reducible]

abbrev CategoryTheory.Abelian.coimage {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] {P : C} {Q : C} (f : P ⟶ Q) : C

The cokernel of the kernel of f is called the (abelian) coimage of f.

@[inline, reducible]

abbrev CategoryTheory.Abelian.coimage.π {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] {P : C} {Q : C} (f : P ⟶ Q) : P ⟶ CategoryTheory.Abelian.coimage f

The projection onto the coimage.

@[inline, reducible]

abbrev CategoryTheory.Abelian.factorThruCoimage {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] {P : C} {Q : C} (f : P ⟶ Q) : CategoryTheory.Abelian.coimage f ⟶ Q

There is a canonical monomorphism i : coimage f ⟶ Q.

theorem CategoryTheory.Abelian.coimage.fac {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] {P : C} {Q : C} (f : P ⟶ Q) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimage.π f) (CategoryTheory.Abelian.factorThruCoimage f) = f

f factors through its coimage via the canonical morphism p.

instance CategoryTheory.Abelian.epi_factorThruCoimage {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] {P : C} {Q : C} (f : P ⟶ Q) [CategoryTheory.Epi f] : CategoryTheory.Epi (CategoryTheory.Abelian.factorThruCoimage f)

def CategoryTheory.Abelian.coimageImageComparison {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] {P : C} {Q : C} (f : P ⟶ Q) : 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.

See https://stacks.math.columbia.edu/tag/0107

def CategoryTheory.Abelian.coimageImageComparison' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] {P : C} {Q : C} (f : P ⟶ Q) : CategoryTheory.Abelian.coimage f ⟶ CategoryTheory.Abelian.image f

An alternative formulation of the canonical map from the abelian coimage to the abelian image.

theorem CategoryTheory.Abelian.coimageImageComparison_eq_coimageImageComparison' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] {P : C} {Q : C} (f : P ⟶ Q) : CategoryTheory.Abelian.coimageImageComparison f = CategoryTheory.Abelian.coimageImageComparison' f

@[simp]

theorem CategoryTheory.Abelian.coimage_image_factorisation_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] {P : C} {Q : C} (f : P ⟶ Q) {Z : C} (h : Q ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimage.π f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimageImageComparison f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.image.ι f) h)) = CategoryTheory.CategoryStruct.comp f h

@[simp]

theorem CategoryTheory.Abelian.coimage_image_factorisation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] {P : C} {Q : C} (f : P ⟶ Q) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimage.π f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimageImageComparison f) (CategoryTheory.Abelian.image.ι f)) = f