module Cat.Diagram.Image {o β} (C : Precategory o β) where

open Cat.Reasoning C open Initial open βObj open βHom open /-Obj open /-Hom private variable a b : Ob β' : Level

# Imagesπ

Let
$f:AβB$
be an ordinary function between sets (or, indeed, arbitrary types). Its
**image**
$imf$
can be computed as the subset
${bβB:(βa)Βb=f(a)},$
but this description does not carry over to more general categories:
More abstractly, we can say that the image embeds into
$B,$
and admits a map from
$A$
(in material set theory, this is
$f$
itself β structurally, it is called the **corestriction**
of
$f).$
Furthermore, these two maps *factor*
$f,$
in that:

While these are indeed two necessary properties of an *image*,
they fail to accurately represent the set-theoretic construction:
Observe that, e.g.Β for
$f(x)=2x,$
we could take
$imf=N,$
taking
$e=f$
itself and
$m=NidβN.$
This factoring clearly recovers
$f,$
as
$idβf=f.$
But by taking this as the image, weβve lost the information that
$f$
lands in the evens!

We can refine the abstract definition by saying that, for a mono
$imfmβB$
to be *the* image of
$f,$
it must be the *smallest* subobject of
$B$
through which
$f$
factors β given any other factoring of
$f=m_{β²}βe_{β²},$
we must have
$mβm_{β²}$
in the proset of subobjects of
$B,$
i.e.Β there exists some
$k$
such that
$m=m_{β²}βk.$

In general categories, monomorphisms of
$C$
may be the wrong notion of βsubobjectβ to use. For example, in topology,
weβd rather talk about the image which admits a *subspace
inclusion* onto
$B.$
We may expand the definition above to work for an arbitrary subclass
$MβMono(C)$
of the monomorphisms of
$C,$
by requiring that the
$M-image$
of
$f$
be the smallest
$M-subobject$
through which
$f$
factors.

Since keeping track of all the factorisations by hand would be fiddly, we formalise the idea of image here using comma categories, namely the idea of universal morphisms as in the construction of adjoints. Fix a morphism $f:aβb,$ and consider it as an object of the slice category $C/b.$

For a given subclass of monomorphisms
$M,$
there is a full subcategory of
$C/b$
spanned by those maps in
$M$
β let us call it
$M/b$
β admitting an evident fully
faithful inclusion
$F:M/bβͺC/b.$
An
**$M-image$
of
$f$**
is a universal morphism from
$f$
to
$F.$

Class-of-monos : β β β Type _ Class-of-monos β = Ξ£[ M β (β {a b} β Hom a b β Type β) ] (β {a b} {f : Hom a b} β M f β is-monic f) M-image : β {a b} β Class-of-monos β' β Hom a b β Type _ M-image {a = a} {b} M f = Universal-morphism (cut f) (Forget-full-subcat {C = Slice C b} {P = (Ξ» o β M .fst (o .map))})

**The** image is the
$M-image$
for
$M$
= the class of all monomorphisms.

Image : β {a b} β Hom a b β Type _ Image {b = b} f = Universal-morphism (cut f) (Forget-full-subcat {C = Slice C b} {P = is-monic β map})

## Friendly interfaceπ

Since this definition is incredibly abstract and indirect, we provide
a very thin wrapper module over `M-image`

which unpacks the
definition into friendlier terms.

module M-Image {a b} {M : Class-of-monos β'} {f : Hom a b} (im : M-image M f) where

The first thing to notice is that, being an initial object in the comma category $fβF,$ we have an object $(c,cmβb)$ β $c$ is the image object, and $m$ is the inclusion map:

Im : Ob Im = im .bot .y .object .domain Imβcodomain : Hom Im b Imβcodomain = im .bot .y .object .map

Furthermore, this map is both an inclusion (since $M$ is a class of monomorphisms), and an $M-inclusion$ at that:

Imβcodomain-is-M : M .fst Imβcodomain Imβcodomain-is-M = im .bot .y .witness Imβcodomain-is-monic : is-monic Imβcodomain Imβcodomain-is-monic = M .snd Imβcodomain-is-M

So far, weβve been looking at the βcodomainβ part of the object in the comma category. We also have the βmorphismβ part, which provides our (universal) factoring of $f:$

corestrict : Hom a Im corestrict = im .bot .map .map image-factors : Imβcodomain β corestrict β‘ f image-factors = im .bot .map .commutes

This is also the *smallest* factorisation, which takes quite a
lot of data to express. Letβs see it:

Suppose we have

- Some other object $c;$ and,
- An $M-monomorphism$ $cmβb;$ and,
- A corestriction map $aiβc;$ such that
- $mβi=f.$

Then we have a map
$k:imfβc$
(written `imβ€other-image`

in the code
below), and the canonical inclusion
$imfβͺB$
factors through
$k:$

universal : β {c} (m : Hom c b) (M-m : M .fst m) (i : Hom a c) β m β i β‘ f β Hom Im c universal m M i p = im .hasβ₯ obj .centre .Ξ² .map where obj : βObj _ _ obj .x = tt obj .y = restrict (cut m) M obj .map = record { map = i ; commutes = p } universal-factors : β {c} {m : Hom c b} {M : M .fst m} {i : Hom a c} β {p : m β i β‘ f} β m β universal m M i p β‘ Imβcodomain universal-factors {m = m} {M} {i} {p} = im .hasβ₯ _ .centre .Ξ² .commutes universal-commutes : β {c} {m : Hom c b} {M : M .fst m} {i : Hom a c} β {p : m β i β‘ f} β universal m M i p β corestrict β‘ i universal-commutes {m = m} {ism} {i} {p} = M .snd ism _ _ (pulll universal-factors Β·Β· image-factors Β·Β· sym p)