On well-founded and recursive coalgebras (Q2200809)

Let \(F: Set \to Set\) be a functor. An \(F\)-algebra \((A, \alpha)\) consists of a set \(A\) and a map \(\alpha: F(A)\to A\). A morphism of \(F\)-algebras are called a homomorphism. Instead of Set, we can take an arbitrary category \(\mathcal{A}\) and a functor \(F:\mathcal{A}\to\mathcal{A}\) to work with \(F\)-algebras \(\alpha: F(A)\to A\) and \(F\)-coalgebras \(\alpha: A\to F(A)\). The initial object \(\mu F\) of the category of \(F\)-algebras is called the initial algebra. A recursion is defined as a unique homomorphism \(\mu F \to (A, \alpha)\). For example, the functor \(F(X)= X+1= X\cup \{X\}\) has the initial \(F\)-algebra \({\,\mathbb N}\), that is the set of nonnegative integers with the map \({\,\mathbb N}+1\to {\,\mathbb N}\) defined by \(n\mapsto n+1\), for \(n\in {\,\mathbb N}\) and \({\,\mathbb N}\mapsto 0\). For every \(F\)-algebra \((A, \alpha)\) with \(\alpha({\,\mathbb N})=a\), the homomorphism \(f(0)=a\) and \(f(n+1)=\alpha(f(n))\) is the recursion. This approach leads to the problem for a given algebra to determine whether this algebra is initial. We provide the text of the answer from the paper under review: ``The answer -- again in slogans -- is that initial algebras are the ones with `no junk and no confusion'.'' However, initiality does not always describe recursive definitions. Let, for example, \((X, R)\) be a relation that is well founded in the sense that it does not contain infinite sequences \(\cdots x_2 R x_1 R x_0\). Let \(A\) be an arbitrary set. Let us denote by \(\mathcal{P} A\) the set of all its subsets. Then for each mapping \(\alpha:\mathcal{P} A \to A\) there is a unique mapping \(f: X \to A\) defined on all \(x\in X\) by the recursive definition \(f(x) = \alpha(\{y : yRx\})\). But it is impossible to determine the function \(f\) using initiality. The purpose of this article is to explore the concepts behind initiality and apply those concepts to situations like recursive definitions for well-defined relationships. The work continues the research undertaken in the articles by \textit{G. Osius} [J. Pure Appl. Algebra 4, 79--119 (1974; Zbl 0282.02027)] and \textit{P. Taylor} [``Towards a unified treatment of induction I: the general recursion theorem, Preprint, \url{www.paultaylor.eu/ordinals/\#towuti}; Practical foundations of mathematics. Cambridge: Cambridge University Press (1999; Zbl 0939.18001)]. Osius first studied the notions of well-founded and recursive coalgebras for the power-set functor on sets (and, moreover, on an elementary topos). Taylor introduced well-founded coalgebras for a general endofunctor. He proved the General Recursion Theorem that all well-founded coalgebras are recursive, for every endofunctor on sets (and on more general categories) preserving inverse images. Recursive coalgebras were also investigated by \textit{A. Eppendahl} [in: CTCS '99. Conference on category theory and computer science, Edinburgh, GB, September 10--12, 1999. Amsterdam: Elsevier. 8 p. (1999; Zbl 0961.18005)], who called them algebra-initial coalgebras. \textit{V. Capretta} et al. [Lect. Notes Comput. Sci. 5902, 84--100 (2009; Zbl 1266.68083)] further studied recursive coalgebras, and they showed how to construct new ones from given ones by using comonads. \textit{J.-B. Jeannin} et al. [Math. Struct. Comput. Sci. 27, No. 7, 1111--1131 (2017; Zbl 1376.68094)] proved the General Recursion Theorem for polynomial functors on the category of many-sorted sets. In order to formulate the main results of the article, we recall definitions. A category is well-powered if the subobjects of each of its objects can be indexed by a set. We assume that \(\mathcal{A}\) is a complete and well-powered category and that \(F:\mathcal{A}\to\mathcal{A}\) preserves monomorphisms. Definition 2.8. (1) A category \(\mathcal{A}\) has smooth monomorphisms if for every ordinal \(\lambda\) and a diagram \(C: \lambda\to\mathcal{A}\) of monomorphisms, a colimit exists, its colimit cocone is formed by monomorphisms, and for every cone of \(C\) formed by monomorphisms, the factorizing morphism from \(\mathrm{colim\,} C\) is monic. (2) \(\mathcal{A}\) has universally smooth monomorphisms if \(\mathcal{A}\) also has pullbacks, and for every morphism \(f : X \to\mathrm{colim\,} C\), the functor \(\mathcal{A} /\mathrm{colim\,} C \to\mathcal{A} /X\) forming pullbacks along \(f\) preserves the colimit of \(C\). Definition 3.2. A coalgebra \(\alpha: A \to FA\) is called recursive if for every algebra \(e: FX\to X\) there exists a unique coalgebra-to-algebra morphism \(e^{\dagger}: A\to X\), i.e. a unique morphism such that \(e^{\dagger}= e F(e^{\dagger})\alpha\). A coalgebra \((A, \alpha)\) is called parametrically recursive if for every morphism \(e: FX \times A \to X\) there is a unique morphism \(e^{\dagger} : A \to X\) such that \(e^{\dagger}= e (F(e^{\dagger})\times 1_A) (\alpha, 1_A)\). Definition 4.1. Every coalgebra \(\alpha: A \to FA\) induces an endofunction on \(\mathrm{Sub}(A)\), called the next time operator \(\bigcirc:\mathrm{Sub}(A) \to\mathrm{Sub}(A)\), \(\bigcirc(s) = \overleftarrow\alpha (Fs)\) for \(s \in\mathrm{Sub}(A)\). Here, the \(\bigcirc s: \bigcirc S\to A\) denotes the side of the pullback built on the morphisms \(\alpha: A\to FA\) and \(Fs: FS\to FA\). Theorem 5.1 (General Recursion Theorem). Let \(\mathcal{A}\) be a complete and well-powered category with smooth monomorphisms. For \(F:\mathcal{A} \to\mathcal{A}\) preserving monomorphisms, every well-founded coalgebra is parametrically recursive. The assumptions are considered when the converse statement exists. Theorem 5.5. Let \(\mathcal{A}\) be a complete and well-powered category with universally smooth monomorphisms, and suppose that \(F : \mathcal{A} \to\mathcal{A}\) preserves inverse images and has a pre-fixed point. Then every recursive coalgebra is well-founded. Under these assumptions, the paper gives a new equivalent characterization of recursiveness and validity: a coalgebra is recursive if it has a morphism from the coalgebra to the algebra to the original algebra. Corollary 5.6. Let \(\mathcal{A}\) and \(F\) satisfy the assumptions of Theorem 5.5. Then the following properties of a coalgebra are equivalent: (1) well-foundedness, (2) parametric recursiveness, (3) recursiveness, (4) existence of a homomorphism into \((\mu F, \iota^{-1})\), (5) existence of a homomorphism into a well-founded coalgebra. The other converse of the above implication is due to Taylor using the concept of a subobject classifier (Theorem 5.8). It implies that `recursive' and `well-founded' are equivalent concepts for all set functors preserving inverse images. It is also proved in the paper that a similar result is true for the category of vector spaces over a fixed field (Theorem 5.12). For the entire collection see [Zbl 1440.68008].