On Final Coalgebras of Power-Set Functors and Saturated Trees

• DOI: 10.1007/s10485-014-9372-9
• Publication Date: 2014-06-19T08:25:24Z
• Authors: Jiří Adámek; Paul B. Levy; Stefan Milius; Lawrence S. Moss; Lurdes Sousa
• Keywords: 0102 computer and information sciences; 0101 mathematics; 10. No inequality; 16. Peace & justice; 01 natural sciences

The final coalgebra for the finite power-set functor was described by Worrell who also proved that the final chain converges in ω+ω steps. We describe the step ω as the set of saturated trees, a concept equivalent to the modally saturated trees introduced by K. Fine in the 1970s in his study of modal logic. And for the bounded power-set functors P λ , where λ is an infinite regular cardinal, we prove that the construction needs precisely λ+ω steps. We also generalize Worrell’s result to M-labeled trees for a commutative monoid M, yielding a final coalgebra for the corresponding functor ℳ f studied by H.-P. Gumm and T. Schroder. We describe the final chain of the power-set functor by introducing the concept of i-saturated tree for all ordinals i, and then prove that for i of cofinality ω, the i-th step in the final chain consists of all i-saturated, strongly extensional trees.