Trees in Coalgebra from Generalized Reachability

Abstract

An automaton is called reachable if every state is reachable from the initial state. This notion has been generalized coalgebraically in two ways: first, via a universal property on pointed coalgebras, namely, that a reachable coalgebra has no proper subcoalgebras; and second, a coalgebra is reachable if it arises as the union of an iterative computation of successor states, starting from the initial state. In the current paper, we present corresponding universal properties and iterative constructions for trees. The universal property captures when a coalgebra is a tree, namely, when it has no proper tree unravellings. The iterative construction unravels an arbitrary coalgebra to a tree. We show that this yields the expected notion of tree for a variety of standard examples. We obtain our characterization of trees by first generalizing the previous theory of reachable coalgebras and of a minimal object in a category, related to projectivity. Surprisingly, both the universal property and the iterative construction for trees arise as instances of this generalized notion of reachability. Our iterative construction works for all analytic set functors.