module Cat.Regular.Image
  {o β„“} {C : Precategory o β„“}
  (reg : is-regular C)
  where

Images in regular categoriesπŸ”—

This module provides tools for working with the image factorisation of morphisms in regular categories, regarded as subobjects of the map’s codomain. We start by defining a Subobject of standing for whenever

Im : βˆ€ {x y} (f : Hom x y) β†’ Subobject y
Im f .domain = _
Im f .map    = factor f .forget
Im f .monic  = out! (factor f .forget∈M)

We may then use this to rephrase the universal property of as the initial subobject through which factors.

Im-universal
  : βˆ€ {x y} (f : Hom x y)
  β†’ (m : Subobject y) {e : Hom x (m .domain)}
  β†’ f ≑ m .map ∘ e
  β†’ Im f β‰€β‚˜ m
Im-universal f m {e = e} p = r where
  the-lift = out! {pa = is-strong-epi-is-prop C _} (factor f .mediate∈E) .snd
    record { Subobject m } (sym (factor f .factors) βˆ™ p)

  r : _ β‰€β‚˜ _
  r .map = the-lift .centre .fst
  r .sq  = idl _ βˆ™ sym (the-lift .centre .snd .snd)

An important fact that will be used in calculating associativity for relations in regular categories is that precomposing with a strong epimorphism preserves images. Intuitively, this is because a strong epimorphism expresses as a quotient, but this decomposition does not alter the image of a map

image-pre-cover
  : βˆ€ {a b c}
  β†’ (f : Hom b c)
  β†’ (g : Hom a b)
  β†’ is-strong-epi C g
  β†’ (Im f) Sub.β‰… (Im (f ∘ g))
image-pre-cover {a = a} {b} {c} f g g-covers = Sub-antisym imf≀imfg imfg≀imf where
  imfg≀imf : Im (f ∘ g) β‰€β‚˜ Im f
  imfg≀imf = Im-universal _ _ (pushl (factor f .factors))

  the-lift : Σ (Hom b im[ f ∘ g ]) _
  the-lift = g-covers .snd
    (β‰€β‚˜β†’mono imfg≀imf)
    {factor (f ∘ g) .mediate}
    {factor f .mediate}
    (out! (factor f .forget∈M) _ _ (sym (pulll (sym (imfg≀imf .sq) βˆ™ idl _) βˆ™ sym (factor (f ∘ g) .factors) βˆ™ pushl (factor f .factors)))) .centre

  inverse : is-invertible (imfg≀imf .map)
  inverse = is-strong-epiβ†’is-extremal-epi C (out! {pa = is-strong-epi-is-prop C _} (factor f .mediate∈E))
    (β‰€β‚˜β†’mono imfg≀imf) (the-lift .fst) (sym (the-lift .snd .snd))

  imf≀imfg : Im f β‰€β‚˜ Im (f ∘ g)
  imf≀imfg .map = inverse .is-invertible.inv
  imf≀imfg .sq = invertibleβ†’epic inverse _ _ $
    pullr (sym (imfg≀imf .sq) βˆ™ idl _)
    βˆ™ sym (cancelr (inverse .is-invertible.invr) βˆ™ introl refl)