Coalgebras over Preorders

(draft … reference to be added) … (up)

The notion of "bisimulation" canonically associated to a functor

$T:\mathsf{O}\mathsf{r}\mathsf{d}\to \mathsf{O}\mathsf{r}\mathsf{d}$ on ordered sets is typically not a bisimulation but a (forward or backward) simulation. But, depending on the choice of

$T$, it can include ordinary bisimulation as well. I therefore decided to call it (bi)simulation.

Simulations are one of the main reasons to be interested in coalgebras over orders. Of course, orders are also interested in their own right. Moreover, order-enriched category theory is similar to quantale-enriched category theory, which allows to include metric bisimulations in the coalgebraic setting.

For the remainder of this introduction, we review some of the material of the note on powerdomains with the category of preorders instead of posets. We start again with

but we now allow

$X,X^{\prime }$ to be preorders (and require all maps to be order-preserving). We consider three versions of

$\mathcal{P}$ according to whether

$\mathcal{P}X$ is equipped with any of the following orders:

$$\begin{array}{|cccl|}\hline \mathcal{P}& (\mathcal{P}X,\equiv )& \text{bisimulation}& a\equiv b⟺\mathrm{\forall }x\in a\mathrm{\exists }y\in b(x\le y)\mathrm{\&}\mathrm{\forall }y\in b\mathrm{\exists }x\in a(x\le y)\\ \mathcal{U}& (\mathcal{P}X,⊑)& \text{forward simulation}& a⊑b⟺\mathrm{\forall }x\in a\mathrm{\exists }y\in b(x\le y)\\ \mathcal{D}& (\mathcal{P}X,⊒)& \text{backward simulation}& a⊒b⟺\mathrm{\forall }y\in b\mathrm{\exists }x\in a(x\le y)\\ \hline\end{array}$$

Coalgebra homomorphisms are still (functional) bisimulations in all cases but (bi)simulations and the final coalgebra can now have a richer structure.

Remark: Note that

$\mathcal{U}$ and

$\mathcal{D}$ are on preorders (as opposed to on posets) not defined by taking up- or downsets. Both take arbitrary subsets preordered as indicated. If these preorders are quotiented by equivalence, then the order on the quotient of

$\mathcal{U}X$ is isomorphic to inclusion of upsets and and the order on the quotient of

$\mathcal{D}X$ is isomorphic to reverse inclusion of downsets.

Remark: The forgetful functor

$V:\mathsf{P}\mathsf{r}\mathsf{e}\to \mathsf{S}\mathsf{e}\mathsf{t}$ has the discrete functor

$D$ as an ordinary left adjoint. Moreover, in the three examples above,

$VT\cong \mathcal{P}V$. It follows by doctrinal adjunction that

$V$ lifts to right-adjoint between categories of coalgebras. Since right adjoints preserve final objects, forgetting the order of the final

$T$-coalgebra gives us the final

$\mathcal{P}$-coalgebra. In other words, in each of the three cases, equality on the final coalgebra is ordinary bisimilarity. (This is not true if we replace preorders by posets because bisimulation is stronger than forward and backward simulation.)