nLab
initial algebra of an endofunctor

Context

Algebra

Induction

Contents

Definition

An initial algebra for an endofunctor F on a category C is an initial object in the category of algebras of F.

Properties

Relation to algebras over a monad

The concept of an algebra of an endofunctor is arguably somewhat odd, a more natural concept being that of an algebra over a monad. However, the former can often be reduced to the latter.

Proposition

If 𝒞 is a complete category, then the category of algebras of an endofunctor F:𝒞𝒞 is equivalent to the category of algebras over a monad of the free monad on F, if the latter exists.

The proof is fairly straightforward, see for instance (Maciej) or at free monad.

The existence of free monads, on the other hand, can be a tricky question. One general technique is the transfinite construction of free algebras.

Lambek’s theorem

Theorem

If F has an initial algebra α:F(X)X, then X is isomorphic to F(X) via α.

Remark

In this sense, X is a fixed point of F. Being initial, X is the smallest fixed point of F in that there is a map from X to any other fixed point (indeed, any other algebra), and this map is an injection if C is Set.

Remark

The dual concept is terminal coalgebra, which is the largest fixed point of F.

Proof

Given an initial algebra structure α:F(X)X, define an algebra structure on F(X) to be F(α):F(F(X))F(X). By initiality, there exists an F-algebra map i:XF(X), so that

F(X) F(i) F(F(X)) α F(α) X i F(X)\array{ F(X) & \overset{F(i)}{\to} & F(F(X)) \\ \alpha \downarrow & & \downarrow F(\alpha) \\ X & \underset{i}{\to} & F(X) }

commutes. Now it is trivial, in fact tautological that α is itself an F-algebra map F(X)X. Thus αi=1 X, since both sides of the equation are F-algebra maps XX and X is initial. As a result, F(α)F(i)=1 F(X), so that iα=1 F(X) according to the commutative square. Hence α is an isomorphism, with inverse i.

Adámek’s theorem

In many cases, initial algebras can be constructed in recursive fashion, using the following special case of a theorem due to Adámek.

Theorem (Adámek)

Let C be a category with an initial object 0 and transfinite composition of lengh ω, hence colimits of sequences ωC (where ω is the first infinite ordinal), and suppose F:CC preserves colimits of ω-chains. Then the colimit γ of the chain

0iF(0)F(i)F (n)(0)F (n)(i)F (n+1)(0)0 \overset{i}{\to} F(0) \overset{F(i)}{\to} \ldots \to F^{(n)}(0) \overset{F^{(n)}(i)}{\to} F^{(n+1)}(0) \to \ldots

carries a structure of initial F-algebra.

Proof

The F-algebra structure Fγγ is inverse to the canonical map γFγ out of the colimit (which is invertible by the hypothesis on F). The proof of initiality may be extracted by dualizing the corresponding proof given at terminal coalgebra.

This approach can be generalized to the transfinite construction of free algebras.

Semantics for inductive types

Initial algebras of endofunctors are the categorical semantics of extensional inductive types. The generalization to weak initial algebras? captures the notion in intensional type theory and homotopy type theory.

Examples

Natural numbers

The archetypical example of an initial algebra is the set of natural numbers.

Proposition

Let 𝒯 be topos and let F:𝒯𝒯 the functor given by

F:X*X.F : X \mapsto * \coprod X \,.

Then an initial algebra over F is precisely a natural number object in 𝒯.

Proof

By definition, an F-algebra is an object X equipped with a morphism

(0,s):*XX,(0,s) : * \coprod X \to X \,,

hence equivalently with a point 0:*X and an endomorphism s:XX. This being inital means that for (0 Y,s Y):*YY any other morphism, there is a unique morphism f:XY such that the diagram

* 0 X s X f f * 0 Y s Y\array{ * &\stackrel{0}{\to}& X &\stackrel{s}{\to}& X \\ \downarrow && \downarrow^{\mathrlap{f}} && \downarrow^{\mathrlap{f}} \\ * &\stackrel{0}{\to}& Y &\stackrel{s}{\to}& Y }

commutes. This is the very definition of natural number object X=.

More examples

Theorem 2 applies in particular to any functor F:SetSet which is a colimit of finitely representable functors hom(n,):XX n, as in the following examples.

  • Let A be a set, and let F:SetSet be the functor F(X)=1+A×X. Then the initial F-algebra is A *, the free monoid on A. The F-algebra structure is

    (e,m):1+A×A *A *(e, m| ): 1 + A \times A^* \to A^*

    where e:1A * is the identity and m:A×A *A * is the restriction of the monoid multiplication along the evident inclusion i×1:A×A *A *×A *.

    This “fixed point” of F can be thought of as the result of the (slightly nonsensical) calculation

    1+A×X=XX=11A=1+A+A 2+=A *1 + A \times X = X \Rightarrow X = \frac1{1 - A} = 1 + A + A^2 + \ldots = A^*

    which can be made rigorous by interpreting the initial equality as defining the solution X by recursion, and applying the theorem above.

  • Let F:SetSet be the functor F(X)=1+X 2. Then the initial F-algebra is the set T of isomorphism classes of finite (planar, rooted) binary trees. The F-algebra structure is

    (r,j):1+T 2T(r, j): 1 + T^2 \to T

    where r:1T names the tree consisting of just a root vertex, and j:T 2T creates a tree tt from two trees t, t by joining their roots to a new root, so that the root of t becomes the left child and the root of t the right child of the new root.

    The recursive equation

    T=1+T 2T = 1 + T^2

    would seem to imply that the structure T behaves something like a structural “sixth root of unity”, and indeed the structural isomorphism TF(T) allows one to exhibit an isomorphism

    T=T 7T = T^7

    constructively, as famously explored in the paper by Andreas Blass, Seven Trees in One.

  • Let F:SetSet be the functor F(X)=X * (the free monoid from an earlier example). Then the initial F-algebra is the set of isomorphism classes of finite planar rooted trees (not necessarily binary as in the previous example).

  • Let C be the coslice category Ab, and let F:CC be the functor which pushes out along the multiplication-by-p map p:. Then the initial F-algebra is the Pruefer group [p 1]/. See the discussion at the n-Category Café, starting here.

  • Let Ban be the category of complex Banach spaces and maps of norm bounded above by 1, and let F:BanBan be the squaring functor XX×X. Then the initial F-algebra is L 1([0,1]) (with respect to the usual Lebesgue measure). This result is due to Tom Leinster; see this MathOverflow discussion.

References

A textbook account of the basic theory is in chapter 10 of

A brief review of some basics with an eye towards inductive types is in section 2 of

The relation to free monads is discussed in

Revised on December 6, 2012 08:30:26 by Mike Shulman (192.16.204.218)