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

Images in abelian categoriesπŸ”—

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

Aβ† pcoker⁑(ker⁑f)β‰…ker⁑(coker⁑f)β†ͺ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⁑(coker⁑f)β†ͺ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:Aβ† ker⁑(coker⁑f)p : A \epi \ker (\coker f) followed by a mono i:ker⁑(coker⁑f)β†ͺ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 fβ€²f' in the decomposition

Aβ† pcoker⁑(ker⁑f)β†’fβ€²ker⁑(coker⁑f)β†ͺ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

Aβ†’qXβ†ͺiβ€²BΓ—, A \xto{q} X \mono{i'} B\times{,}

and we wish to construct a map g:i′≀ig : i' \le i1, hence a map im⁑fβ†’X\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⁑(ker⁑f)\coker (\ker f)2, if we have a map q:Aβ†’Xq : A \to X such that 0=qker⁑f0 = q\ker f, then we can obtain a (unique) map coker⁑(ker⁑f)β†’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 iβ€²i' is monic, it suffices to show that iβ€²0=iβ€²qker⁑fi'0 = i'q\ker f, but we have assumed that iβ€²q=fi'q = f, and fker⁑f=0f\ker f = 0 by the definition of kernel. Some tedious isomorphism-algebra later, we have shown that ker⁑(coker⁑f)β†ͺ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 iβ€²β†’ii' \to i in the slice over BB.β†©οΈŽ

  2. hence of ker⁑(coker⁑f)\ker (\coker f), after adjusting by our old friendly isomorphismβ†©οΈŽ