On the final sequence of a finitary set functor

Applications of set theory (03E75) Categories of sets, characterizations (18B05) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Abstract data types; algebraic specification (68Q65)

Review text

Final coalgebras of set functors were offered by \textit{P. Aczel} and \textit{N. Mendler} [``A final coalgebra theorem, in: Category theory and computer science, Lect. Notes Comput. Sci. 389, 357--365 (1989; Zbl 0712.68006)] as a way of modeling infinite abstract data types, and generalize the notion of greatest fixed point of a monotone function on a complete lattice. The process of obtaining either style of object involves a transfinite iteration, and it is the purpose of this paper to give conditions under which the process may be carried out successfully. In brief, if \(T: {\mathcal C}\to{\mathcal C}\) is an endofunctor on a category \({\mathcal C}\), then a \(T\)-coalgebra is a pair \((A, f)\), where \(A\) is an object in \({\mathcal C}\) and \(f: A\to T(A)\) is a morphism in \({\mathcal C}\). If \((A, f)\) and \((B, g)\) are \(T\)-coalgebras, then a \(T\)-coalgebra homomorphism from the first to the second is a \({\mathcal C}\)-morphism \(h: A\to B\) such that \(T(h)\circ f= g\circ h\). A final \(T\)-coalgebra, then, is a final object in the category of \(T\)-coalgebras and \(T\)-coalgebra homomorphisms. Suppose the ground category \({\mathcal C}\) has limits for all ordinal-indexed inverse systems. Then, in particular, \({\mathcal C}\) has a final object; so, given an endofunctor \(T\), we may define the final sequence for \(T\) by iterating \(T\) on that object: the first morphism is given by definition, the second is the image of the first under \(T\), and so on. At limit ordinals, we take colimits. A theorem of \textit{J. Adámek} and \textit{V. Koubek} [``On the greatest fixed point of a set functor, Theor. Comput. Sci. 150, 57--75 (1995; Zbl 0874.18001)], and independently by \textit{M. Barr} [``Terminal coalgebras in well-founded set theory, Theor. Comput. Sci. 114, 299--315 (1993; Zbl 0779.18004)], gives a provisional existence theorem for final \(T\)-coalgebras by saying that: if \(A_\alpha\) is the \(\alpha\)th stage in the final sequence, with \(f^\gamma_\beta: A_\gamma\to A_\beta\) the uniquely-defined morphism, \(\beta\leq \gamma\), and if there is some \(\kappa\) such that \(f^{\kappa+1}_\kappa\) is an isomorphism, then \((A_\kappa,(f^{\kappa+1}_\kappa)^{-1})\) is a final \(T\)-coalgebra. For any regular cardinal \(\kappa\), an endofunctor \(T\) is called \(\kappa\)-accessible if it preserves colimits (i.e., inverse limits) of systems, where the directed index set is equipped with upper bounds for all subsets of cardinality \(<\kappa\). In the present paper the focus is on the ground category \({\mathcal C}\) being the category \({\mathcal S}et\) of sets and functions. The main theorem provides a sufficient condition for the hypothesis of the Adámek-Koubek and Barr theorem to hold; namely it says that: whenever \(T\) is a \(\kappa\)-accessible endofunctor on \({\mathcal S}et\), where \(\kappa\) is a regular cardinal, then the morphism \(f^{\kappa+\kappa+1}_{\kappa+\kappa}\) in the final sequence is an isomorphism. The author then presents in detail the final sequence for the finite powerset functor, which is \(\omega\)-accessible, and shows that there is no ordinal \(\alpha< \omega+\omega\) for which \(f^{\alpha+1}_\alpha\) is an isomorphism.

Recommendations

Cites work

Cited in

(59)

This page was built for publication: On the final sequence of a finitary set functor

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q557796)