open import Cat.Diagram.Equaliser.Kernel
open import Cat.Instances.Shape.Terminal
open import Cat.Functor.FullSubcategory
open import Cat.Diagram.Initial
open import Cat.Instances.Comma
open import Cat.Instances.Slice
open import Cat.Abelian.Base
open import Cat.Prelude

open /-Obj
open /-Hom
open βObj
open βHom

module Cat.Abelian.Images {o β} {C : Precategory o β} (A : is-abelian C) where
open is-abelian A


# Images in abelian categoriesπ

Let be a morphism in an abelian category which (by definition) admits a canonical decomposition as

where the map is epic, is monic, and the indicated isomorphism arises from in a canonical way, using the universal properties of kernels and cokernels. What we show in this section is that the arrow is an image factorisation for It is the largest monomorphism through which factors. Since this construction does not depend on any specificities of we conclude that every map in an abelian category factors as a regular epi followed by a regular mono.

## The imageπ

images : β {A B} (f : Hom A B) β Image f
images f = im where
the-img : βObj (const! (cut f)) Forget-full-subcat
the-img .x = tt
the-img .y .object = cut (Ker.kernel (Coker.coeq f))
the-img .y .witness {c} = kernels-are-subobjects C β _ (Ker.has-is-kernel _)


Break down as an epi followed by a mono We can take the map as the βimageβ subobject. We must provide a map filling the dotted line in

but this is the epimorphism in our factorisation. More precisely, itβs the epimorphism followed by the isomorphism in the decomposition

  the-img .map ./-Hom.map = decompose f .fst β Coker.coeq _
the-img .map ./-Hom.commutes = pulll (Ker.factors _) β Coker.factors _


## Universalityπ

Suppose that weβre given another decomposition of as

and we wish to construct a map 1, hence a map such that the triangle

commutes.

  im : Image f
im .Initial.bot = the-img
im .Initial.hasβ₯ other = contr factor unique where
factor : βHom (const! (cut f)) Forget-full-subcat the-img other
factor .Ξ± = tt
factor .Ξ² ./-Hom.map =
Coker.universal (Ker.kernel f) {e' = other .map .map} path
β coker-kerβker-coker f .is-invertible.inv


Observe that by the universal property of 2, if we have a map such that then we can obtain a (unique) map s.t. the triangle above commutes!

      where abstract
path : other .map .map β 0m β‘ other .map .map β kernel f .Kernel.kernel
path =
other .y .witness _ _ $sym$
pulll (other .map .commutes)
Β·Β· Ker.equal f
Β·Β· β.zero-βr _
Β·Β· 0m-unique
Β·Β· sym (apβ _β_ refl β-zero-r β β-zero-r)


To satisfy that equation, observe that since is monic, it suffices to show that but we have assumed that and by the definition of kernel. Some tedious isomorphism-algebra later, we have shown that is the image of

Hereβs the tedious isomorphism algebra.
    factor .Ξ² ./-Hom.commutes = invertibleβepic (coker-kerβker-coker f) _ _ $Coker.uniqueβ (Ker.kernel f) (sym (Ker.equal f β β .zero-βr _ β 0m-unique β sym β-zero-r)) (apβ _β_ ( sym (assoc _ _ _) β apβ _β_ refl (cancelr (coker-kerβker-coker f .is-invertible.invr))) refl β pullr (Coker.factors _) β other .map .commutes) (sym (decompose f .snd β assoc _ _ _)) factor .sq = /-Hom-path$ sym $other .y .witness _ _$
pulll (factor .Ξ² .commutes)
β the-img .map .commutes
Β·Β· sym (other .map .commutes)
Β·Β· ap (other .y .object .map β_) (intror refl)

unique : β x β factor β‘ x
unique x = βHom-path _ _ refl $/-Hom-path$ other .y .witness _ _ \$
sym (x .Ξ² .commutes β sym (factor .Ξ² .commutes))


1. this is an inequality in the poset of subobjects of which is a map in the slice over β©οΈ

2. hence of after adjusting by our old friendly isomorphismβ©οΈ