open import Cat.Functor.FullSubcategory
open import Cat.Diagram.Initial
open import Cat.Functor.Adjoint
open import Cat.Instances.Comma
open import Cat.Instances.Slice
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Reasoning

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


Let f:ABf : A \to B be an ordinary function between sets (or, indeed, arbitrary types). Its image imf\im f can be computed as the subset {bB:(a) b=f(a)}\{ b \in B : (\exists 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 BB, and admits a map from AA (in material set theory, this is ff itself — structurally, it is called the corestriction of ff). Furthermore, these two maps factor ff, in that:

(AeimfmB)=(AfB) (A \xto{e} \im f \xmono{m} B) = (A \xto{f} B)

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)=2xf(x) = 2x, we could take imf=N\im f = \bb{N}, taking e=fe = f itself and m=NidNm = \bb{N} \xmono{\id{id}} \bb{N}. This factoring clearly recovers ff, as idf=f\id{id} \circ f = f. But by taking this as the image, we’ve lost the information that ff lands in the evens!

We can refine the abstract definition by saying that, for a mono imfmB\im f \xmono{m} B to be the image of ff, it must be the smallest subobject of BB through which ff factors — given any other factoring of f=mef = m' \circ e', we must have mmm \sube m' in the proset of subobjects of BB, i.e. there exists some kk such that m=mkm = m' \circ k.

In general categories, monomorphisms of C\ca{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 BB. We may expand the definition above to work for an arbitrary subclass MMono(C)M \sube \id{Mono}(\ca{C}) of the monomorphisms of CC, by requiring that the MM-image of ff be the smallest MM-subobject through which ff 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:abf : a \to b, and consider it as an object of the slice category C/b\ca{C}/b.

For a given subclass of monomorphisms MM, there is a full subcategory of C/b\ca{C}/b spanned by those maps in MM — let us call it M/bM/b — admitting an evident ff inclusion F:M/bC/bF : M/b \mono \ca{C}/b. An MM-image of ff is a universal morphism from ff to FF.

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)
    {C = Slice C b}
    {P =  o  M .fst (o .map))})

The image is the MM-image for MM = 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 fFf \swarrow F, we have an object (c,cmb)(c, c \xmono{m} b)cc is the image object, and mm 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 MM is a class of monomorphisms), and an MM-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 ff:

  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 cc; and,
  • An MM-monomorphism cmbc \xmono{m} b; and,
  • A corestriction map aica \xto{i} c; such that
  • mi=fm \circ i = f.

Then we have a map k:imfck : \im f \to c (written im≤other-image in the code below), and the canonical inclusion imfB\im f \mono B factors through kk:

    :  {c} (m : Hom c b) (M-m : M .fst m) (i : Hom a c)
     m  i  f
     Hom Im c
  im≤other-image m M i p = im .has⊥ obj .centre .β .map where
    obj : ↓Obj _ _
    obj .x = tt
    obj .y = cut m , M
    obj .map = record { map = i ; commutes = p }

    :  {c} {m : Hom c b} {M : M .fst m} {i : Hom a c}
     {p : m  i  f}
     m  im≤other-image m M i p  Im→codomain
  im≤other-image-factors {m = m} {M} {i} {p} = im .has⊥ _ .centre .β .commutes