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

ImagesπŸ”—

Let be an ordinary function between sets (or, indeed, arbitrary types). Its image can be computed as the subset but this description does not carry over to more general categories: More abstractly, we can say that the image embeds into and admits a map from (in material set theory, this is itself β€” structurally, it is called the corestriction of Furthermore, these two maps factor 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 we could take taking itself and This factoring clearly recovers as But by taking this as the image, we’ve lost the information that lands in the evens!

We can refine the abstract definition by saying that, for a mono to be the image of it must be the smallest subobject of through which factors β€” given any other factoring of we must have in the proset of subobjects of i.e.Β there exists some such that

In general categories, monomorphisms of 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 We may expand the definition above to work for an arbitrary subclass of the monomorphisms of by requiring that the of be the smallest through which 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 and consider it as an object of the slice category

For a given subclass of monomorphisms there is a full subcategory of spanned by those maps in β€” let us call it β€” admitting an evident fully faithful inclusion An of is a universal morphism from to

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 for = 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 we have an object β€” is the image object, and 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 is a class of monomorphisms), and an 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

  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 and,
  • An and,
  • A corestriction map such that

Then we have a map (written im≀other-image in the code below), and the canonical inclusion factors through

  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)