module Cat.Diagram.Equaliser.RegularMono 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 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.

  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!