Todd Trimble Some notes on the theme of well-foundedness

Contents

Introduction

In these notes, I would like to write down some details on a body of related results pertaining to corecursion and recursion theory. They include (but are not limited to) the following.

• The category of trees is the terminal coalgebra for the small coproduct completion (as an endofunctor on locally small categories).

• The category of well-founded trees is the initial algebra for the small coproduct completion endofunctor on locally small categories.

• The category of bisimulation classes of well-founded trees is the initial algebra for the small sup-cocompletion endofunctor $P$ on “locally small” (i.e., possibly large) posets.

The point of this exercise is not so much for these results (important though they are) as it is to develop techniques for proving these and related results. These are supposed to be test cases for a general sort of problem which for now I’ll state only very imprecisely: how to construct initial algebras of inaccessible endofunctors on accessible categories. My hunch is that in many such situations, it is technically easier to attack the problem starting from the coalgebraic end, or at least this can free us from having to consider potentially tricky set-theoretic issues involving transfinite constructions over all ordinal ranks, and work rather more cleanly and conceptually.

Most of this is inspired by Paul Taylor’s idea of understanding recursion in terms of well-founded coalgebras. These notes can be seen as a detailed application of his ideas, or rather a categorified version of his ideas, in some special cases.

Another motivation for these notes is to rewrite certain aspects of Algebraic Set Theory (about which I am hardly expert) in terms I can more readily follow. In particular, I had been reading the book by Joyal and Moerdijk, where everything seems to come together in the final chapter on construction of models; here one really sees how the smallness axioms and representability results conspire in the construction of initial ZF-algebras. In my reading, many of the core concepts in this development (open maps of forests, simulations, well-foundedness, extensionality, etc.) can be expressed directly in the coalgebraic language, and in this way are conceptually unified.

Trees as terminal coalgebra

By forest, we mean simply a presheaf $F: \omega^{op} \to Set$ on the first infinite ordinal $\omega$. A tree can be understood in one of two ways:

• A tree $T$ is a connected forest (meaning $\hom(T, -): Forest \to Set$ preserves arbitrary coproducts).

• A tree $T$ is a forest such that $T(0)$ is terminal.

It is clear that a forest admits an essentially unique decomposition as a coproduct of trees, namely its connected components.

Let $s^\ast: Forest \to Forest$ be the pulling back (precomposing) with the successor operation $s: \omega \to \omega$:

Concretely, $s^\ast(F)(n) = F(n+1)$ gives the shift functor $s^\ast$. This clearly has a right adjoint $s_\ast: Forest \to Forest$, defined by the formula

Thus $s_\ast(G)$ is a tree for any forest $G$. The following result is almost a tautology.

The category of forests is in fact the free small-coproduct completion of the category of trees, so this proposition means that $Tree$ (or $Forest$) is a fixpoint of the free small-coproduct cocompletion. In fact, we have the stronger result:

Well-founded trees as initial algebra

The idea in this section will be to exploit a relationship between “macrocosms” of well-founded (extensional) $\Sigma$-subcoalgebras of the category of forests, and “microcosms” which consist of individual well-founded forests.

Well-founded coalgebras

In ordinary 1-category theory, Paul Taylor introduces the concept of well-founded coalgebra as follows.

Let $C$ be a finitely complete category, and let $T$ be an endofunctor on $C$. We will suppose that $T$ preserves pullbacks of monomorphisms (that is, it preserves limits of cospans in which one of the cospan arrows is monic). In particular, this implies that $T$ preserves monos. An example is the covariant power-set functor $P: Set \to Set$.

• Example: Suppose $X$ is an initial algebra for the endofunctor $T$, with algebra structure map $\alpha: T X \to X$. By Lambek’s theorem, $\alpha$ is invertible, so that $X$ carries a coalgebra structure $\theta = \alpha^{-1}: X \to T X$. It is easy to check that an inductive subobject gives a subalgebra $i: U \to X$, but a subalgebra of an initial algebra must be the initial algebra itself. Hence $(X, \theta)$ is well-founded.

