nLab polynomial functor

Redirected from "dependent polynomial functor".
Polynomial functors

This entry is about a notion in category theory. For a different notion of the same name in (stable) homotopy theory see at Goodwillie calculus.

Polynomial functors

Idea

The concept of polynomial functor is a categorification of that of polynomial.

Polynomial endo-functors are used to encode a class of inductive types called W-types, and also as the underlying data of polynomial monads.

Definition

Let CC be a locally cartesian closed category. A polynomial is a diagram

WfXgYhZ W \overset{f}{\leftarrow} X \overset{g}{\to} Y \overset{h}{\to} Z

in CC. The corresponding polynomial functor is the composite

C/Wf *C/XΠ gC/YΣ hC/Z, C/W \overset{f^*}{\to} C/X \overset{\Pi_g}{\to} C/Y \overset{\Sigma_h}{\to} C/Z \,,

where Π g\Pi_g and Σ h\Sigma_h are the dependent product and dependent sum operations, right and left adjoint respectively to pullback functors g *g^* and h *h^*.

When W=ZW=Z, this is a polynomial endofunctor.

Sometimes this general notion is called a dependent polynomial functor (also typed or colored (FMLS, p. 68)), with “polynomial (endo)functor” reserved for the “one-variable” case, when W=Z=1W=Z=1 is the terminal object.

The data ff, gg, and hh that specify a polynomial functor is sometimes referred to as a container (or an indexed container, with container reserved for the case W=Z=1W=Z=1). Other times container is used as a synonym for “polynomial functor”. Sometimes the data f,g,hf,g,h are instead referred to as a polynomial to distinguish them from the “polynomial functor” they determine.

If gg is an identity, the functor is sometimes called a linear functor or a linear polynomial functor. Note that this notion makes sense even if CC is not locally cartesian closed; all it needs are pullbacks. More generally, we can make sense of polynomial functors in any category with pullbacks if we restrict gg to be an exponentiable morphism.

Examples

On sets

For CC = Set the polynomial functor induced from a function gg

*XgY* \ast \stackrel{}{\leftarrow} X \stackrel{g}{\longrightarrow} Y \stackrel{}{\longrightarrow} \ast

is given by

SP g(S)= yYS X y, S \mapsto P_g(S) = \coprod_{y \in Y} S^{X_y} \,,

where X yX_y is the fiber of gg over yYy \in Y, and where the exponential object S X yS^{X_y} is the function set of functions from the fiber to SS. The cardinality of the set on the right is

|P g(S)|= yY|S| |X y| {\vert P_g(S)\vert} = \sum_{y \in Y} {\vert S\vert}^{\vert X_y\vert}

and it is in this sense that the concept of polynomial functor is a kind of categorification of that of polynomial.

On the other hand the dependent polynomial functor associated to

Ap 1XidXp 2B A \stackrel{p_1}{\leftarrow} X \stackrel{id}{\longrightarrow} X \stackrel{p_2}{\longrightarrow} B

acts by

(S a) aA( aAS a×X ab) bB. (S_a)_{a \in A} \mapsto \left(\coprod_{a \in A} S_a \times X_{a b} \right)_{b \in B} \,.

Under cardinality this becomes matrix multiplication acting on vectors (with entries in the natural numbers). So in this case the dependent polynomial functor is a linear functor of several variables, an integral transform.

In a general lextensive category

Taking the fibres in the previous example to be finite, uniformly bounded (in the sense that all the fibres have size at most NN), we can partition the set YY as nN{yY|g 1(y)|=n}= nNY n\coprod_{n \leq N} \{y\in Y\mid |g^{-1}(y)| = n \} = \coprod_{n \leq N} Y_n. Then, after choosing isomorphisms g 1(y){1,,|g 1(y)|}g^{-1}(y) \simeq \{1,\ldots,|g^{-1}(y)|\} for each yYy\in Y, the polynomial endofunctor P gP_g is naturally isomorphic to the functor

S n=0 NY n×S n, S \mapsto \coprod_{n=0}^N Y_n\times S^n\,,

as the hom-set S {1,,n}S nS^{\{1,\ldots,n\}} \simeq S^n. Thus we have a “literal polynomial” in the object argument of the functor. Such literal polynomials make sense as endofunctors of any lextensive category, for example any pretopos. However, this does not automatically mean that these endofunctors are actually polynomial endofunctors, strictly speaking.

Proposition

Literal polynomial endofunctors on an lextensive category are polynomial endofunctors.

Proof

Note that in an arbitrary lextensive category there is little guarantee that any dependent products exist. However, the right adjoint to pullback functor associated to an iterated codiagonal k=1 nAA\coprod_{k=1}^n A\to A does exist, for any lextensive category. And this is all that is needed.

Consider, then, the map gg defined as

n=1 N( k=1 nY n) n=1 N Y n n=0 NY n \coprod_{n=1}^N \left(\coprod_{k=1}^n Y_n \right) \stackrel{\coprod_{n=1}^N \nabla_{Y_n}}{\longrightarrow} \coprod_{n=0}^N Y_n

