Equalizers
Def Equalizer
In any category
e.g.
- In
, given functions , their equalizer is the injection into of the equationally defined subset . Since if for some , then for all . Then there is a unique with such that as is monic.
Prop In any category
Prop
Prop Given a set
Proof Let set
Prop Write
Proof Inherit the notation from the above proof, clearly we can derive that
Prop In any category
Proof Suppose
Prop In the category
Coequalizers
Def Coequalizer
For any parallel morphisms That is, given any
Prop If
Proof Observe by duality, we know that such a coequalizer
e.g.
-
Let
be an equivalence relation on a set with are the two projections of the inclusion . The canonical projection defined by is then a coequalizer: - The coequalizer in
of an arbitrary parallel pair of functions can be constructed by quotienting by the equivalence relation generated by the equations for all .
- The coequalizer in
Prop For every monoid