nLab comonad

Definition

A comonad (or cotriple) on a category $A$ is a comonoid in the monoidal category of endofunctors $A \to A$. More generally, a comonad in a 2-category $E$ is a comonoid in the monoidal category $E(X,X)$ for some object $X\in K$.

Just as a monad may be defined for any 2-category, $E$, as a lax 2-functor from $\mathbf{1}$ to $E$, so a comonad in $E$ is an oplax 2-functor from $\mathbf{1} \to E$.

See at monad for more.

Properties

Coalgebras

A coalgebra over a comonad (or comodule) over a comonad $C$ on a category $A$ is an object $a\in A$ with a map $a\to C a$ satisfying dual axioms to those for an algebra over a monad. The category of coalgebras is called its (co-)Eilenberg-Moore category and satisfies a universal property dual to that of the Eilenberg-Moore object for a monad; it can thereby be internalized to any 2-category. The forgetful functor from the category of coalgebras to the category $A$ is called a comonadic functor. Similarly, a comonad also has a co-Kleisli category.

Comonadic homology and descent

Any comonad on $A$ induces an augmented simplicial endofunctor of $A$ consisting of its iterates. If $A$ is an abelian category and the comonad is additive, then this is the basis of comonadic homology?. Comodules (= coalgebras) over the comonad with underlying endofunctor $M_R\mapsto M_R\otimes_R S$ in $R$-$Mod$ for the extension of rings $R\hookrightarrow S$ correspond to the descent data for that extension. Gluing of categories from localizations may also be formalized via comonads.

Mixed distributive laws

Distributive laws between a monad and a comonad are so-called mixed distributive laws; a special case has been rediscovered in physics under the name entwining structures (Brzeziński, Majid 1997). Their theory is often studied in the connection with the theory of comonads in the bicategory of rings, modules and morphisms of modules, that is corings. There is a homomorphism of bicategories from a bicategory of entwinings to a bicategory of corings (Škoda 2008), which is an analogue of the 2-functor $comp$ (R. Street, Formal theory of monads, JPAA 1972) of strict 2-categories in the case of distributive laws of monads (recall also that a distributive law among monads corresponds to a monad in the 2-category of monads).

Examples

• necessity

• writer comonad

• store comonad

• flat modality, infinitesimal flat modality, reduction modality, bosonic modality

• jet comonad

Related concepts

• model structure on coalgebras over a comonad

• polynomial comonad

References

General

• Harry Applegate, Myles Tierney, Iterated cotriples, Lecture Notes in Math. 137 (1970) 56-99 (doi:10.1007/BFb0060440)

Some introductory material on comonads, coalgebras and co-Kleisli morphisms can be found in

• Paolo Perrone, Notes on Category Theory with examples from basic mathematics, Chapter 5. (arXiv)

As contexts in computer science

On comonads in computer science:

• Tarmo Uustalu, Varmo Vene, Comonadic Notions of Computation, Electronic Notes in Theoretical Computer Science 203 5 (2008) 263-284 [doi:10.1016/j.entcs.2008.05.029]

• Tomas Petricek, Dominic Orchard, Alan Mycroft, Coeffects: Unified Static Analysis of Context-Dependence, in: Automata, Languages, and Programming. ICALP 2013, Lecture Notes in Computer Science 7966 Springer (2013) [doi:10.1007/978-3-642-39212-2_35]

• Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Flavien Breuvart, Tarmo Uustalu, Combining effects and coeffects via grading, ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (2016) 476–489 [doi:10.1145/2951913.2951939, talk abstract, video rec]

• Shin-ya Katsumata, Exequiel Rivas, Tarmo Uustalu, LICS (2020) 604-618 Interaction laws of monads and comonads [arXiv:1912.13477, doi:10.1145/3373718.3394808]

Game comonads in logic

Comonads encode positions in back-and-forth games and bisimulations in various fragments of first-order and modal logics. See, for example, the Ehrenfeucht-Fraïssé comonad.

• Samson Abramsky. Structure and Power: an emerging landscape. Fundamenta Informaticae 186(1-4) : 1–26, 2022 (doi:10.3233/FI-222116, arXiv:quant-ph/2206.07393)

• Samson Abramsky and Nihil Shah?, Relating Structure and Power: Comonadic Semantics for Computational Resources (arXiv:1806.09031)

• Samson Abramsky, Anuj Dawar, and Pengming Wang. The pebbling comonad in finite model theory. 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE, 2017 (arXiv:1704.05124)

• Samson Abramsky and Dan Marsden. Comonadic semantics for guarded fragments. 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE, 2021. (arXiv:2008.11094)

• Adam Ó Conghaile and Anuj Dawar. Game Comonads & Generalised Quantifiers. 29th EACSL Annual Conference on Computer Science Logic. 2021. (arXiv:2006.16039)

• Yoàv Montacute and Nihil Shah. The pebble-relation comonad in finite model theory. Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science. 2022. (arXiv:2110.08196)