Identity-Preserving Lax Extensions and Where to Find Them

TL;DR

This paper investigates conditions under which functors in universal coalgebra admit identity-preserving lax extensions, providing new necessary and sufficient criteria related to specific pullback preservation properties.

Contribution

It establishes new necessary conditions and sufficient criteria for the existence of normal lax extensions of functors, advancing the understanding of their structural properties.

Findings

Functors admitting a normal lax extension preserve 1/4-iso pullbacks.

Sufficient conditions include weak preservation of 1/4-iso and 4/4-epi pullbacks or inverse images.

Applied criteria to functors modeling neighbourhood and weighted systems.

Abstract

Generic notions of bisimulation for various types of systems (nondeterministic, probabilistic, weighted etc.) rely on identity-preserving (normal) lax extensions of the functor encapsulating the system type, in the paradigm of universal coalgebra. It is known that preservation of weak pullbacks is a sufficient condition for a functor to admit a normal lax extension (the Barr extension, which in fact is then even strict); in the converse direction, nothing is currently known about necessary (weak) pullback preservation conditions for the existence of normal lax extensions. In the present work, we narrow this gap by showing on the one hand that functors admitting a normal lax extension preserve 1/4-iso pullbacks, i.e. pullbacks in which at least one of the projections is an isomorphism. On the other hand, we give sufficient conditions, showing that a functor admits a normal lax extension if it weakly preserves either 1/4-iso pullbacks and 4/4-epi pullbacks (i.e. pullbacks in which all morphisms are epic) or inverse images. We apply these criteria to concrete examples, in particular to functors modelling neighbourhood systems and weighted systems.