nLab
equalizer

Contents

Definition

In category theory

An equalizer is a limit

eqexgfy\operatorname{eq}\underset{\quad e \quad}{\to}x\underoverset{\quad g \quad}{f}{\rightrightarrows}y

over a parallel pair i.e. of the diagram of the shape

{xgfy}.\left\lbrace x \underoverset{\quad g \quad}{f}{\rightrightarrows} y \right\rbrace.

(See also fork diagram).

This means that for f:xyf : x \to y and g:xyg : x \to y two parallel morphisms in a category CC, their equalizer is, if it exists

The dual concept is that of coequalizer.

In type theory

In type theory the equalizer

PAgfBP \to A \stackrel{\overset{f}{\longrightarrow}}{\underset{g}{\longrightarrow}} B

is given by the dependent sum over the dependent equality type

P a:A(f(a)=g(a)).P \simeq \sum_{a : A} (f(a) = g(a)).

Examples

Properties

Proposition

A category has equalizers if it has binary products and pullbacks.

Proof

For SfgTS \stackrel{\overset{g}{\longrightarrow}}{\underset{f}{\longrightarrow}} T the given diagram, form the pullback along the diagonal morphism of TT:

eq(f,g) S (f,g) T (id,id) T×T.\array{ eq(f,g) &\longrightarrow& S \\ \big\downarrow && \big\downarrow {}^{\mathrlap{(f, g)}} \\ T &\underset{(id, id)}{\longrightarrow}& T \times T }.

One checks that the horizontal morphism eq(f,g)Seq(f,g) \to S equalizes ff and gg and that it does so universally.

Proposition

If a category has equalizers and (finite) products, then it has (finite) limits.

For the finite case, we may say equivalently:

Proposition

If a category has equalizers, binary products and a terminal object, then it has finite limits.

Proposition

(Eckmann and Hilton EH, Proposition 1.3.) Let e:EXe: E \rightarrow X be an arrow in a category 𝒞\mathcal{C} which is an equaliser of a pair of arrows of 𝒞\mathcal{C}. Then ee is a monomorphism.

Proof

If g,h:AEg,h : A \rightarrow E are arrows of 𝒞\mathcal{C} such that eg=ehe \circ g = e \circ h, then it follows immediately from the uniqueness part of the universal property of an equaliser that g=hg = h.

References

Equalizers were defined in the paper

for any finite collection of parallel morphisms. The paper refers to them as left equalizers, whereas coequalizers are referred to as right equalizers.

Textbook account: