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{P}X$ 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
  $\{◻a\mid a\in PX\}$ and the equations stating that
  $◻$ preserves finite meets. This gives an isomorphism
  $$U^{\partial }PX\to UPX$$

  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
  $\{◊a\mid a\in PX\}$ and the equations stating that
  $◊$ preserves finite meets. This gives an isomorphism
  $$D^{\partial }PX\to DPX$$

for finite posets

$X$.

The 2-sorted view

We can also think of coalgebras

$$X\to UDX$$

as special 2-dimensional coalgebras

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

The dual of these coalgebras on the algebraic side are algebras

$$(D^{\partial }B,U^{\partial }A)\to (A,B)$$

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).$$

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: …

…