# Proper Functors and Fixed Points for Finite Behaviour

## TL;DR

This paper introduces proper functors on algebraic categories, showing they ensure the rational fixed point is a subcoalgebra of the final coalgebra, aiding in coalgebraic regular expression calculus.

## Contribution

It defines proper functors and proves their properties, connecting rational fixed points with subcoalgebras in algebraic categories.

## Key findings

- Proper functors ensure the rational fixed point is a subcoalgebra.
- The colimit of coalgebras with finitely generated free algebras is a subcoalgebra.
- Characterization of proper functors via colimit subcoalgebra property.

## Abstract

The rational fixed point of a set functor is well-known to capture the behaviour of finite coalgebras. In this paper we consider functors on algebraic categories. For them the rational fixed point may no longer be fully abstract, i.e. a subcoalgebra of the final coalgebra. Inspired by \'Esik and Maletti's notion of a proper semiring, we introduce the notion of a proper functor. We show that for proper functors the rational fixed point is determined as the colimit of all coalgebras with a free finitely generated algebra as carrier and it is a subcoalgebra of the final coalgebra. Moreover, we prove that a functor is proper if and only if that colimit is a subcoalgebra of the final coalgebra. These results serve as technical tools for soundness and completeness proofs for coalgebraic regular expression calculi, e.g. for weighted automata.