Lambek's theorem
Table of Contents
1. statement
If a functor \( F \) has an initial algebra \( \alpha : F(x) \to x \), then \( F(x) \) is isomorphic to \( x \) via \( \alpha \).
In other words, \( x \) is a fixed point of \( F \) (up to isomorphism).
Dually, if \( F \) has a final coalgebra \( \alpha : x \to F(x) \), then \( F(x) \) is isomorphic to \( x \) via \( \alpha \).
2. proof
Consider the iterated algebra \( F(\alpha) : F(F(x)) \to F(x) \). By initiality of \( \alpha \), there exists a unique arrow \( i : x \to F(x) \) such that the following diagram commutes:
\begin{tikzcd} {F(x)} & {F(F(x))} \\ x & F(x) \arrow["{F(i)}", from=1-1, to=1-2] \arrow["\alpha"', from=1-1, to=2-1] \arrow["F(\alpha)", from=1-2, to=2-2] \arrow["i"', from=2-1, to=2-2] \end{tikzcd}Note that we can compose \( i \) and \( \alpha \) (in opposite order relative to the above diagram) to obtain \( i\alpha : x \to x \). But since \( x \) is initial, there is exactly one arrow \( x \to x \), namely \( 1_x \). Therefore, \( i\alpha = 1_x \).