Final coalgebras over R-modules

Final coalgebras and the coinduction principle for coalgebras over $R$-modules, where $R$ is a commutative ring, are essential in determining the denotational behaviour of various types of linear weighted automata. The goal of this paper is to provide lower and upper bounds on the ordinals that are needed to construct final coalgebras over $R$-modules as the limit of a transfinite sequence of functor iterations. We give an example of a binary intersection preserving finitary functor on the category of abelian groups, which is the category of modules over integers, that fails to converge in $ω\cdot 2$ steps, thus settling an open problem of Adámek, Milius, and Moss. Then we relate this to the failure of the Artinian property of the integers and show that all finitary functors on $R$-modules for a Noetherian ring $R$ with Krull dimension $n$, which preserve countable directed intersections and a generalised notion of monomorphism, converge in $ω\cdot (n + 2)$ steps. We also establish how the connection between Aczel-Mendler bisimulation and behavioural equivalence is mediated by the functor $\operatorname{Ext}^1$. These results show that homological algebra tools can play an important role in coalgebra.