Difference between revisions of "Public:Known Game Comonads"
(Page created) |
(kicking off) |
||
Line 1: | Line 1: | ||
<div style="display:none;"><math> |
|||
⚫ | |||
\newcommand\Ck{\mathbb C_k} |
|||
\newcommand\Lk{\mathcal L_k} |
|||
\newcommand\Hom{\mathrm{Hom}} |
|||
\newcommand\qtq[1]{\quad\text{#1}\quad} |
|||
</math></div> |
|||
⚫ | |||
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 [[Public:locally invertible|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 |
|||
\[ |
|||
A \leftrightarrows_k B \qtq{iff} A \equiv^{\exists \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$$. |
|||
{| class="wikitable" |
|||
! '''Comonad''' |
|||
! $$\Ck$$ |
|||
! $$\Lk$$ |
|||
! $$\leftrightarrows_k$$ |
|||
! $$\leftrightarrow_k$$ |
|||
! $$\cong_{\mathrm{Kl}(\Ck)}$$ |
|||
! '''Coalgebras''' |
|||
|- |
|||
| Pebbling |
|||
| $$\mathbb P_k$$ |
|||
| $$k$$-variable fragment of FO |
|||
| ✓ |
|||
| ✓ |
|||
| ✓ |
|||
| tree width $${\leq} k$$ |
|||
|- |
|||
| Ehrenfeucht-Fraissé |
|||
| $$\mathbb E_k$$ |
|||
| quantifier rank $${\leq} k$$ fragment of FO |
|||
| ✓ |
|||
| ✓ |
|||
| ✓ |
|||
| tree depth $${\leq} k$$ |
|||
|- |
|||
| Modal (*) |
|||
| $$\mathbb M_k$$ |
|||
| modal depth $${\leq} k$$ fragment of ML |
|||
| ✓ |
|||
| ✓ |
|||
| ✓ |
|||
| synchronization tree<br>depth $${\leq} k$$ |
|||
|} |
|||
The comonads marked with ``(*)`` denote the comonads over the category of pointed structures. |
Revision as of 13:00, 14 May 2020
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 \[ A \leftrightarrows_k B \qtq{iff} A \equiv^{\exists \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$$.
Comonad | $$\Ck$$ | $$\Lk$$ | $$\leftrightarrows_k$$ | $$\leftrightarrow_k$$ | $$\cong_{\mathrm{Kl}(\Ck)}$$ | Coalgebras |
---|---|---|---|---|---|---|
Pebbling | $$\mathbb P_k$$ | $$k$$-variable fragment of FO | ✓ | ✓ | ✓ | tree width $${\leq} k$$ |
Ehrenfeucht-Fraissé | $$\mathbb E_k$$ | quantifier rank $${\leq} k$$ fragment of FO | ✓ | ✓ | ✓ | 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 structures.