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 where

module _ {o β} (C : Precategory o β) where
open Cat.Reasoning C
private variable a b : Ob


# 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 diagrammatically about objects directly involved in the definition.

The definition is as follows: A regular monomorphism is an equaliser of some pair of arrows

  record is-regular-mono (f : Hom a b) : Type (o β β) where
no-eta-equality
field
{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 _ has-is-eq

open is-regular-mono using (is-regular-monoβis-mono) public


## Effective monomorphismsπ

Proving that a map is a regular monomorphism involves finding two maps which it equalises, but if is a category with pushouts, there is often a canonical choice: The cokernel pair of that is, the pushout of 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
no-eta-equality
field
{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 has a cokernel pair, and it is a regular monomorphism, then it is also effective β it is the equaliser of its cokernel pair.

module _ {o β} (C : Precategory o β) where
open Cat.Reasoning C
open Initial
open βObj
open βHom
open /-Obj
open /-Hom

  is-regular-monoβis-effective-mono
: β {a b} {f : Hom a b}
β Pushout C f f
β is-regular-mono C f
β is-effective-mono C f
is-regular-monoβis-effective-mono {f = f} cokern reg = mon where
module fβf = Pushout cokern
module reg = is-regular-mono reg


Let be the equaliser of By the universal property of the cokernel pair of we have a map such that and

    phi : Hom fβf.coapex reg.c
phi = fβf.universal reg.equal

open is-effective-mono
mon : is-effective-mono C f
mon .cokernel = fβf.coapex
mon .iβ = fβf.iβ
mon .iβ = fβf.iβ
mon .is-cokernel-pair = fβf.has-is-po
mon .has-is-equaliser = eq where


To show that also has the universal property of the equaliser of suppose that also equalises the injections. Then we can calculate:

So equalises the same arrows that does, hence there is a universal map which commutes with βeverything in sightβ:

      open is-equaliser
eq : is-equaliser _ _ _ _
eq .equal     = fβf.square
eq .universal {F = F} {e' = e'} p = reg.universal p' where
p' : reg.arrβ β e' β‘ reg.arrβ β e'
p' =
reg.arrβ β e'       β‘Λβ¨ ap (_β e') fβf.universalβiβ β©β‘Λ
(phi β fβf.iβ) β e' β‘β¨ extendr p β©β‘
(phi β fβf.iβ) β e' β‘β¨ ap (_β e') fβf.universalβiβ β©β‘
reg.arrβ β e'       β
eq .factors = reg.factors
eq .unique = reg.unique


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

  equalises-cokernel-pairβis-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 C 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 be an effective mono, or, in a category with pushouts, a regular mono. We show that admits an image relative to the class of regular monomorphisms. The construction of the image is as follows: We let and factor as

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

  is-effective-monoβimage
: β {a b} {f : Hom a b}
β is-effective-mono C f
β M-image C (is-regular-mono C , is-regular-monoβis-mono) f
is-effective-monoβimage {f = f} mon = im where
module eff = is-effective-mono mon

itself : βObj _ _
itself .x = tt
itself .y = cut f , eff.is-effective-monoβ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 = trivial!

unique : β x β hom β‘ x
unique x = βHom-path _ _ refl
(ext (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!