symmetric monoidal (∞,1)-category of spectra
The existence of free monads, on the other hand, can be a tricky question. One general technique is the transfinite construction of free algebras.
If has an initial algebra , then is isomorphic to via .
In this sense, is a fixed point of . Being initial, is the smallest fixed point of in that there is a map from to any other fixed point (indeed, any other algebra), and this map is an injection if is Set.
The dual concept is terminal coalgebra, which is the largest fixed point of .
Given an initial algebra structure , define an algebra structure on to be . By initiality, there exists an -algebra map , so that
commutes. Now it is trivial, in fact tautological that is itself an -algebra map . Thus , since both sides of the equation are -algebra maps and is initial. As a result, , so that according to the commutative square. Hence is an isomorphism, with inverse .
In many cases, initial algebras can be constructed in recursive fashion, using the following special case of a theorem due to Adámek.
Let be a category with an initial object and transfinite composition of lengh , hence colimits of sequences (where is the first infinite ordinal), and suppose preserves colimits of -chains. Then the colimit of the chain
carries a structure of initial -algebra.
The -algebra structure is inverse to the canonical map out of the colimit (which is invertible by the hypothesis on ). 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.
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.
The archetypical example of an initial algebra is the set of natural numbers.
Let be topos and let the functor given by
By definition, an -algebra is an object equipped with a morphism
commutes. This is the very definition of natural number object .
Let be a set, and let be the functor . Then the initial -algebra is , the free monoid on . The -algebra structure is
where is the identity and is the restriction of the monoid multiplication along the evident inclusion .
This “fixed point” of can be thought of as the result of the (slightly nonsensical) calculation
which can be made rigorous by interpreting the initial equality as defining the solution by recursion, and applying the theorem above.
Let be the functor . Then the initial -algebra is the set of isomorphism classes of finite (planar, rooted) binary trees. The -algebra structure is
where names the tree consisting of just a root vertex, and creates a tree from two trees , by joining their roots to a new root, so that the root of becomes the left child and the root of the right child of the new root.
The recursive equation
would seem to imply that the structure behaves something like a structural “sixth root of unity”, and indeed the structural isomorphism allows one to exhibit an isomorphism
constructively, as famously explored in the paper by Andreas Blass, Seven Trees in One.
Let be the functor (the free monoid from an earlier example). Then the initial -algebra is the set of isomorphism classes of finite planar rooted trees (not necessarily binary as in the previous example).
Let be the coslice category , and let be the functor which pushes out along the multiplication-by- map . Then the initial -algebra is the Pruefer group . See the discussion at the n-Category Café, starting here.
Let be the category of complex Banach spaces and maps of norm bounded above by , and let be the squaring functor . Then the initial -algebra is (with respect to the usual Lebesgue measure). This result is due to Tom Leinster; see this MathOverflow discussion.
inductive type, initial algebra of an endofunctor
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