nLab
equalizer

Definition

In category theory

An equalizer is a limit

$$\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

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

(See also fork diagram).

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

• an object $eq(f,g) \in C$;

• a morphism $eq(f,g) \to x$

• such that

  • pulled back to $eq(f,g)$ both morphisms become equal: $(eq(f,g) \to x \stackrel{f}{\to} y) = (eq(f,g) \to x \stackrel{g}{\to} y)$
  • and $eq(f,g)$ is the universal object with this property.

The dual concept is that of coequalizer.

In type theory

In type theory the equalizer

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

is given by the dependent sum over the dependent equality type

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

Examples

• In $C =$ Set the equalizer of two functions of sets is the subset of elements of $c$ on which both functions coincide.

  $$eq(f,g) = \left\{ s \in c | f(s) = g(s) \right\} \,.$$

• For $C$ a category with zero object the equalizer of a morphism $f : c \to d$ with the corresponding zero morphism is the kernel of $f$.

Properties

Proposition

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

Proof

For $S \stackrel{\overset{g}{\longrightarrow}}{\underset{f}{\longrightarrow}} T$ the given diagram, first form the pullback

$$\array{ S \times_{f,g} S &\to& S \\ \downarrow && \downarrow^{\mathrlap{g}} \\ S &\stackrel{f}{\to}& T } \,.$$

This gives a morphism $S \times_{f,g} S \to S \times S$ into the product.

Define $eq(f,g)$ to be the further pullback

$$\array{ eq(f,g) &\to& S \times_{f,g} S \\ \downarrow && \downarrow \\ S &\stackrel{(id, id)}{\to}& S \times S } \,.$$

One checks that the vertical morphism $eq(f,g) \to S$ equalizes $f$ and $g$ and that it does so universally.

Proposition

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

Equivalently:

Proposition

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