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: theory: applied category theory

Topic: Algebras

Bartosz Milewski (Mar 24 2020 at 01:11):

I came up with these (co)end formulas for initial and terminal (co)algebras for the endofunctor $f$. Does it make sense? Has anyone seen these?

Here's the carrier for the initial algebra

$\mu f = \int_a a^{C(f a, a)}$

with power defined as

$C(x, a^s) \cong Set(s, C(x, a))$

And the terminal coalgebra

$\nu f = \int^a C(a, f a) \cdot a$

with copower

$C(s \cdot a, x) \cong Set(s, C(a, x))$

Bartosz Milewski (Mar 24 2020 at 01:38):

You can see that a projection

$\pi_a \colon \mu f \to a^{C(f a, a)}$

is a catamorphism. It's a member of the hom-set

$C(\mu f, a^{C(f a, a)})$

or an element of

$Set(C(f a, a), C(\mu f, a))$

Christian Williams (Mar 24 2020 at 01:50):

this is really interesting. I've never seen this construction before

Christian Williams (Mar 24 2020 at 01:51):

by the way, would this be more a #category theory thing than a #applied category theory thing? no big deal though.

Christian Williams (Mar 24 2020 at 01:53):

what is the usual construction of initial algebra you have in mind to compare this to?

Philip Zucker (Mar 24 2020 at 01:57):

Is that the Bohm-Berarducci encoding of Fix?

Philip Zucker (Mar 24 2020 at 01:58):

(translated into Hask I guess)

Nathanael Arkor (Mar 24 2020 at 01:59):

ah, it does look somewhat like Boehm–Berarducci now that you mention it

Christian Williams (Mar 24 2020 at 02:01):

because the one I have in mind is for some signature $\Sigma:\mathrm{Set}\to\mathrm{Set}$, the initial algebra would be given by the directed colimit of $\Sigma (\emptyset) \subset \Sigma(\Sigma (\emptyset)) \subset \dots$

Philip Zucker (Mar 24 2020 at 02:05):

It also reminds me of figure 5 in this paper, which I thought had some interest connections between fixpoint operations and yoneda-y stuff https://arxiv.org/pdf/1907.03481.pdf

Bartosz Milewski (Mar 24 2020 at 02:47):

It's also reminiscent of Kan extensions, but Kan extensions are in Set, and here we are in the category of algebras.

Christian Williams (Mar 24 2020 at 02:50):

I'm not yet seeing how to reconcile the more familiar construction with the new one. I'm mainly just surprised that the initial algebra would be an end, because ends are terminal.

Bartosz Milewski (Mar 24 2020 at 02:53):

In Haskell, this encoding could possibly be considered Boehm-Berarducci.

newtype Mu f = Mu (forall a. (f a -> a) -> a)

and

data Nu f where
  Nu :: (a -> f a) -> a -> Nu f

Bartosz Milewski (Mar 24 2020 at 03:04):

The usual construction is what @Christian Williams mentioned: a colimit of a chain $0 \to f 0 \to f^2 0 \to f^3 0 \to ...$ for initial algebra. For terminal coalgebra it's a limit of $1 \leftarrow f 1 \leftarrow f^2 1 ...$. In Haskell we usually just use Fix, but that's cheating.

Christian Williams (Mar 24 2020 at 03:08):

yes. so for the initial algebra, how can we translate between this directed colimit and the end construction?

Christian Williams (Mar 24 2020 at 05:26):

wow, this is extremely relevant to a problem I've been stuck on, thanks for bringing this up.

Christian Williams (Mar 24 2020 at 05:26):

hope we'll talk about it more tomorrow. also I found this nice webpage by Wadler: http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt

Bartosz Milewski (Mar 24 2020 at 05:46):

I have some notes about (co)algebras, (co)limits, and (co)ends on github: https://github.com/BartoszMilewski/Publications/blob/master/Algebras.pdf

Cody Roux (Mar 24 2020 at 13:26):

I have a somewhat related question: In his recent video (https://www.youtube.com/watch?v=H7l1hwgRUQc) Paolo mentions in passing that every monad on set can be seen as an infinitary free algebra (of some sort) over a set of variables. Can anyone enlighten me with the construction?

Nathanael Arkor (Mar 24 2020 at 13:28):

it's due to the correspondence between Lawvere theories and finitary monads on $\mathbf{Set}$, which extends to a correspondence between (well-behaved) infinitary algebraic theories and monads on $\mathbf{Set}$

Nathanael Arkor (Mar 24 2020 at 13:28):

there's a good introduction to Lawvere theories and monads here: https://www.irif.fr/~mellies/mpri/mpri-ens/articles/hyland-power-lawvere-theories-and-monads.pdf

Cody Roux (Mar 24 2020 at 13:29):

Thanks! What's a "finitary" monad?

Nathanael Arkor (Mar 24 2020 at 13:33):

intuitively, it's a monad whose underlying functor is "morally" one from $\mathbf{FinSet} \to \mathbf{Set}$ — it only depends on finitely-many variables

Nathanael Arkor (Mar 24 2020 at 13:33):

the usual precise definition is a monad whose underlying endofunctor preserves filtered colimits, though

Cody Roux (Mar 24 2020 at 13:39):

Ah cool thanks.

David Spivak (Apr 01 2020 at 21:12):

Bartosz Milewski said:

You can see that a projection

$\pi_a \colon \mu f \to a^{C(f a, a)}$

is a catamorphism. It's a member of the hom-set

$C(\mu f, a^{C(f a, a)})$

or an element of

$Set(C(f a, a), C(\mu f, a))$

Neat!