The pullback along Y n\nabla_{Y_n} of an arbitrary map f:TY nf\colon T\to Y_n is k=1 nT k=1 nf k=1 nY n\coprod_{k=1}^n T \stackrel{\coprod_{k=1}^n f}{\longrightarrow} \coprod_{k=1}^n Y_n. The dependent product along Y n\nabla_{Y_n} of an arbitrary map can be written as a composite of dependent product functors, which are themselves coproducts of dependent product along the ordinary codiagonal Y nY nY nY_n \sqcup Y_n \to Y_n, and along identity maps. The dependent product of STfgY nY nS\sqcup T \stackrel{f\sqcup g}{\longrightarrow} Y_n \sqcup Y_n along the codiagonal can be easily checked to be S× Y nTY nS\times_{Y_n} T \to Y_n. So we know that the functor Π Y n\Pi_{\nabla_{Y_n}} exists, and it remains to calculate what the polynomial functor associated to gg is.

This can be done summand by summand, i.e. for each n=1,,Nn=1,\ldots, N, since the final dependent sum merely takes the coproduct of each dependent product. So the only thing to double check is that, for each nn,

Π Y n( k=1 nY n×S k=1 nY n)=(Y n×S nY n), \Pi_{\nabla_{Y_n}} (\coprod_{k=1}^n Y_n \times S \to \coprod_{k=1}^n Y_n) = (Y_n\times S^n \to Y_n)\,,

which follows from the description of the pullback along Y n\nabla_{Y_n} and the defining properties of products, coproducts, and their interactions in a lextensive category. There is a boundary case, namely that corresponding to n=0n=0, which amounts to dependent product along 0Y 00 \to Y_0. But in an extensive category, initial objects are strict, and so we need to take the dependent product of 0×S=000\times S = 0 \to 0, which is then just the identity map on Y 0Y_0.

The final dependent product then gives the output of the polynomial functor, which is then the literal polynomial we started with, namely n=0 NY n×S n\coprod_{n=0}^N Y_n\times S^n.

In the above proof, the only place that the existence of arbitrary pullbacks in a lextensive category was used is in constructing the general dependent product along the codiagonal. Obviously one still needs finite products, just to get off the ground. For the purposes of expressing the literal polynomial as a polynomial functor, this dependent product only need be applied to the projection map (YY)×S(YY)(Y\sqcup Y) \times S \to (Y\sqcup Y). Thus while Π Y n\Pi_{\nabla_{Y_n}} may not exist in a general extensive category with binary products, the composite Π Y n(YY) *\Pi_{\nabla_{Y_n}}\circ (Y\sqcup Y)^* does. The extent to which such an endofunctor deserves to be called a polynomial endofunctor is up for debate.

In a lextensive category with countable coproducts (and the corresponding compatibility with pullbacks), for instance an infinitary pretopos one can extend the above example to endofunctors of the form

S n=0 Y n×S n, S \mapsto \coprod_{n=0}^\infty Y_n\times S^n\,,

with practically identical proof and no additional assumptions.

The 2-category of polynomial functors

Any polynomial functor, as defined above, is automatically equipped with a tensorial strength, when the slice categories of CC are regarded as tensored over CC in the canonical way. The following theorem is proven in Gambino–Kock:

Theorem

There is a bicategory whose objects are the objects of CC, whose morphisms from WW to ZZ are diagrams of the form

WfXgYhZ, W \overset{f}{\leftarrow} X \overset{g}{\to} Y \overset{h}{\to} Z,

and whose 2-morphisms are diagrams of the form

X Y id W X× YY Y Z X Y. \array{ & & X & \to & Y \\ & \swarrow & \uparrow & & \mathllap{id}\uparrow & \searrow\\ W && X' \times_{Y'} Y & \to & Y && Z\\ &\nwarrow & \downarrow & & \downarrow & \nearrow \\ && X' & \to & Y'. }

This bicategory is equivalent to the 2-category whose objects are slice categories of CC, whose morphisms are polynomial functors regarded as strong functors, and whose 2-morphisms are strength-respecting natural transformations.

In particular, “being polynomial” is a mere property of a strong functor between slice categories. That is, the data f,g,hf,g,h are uniquely determined, up to isomorphism, by the strong functor they generate. (Note, though, that the property of “being polynomial” depends on a prior identification of the domain and codomain as being slice categories of some specified ambient category CC. In particular, a functor C/ZC/ZC/Z \to C/Z might be polynomial when its domain and codomain are regarded as slice categories of CC, but not when they are regarded as slices of C/ZC/Z over 11 — this happens when W=ZW=Z but hgfh g \neq f.)

Note that the above bicategory contains, as a locally full sub-bicategory, the usual bicategory of spans. Thus, as a special case, the bicategory of spans is equivalent to the 2-category of “linear” polynomial functors. Both of these are instances of Lack's coherence theorem.

There is a particular subclass of the 2-morphism in this bicategory that is also interesting: a 2-morphism corresponds to a cartesian natural transformation if and only if the map X× YYXX' \times_{Y'} Y \to X is an isomorphism. Since anything isomorphic to a pullback is a pullback, in this case the diagram can be drawn more simply by omitting the upper square and merely asking that the lower square be a pullback.

