open import Cat.Prelude

import Cat.Reasoning

module Cat.Diagram.Equaliser where

module _ {o β} (C : Precategory o β) where
open Cat.Reasoning C
private variable
A B : Ob
f g h : Hom A B


# Equalisersπ

The equaliser of two maps when it exists, represents the largest subobject of where and agree. In this sense, the equaliser is the categorical generalisation of a solution set: The solution set of an equation in one variable is largest subset of the domain (i.e.Β what the variable ranges over) where the left- and right-hand-sides agree.

  record is-equaliser {E} (f g : Hom A B) (equ : Hom E A) : Type (o β β) where
field
equal     : f β equ β‘ g β equ
universal : β {F} {e' : Hom F A} (p : f β e' β‘ g β e') β Hom F E
factors   : β {F} {e' : Hom F A} {p : f β e' β‘ g β e'} β equ β universal p β‘ e'
unique
: β {F} {e' : Hom F A} {p : f β e' β‘ g β e'} {other : Hom F E}
β equ β other β‘ e'
β other β‘ universal p

equal-β : f β equ β h β‘ g β equ β h
equal-β {h = h} =
f β equ β h β‘β¨ extendl equal β©β‘
g β equ β h β

uniqueβ
: β {F} {e' : Hom F A}  {o1 o2 : Hom F E}
β f β e' β‘ g β e'
β equ β o1 β‘ e'
β equ β o2 β‘ e'
β o1 β‘ o2
uniqueβ p q r = unique {p = p} q β sym (unique r)


We can visualise the situation using the commutative diagram below:

There is also a convenient bundling of an equalising arrow together with its domain:

  record Equaliser (f g : Hom A B) : Type (o β β) where
field
{apex}  : Ob
equ     : Hom apex A
has-is-eq : is-equaliser f g equ

open is-equaliser has-is-eq public


## Equalisers are monicπ

As a small initial application, we prove that equaliser arrows are always monic:

module _ {o β} {C : Precategory o β} where
open Cat.Reasoning C
private variable
A B : Ob
f g h : Hom A B

  is-equaliserβis-monic
: β {E} (equ : Hom E A)
β is-equaliser C f g equ
β is-monic equ
is-equaliserβis-monic equ equalises g h p =
uniqueβ (extendl equal) p refl
where open is-equaliser equalises


## Uniquenessπ

As universal constructions, equalisers are unique up to isomorphism. The proof follows the usual pattern: if both equalise then we can construct maps between and via the universal property of equalisers, and uniqueness ensures that these maps form an isomorphism.

  is-equaliserβiso
: {E E' : Ob}
β {e : Hom E A} {e' : Hom E' A}
β is-equaliser C f g e
β is-equaliser C f g e'
β E β E'
is-equaliserβiso {e = e} {e' = e'} eq eq' =
make-iso (eq' .universal (eq .equal)) (eq .universal (eq' .equal))
(uniqueβ eq' (eq' .equal) (pulll (eq' .factors) β eq .factors) (idr _))
(uniqueβ eq (eq .equal) (pulll (eq .factors) β eq' .factors) (idr _))
where open is-equaliser


## Properties of equalisersπ

The equaliser of the pair always exists, and is given by the identity map

  id-is-equaliser : is-equaliser C f f id
id-is-equaliser .is-equaliser.equal = refl
id-is-equaliser .is-equaliser.universal {e' = e'} _ = e'
id-is-equaliser .is-equaliser.factors = idl _
id-is-equaliser .is-equaliser.unique p = sym (idl _) β p


If is an equaliser and an epimorphism, then is an iso.

  equaliser+epiβinvertible
: β {E} {e : Hom E A}
β is-equaliser C f g e
β is-epic e
β is-invertible e


Suppose that equalises some pair By definition, this means that however, is an epi, so This in turn means that can be extended into a map via the universal property of and universality ensures that this extension is an isomorphism!

  equaliser+epiβinvertible {f = f} {g = g} {e = e} e-equaliser e-epi =
make-invertible
(universal {e' = id} (apβ _β_ fβ‘g refl))
factors
(uniqueβ (apβ _β_ fβ‘g refl) (pulll factors) id-comm)
where
open is-equaliser e-equaliser
fβ‘g : f β‘ g
fβ‘g = e-epi f g equal


# Categories with all equalisersπ

We also define a helper module for working with categories that have equalisers of all parallel pairs of morphisms.

has-equalisers : β {o β} β Precategory o β β Type _
has-equalisers C = β {a b} (f g : Hom a b) β Equaliser C f g
where open Precategory C

module Equalisers
{o β}
(C : Precategory o β)
(all-equalisers : has-equalisers C)
where
open Cat.Reasoning C
module equaliser {a b} (f g : Hom a b) = Equaliser (all-equalisers f g)

Equ : β {a b} (f g : Hom a b) β Ob
Equ = equaliser.apex