Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: coalgebraic logic basics

David Egolf (Feb 10 2022 at 16:10):

Nima Motamed said:

I would be glad to; though it might be best to talk about the basics and specifics of modal logic, coalgebra and coalgebraic logic in a different topic, so the focus here can stay on applications of the Yoneda lemma. I'll answer the following here though, just for clarity :)

Wonderful!
In this thread, I am hoping we can ask and answer questions regarding the basics of modal logic, coalgebras and coalgebraic logic - at least enough to understand @Nima Motamed's example application of the Yoneda lemma in #learning: questions > yoneda lemma applications .

(I'll post some specific questions here later today! Hopefully we can have an interesting discussion).

David Egolf (Feb 10 2022 at 20:50):

The first question I have is: What is a coalgebra?
I found a definition in "Coalgebraic logic" by Moss (p. 288):
A coalgebra for an endofunctor $F: Set \to Set$ is a pair $(A,e)$ such that $A$ is a set or class, together with a map $e: A \to FA$. $A$ is called the carrier, and $e$ is the coalgebra map.

David Egolf (Feb 10 2022 at 20:51):

Would this be called an $F$-coalgebra? (I think so!)

David Egolf (Feb 10 2022 at 20:56):

Take Kripke frames, which are just unlabelled non-deterministic transition systems, or more simply just binary relations $R$ on a set $S$. Such a binary relation $R$ can equivalently be treated as a function $r: S \to \mathcal{P} S$, with $r(s) = \{t \in S \mid sRt\}$, i.e. the set of all successor states of $s$.

Let me see if I can understand how this is a coalgebra. We start with the functor $\mathcal{P}: Set \to Set$ that sends any set to its powerset, and any function $f$ to the corresponding function between powersets (that sends any subset to the image of that subset under $f$).
A $\mathcal{P}$-coalgebra I think is a pair $(S,r)$ where $S$ is a set and $r$ is a map $r: S \to \mathcal{P}(S)$. This is indeed what we have - the map $r$ sends any given state to the set of successor states. (Here $S$ is a set of states).
So, we do indeed have a $\mathcal{P}$-coalgebra.

David Egolf (Feb 10 2022 at 21:11):

Nima Motamed said:

If you would be interested in deterministic automata for some alphabet $\Sigma$, then you can verify that these are precisely coalgebras for the functor $TX = X^\Sigma \times 2$, ignoring the requirements of a finite set of states and a distinguished initial state.

Let's see if I can now understand this^.
Let $T$ be a functor $T: Set \to Set$ that acts on objects by $TX = X^\Sigma \times 2$. Then, a $T$-coalgebra is a pair $(Q, f)$, where $Q$ is a set and $f$ is a map $f: Q \to TQ$.
Here $Q$ is a set of states. What is $f$? It is a map $f: Q \to Q^\Sigma \times 2$.
Say we evaluate $f$ on some particular state $q \in Q$. Then $f(q) \in Q^\Sigma \times 2$. I think this can be viewed as describing the way in which the system moves to the next state from $q$. To start with, the first part of $f(q)$ is a function from $\Sigma$ (which might be a set of possible inputs) to $Q$, the possible states. So, this part of $f(q)$ can be viewed as describing which state is next after $q$, and this next state is allowed to depend on inputs provided. I'm not sure what the $\times 2$ part does - I suppose it could be viewed as providing some kind of label for the "kind" of the next state?

John Baez (Feb 10 2022 at 21:14):

David Egolf said:

The first question I have is: What is a coalgebra?
I found a definition in "Coalgebraic logic" by Moss (p. 288):
A coalgebra for an endofunctor $F: Set \to Set$ is a pair $(A,e)$ such that $A$ is a set or class, together with a map $e: A \to FA$. $A$ is called the carrier, and $e$ is the coalgebra map.

Just to warn you, "coalgebra" means three main things:

1) a "coalgebra of a functor", which you've described: nice and simple.

2) a "coalgebra of a comonad", which is very much like an algebra of a monad, but with all the arrows turned around.

2) to algebraists, a "coalgebra" is a monoid in $(\mathrm{Vect}^{\mathrm{op}}, \otimes)$ just as an "algebra" is a monoid in $(\mathrm{Vect}, \otimes)$. For example, the vector space of $n \times n$ matrices is an algebra with the usual matrix multiplication, but there's also a way to make it into a coalgebra.

You definitely don't want to learn all three of these things at once! You can probably ignore two of them. I only mention them because for beginners it can be confusing that different people use the word "coalgebra" in different ways, when they're looking around online.

