symmetric monoidal (∞,1)-category of spectra
Definitions
Transfors between 2-categories
Morphisms in 2-categories
Structures in 2-categories
Limits in 2-categories
Structures on 2-categories
A polynomial monad is a monad on a category whose underlying endofunctor is a polynomial functor and whose unit and multiplication are cartesian natural transformations. This is of course equivalent to being a monad in the bicategory of polynomial functors and cartesian transformations.
A basic example is the free-monoid monad (Gambino-Kock 09, Example 1.9). This is exhibited by the polynomial where the middle arrow is such that for all its fiber over has cardinality .
One can construct the free monad on a polynomial endofunctor, and it is a polynomial monad.
Every polynomial monad is a p.r.a. monad.
Since all polynomial functors preserve pullbacks, a polynomial monad is necessarily a cartesian monad. Note that cartesian transformations between polynomial functors also have an explicit description: they are given by diagrams
in which the middle square is a pullback. Thus, all the data of a polynomial monad can be described very concretely. This gives a convenient way to produce cartesian monads, and indeed very many cartesian monads arising in practice are in fact polynomial. Polynomial monads have close relations with a number of other notions.
Polynomial monads (on rather than a slice of it) are, in some sense, the most natural base monads for the theory of clubs. Although the club construction can be performed over any cartesian monad, if this monad is polynomial, then all clubs over it are also polynomial, since polynomial functors are a sieve with respect to cartesian transformations. Moreover, the club monoidal structure can be seen as just an instance of the explicit construction of composition for polynomials (see 1.11 of (Gambino-Kock)).
The bicategory of polynomial functors and cartesian transformations is in fact the horizontal bicategory of a double category , whose vertical arrows are the morphisms of and whose cells are diagrams like
in which the middle square (only) is a pullback. Suppose , so the bottom polynomial is determined by a single morphism , and that . Then to give the rest of the diagram is to give an object , a morphism , and a morphism . By adjointness, the latter is equivalent to giving a morphism ; but this codomain is just , where is the polynomial functor determined by .
Thus, a polynomial equipped with a cartesian transformation to is exactly a “-span” such as arises in the theory of generalized multicategories. A similar argument shows that if is a polynomial monad, then the slice double category of over is equivalent to the double category of -spans (a.k.a. the “horizontal Kleisli” double category). Therefore, polynomial monads cartesianly-over , being the horizontal monads in this double category, are precisely -multicategories. (Such polynomial monads on itself, rather than any slice, are the -clubs mentioned above; in general a -multicategory is identified with the monad it induces on .)
Polynomial monads have a natural interpretation in terms of object classifiers. Specifically, given any polynomial , generating a polynomial functor , we can consider the class of all pullbacks of . A cartesian unit says that is a pullback of , and therefore so are all identities. Similarly, the composite involves the classifying object for a pair of composable -morphisms, and so a cartesian multiplication tells us that is closed under composition.
Thus, a polynomial monad (on ) can be regarded as a morphism together with a coherent way to make into a category. More precisely, consider the slice category , where is the category whose objects are morphisms of and whose morphisms are pullback squares. This comes with source and target functors . To make into a polynomial monad is then equivalent to giving unit and composition functors enhancing to a double category such that the forgetful map is a double functor.
This claim could stand some independent verification.
For example, consider the free monoid monad above determined by . To exhibit a function as a pullback of this is to say that its fibers are finite and have been equipped with bijections to canonical finite sets, which we may as well think of as giving them linear orders. To give the monad structure on this functor is equivalent to noting that every identity map has ordered finite fibers, and the composite of functions with ordered finite fibers again has ordered finite fibers, in a way that is associative, unital, and stable under pullback.
Other interesting examples include:
The class of discrete Conduche functors with ordered finite fibers is almost an example; it wants to be classified by the bicategory of spans between finite sets, but that is not an object of . Thus, a polynomial monad in determined by a discrete Conduche functor with ordered finite fibers is a reasonable substitute for the nonexistent notion of “-club”.
Identifying the classes of morphisms corresponding to standard polynomial monads like these also tells us how to identify when a polynomial monad is induced by a club (or more generally a generalized multicategory) over them: when the for that monad belongs to the appropriate class, compatibly. For instance, if is the monad for cartesian strict monoidal categories, then a polynomial monad on is an -club just when the morphism in its defining polynomial is a discrete fibration with ordered finite fibers, and its composition and unit respect that structure.
A fairly comprehensive discussion of the notion is due to
The homotopy theory of algebras over polynomial monads is in
An application to the theory of opetopes in discussed in
, §4.3-4.6, where the main result is that the polynomial monad of stable opetopes is a least fixpoint of the Baez-Dolan construction for polynomial monads.
An extension of type theory with a universe of associative and unital polynomial monads to define opetopic types in order to encode fully coherent algebraic structures is in
Polynomial monads as a “generalization of small categories” for homotopy theory are studied in
The relation between polynomial monads, object classifiers, and models of (homotopy) type theory is studied in
Steve Awodey, Natural models of homotopy type theory, 2017: arxiv
Steve Awodey, Clive Newstead; Polynomial pseudomonads and dependent type theory, 2018: arxiv
Clive Newstead, Algebraic models of dependent type theory, 2021: arxiv
Steve Awodey, Algebraic type theory, slides from HoTT 2023
Last revised on July 10, 2023 at 07:25:04. See the history of this page for a list of all contributions to it.