Furthermore, this bicategory is actually the horizontal bicategory of a double category, indeed a framed bicategory, in which the vertical arrows are the arrows of CC, and the cells are diagrams as above but allowing also morphisms WWW\to W' and ZZZ\to Z' on the left and right.

The multicategory of single-variable polynomials

Let \mathcal{E} be a category with (chosen) pullbacks and let 𝒟\mathcal{D} be a class of morphisms in \mathcal{E} called display maps.

There is a multicategory Poly()\mathbf{Poly}(\mathcal{E}), first introduced by Garner, 2019 and attributed to Weber, 2015, whose:

  • objects are 𝒟\mathcal{D}-maps p:EBp \colon E \rightarrow B (that is, a polynomial *EB** \leftarrow E \rightarrow B \rightarrow *)

  • nullary morphisms σ:()p\sigma \colon () \rightarrow p are sections of pp

  • unary morphisms (φ 1,φ ):(p 1)p(\varphi_{1}, \varphi^{\sharp}) \colon (p_{1}) \rightarrow p are pairs of morphisms in \mathcal{E} making the following diagram commute
  • binary morphisms (φ 1,φ 2,φ ):(p 2,p 1)p(\varphi_{1}, \varphi_{2}, \varphi^{\sharp}) \colon (p_{2}, p_{1}) \rightarrow p are triples of morphisms in \mathcal{E} making the following diagram commute:
  • nn-ary morphisms (φ 1,φ 2,,φ n,φ ):(p n,,p 2,p 1)p(\varphi_{1}, \varphi_{2}, \ldots, \varphi_{n}, \varphi^{\sharp}) \colon (p_{n}, \ldots, p_{2}, p_{1}) \rightarrow p are n+1n+1 morphisms in \mathcal{E} making the following diagram commute:
  • identity morphism on an object p:EBp \colon E \rightarrow B is the pair (1 B,1 E)(1_{B}, 1_{E}).

  • composition of unary morphisms (ψ,ψ ):pp(\psi, \psi^{\sharp}) \colon p \rightarrow p' and (φ,φ ):pp(\varphi, \varphi^{\sharp}) \colon p' \rightarrow p'' is given by (ψφ,φ ψ¯ ):pp(\psi \circ \varphi, \varphi^{\sharp} \circ {\bar{\psi}}^{\sharp}) \colon p \rightarrow p'' as depicted below

Composition extends to nn-ary morphisms in an analogous way.

Proposition

If the 𝒟\mathcal{D}-maps are exponentiable, then the multicategory Poly()\mathbf{Poly}(\mathcal{E}) is a representable multicategory. (Garner, 2019)

  • Polynomial endofunctors are important in the definition of W-types in categories.

  • Polynomial functors are a special case of parametric right adjoints.

  • Polynomial functors can be defined using exponentiable morphisms in a category that may not be locally cartesian closed. See also distributivity pullback.

  • Kripke frames (R,S)(R,S) (with a transition relation RR of arity 22) as studied in modal logic are coalgebras for the power-set functor PP. Kripke frames for a more general modal similarity type tt are a coalgebras of a functor of the form X dtP(S arity(d))X\mapsto \product_{d\in t} P(S^{arity(d)}). Kripke models are coalgebras of functor K:XP(Prop)×P(X)K:X\mapsto P(Prop)\times P(X) where PropProp is the set of propositional variables of the logic in consideration. In particular all the functors appearing here are polynomial functors. So, at least in some aspects, the study of modal logics reduces to the study of (certain) polynomial functors.

Examples

References

The standard reference, which considers dependent (multivariate) polynomial functors, is:

The relation of plain polynomial functors to trees is discussed in

The category, PolyPoly, of one-variable polynomial functors on SetSet and its application to dynamical systems is considered in

Talks on polynomial functors are available at

  • Workshop on Polynomial Functors, Topos Institute, 15–19 March 2021. (website)

  • Workshop on Polynomial Functors 2, Topos Institute, March 14–18, 2022. (website)

Monograph on polynomial functors in view of categorical systems theory:

Generalization to homotopy theory and higher category theory is discussed in

See also

  • Yde Venema, Algebras and Coalgebras, §6 (p.332–426) in Blackburn, van Benthem, Wolter, Handbook of modal logic, Elsevier, 2007.

  • Mark Weber, Polynomials in categories with pullbacks, Theory and Applications of Categories, 30:16 (2015) 533–598. (journal)

  • Charles Walker, Universal properties of polynomials, (arXiv:1806.10477)

  • Ross Street, Polynomials as spans, Cahiers de topologie et géométrie différentielle catégoriques, Vol. LXI-2 (2020), pp 113-153 (pdf)

  • Richard Garner, Polynomial comonads and comodules, HoTTEST Seminar (2019) [slides, video]

Using wreath products of groups

  • I. G. Macdonald, Polynomial functors and wreath products, J. Pure Appl. Alg. 18 (1980) 173–204 pdf

Last revised on October 28, 2024 at 20:45:23. See the history of this page for a list of all contributions to it.