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\mathcal{A}, which (by definition) admits a canonical decomposition as

Aβ† pcoker⁑(ker⁑f)β‰…ker⁑(coker⁑f)β†ͺiB, A \xtwoheadrightarrow{p} \operatorname{coker}(\ker f) \cong \ker (\operatorname{coker}f) \xhookrightarrow{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 (\operatorname{coker}f) \hookrightarrow B is an image factorisation 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 \twoheadrightarrow \ker (\operatorname{coker}f) followed by a mono i:ker⁑(coker⁑f)β†ͺBi : \ker (\operatorname{coker}f) \hookrightarrow 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 \xtwoheadrightarrow{p} \operatorname{coker}(\ker f) \xrightarrow{f'} \ker (\operatorname{coker}f) \xhookrightarrow{i} B\text{.}

  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 ff as

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

and we wish to construct a map g:i′≀ig : i' \le i1, hence a map im⁑fβ†’X\operatorname*{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.universal (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)\operatorname{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\operatorname{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 (\operatorname{coker}f) \hookrightarrow 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)
        (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 BB, which is a map iβ€²β†’ii' \to i in the slice over BB.β†©οΈŽ

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