Difference between revisions of "Public:Known Game Comonads"

m (I just realised that we need to mention I-morphisms, probably the rest of the table needs to be reviewed too)
(added an explanation)
Line 15: Line 15:


Typically, each of those equivalences corresponds to a certain logical equivalence. That is, we have that
Typically, each of those equivalences corresponds to a certain logical equivalence. That is, we have that
# $$A \leftrightarrows_k B \qtq{iff} A \equiv^{\exists \Lk} B$$
\[
A \leftrightarrows_k B \qtq{iff} A \equiv^{\exists \Lk} B,
# $$A \leftrightarrow_k B \qtq{iff} A \equiv^{\Lk} B$$
# $$A \cong_{\mathrm{Kl}(\Ck)} B \qtq{iff} A \equiv^{\Lk^\#} B$$
\qquad
A \leftrightarrow_k B \qtq{iff} A \equiv^{\Lk} B,
\qtq{and}
A \cong_{\mathrm{Kl}(\Ck)} B \qtq{iff} A \equiv^{\Lk^\#} B
\]
where $$\exists \Lk$$ is the existential-positive fragment of $\\Lk$ and $$\Lk^\#$$ is the extension of $$\Lk$$ by adding counting quantifiers $$\exists_{{\geq} n}$$ and $$\exists_{{\leq} n}$$.
where $$\exists \Lk$$ is the existential-positive fragment of $\\Lk$ and $$\Lk^\#$$ is the extension of $$\Lk$$ by adding counting quantifiers $$\exists_{{\geq} n}$$ and $$\exists_{{\leq} n}$$.


Line 38: Line 34:
| $$k$$-variable fragment of FO
| $$k$$-variable fragment of FO
| ✓
| ✓
| ✓ with <br> $$I$$-morphisms
| ✓
| ✓ with <br> $$I$$-morphisms
| ✓
| tree width $${\leq} k$$
| tree width $${\leq} k$$
|-
|-
Line 46: Line 42:
| quantifier rank $${\leq} k$$ fragment of FO
| quantifier rank $${\leq} k$$ fragment of FO
| ✓
| ✓
| ✓ with <br> $$I$$-morphisms
| ✓
| ✓ with <br> $$I$$-morphisms
| ✓ with <br> $$I$$-morphisms
| tree depth $${\leq} k$$
| tree depth $${\leq} k$$
Line 59: Line 55:
|}
|}


The comonads marked with ``(*)`` denote the comonads over the category of pointed labeled graphs.
The comonads marked with ``(*)`` denote the comonads over the category of pointed labeled graphs. The $$\leftrightarrows_k$$, $$\leftrightarrow_k$$, and $$\cong_{\mathrm{Kl}(\Ck)}$$ columns mark whether the equivalence in (1), (2), resp. (3) above holds.

Revision as of 16:31, 15 May 2020

\( \newcommand\Ck{\mathbb C_k} \newcommand\Lk{\mathcal L_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 exist non-empty sets $$F\subseteq \Hom(\Ck A, B)$$ and $$G\subseteq \Hom(\Ck B, A)$$ which are locally invertible
  • $$A \cong_{\mathrm{Kl}(\Ck)} B$$ iff $$A$$ and $$B$$ are isomorphic in the coKleisly 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 \Lk} B$$
  2. $$A \leftrightarrow_k B \qtq{iff} A \equiv^{\Lk} B$$
  3. $$A \cong_{\mathrm{Kl}(\Ck)} B \qtq{iff} A \equiv^{\Lk^\#} B$$

where $$\exists \Lk$$ is the existential-positive fragment of $\\Lk$ and $$\Lk^\#$$ is the extension of $$\Lk$$ by adding counting quantifiers $$\exists_{{\geq} n}$$ and $$\exists_{{\leq} n}$$.


Comonad $$\Ck$$ $$\Lk$$ $$\leftrightarrows_k$$ $$\leftrightarrow_k$$ $$\cong_{\mathrm{Kl}(\Ck)}$$ Coalgebras
Pebbling $$\mathbb P_k$$ $$k$$-variable fragment of FO ✓ with
$$I$$-morphisms
✓ with
$$I$$-morphisms
tree width $${\leq} k$$
Ehrenfeucht-Fraissé $$\mathbb E_k$$ quantifier rank $${\leq} k$$ fragment of FO ✓ with
$$I$$-morphisms
✓ with
$$I$$-morphisms
tree depth $${\leq} k$$
Modal (*) $$\mathbb M_k$$ modal depth $${\leq} k$$ fragment of ML synchronization tree
depth $${\leq} k$$

The comonads marked with ``(*)`` denote the comonads over the category of pointed labeled graphs. The $$\leftrightarrows_k$$, $$\leftrightarrow_k$$, and $$\cong_{\mathrm{Kl}(\Ck)}$$ columns mark whether the equivalence in (1), (2), resp. (3) above holds.