Logic of Ordered Neighbourhood Coalgebras

(draft ... references to be added) ... (up)

Introduction¶

We write 2 for the 2-chain $0<1$ in various ordered categories such as posets or bounded distributed lattices.

Let

$U:Pos\to Pos$ take upsets ordered by reverse inclusion: $UX=[X,2]^o$
$D:Pos\to Pos$ take downsets ordered by inclusion: $DX=[X^o,2]$

Let

$\mathcal X$ be the category of poset
$\mathcal A$ be the category of bounded distributive lattices
$T=DU$

Then $Coalg(T)$ is category of (monotone) neighbourhood frames (over posets). In particular $DUX=Up\mathcal PX$ for discrete $X$ . Note that $DUX=2^{2^X}$ if we define $2^X$ as the poset of monotone maps $X\to 2$ .

Let

$P:\mathcal X\to\mathcal A$ be the contravariant functor $X\mapsto 2^X$ .
$S:\mathcal A\to\mathcal X$ the contravariant functor $A\mapsto DL(A,2)$ .

Then

the dual $U^\partial:DL\to DL$ of $U$ is presented by operations and equations as follows. $U^\partial A$ is generated by $\{\Box a\mid a\in PX\}$ and the equations stating that $\Box$ preserves finite meets. This gives an isomorphism

U^\partial PX\to UPX

(1)

for finite posets $X$ .

the dual $D^\partial:DL\to DL$ of $D$ is presented by operations and equations as follows. $D^\partial A$ is generated by $\{\Diamond a\mid a\in PX\}$ and the equations stating that $\Diamond$ preserves finite meets. This gives an isomorphism

D^\partial PX\to DPX

(2)

for finite posets $X$ .

The 2-sorted view¶

We can also think of coalgebras

X \to UDX

(3)

as special 2-dimensional coalgebras

(X,Y) \to (UY,DX).

(4)

The dual of these coalgebras on the algebraic side are algebras

(D^\partial B,U^\partial A)\to (A,B)

(5)

Remark: Given functors $F$ and $G$ , Kurz-Petrisan calls the functor which maps $(X,Y)$ to $(FY,GX)$ the symmetric composition of $F$ and $G$ . While the presentation of the functor $FG$ is typically not compositional in the presentations of $F$ and $G$ , the symmetric composition does have the obvious componentwise presentation.

An adjunction¶

Let $Coalg(F,G)$ be the category of 2-sorted coalgebras of the kind

(X,Y)\to (FY,GX).

(6)

Theorem: $Coalg(FG)$ is a full reflective subcategory of $Coalg(F,G)$ .

Proof: We map $X\to FGX$ to $(X,GX)\to (FGX,GX)$ where the second component is the identity. This functor has a left adjoint which maps $(X,Y)\to (FY,GX)$ to $X\to FY\to FGX$ .

The unit of the adjunction is the obvious coalgebra morphism from $(X,Y)\to (FY,GX)$ to $(X,GX)\to (FGX,GX)$ . The counit is the identity.

Moreover, the right-adjoint is full and faithful. QED

Corollary: $Coalg(FG)$ is closed under limits in $Coalg(F,G)$ . In particular, the final coalgebra in $Coalg(F,G)$ is also the final coalgebra in $Coalg(FG)$ .

Corollary: $Alg(FG)$ is a full co-reflective subcategory of $Alg(F,G)$ .

Corollary: The category of $D^\partial U^\partial$ -algebras is a full coreflective subcategory of $Alg(D^\partial, U^\partial)$ .

Corollary: $Alg(FG)$ is closed under colimits in $Alg(F,G)$ . In particular, the initial algebra in $Alg(F,G)$ is also the initial algebra in $Alg(FG)$ .

References¶

Pauly: ...

Hansen, Kupke: ...

Kurz, Petrisan: ...

...