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: choosing all list objects in a category simulateously

Nico Beck (Aug 17 2023 at 12:20):

When $C$ is a finitely complete and cocomplete category, then the list object $L(A)$ of an object $A$ is the initial $F_A$-algebra where $F_A$ is the endofunctor $X\mapsto \mathbf 1 + X\times A$ on $C$. This means I can choose a list object of $A$ by choosing an initial object in $F_A\operatorname{Alg}$.

I need a version of the universal property where I can choose all list objects simultaneously. That is I am looking for a category $D$ and some functor $U:D\to C$ such that choosing list objects in $C$ is the same thing as choosing a left adjoint of $U$. I'd also be satisfied with any other way which allows me to choose the list objects of a category $C$ all at once.

Is it possible to do that?

Morgan Rogers (he/him) (Aug 17 2023 at 13:26):

Sounds like (a category equivalent to) the Kleisli category?

Mike Shulman (Aug 17 2023 at 16:38):

Well, $L(A)$ is usually also the free monoid generated by $A$, so a natural thought is to take $D$ the category of monoid objects in $C$ and $U$ the forgetful functor. But I don't remember offhand what hypotheses on $C$ are necessary to ensure that every list object is a free monoid and every free monoid is a list object. It certainly suffices for $C$ to be a topos, but that's probably not necessary.

Nico Beck (Aug 17 2023 at 16:52):

Mike Shulman said:

Well, $L(A)$ is usually also the free monoid generated by $A$, so a natural thought is to take $D$ the category of monoid objects in $C$ and $U$ the forgetful functor. But I don't remember offhand what hypotheses on $C$ are necessary to ensure that every list object is a free monoid and every free monoid is a list object. It certainly suffices for $C$ to be a topos, but that's probably not necessary.

Yes, I was also thinking about that. But I wasn't able to show that free monoids = list objects in my category. My category C is finitely complete, infinitary extensive and constructively well pointed (also I am only allowed to use intuitionistic arguments due to the situation I am currently in :/).

Nico Beck (Aug 17 2023 at 16:57):

I spend the afternoon on it and came up with the endofunctor $F:C\times C\to C\times C$ with $F(A,L) = (\varnothing, \mathbf 1 + A\times L)$. When I let $U:F\operatorname{Alg}\to C$ be the functor which sends an algebra $((A,L),\alpha)$ to $A$ then sending $A$ to the algebra $(!,[(),\operatorname{cons}_A]):(\varnothing, \mathbf 1 + \operatorname{List}(A)\times A)\to (A,\operatorname{List}(A))$ should be left adjoint to $U$ if I am not crazy.

Nathanael Arkor (Aug 17 2023 at 17:08):

My understanding is that if you work with parameterised list objects, then they are always free monoids (e.g. see Lemma 3.4 of Saville–Fiore's List Objects with Algebraic Structure). Therefore, so long as your category has parameterised list objects, the two notions will coincide. I believe that the parameterised universal property often holds in examples, so it could be worth checking in your setting. @Philip Saville would be able to say more.

Mike Shulman (Aug 17 2023 at 17:08):

Nico Beck said:

I spend the afternoon on it and came up with the endofunctor $F:C\times C\to C\times C$ with $F(A,L) = (\varnothing, \mathbf 1 + A\times L)$. When I let $U:F\operatorname{Alg}\to C$ be the functor which sends an algebra $((A,L),\alpha)$ to $A$ then sending $A$ to the algebra $(!,[(),\operatorname{cons}_A]):(\varnothing, \mathbf 1 + \operatorname{List}(A)\times A)\to (A,\operatorname{List}(A))$ should be left adjoint to $U$ if I am not crazy.

Yes, I think that's true if you have list objects. But is it true that any left adjoint to that $U$ is of that form? In particular, if $G\dashv U$ then is the first component of $G(A)$ necessarily equal to $A$?

Nico Beck (Aug 17 2023 at 18:14):

Nathanael Arkor said:

My understanding is that if you work with parameterised list objects, then they are always free monoids (e.g. see Lemma 3.4 of Saville–Fiore's List Objects with Algebraic Structure). Therefore, so long as your category has parameterised list objects, the two notions will coincide. I believe that the parameterised universal property often holds in examples, so it could be worth checking in your setting. Philip Saville would be able to say more.

This sounds promising, I will look at it later. :) My situation is that I only need a way to lift list objects from their mere existence to their actual existence (in the sigma type sense). I have a rule in my type theory which allows me to construct an actual adjoint of a functor $U:C\to D$ when it satisfies the property that $$\forall d:D.\ulcorner \text{there merely exists $$\eta: d\to Uc$$initial among such pairs}\urcorner$$, but that left-adjoint functor constructor can only be applied in the empty context, hence my desire to get rid of the $A:ob(C)$ in the context. But I believe that when the free monoids actually exists, then I can use the mere existence of the list types and your result to show that the actual existing free monoids are also list types.

Anyway, thank you for the reference, I will check it out! :):)