You probably picked the right one to focus on, number 1), though of course @Nima Motamed will be the one who knows what he wants to talk about.

John Baez (Feb 10 2022 at 21:15):

Number 2) may also show up at some point in your studies with Nima; hard to tell.

John Baez (Feb 10 2022 at 21:16):

It's delightful how all 3 fit together in the end, but don't think about that. :upside_down:

David Egolf (Feb 10 2022 at 21:22):

I appreciate the warning/clarification! Googling the term "coalgebra" was indeed rather confusing.

Peter Arndt (Feb 11 2022 at 09:47):

About what the $\times 2$ part does: The composite map $Q \to Q^\Sigma \times 2 \to 2$ (second arrow the projection) singles out a subset of $Q$, the set of "accepted states". The idea is that the automaton reads a string of symbols from the alphabet, symbol by symbol, and if it ends in an accepted state, the string is accepted.

Peter Arndt (Feb 11 2022 at 09:55):

In detail: You start in a starting state. You apply the map $Q \to Q^\Sigma \times 2 \to Q^\Sigma$ (first projection this time) to your current state and get a map $\Sigma \to Q$. You read a symbol from your string and apply that map to it. You go into the new state you obtained. You repeat this until your string of symbols ends. Then you apply $Q \to Q^\Sigma \times 2 \to 2$ and see if you get $1$ (i.e. whether you are in a an accepted state). If yes, the string is accepted, otherwise not. In this way automata define subsets of the set of all words over the alphabet (e.g. the well-formed formulas of a logic, or the syntactically correct programs in some programming language).

Nima Motamed (Feb 11 2022 at 12:58):

David Egolf said:

The first question I have is: What is a coalgebra?
I found a definition in "Coalgebraic logic" by Moss (p. 288):
A coalgebra for an endofunctor $F: Set \to Set$ is a pair $(A,e)$ such that $A$ is a set or class, together with a map $e: A \to FA$. $A$ is called the carrier, and $e$ is the coalgebra map.

John Baez said:

Just to warn you, "coalgebra" means three main things:

1) a "coalgebra of a functor", which you've described: nice and simple.

2) a "coalgebra of a comonad", which is very much like an algebra of a monad, but with all the arrows turned around.

2) to algebraists, a "coalgebra" is a monoid in $(\mathrm{Vect}^{\mathrm{op}}, \otimes)$ just as an "algebra" is a monoid in $(\mathrm{Vect}, \otimes)$. For example, the vector space of $n \times n$ matrices is an algebra with the usual matrix multiplication, but there's also a way to make it into a coalgebra.

You definitely don't want to learn all three of these things at once! You can probably ignore two of them. I only mention them because for beginners it can be confusing that different people use the word "coalgebra" in different ways, when they're looking around online.

You probably picked the right one to focus on, number 1), though of course Nima Motamed will be the one who knows what he wants to talk about.

Indeed. Sorry I didn't specify the type of coalgebra I meant - that is very confusing. While all three notions mentioned by @John Baez are highly related, it is most relevant to the examples we've been discussing to stick to the simple definition of a $T$-coalgebra for a general functor $T: \mathbf{Set} \to \mathbf{Set}$, which is the definition you found in Moss' work. The coalgebraic logic he speaks of is by the way not precisely of the same flavor of logic I was talking about - his logic is truly beautiful, but also very strange, at least when you first encounter it. I'd love to also chat about that, but I don't think it would aid in understanding coalgebraic logic right now :)

David Egolf said

Let me see if I can understand how this is a coalgebra. We start with the functor $\mathcal{P}: Set \to Set$ that sends any set to its powerset, and any function $f$ to the corresponding function between powersets (that sends any subset to the image of that subset under $f$).
A $\mathcal{P}$-coalgebra I think is a pair $(S,r)$ where $S$ is a set and $r$ is a map $r: S \to \mathcal{P}(S)$. This is indeed what we have - the map $r$ sends any given state to the set of successor states. (Here $S$ is a set of states).
So, we do indeed have a $\mathcal{P}$-coalgebra.

Precisely!

Let's see if I can now understand this^.

@Peter Arndt explained this perfectly - I hope that helps, and if not, give a shout.

Nima Motamed (Feb 11 2022 at 12:58):

