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 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 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 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 .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 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 .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))