Public:Known Game Comonads

\( \newcommand\Ck{\mathbb C_k} \newcommand\Hom{\mathrm{Hom}} \newcommand\qtq[1]{\quad\text{#1}\quad} \)

In this page we gather the list all comonads we've explored so far.

Convention:

• $$A \leftrightarrows_k B$$ iff there exist homomorphisms $$\Ck A \to B$$ and $$\Ck B \to A$$
• $$A \leftrightarrow_k B$$ iff there exists a span of open pathwise embeddings $$R \to \Ck A$$ and $$R \to \Ck B$$
• $$A \cong_{\mathrm{Kl}(\Ck)} B$$ iff $$A$$ and $$B$$ are isomorphic in the coKleisli category for $$\Ck$$, i.e. there exist homomorphisms $$f\colon\Ck A \to B$$ and $$g\colon\Ck B \to A$$ such that both $$f^* g^*$$ and $$g^* f^*$$ are identities

Typically, each of those equivalences corresponds to a certain logical equivalence. That is, we have that

1. $$A \leftrightarrows_k B \qtq{iff} A \equiv^{\exists^+ \mathcal L} B$$
2. $$A \leftrightarrow_k B \qtq{iff} A \equiv^{\mathcal L} B$$
3. $$A \cong_{\mathrm{Kl}(\Ck)} B \qtq{iff} A \equiv^{\mathcal L^\#} B$$

where $$\exists^+ \mathcal L$$ is the existential-positive fragment of a certain logic $$\mathcal L$$ and $$\mathcal L^\#$$ is the extension of $$\mathcal L$$ by adding counting quantifiers $$\exists_{{\geq} n}$$ and $$\exists_{{\leq} n}$$.

Comonad	$$\Ck$$	Logic $$\mathcal L$$	$$\leftrightarrows_k$$	$$\leftrightarrow_k$$	$$\cong_{\mathrm{Kl}(\Ck)}$$	Coalgebras
Pebbling	$$\mathbb P_k$$	$$k$$-variable fragment $$\mathcal L^k$$ of FOL	$$\exists^+ \mathcal L^k$$	$$\mathcal L^k$$ (wrt $$I$$-morphisms)	$$(\mathcal L^k)^\#$$ (wrt $$I$$-morphisms)	tree width $${<} k$$
Ehrenfeucht-Fraissé	$$\mathbb E_k$$	quantifier rank $${\leq} k$$ fragment $$\mathcal L_k$$ of FOL	$$\exists^+ \mathcal L_k$$	$$\mathcal L_k$$ (wrt $$I$$-morphisms)	$$(\mathcal L_k)^\#$$ (wrt $$I$$-morphisms)	tree depth $${\leq} k$$
Modal (*)	$$\mathbb M_k$$	modal depth $${\leq} k$$ fragment $$\mathcal M_k$$ of ML	$$\exists^+ \mathcal M_k$$	$$\mathcal M_k$$	$$\mathcal M_k$$ + graded modalities	synchronization tree depth $${\leq} k$$
Pebble Relation	$$\mathbb {PR}_k$$		a fragment $$M^k$$ of $$\exists^+ \mathcal L^k$$			path width $${<} k$$
"Hella's game"	$$\mathbb P_{n,k}$$ [1]	extension of $$\mathcal L^k$$ with generalised quantifiers	$$\exists^+ \mathcal L^k(\mathcal Q_n^H)$$	$$\mathcal L^k(\mathcal Q_n^H)$$	$$\mathcal L^k_{\infty,\omega}(\mathcal{Q}_{n})$$	$$n$$-ary generalised tree width $${\leq} k$$
Guarded Fragment	$$\mathbb G^{\mathfrak g}_{k}$$ [2]
Hypergraph comonad	$$\mathbb H_{k}$$

The comonads marked with ``(*)`` denote the comonads over the category of pointed labeled graphs with unary predicates. Note that $$\exists^+ \mathcal M_k$$ denotes the positive $$\Box$$-free fragment of $$\mathcal M_k$$. The $$\leftrightarrows_k$$, $$\leftrightarrow_k$$, and $$\cong_{\mathrm{Kl}(\Ck)}$$ columns mark logic $$\mathcal L$$ such that they correspond to $$\equiv^{\mathcal L}$$ of that logic. Note that \(I\)-morphisms are simply homomorphisms w.r.t. an extended signature, see I-morphisms page.