symmetric monoidal (∞,1)-category of spectra
The notion of well-founded coalgebra is due to Paul Taylor (with antecedents in the work of Gerhard Osius). Our account is largely based on (Taylor, section 6.3)), and on his paper The General Recursion Theorem, although in some cases we work with slightly different hypotheses.
Let be a finitely complete category, and let be an endofunctor on . We will suppose that is taut, i.e., preserves pullbacks of monomorphisms (preserves limits of cospans in which one of the cospan arrows is monic). In particular, this implies that preserves monos. A helpful example to keep in mind is the covariant power-set functor .
the map factors through (note that is monic since preserves monos).
A coalgebra is well-founded if the only inductive subobject of is itself.
Example: Suppose is an initial algebra for the endofunctor , with algebra structure map . By Lambek’s theorem, is invertible, so that carries a coalgebra structure . It is easy to check that an inductive subobject gives a subalgebra , but a subalgebra of an initial algebra must be the initial algebra itself. Hence is well-founded.
Our goal in this article is to show that one can perform inductive arguments and recursive constructions in the abstract context of well-founded coalgebras. An interesting challenge is to make precise what is meant by a recursive construction of a map , where the problem is to show how to build from the ground up, as it were. Stages in the recursive construction of a morphism will be partial maps, defined as usual as spans
for which the arrow is monic. Composition of partial maps is effected by span composition, for which we need only finite cocompleteness (we do not need to be a regular category, as we would if we were composing general relations between and ). Notice that since preserves the pulling back of monos, it carries partial maps to partial maps and also preserves partial map composition.
We denote a partial map by a dashed arrow
(generally without explicitly mentioning the domain of ), or sometimes by a harpoon notation.
One way of constructing the initial algebra of an endofunctor, , is by constructing first some fixed point of , that is, an object together with an isomorphism . (For example, it might be the terminal coalgebra, whose existence is sometimes easy to establish.) Then, inside consider the system of well-founded subcoalgebras of . The colimit of this system, assuming it exists, will be the initial algebra. (More theory to develop here.)
The connection with initial algebras goes a little further. Firstly, an initial -algebra is a Peano -algebra in the sense of the following definition:
A -algebra is semi-Peano if every -subalgebra inclusion is an isomorphism, and Peano if in addition is an isomorphism.
If is initial and is a subalgebra, then there is a unique algebra map , and by initiality, whence and then as is monic. Hence initial algebras are semi-Peano, and Peano by Lambek’s theorem.
Secondly, a functor induces, for any object of , a functor between slices , and so if is a coalgebra, we may form an endofunctor on :
and of course the terminal object is automatically and uniquely a -algebra. The next two propositions then follow immediately from the definitions of inductive subobject and well-founded coalgebra:
A subobject of a -coalgebra is inductive precisely when is a -subalgebra of the terminal object of .
A -coalgebra is well-founded precisely when the terminal -algebra is semi-Peano.
The prototype of the notion of well-founded coalgebra is a well-founded relation, which is essentially the same thing as a well-founded coalgebra over the covariant power-set functor . In brief, a binary relation on a set corresponds to a coalgebra , by saying if and only if . See well-founded relation for more information.
Most of the constructions of this article are well-illustrated by checking them against the background of this prototypical case.
A proof by induction, say a proof of a property or predicate where varies over a domain , proceeds by showing that the subobject defined by is an inductive subset with respect to a relation on . It follows that is universally true on , if the relation is well-founded. The same idiom applies more generally to well-founded coalgebras.
A recursive construction on the other hand involves a dependency on prior stages of the construction. A typical application is to define a map by recursion with respect to a well-founded relation, where is specified in three stages:
Consider the collection of all elements preceding ;
Pass to the values defined earlier in the construction, giving a subset of ;
Apply a given operation to this subset , to obtain .
In the last step, the operation may be only partially defined on . In fact, the map itself may be only partially defined; is defined only if is defined “when we call for it”.
An inductive argument is used to show that , so far as it is defined, is uniquely determined. The recursive equation that uniquely determines (to the extent that it exists, of course) is
Letting denote the down-closure of an element with respect to (and containing ), we may then form the set
whence the existence of a map satisfying the recursive equation might indeed be proven by appeal to an inductive argument.
However, notice that this set is defined by a construction in dependent type theory. For other categories , we might not have the luxury of interpreting dependent types, so there it wouldn’t be right to conflate recursion with induction.
It is nevertheless true that one can prove, in rather considerable generality, both an induction principle and recursion theorem for well-founded coalgebras; this will occupy us in the following sections.