I don't want to push any material on you and risk not matching the pace at which you'd like to explore all of this, so please feel free to ask any questions - coalgebra and coalgebraic logic are honestly some of my favorite branches of mathematics/logic, so it's always great to have an excuse to talk about them. (This also increases the risk of me dumping a tidal wave of information on you, hence why I'm being a bit careful ;) )

Until you come with questions, I do want to point you towards some excellent, detailed and approachable material on the subject, all of which is freely and legally available online.

For the general theory of coalgebra (for a functor), also referred to as universal coalgebra, Jan Rutten's most recent book is hard to beat. He focuses on coalgebras for $\mathbf{Set}$-functors, and provides a good amount of examples of dynamical systems that can be studied through the coalgebraic lens.

If you then want to look at the interplay between coalgebra and (modal) logic, this article, written by several coalgebraic logicians, gives a nice conceptual introduction to a broad audience. I am a big fan of one of the arguments they give for the use of coalgebraic logic: whenever you are considering a new type of transition structure and/or its logic, you can often just plug it into the general theory of coalgebraic logic, and get a bunch of definitions, theorems and even algorithms for free! Coalgebra and coalgebraic logic find a lot of their strength in this plug-and-play approach.

Finally, if you want to get into the more technical side of coalgebraic logic, there's this article by Clemens Kupke and Dirk Pattinson.

There's of course a lot more material to be found than this -the rabbit hole goes deep, moving through (Stone) duality theory and factorization systems- but the articles I mentioned give a strong, and more importantly pleasant introduction.

David Egolf (Feb 11 2022 at 23:17):

Thanks for the wonderful recommendations, @Nima Motamed ! I started looking at Rutten's book , and it looks excellent.
I don't have a specific question for you right now. However, I wanted to express how cool the idea of an "algebra" is, as introduced in that book!

Before Rutten's book defines a coalgebra, it defines an algebra:
"Let $F: C \to C$ be a functor from a category $C$ to itself. An $F$-algebra is a pair $(A, \alpha)$ consisting of an object $A$ an arrow $\alpha: F(A) \to A$".
This seems like an amazing framework for making your own algebraic structures!

For example, say we want an algebraic structure corresponding to a binary operation on the real numbers, together with some distinguished element of the real numbers. Then, we could consider maps of the form: $\alpha: 1 + \mathbb{R}^2 \to \mathbb{R}$, where + is the disjoint union, and 1 is a set with a single element.
$\alpha$ is a function that takes in an element from 1 OR an element from $\mathbb{R}^2$, and returns a real number. So, it contains information about two maps: $\alpha_1: 1 \to \mathbb{R}$ and $\alpha_2: \mathbb{R}^2 \to \mathbb{R}$. It describes both a distinguished element of $\mathbb{R}$ and a binary operation on $\mathbb{R}$. Maps of this form will corresponds to $F$-algebras, where $F(S) = 1 + S^2$ for a set $S$.

This strategy for thinking about algebraic structures also lets one start with a functor $F$ of interest and then ask what an $F$-algebra would correspond to. For example, in the context of imaging, say $F: Set \to Set$ sends a set $S$ to the set of "observations" of its elements $F(S)$. Then an $F$-algebra would correspond to a map $\alpha: F(A) \to A$ for some set $A$, which sends observations to (perhaps) estimates for unknown objects. I guess a $F$-coalgebra in this case would be a map $\beta: A \to F(A)$ that sends set elements to their observations. In imaging system in general is going to have both of these. (This makes me wonder if morphisms of algebras and morphisms of coalgebras would correspond to an interesting way to relate image reconstruction schemes, and observation schemes, respectively).

It feels exciting to have a clean framework to describe and generate custom algebraic structures in terms of functors!

David Egolf (Feb 13 2022 at 15:52):

It seems like coalgebras correspond to components of a particular kind of natural transformation.
Let $F: Set \to Set$ be a functor and $id: Set \to Set$ be the identity functor.
Let $\eta: id \to F$ be a natural transformation.
Then the component of $\eta$ for a set $A$ is a function $\eta_A: A \to F(A)$. This is a coalgebra $(\eta_A, A)$.

Also, if $\eta_A$ and $\eta_B$ are components of $\eta$, and there is a function $f: A \to B$, I believe there is a morphism of coalgebras between $(\eta_A, A)$ and $(\eta_B, B)$ corresponding to $f$. The existence of this morphism (a commutative square) corresponds to the fact that $\eta$ is a natural transformation.

I suppose this means we can view this kind of natural transformation as corresponding to a collection of coalgebras, and morphisms between them. Does this seem right? (If so - do we care about this connection?)