The proof may be found in section 6.3 of Taylor’s book Practical Foundations of Mathematics.

Categorification

Now we categorify the results of the preceding subsection so as to apply to the context of 2-categories, at least in the special case $CAT_{ls}$ (locally small, but not necessarily small, categories). The role of “mono” will be played by fully faithful functors (so in effect, we are considering a factorization system on $CAT_{ls}$ given by essentially surjective functors followed by fully faithful functors). 1-pullbacks are categorified to weak pullbacks. Observe that the weak pullback of a fully faithful functor along any functor is again fully faithful.

The expectation is that the proof is a straightfoward categorification of the proof of theorem 1

$WFF$ as initial $\Sigma$-algebra

We now wish to show that the category of well-founded forests (or well-founded trees) $WFF$, as a full subcategory of the category of forests, is an initial algebra of the free small-coproduct completion $\Sigma$. In particular, we will need that

• $WFF$ is a well-founded $\Sigma$-coalgebra,

• The coalgebra structure $WFF \to \Sigma (WFF)$ is an equivalence.

For this we will need some preliminaries.

Forests as coalgebras

The data of a forest structure can be expressed internally as a function $F \to \mathbb{N}$ together with a map

over $\mathbb{N}$, where $s^\ast F$ is the evident pullback

Committing an abuse of language, if as before we also let $s^\ast = Set^{s^{op}}: Set^{\omega^{op}} \to Set^{\omega^{op}}$ be the pulling back along the successor map $\omega \to \omega$, then every forest $F$ is canonically an algebra of the endofunctor $s^\ast$, with structure map $\alpha: s^\ast F \to F$ as before (but now seen as a map between presheaves over $\omega$). The graph of this map is a subobject

which is classified by a map $F \to P s^\ast F$ in $Set^{\omega^{op}}$, where $P$ is the covariant power-object functor. In this way, every forest $F$ carries a canonical $P s^\ast$-coalgebra structure. (Morphisms of forests are actually colax $P s^\ast$-coalgebra maps.) We observe that $P s^\ast$ preserves the pulling back of monos.

(This definition is at the ordinary 1-categorical level, not the categorified level.)

Category of initial segments

Next, we associate to each forest $F$ a simple but fundamental category, the category of initial segments of $F$ (denoted by $\downarrow F$), whose objects are elements (nodes) $p$ of $F$, and whose morphisms $p \to q$ are maps between the trees $T_p \to T_q$ “above” the nodes $p$ and $q$. To be just a bit more formal: for each forest

there is a canonical map $F \to F_0 = F_0$, because $0$ is initial in $\omega$; this takes each node $p \in F(n)$ to the node at height $0$ (“the root”) below it. If $x: 1 \to F_0$ is an element, we define the tree above $x$ to be the pullback

considered as a subforest, in fact a connected component (a tree) of $F$. This may be generalized: for each $n \in \mathbb{N}$, let $n^\ast F$ be an abbreviation for $(s^n)^\ast F$. Each $p \in F$ may be regarded as a root of the forest $(\pi(p))^\ast F$, and we define the tree above $p$ to be

Thus we have an internal category $\downarrow F$ whose nodes are elements $p \in F$ and whose morphisms are tree maps $T_p \to T_q$. This entire construction can be expressed in the internal language of ETCS, or indeed in the Mitchell-Bénabou language of a general topos in place of $Set$.

The point is that $\downarrow F$ has a $\Sigma$-coalgebra construction that matches exactly the $P s^\ast$-coalgebra construction on $F$. The functor $\downarrow F \to \Sigma(\downarrow F)$ takes a node $p \in F_n$ (or, if you prefer, the tree $T_p$) to the formal coproduct

(or, if you prefer, the formal coproduct of trees $T_q$ where $q$ ranges over immediate predecessors of $p$). This is practically the same thing as the $P s^\ast$-coalgebra structure $F \to P s^\ast F$, which takes $p \in F$ to the disjoint union

