module Cat.Diagram.Equaliser {β β'} (C : Precategory β β') where
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 (β β β') 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 (β β β') 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:
is-equaliserβis-monic : β {E} (equ : Hom E A) β is-equaliser 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
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 : Type _ has-equalisers = β {a b} (f g : Hom a b) β Equaliser f g module Equalisers (all-equalisers : has-equalisers) where 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