open import Cat.Functor.FullSubcategory
open import Cat.Diagram.Equaliser
open import Cat.Diagram.Initial
open import Cat.Diagram.Pushout
open import Cat.Instances.Comma
open import Cat.Instances.Slice
open import Cat.Diagram.Image
open import Cat.Prelude

import Cat.Reasoning

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

Regular monomorphismsπŸ”—

A regular monomorphism is a morphism that behaves like an embedding, i.e.Β it is an isomorphism onto its image. Since images of arbitrary morphisms do not exist in every category, we must find a definition which implies this property but only speaks diagramatically about objects directly involved in the definition.

The definition is as follows: A regular monomorphism f:aβ†ͺbf : a \mono b is an equaliser of some pair of arrows g,h:bβ†’cg, h : b \to c.

record is-regular-mono (f : Hom a b) : Type (o βŠ” β„“) where
    {c}       : Ob
    arr₁ arrβ‚‚ : Hom b c
    has-is-eq : is-equaliser C arr₁ arrβ‚‚ f

  open is-equaliser has-is-eq public

From the definition we can directly conclude that regular monomorphisms are in fact monomorphisms:

  is-regular-mono→is-mono : is-monic f
  is-regular-mono→is-mono = is-equaliser→is-monic C _ has-is-eq

open is-regular-mono using (is-regular-mono→is-mono) public

Effective epimorphismsπŸ”—

Proving that a map ff is a regular monomorphism involves finding two maps which it equalises, but if C\ca{C} is a category with pushouts, there is often a canonical choice: The cokernel pair of ff, that is, the pushout of ff along with itself. Morphisms which a) have a cokernel pair and b) equalise their cokernel pair are called effective monomorphisms.

record is-effective-mono (f : Hom a b) : Type (o βŠ” β„“) where
    {cokernel}       : Ob
    i₁ iβ‚‚            : Hom b cokernel
    is-cokernel-pair : is-pushout C f i₁ f iβ‚‚
    has-is-equaliser : is-equaliser C i₁ iβ‚‚ f

Every effective monomorphism is a regular monomorphism, since it equalises the inclusions of its cokernel pair.

  is-effective-mono→is-regular-mono : is-regular-mono f
  is-effective-mono→is-regular-mono = rm where
    open is-regular-mono
    rm : is-regular-mono f
    rm .c = _
    rm .arr₁ = _
    rm .arrβ‚‚ = _
    rm .has-is-eq = has-is-equaliser

If ff has a cokernel pair, and it is a regular monomorphism, then it is also effective β€” it is the equaliser of its cokernel pair.

  : βˆ€ {a b} {f : Hom a b}
  β†’ Pushout C f f
  β†’ is-regular-mono f
  β†’ is-effective-mono f
is-regular-mono→is-effective-mono {f = f} cokern reg = eff where
  module fβŠ”f = Pushout cokern
  module reg = is-regular-mono reg

Let f:aβ†ͺbf : a \mono b be the equaliser of arr1,arr2:bβ†’c\id{arr_1}, \id{arr_2} : b \to c. By the universal property of the cokernel pair of ff, we have a map Ο•:BβŠ”ABβ†’C\phi : B \sqcup_A B \to C such that Ο•βˆ˜i1=arr1\phi \circ i_1 = \id{arr_1} and Ο•βˆ˜i2=arr2\phi \circ i_2 = \id{arr_2}.

  phi : Hom fβŠ”f.coapex reg.c
  phi = fβŠ”f.colimiting reg.equal

  open is-effective-mono
  eff : is-effective-mono f
  eff .cokernel = fβŠ”f.coapex
  eff .i₁ = fβŠ”f.i₁
  eff .iβ‚‚ = fβŠ”f.iβ‚‚
  eff .is-cokernel-pair = fβŠ”f.has-is-po
  eff .has-is-equaliser = eq where

To show that ff also has the universal property of the equaliser of i1,i2i_1, i_2, suppose that e′:E→be\prime : E \to b also equalises the injections. Then we can calulate:

arr1eβ€²=(Ο•i1)eβ€²=(Ο•i2)eβ€²=arr2eβ€² \id{arr_1}e\prime = (\phi i_1)e\prime = (\phi i_2)e\prime = \id{arr_2}e\prime

So eβ€²e\prime equalises the same arrows that ff does, hence there is a universal map Eβ†’aE \to a which commutes with β€œeverything in sight”:

    open is-equaliser
    eq : is-equaliser _ _ _ _
    eq .equal     = fβŠ”f.square
    eq .limiting {F = F} {eβ€² = eβ€²} p = reg.limiting pβ€² where
      pβ€² : reg.arr₁ ∘ eβ€² ≑ reg.arrβ‚‚ ∘ eβ€²
      pβ€² =
        reg.arr₁ ∘ eβ€²       β‰‘Λ˜βŸ¨ ap (_∘ eβ€²) fβŠ”f.iβ‚βˆ˜colimiting βŸ©β‰‘Λ˜
        (phi ∘ fβŠ”f.i₁) ∘ eβ€² β‰‘βŸ¨ extendr p βŸ©β‰‘
        (phi ∘ fβŠ”f.iβ‚‚) ∘ eβ€² β‰‘βŸ¨ ap (_∘ eβ€²) fβŠ”f.iβ‚‚βˆ˜colimiting βŸ©β‰‘
        reg.arrβ‚‚ ∘ eβ€²       ∎
    eq .universal = reg.universal
    eq .unique = reg.unique

If f:A→Bf : A \to B has a canonical choice of pushout along itself, then it suffices to check that it equalises those injections to show it is an effective mono.

  : βˆ€ {a b} {f : Hom a b}
  β†’ (P : Pushout C f f)
  β†’ is-equaliser C (P .Pushout.i₁) (P .Pushout.iβ‚‚) f
  β†’ is-effective-mono f
equalises-cokernel-pair→is-effective-mono P eq = em where
  open is-effective-mono
  em : is-effective-mono _
  em .cokernel = _
  em .i₁ = _
  em .iβ‚‚ = _
  em .is-cokernel-pair = P .Pushout.has-is-po
  em .has-is-equaliser = eq

Images of regular monosπŸ”—

Let f:Aβ†ͺBf : A \mono B be an effective mono, or, in a category with pushouts, a regular mono. We show that ff admits an image relative to the class of regular monomorphisms. The construction of the image is as follows: We let im⁑f=A\im f = A and factor ff as

Aβ†’idAβ†ͺfB A \xto{\id{id}} A \xmono{f} B

This factorisation is very straightforwardly shown to be universal, as the code below demonstrates.

  : βˆ€ {a b} {f : Hom a b}
  β†’ is-effective-mono f
  → M-image C (is-regular-mono , is-regular-mono→is-mono) f
is-effective-mono→image {f = f} eff = im where
  module eff = is-effective-mono eff

  itself : ↓Obj _ _
  itself .x = tt
  itself .y = cut f ,→is-regular-mono
  itself .map = record { map = id ; commutes = idr _ }

  im : Initial _
  im .bot = itself
  im .hasβŠ₯ other = contr hom unique where
    hom : ↓Hom _ _ itself other
    hom .Ξ± = tt
    hom .Ξ² = other .map
    hom .sq = /-Hom-path refl

    unique : βˆ€ x β†’ hom ≑ x
    unique x = ↓Hom-path _ _ refl
      (/-Hom-path (intror refl βˆ™ ap map (x .sq) βˆ™ elimr refl))

Hence the characterisation of regular monomorphisms given in the introductory paragraph: In a category with pushouts, every regular monomorphism β€œis an isomorphism” onto its image. In reality, it gives its own image!