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 C f
images f = im where
  the-img : ↓Obj (!Const (cut f)) Forget-full-subcat
  the-img .x = tt
  the-img .y .fst = cut (Ker.kernel (Coker.coeq f))
  the-img .y .snd {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 C 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 .snd _ _ $ 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 .snd _ _ $
      pulll (factor .Ξ² .commutes)
      βˆ™ the-img .map .commutes
      Β·Β· sym (other .map .commutes)
      ·· ap (other .y .fst .map ∘_) (intror refl)

    unique : βˆ€ x β†’ factor ≑ x
    unique x = ↓Hom-path _ _ refl $ /-Hom-path $ other .y .snd _ _ $
      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β†©οΈŽ