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: practice: terminology & notation

Topic: Definition of streams

Madeleine Birchfield (Dec 24 2023 at 20:14):

On the nLab there is currently a number of discussions over whether the set of streams of a set $A$ is defined as the final coalgebra of the endofunctor $X \mapsto A \times X$ or the endofunctor $X \mapsto 1 + A \times X$:

https://nforum.ncatlab.org/discussion/17554/list-of-notable-initial-algebras-and-terminal-coalgebras/#Item_0

https://nforum.ncatlab.org/discussion/17572/stream/#Item_0

Nathaniel Virgo (Dec 25 2023 at 08:05):

I'd say both deserve to be called "streams", but personally I'd assume $X\mapsto A\times X$ unless you said otherwise. There's lots of work that uses that definition, e.g. Rutten's work on "stream calculus".

fosco (Dec 25 2023 at 11:14):

I'm far from being an expert, but now that I think about it, I have seen both definitions; usually I intend $A\times-$, but Jacobs' coalgebra book (iirc) uses instead $1+A\times-$...

Matteo Capucci (he/him) (Dec 27 2023 at 14:05):

In Glasgow the first are called streams and the latter colists

Oscar Cunningham (Dec 28 2023 at 14:40):

Would it be right to say that costreams are well defined, but that there aren't any?

Morgan Rogers (he/him) (Dec 29 2023 at 09:20):

@Oscar Cunningham what would be your intuitive definition of costream and why do you expect there not to be any?

Oscar Cunningham (Dec 29 2023 at 12:45):

I was checking my understanding of recursion and corecursion. The set of lists is defined as an initial algebra of the endofunctor $X\mapsto 1+A×X$, which is the set of finite sequences valued in $A$. @Matteo Capucci (he/him) suggested using the term colist for the elements of the terminal coalgebra of this endofunctor; sequences of elements of $A$ that are allowed to be finite or infinite.

The set of streams is defined as the terminal coalgebra of $X\mapsto A×X$, which is precisely the infinite sequences valued in $A$. So the set of costreams would be the initial algebra of this endofunctor. But I think this is just the empty set, since there's nothing like the $1+$ in the endofunctor to force you to have any elements at all.

fosco (Dec 29 2023 at 13:10):

Maybe this argument works: on the category of Sets, or any other Cartesian closed category, $A\times-$ commutes with colimits; its category of endofunctor algebras then has colimits and they are "well-behaved", so the initial object in the base (=the empty set) is created and becomes the initial object in the category of algebras, and also a fixpoint: so the initial costream is indeed the emtpy set.

Matteo Capucci (he/him) (Dec 29 2023 at 13:28):

I don't think there's any mathematical doubt here, the question is whether to adopt the nomenclature 'costreams' for such an object, I'd say it's technically OK but not very useful. Hence my :shrug::

Matteo Capucci (he/him) (Dec 29 2023 at 13:28):

To me adding the co makes sense in the initial->terminal direction, not much conversely

Matteo Capucci (he/him) (Dec 29 2023 at 13:29):

But the rules are made up so :shrug:

Ralph Sarkis (Dec 29 2023 at 13:49):

Matteo Capucci (he/him) said:

To me adding the co makes sense in the initial->terminal direction, not much conversely

:face_with_raised_eyebrow: limits->colimits are in the converse direction

Morgan Rogers (he/him) (Dec 29 2023 at 13:51):

They might be more interesting in other categories though.

Kenji Maillard (Dec 29 2023 at 15:49):

I would expect costreams to be inhabited in the category of pointed sets for instance

Matteo Capucci (he/him) (Dec 29 2023 at 16:07):

Ralph Sarkis said:

Matteo Capucci (he/him) said:

To me adding the co makes sense in the initial->terminal direction, not much conversely

:face_with_raised_eyebrow: limits->colimits are in the converse direction

I'm talking about this specific terminological pattern (terminal algebras being named after the corresponding initial algebra)

Notification Bot (Dec 29 2023 at 16:07):

This topic was moved here from #theory: category theory > Definition of streams by Matteo Capucci (he/him).

Mike Shulman (Dec 29 2023 at 16:56):

It would be nice if we could make a uniform choice of which side has the "co", but I don't think we can hope for that.