According to the way we have defined the $\Sigma$-coalgebra structure on $\downarrow F$, the full inclusion $i: \downarrow F \to Set^{\omega^{op}}$, taking $p$ to $T_p$, is a $\Sigma$-coalgebra map.

Well-foundedness of initial segments

The proof will be omitted (at least for now).

$WFF$ is a $\Sigma$-fixpoint

Now we show only that the coalgebra structure $WFF \to \Sigma (WFF)$ is an equivalence.

The coalgebra structure $WFF \to \Sigma(WFF)$ is evidently full and faithful (since the composite in (2) is fully faithful). Thus we have only to show that it is essentially surjective.

However, this is clear: given an object $(X, F: X_d \to WFF)$ of $\Sigma(WFF)$, the forest $G$ defined by

with transition maps defined in the obvious way, is also well-founded. This $G$ maps to the object $(X, F)$ in $\Sigma(WFF)$, and therefore $WFF \to \Sigma(WFF)$ is essentially surjective.

Junk from a prior revision

I am particularly interested in understanding better what is really going on in the chapter on Existence Theorems in AST, or at least try to develop it along clean (co)algebraic lines. The object is to construct initial ZF-structures of various kinds (with a successor, with a monotone successor, etc.) from the structure of a (Heyting) pretopos with a suitable notion of small map. One could think of the pretopos as a category of “classes”, and small maps as a function $f: X \to Y$ between classes with small fibers, and the object is to construct, for example, a cumulative hierarchy out of this data.

The basic picture is more or less clear: a set as conceived in a material theory of well-founded sets is, by the extensionality and foundation axioms, completely determined by its membership tree. So, one could think of the structure of a material set as that of a well-founded tree. Except: trees must be identified according to the extensionality axiom; for example, we have the equality between sets

where each side of the set equation is a tree formed by attaching a root to the disjoint union of four trees. Such equations are closely related to the notions of simulation and bisimulation, so that the cumulative hierarchy may be constructed or construed as the class of bisimulation-equivalence classes of well-founded trees, and inclusions between such classes are given by simulations.

The last line is really a take-off point for algebraic set theory, or at least the AST approach to the cumulative hierarchy. For instance, the standard ZF axioms are shown to hold for the initial algebra of the small sup-cocompletion.

Remark: Joyal and Moerdijk actually have a more flexible approach: they define a ZF-algebra as a (small sup)-lattice $L$ equipped with a function $s: L \to L$ (called “successor”), where a (small sup)-lattice is defined to be an algebra over the monad $P_s$. The initial algebra of the endofunctor $P_s$ is the same as the initial ZF-algebra. However, ZF-algebras allow some extra generality: by adding extra assumptions on $s$, such as that $s$ is monotone, or inflationary, etc., they are able to account for other classes of sets as suitable initial ZF-algebras. These include various notions of ordinal that are distinguished from one another when we move to an intuitionistic setting.

Initially, the role played by simulations and bisimulations in AST was quite mysterious to me; I really don’t think the underlying intuitions were explained too well by Joyal and Moerdijk. The tack I am hoping to take is that the initial algebra for the free small sup cocompletion is obtained by localizing the initial algebra for the free small coproduct cocompletion with respect to a suitable class of maps. Well, that’s not quite right. What we do is localize the category of well-founded trees and simulations with respect to the class of surjective simulations.

But the sweet way to describe all these things is coalgebraic.

More on recursion theory

Let $C$ be a category with pullbacks. Throughout this section, $P$ will be an endofunctor on $C$ that preserves inverse images of monos. In other words, we assume $P$ preserves pullback squares of the form

where $i$ is monic. This implies that $P$ preserves monos in particular and also intersections of subobjects.

We define algebras and coalgebras of $P$ and their morphisms in the usual way.

For the next lemma, assume the category $C$ is locally cartesian closed.

References

• Paul Taylor, Practical Foundations of Mathematics, Cambridge University Press, 1999.