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: deprecated: id my structure

Topic: Reference requests for polynomial monads

Patrick Nicodemus (Feb 20 2023 at 08:30):

This week I have been investigating polynomial functors on locally Cartesian closed categories whose polynomial is of the form

$1 \leftarrow 1 \xrightarrow{e} I \to 1$

where $1$ is the terminal object and $I, e$ are the only data one has to supply.
In $\mathbf{Sets}$ we must have $I = 1+A$ for some set $A$ and so these are just the monads $X\mapsto X+ A$ for some fixed object $A$. Outside of $\mathbf{Sets}$ things can be more complicated. I have some interesting results.

I would like any references anyone can dig up on polynomial functors of this particular form.

Patrick Nicodemus (Jun 19 2023 at 01:20):

It turns out that what I needed here was precisely G. Rosolini's PhD thesis on "Continuity and effectiveness in topoi."

There are some very interesting results in here which are absolutely exactly what I needed.
Let C be a category with pullbacks.
Let M be a class of monic morphisms in C, stable under pullback, including all isomorphisms, and closed under composition.

We say M is classified if the category of M-maps and pullback squares has a terminal object, i.e. every M-map is a pullback of this distinguished morphism. If this terminal object exists, we can prove that its domain is the terminal object of C, thus we can write $e : 1\to I$ for this distinguished classifying morphism. If the morphism $e$ is exponentiable, as it always is in a topos, then the $M$-maps are actually the algebras of a certain comonad on the arrow category. The polynomial monad above plays an important role in this theory: if we write $T$ for the polynomial monad, and $A$ and $B$ are given objects, then maps $f: B\to T(A)$ are in one-to-one correspondence with $M$-partial maps $B\to A$, i.e., partial maps defined on an $M$-subobject of $A$. Thus, $T$ sends each object to its $M$-partial map classifier. In a topos, we can take $I=\Omega$, the object of truth values, and we get the (covariant) powerset monad.

Patrick Nicodemus (Jun 19 2023 at 01:22):

Richard Garner has proved that the $M$-partial maps in this setting are precisely the coalgebras of a certain comonad on the arrow category, and there is an algebraic weak factorization system on the category which gives a functorial factorization of any map through an $M$-map.

Patrick Nicodemus (Jun 19 2023 at 01:23):

This is particularly interesting for simplicial sets, when $I$ is the unit interval and $e$ is the inclusion at time $t=0$. The class $M$ contains the "left subobjects". The resulting monad is the cone monad. His work on simplicial lalis is very interesting.

Patrick Nicodemus (Jun 23 2023 at 00:18):

Can somebody give me a formal reference for the material on "Relation to object classifiers" here?
https://ncatlab.org/nlab/show/polynomial+monad

Patrick Nicodemus (Jun 23 2023 at 00:18):

I have the paper by Gambino and Kock but I can't find this perspective here.

Patrick Nicodemus (Jun 23 2023 at 00:34):

@Mike Shulman It seems like you added this material to the nlab, from the comments on the page. If I want to cite a source for this do you know of any clean write up? https://nforum.ncatlab.org/discussion/5597/polynomial-monad/?Focus=59047#Comment_59047

Patrick Nicodemus (Jun 23 2023 at 00:42):

https://mathoverflow.net/questions/434602/reference-request-a-lemma-on-universes-and-polynomial-monads
This question has been asked on stackexchange and has received no answer

Mike Shulman (Jun 26 2023 at 17:01):

No, I don't know of anywhere that stuff has been written up more carefully, sorry.

Mike Shulman (Jun 26 2023 at 17:03):

Steve Awodey and his students have been working on the relation between polynomial composition structure and models of type theory, which is at least related, particularly to the MO question, e.g. Clive Newstead's thesis https://arxiv.org/abs/2103.06155.

Mike Shulman (Jun 26 2023 at 17:12):

Also relevant is Steve's HoTT 2023 talk on algebraic type theory.

Steve Awodey (Jul 09 2023 at 14:06):

Patrick Nicodemus said:

Can somebody give me a formal reference for the material on "Relation to object classifiers" here?
https://ncatlab.org/nlab/show/polynomial+monad

I added the relevant references to Natural models, Algebraic type theory, etc., on the nLab page.