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

ImagesπŸ”—

Let f:Aβ†’Bf : A \to B be an ordinary function between sets (or, indeed, arbitrary types). Its image im⁑f\im f can be computed as the subset {b∈B:(βˆƒ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:

(Aβ†’eim⁑fβ†ͺmB)=(Aβ†’fB) (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 im⁑f=N\im f = \bb{N}, taking e=fe = f itself and m=Nβ†ͺidNm = \bb{N} \xmono{\id{id}} \bb{N}. This factoring clearly recovers ff, as id∘f=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 im⁑fβ†ͺmB\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=mβ€²βˆ˜eβ€²f = m' \circ e', we must have mβŠ†mβ€²m \sube m' in the proset of subobjects of BB, i.e.Β there exists some kk such that m=mβ€²βˆ˜km = 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 MβŠ†Mono(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:a→bf : 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/bβ†ͺC/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)
  (Forget-full-subcat
    {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 f↙Ff \swarrow F, we have an object (c,cβ†ͺmb)(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 cβ†ͺmbc \xmono{m} b; and,
  • A corestriction map aβ†’ica \xto{i} c; such that
  • m∘i=fm \circ i = f.

Then we have a map k:im⁑fβ†’ck : \im f \to c (written im≀other-image in the code below), and the canonical inclusion im⁑fβ†ͺB\im f \mono B factors through kk:

  im≀other-image
    : βˆ€ {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 }

  im≀other-image-factors
    : βˆ€ {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