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

Images in abelian categories🔗

Let f:ABf : A \to B be a morphism in an abelian category A\ca{A}, which (by definition) admits a canonical decomposition as

Apcoker(kerf)ker(cokerf)iB, A \xepi{p} \coker (\ker f) \cong \ker (\coker f) \xmono{i} B\text{,}

where the map pp is epic, ii is monic, and the indicated isomorphism arises from ff in a canonical way, using the universal properties of kernels and cokernels. What we show in this section is that the arrow ker(cokerf)B\ker (\coker f) \mono B is an image for ff: It is the largest monomorphism through which ff factors. Since this construction does not depend on any specificities of ff, 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 ff down as an epi p:Aker(cokerf)p : A \epi \ker (\coker f) followed by a mono i:ker(cokerf)Bi : \ker (\coker f) \mono B. We can take the map ii as the “image” subobject. We must provide a map filling the dotted line in

but this is the epimorphism pp in our factorisation. More precisely, it’s the epimorphism pp followed by the isomorphism ff' in the decomposition

Apcoker(kerf)fker(cokerf)iB. A \xepi{p} \coker (\ker f) \xto{f'} \ker (\coker f) \xmono{i} B\text{.}

  the-img .map ./-Hom.map = decompose f .fst  Coker.coeq _
  the-img .map ./-Hom.commutes = pulll (Ker.universal _)  Coker.universal _

Universality🔗

Suppose that we’re given another decomposition of ff as

AqXiB×, A \xto{q} X \mono{i'} B\times{,}

and we wish to construct a map g:iig : i' \le i1, hence a map imfX\im f \to X 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.coequalise (Ker.kernel f) {e′ = other .map .map} path
       coker-ker≃ker-coker f .is-invertible.inv

Observe that by the universal property of coker(kerf)\coker (\ker f)2, if we have a map q:AXq : A \to X such that 0=qkerf0 = q\ker f, then we can obtain a (unique) map coker(kerf)X\coker (\ker f) \to X 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 ii' is monic, it suffices to show that i0=iqkerfi'0 = i'q\ker f, but we have assumed that iq=fi'q = f, and fkerf=0f\ker f = 0 by the definition of kernel. Some tedious isomorphism-algebra later, we have shown that ker(cokerf)B\ker (\coker f) \mono B is the image of ff.

Here’s the tedious isomorphism algebra.
    factor .β ./-Hom.commutes = invertible→epic (coker-ker≃ker-coker f) _ _ $
      Coker.unique₂ (Ker.kernel f) {e′ = f}
        {p = sym (Ker.equal f  ∅.zero-∘r _  0m-unique  sym ∘-zero-r)}
        (sym ( ap₂ _∘_ ( sym (assoc _ _ _)
                         ap₂ _∘_ refl (cancelr
                          (coker-ker≃ker-coker f .is-invertible.invr))) refl
               pullr (Coker.universal _)  other .map .commutes))
        (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 BB, which is a map iii' \to i in the slice over BB.↩︎

  2. hence of ker(cokerf)\ker (\coker f), after adjusting by our old friendly isomorphism↩︎