Nico Beck (Aug 17 2023 at 18:17):

Mike Shulman said:

Nico Beck said:

I spend the afternoon on it and came up with the endofunctor $F:C\times C\to C\times C$ with $F(A,L) = (\varnothing, \mathbf 1 + A\times L)$. When I let $U:F\operatorname{Alg}\to C$ be the functor which sends an algebra $((A,L),\alpha)$ to $A$ then sending $A$ to the algebra $(!,[(),\operatorname{cons}_A]):(\varnothing, \mathbf 1 + \operatorname{List}(A)\times A)\to (A,\operatorname{List}(A))$ should be left adjoint to $U$ if I am not crazy.

Yes, I think that's true if you have list objects. But is it true that any left adjoint to that $U$ is of that form? In particular, if $G\dashv U$ then is the first component of $G(A)$ necessarily equal to $A$?

Oh no, I should have done the other half of the proof too.

Philip Saville (Aug 17 2023 at 19:43):

Nathanael Arkor said:

My understanding is that if you work with parameterised list objects, then they are always free monoids (e.g. see Lemma 3.4 of Saville–Fiore's List Objects with Algebraic Structure). Therefore, so long as your category has parameterised list objects, the two notions will coincide. I believe that the parameterised universal property often holds in examples, so it could be worth checking in your setting. Philip Saville would be able to say more.

I don't have much to add off the top of my head but I can say this:

1. List objects do not generally coincide with free monoids, eg if you look at the cocartesian monoidal structure on Set every object is the free monoid on itself but certainly not every object is a list object

2. Another way to look at list objects, beyond being parameterised initial list algebras, is that they are essentially algebraically-free monoids in the sense of Kelly's epic "A unified treatment of transfinite constructions" paper (somewhere around Sec 23 I think) - see the screenshot below, which states things a bit more precisely than in the conference paper. We give some conditions for list objects to exist but Kelly may give others that are more useful to you
   3a7bab9d-4d14-43c9-9d04-d4c6879e34e5.jpg

   

3. I think a full answer would mean developing some of the theory of parameterised initiality /parameterised algebras etc. Marcelo and I did a little in the paper Nathanael linked, and there's also some results in Marcelo's thesis, but as far as I know the full story hasn't been spelled out anywhere - if you're interested on collaborating to do this, let me know! One thing to note is that if you're base category is closed the whole parametrised business goes away - there's no need to carry a parameter because you can curry it into the hom-object.

Philip Saville (Aug 17 2023 at 19:48):

(having just double checked, Marcelo does develop a decent chunk of theory of paramaterised algebras in Chapter 6 of his book "Axiomatic domain theory in categories of partial maps", so that may also be worth a look for the general case)

James Deikun (Aug 17 2023 at 21:01):

Philip Saville said:

3a7bab9d-4d14-43c9-9d04-d4c6879e34e5.jpg

How does (3) in this list get along with list types in categories like $\mathrm{CPO}^{\bot}$? There it seems like list objects exist, but they are not the free monoids. Is there something wrong with the list objects there that makes them not "real" list objects?

Mike Shulman (Aug 17 2023 at 21:07):

Philip Saville said:

1. List objects do not generally coincide with free monoids, eg if you look at the cocartesian monoidal structure on Set every object is the free monoid on itself but certainly not every object is a list object

I meant the case originally mentioned of a category with finite limits and colimits, where the monoids are implicitly w.r.t. the cartesian monoidal structure.

Philip Saville (Aug 17 2023 at 21:30):

James Deikun said:

Philip Saville said:

3a7bab9d-4d14-43c9-9d04-d4c6879e34e5.jpg

How does (3) in this list get along with list types in categories like $\mathrm{CPO}^{\bot}$? There it seems like list objects exist, but they are not the free monoids. Is there something wrong with the list objects there that makes them not "real" list objects?

I wasn't aware of this! Tbh I'm not sure, because as far as I know Cpo is generally quite nice. It's possible you have to take some care which monoidal structure you're using - as Mike points out, the classic notion of list object is for cartesian structure but if I remember right pointed Cpos will have a couple of choices (the generalisation to monoidal takes almost no effort, but has been considered less because the motivation comes from a type theory / programming perspective I guess)

Alternatively, I know people have considered various kinds of lazy list structures in Cpo to model eg lists in call by name PCF. One of the things Marcelo noticed for our paper was that these aren't list objects but are list objects with algebraic structure. So maybe that's what's going on?