In category theory, there is a common problem of the construction of free objects in “algebraic” categories. The idea is that one has to start from some “generators” and repeatedly throw in the results of applying “operations”, subject to some “relations”, over and over again until the result “converges”. In general, this convergence will require a transfinite iteration, and the fact that it converges at all requires some smallness/accessibility hypotheses.
If this construction is performed in sufficient generality, then it includes a large number of important special cases, such as the following (not mutually exclusive):
In 1980, Max Kelly (Kelly) wrote a very long paper detailing very precise and general conditions under which such constructions can be performed, and showing how they can all be reduced to the case of free algebras for well-pointed endofunctors.
In what follows we will summarize Kelly’s constructions, restricted to the special case of accessible functors on locally presentable categories. Much of the technical apparatus of Kelly’s paper (including, among other things, two different ambient orthogonal factorization systems and , and assumptions such as ” preserves the -tightness of -cones”) becomes unnecessary in this case, which also includes many if not most of the important examples.
Let be a locally presentable category. All endofunctors of which we consider will be accessible, that is, they preserve -filtered colimits for some sufficiently large cardinal number . In fact, we will only need to know that they preserve sufficiently long transfinite compositions.
An endofunctor is called pointed if it is equipped with a natural transformation . It is called well-pointed if (as natural transformations ).
If is an endofunctor, then an -algebra is an object together with a map . If is a pointed endofunctor, then an -algebra is an object with a map such that .
We have obvious categories of algebras of both sorts. Of course, any algebra for a monad is also an algebra for that monad qua pointed endofunctor. The converse holds in the well-pointed/idempotent case. In fact, we have:
If is well-pointed, then an object admits at most one -algebra structure. This happens exactly when is an isomorphism, in which case its inverse is that unique algebra structure.
Thus, when is well-pointed, the category of -algebras is a full subcategory of . Well-pointed endofunctors are important, so we mention a few other ways to obtain them.
If is a well-pointed endofunctor and is a natural transformation whose components are epimorphisms, then is also well-pointed.
Suppose is a family of (accessible) well-pointed endofunctors and let be the wide pushout of all the points . Then is (accessible and) well-pointed, and .
Let be an adjunction and an (accessible) well-pointed endofunctor on . Let be the pushout
Then is (accessible and) well-pointed, and is an -algebra exactly when is an -algebra.
The basic theorem to which all others can be reduced is the following.
Given , define inductively the following transfinite sequence in :
in which each transition map is a component of , and we take colimits at limit stages. If we continue this out to some -filtered ordinal , where is -accessible, then will preserve the relevant colimit, and hence we have an induced action . It is easy to check that this makes into a reflection of into .
Some important constructions are directly examples of this theorem.
Let be a set of morphisms in ; recall that an object is said to be orthogonal to if is a bijection for all , which is to say that each functor takes to an isomorphism, where is the arrow category of Set. Now the subcategory of isomorphisms is reflective in , hence is the algebras for a well-pointed endofunctor . By Lemma 4, there is a well-pointed endofunctor on whose algebras are the objects orthogonal to . And by Lemma 3, there is a well-pointed endofunctor whose algebras are those objects orthogonal to all . Thus, by Theorem 1, the category of objects orthogonal to is reflective in .
The rest of the constructions proceed by building, out of other data, a well-pointed endofunctor, and applying Theorem 1.
Now let be a general (accessible) pointed endofunctor, not necessarily well-pointed. Let denote the comma category, whose objects are triples where . Then is again locally presentable.
If is a natural transformation, we have an adjunction in which sends to and is defined by a pushout.
Note that if is , then is the composite in .
The category of -algebras is a reflective full subcategory of .
It is easy to show that it is a full subcategory. Moreover, lies in just when is an isomorphism. The isomorphisms are a reflective subcategory of , hence the algebras for a well-pointed endofunctor . Now by Lemma 4, there is a well-pointed endofunctor of whose algebras are precisely the -algebras. Now apply Theorem 1.
The category is monadic over , and cocomplete. In particular, the algebraically-free monad on exists and is accessible.
A left adjoint to the forgetful functor is supplied by reflecting the object of into . The monadicity theorem then applies. Colimits can be constructed in and then reflected into .
It is possible to β-reduce this proof and describe the resulting transfinite construction more explicitly. Given , we define inductively a transfinite sequence
such that is equal to .
We begin with , , and . Given and , we define to be the coequalizer of the two composites
At limit ordinals we take colimits, and at successors of limit ordinals we let be the coequalizer of the two maps
An algebra for an unpointed endofunctor is the same as an algebra for the pointed endofunctor . Thus, Theorem 2 can be applied to unpointed endofunctors as well.
In this case, the transfinite sequence for the free -algebra on is much simpler: we have and .
A W-type in a category is an initial algebra for a polynomial functor. Equivalently, it is the free algebra on the initial object for that functor. Thus, we obtain the existence of W-types, and likewise of more general inductive types.
Let be a monad on , and let denote the category of -algebras qua monad.
The category is a reflective subcategory of .
For , consider the pushout
Define to take to in this pushout. Then -algebras (qua pointed endofunctor) are precisely -algebras (qua monad), and we have a pointwise epimorphism , where is the well-pointed endofunctor from the proof of Theorem 2 whose algebras are the -algebras (qua pointed endofunctor). Thus, by Lemma 2, is well-pointed; now apply Theorem 1.
is locally presentable. Moreover, any functor induced by a monad morphism has a left adjoint.
Since is reflective in the cocomplete , it is cocomplete. Since it is accessible by the limit theorem, it is locally presentable. For the second statement, the functor has an easily defined left adjoint; now compose it with the reflection into .
When speaking of colimits of monads, we are not interested merely in colimits in the category of monads, but algebraic colimits in the following sense. Let be a diagram in the category of monads on , and define a -algebra to be an object together with -algebra structures which commute with the images of morphisms in .
An algebraic colimit of is a monad whose usual Eilenberg-Moore category is equivalent, over , to the category of -algebras.
It follows, by arguments similar to those for algebraically-free monads, that an algebraic colimit is also a colimit in the category of monads.
Algebraic colimits of (accessible) monads exist (and are accessible).
WLOG we may assume has an initial object; otherwise, give it a new initial object and define . Let be the (pointwise) colimit of in the category of endofunctors of , with coprojections . Our assumption on gives a unique point such that each is a map of pointed endofunctors. Moreover, a -algebra (qua pointed endofunctor) is an object together with compatible pointed-endofunctor-algebra structures for each . This clearly includes the -algebras, as defined above, as a full subcategory.
We will show the category of -algebras to be reflective in . Given , let be the joint coequalizer of all the parallel pairs
Let , defining an endofunctor of . Then is accessible, and an -algebra is precisely a -algebra.
Moreover, admits an epimorphic transformation from the well-pointed endofunctor defined as in Theorem 2 whose algebras are the -algebras (qua pointed endofunctor). Thus, by Lemma 2, is well-pointed; now apply Theorem 1.
The categorical semantics of higher inductive types can be described using certain “presentations” of monads. (More to come…)