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 $f : A \to B$ be a morphism in an abelian category $\mathcal{A}$, which (by definition) admits a canonical decomposition as

$A \xtwoheadrightarrow{p} \operatorname{coker}(\ker f) \cong \ker (\operatorname{coker}f) \xhookrightarrow{i} B\text{,}$

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

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

$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 $f$ as

$A \xrightarrow{q} X \hookrightarrow{i'} B\times{,}$

and we wish to construct a map $g : i' \le i$1, hence a map $\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 $\operatorname{coker}(\ker f)$2, if we have a map $q : A \to X$ such that $0 = q\ker f$, then we can obtain a (unique) map $\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'$ is monic, it suffices to show that $i'0 = i'q\ker f$, but we have assumed that $i'q = f$, and $f\ker f = 0$ by the definition of kernel. Some tedious isomorphism-algebra later, we have shown that $\ker (\operatorname{coker}f) \hookrightarrow B$ is the image of $f$.

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 $B$, which is a map $i' \to i$ in the slice over $B$.β©οΈ

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