Lambek's lemma

Remarks

The pair $(F(I), F(i))$ is an $F$-algebra, so by initiality there is a unique algebra morphism $j \colon (I, i) \to (F(I), F(i))$. Then $i \circ j$ is an algebra morphism from $(I, i)$ to itself, so it equals $\id_I$ by uniqueness. Also $j \circ i = F(i) \circ F(j) = F(i \circ j) = \id_{F(I)}$, using that $j$ is an algebra morphism. So $j$ is the inverse of $i$.

Example: on the category of sets let $F(X) = 1 + X$, where $1 = \set{*}$. The initial $F$-algebra is the set of natural numbers with the map sending $*$ to $0$ and $n$ to $n + 1$. The lemma says that this map $1 + \N \to \N$ is a bijection: every natural number is either $0$ or a successor, in exactly one way.

Example of a consequence: the power set functor on sets has no initial algebra. An initial algebra would give a bijection between a set and its power set, which Cantor's theorem rules out.

The dual statement holds as well: the structure map of a terminal $F$-coalgebra is an isomorphism.

Going deeper

For a student

The lemma is the starting point of the theory of inductive and coinductive data types. It shows that an initial algebra, when it exists, is a fixed point $F(I) \cong I$ of the functor. It also gives quick non-existence results, as with the power set functor. Its dual, for terminal coalgebras, says that infinite streams over $A$ satisfy $A \times S \cong S$.