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

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

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

  • such that

    • pulled back to eq(f,g)eq(f,g) both morphisms become equal: (eq(f,g)xfy)=(eq(f,g)xgy) (eq(f,g) \to x \stackrel{f}{\to} y) = (eq(f,g) \to x \stackrel{g}{\to} y)
    • and eq(f,g)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

PAgfB P \to A \stackrel{\overset{f}{\to}}{\underset{g}{\to}} 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

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

    eq(f,g)={scf(s)=g(s)}. eq(f,g) = \left\{ s \in c | f(s) = g(s) \right\} \,.
  • For CC a category with zero object the equalizer of a morphism f:cdf : c \to d with the corresponding zero morphism is the kernel of ff.

Properties

Proposition

A category has equalizers if it has products and pullbacks.

Proof

For SfgTS \stackrel{\overset{g}{\to}}{\underset{f}{\to}} T the given diagram, first form the pullback

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

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

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

eq(f,g) S× f,gS S (id,id) S×S. \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)Seq(f,g) \to S equalizes ff and gg and that it does so universally.

Proposition

If a category has products and equalizers, then it has limits; see there.

Revised on November 15, 2012 13:55:18 by Stephan Alexander Spahn (79.227.160.54)