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

import Cat.Reasoning

module Cat.Diagram.Image where

module _ {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\to B$ be an ordinary function between sets (or, indeed, arbitrary types). Its image $\mathrm{im}f$ can be computed as the subset $\{b\in B:(\exists a)b=f(a)\}\text{,}$ but this description does not carry over to more general categories: More abstractly, we can say that the image embeds into $B\text{,}$ and admits a map from $A$ (in material set theory, this is $f$ itself — structurally, it is called the corestriction of $f\text{).}$ Furthermore, these two maps factor $f\text{,}$ 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\text{,}$ we could take $\mathrm{im}f=\mathbb{N}\text{,}$ taking $e=f$ itself and $m=\mathbb{N}\stackrel{\mathrm{id}}{\hookrightarrow }\mathbb{N}\text{.}$ This factoring clearly recovers $f\text{,}$ as $\mathrm{id}\circ f=f\text{.}$ 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 $\mathrm{im}f\stackrel{m}{\hookrightarrow }B$ to be the image of $f\text{,}$ it must be the smallest subobject of $B$ through which $f$ factors — given any other factoring of $f=m^{\prime }\circ e^{\prime }\text{,}$ we must have $m\subseteq m^{\prime }$ in the proset of subobjects of $B\text{,}$ i.e. there exists some $k$ such that $m=m^{\prime }\circ k\text{.}$

In general categories, monomorphisms of $\mathcal{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\text{.}$ We may expand the definition above to work for an arbitrary subclass $M\subseteq \mathrm{Mono}(\mathcal{C})$ of the monomorphisms of $C\text{,}$ by requiring that the $M\text{-image}$ of $f$ be the smallest $M\text{-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\to b\text{,}$ and consider it as an object of the slice category $\mathcal{C}/b\text{.}$

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

  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
    (Forget-full-subcat
      {C = Slice C b}
      {P = (λ o → M .fst (o .map))}) (cut f)

The image is the $M\text{-image}$ for $M$ = the class of all monomorphisms.

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

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\swarrow F\text{,}$ we have an object $(c,c\stackrel{m}{\hookrightarrow }b)$ — $c$ is the image object, and $m$ is the inclusion map:

    Im : Ob
    Im = im .bot .y .fst .domain

    Im→codomain : Hom Im b
    Im→codomain = im .bot .y .fst .map

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

    Im→codomain-is-M : M .fst Im→codomain
    Im→codomain-is-M = im .bot .y .snd

    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\text{:}$

    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\text{;}$ and,
• An $M\text{-monomorphism}$ $c\stackrel{m}{\hookrightarrow }b\text{;}$ and,
• A corestriction map $a\stackrel{i}{\to }c\text{;}$ such that
• $m\circ i=f\text{.}$

Then we have a map $k:\mathrm{im}f\to c$ (written im≤other-image in the code below), and the canonical inclusion $\mathrm{im}f\hookrightarrow B$ factors through $k\text{:}$

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

  module Image {a b} {f : Hom a b} (im : Image f) = M-Image {M = is-monic , λ x → x} im