Spahn polynomial functor (Rev #1, changes)

Showing changes from revision #0 to #1: Added | Removed | Changed

Definition

Let WfXgYhZW\stackrel{f}{\leftarrow}X\stackrel{g}{\to}Y\stackrel{h}{\to}Z be a diagram in a category CC; a diagram of this type is called a container or a indexed container. Let f *f^*, Π g\Pi_g, Σ\Sigma denote base change resp. dependent product resp. dependent sum. Then the composite

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

which we denote by PP, is called a polynomial functor. If gg is the identity we call PP a linear polynomial functor. This construction exists e.g. if CC is locally cartesian closed.

Polynomial functors and display maps

If we consider CC as a semantics for a type theory we can ask how P=Σ hΠ gf *P=\Sigma_h \Pi_g f^* interacts with display maps: recall that by definition the class of display maps is closed under composition, pullbacks along arbitrary morphisms, and forming exponential objects. Since Σ h=()f\Sigma_h=(-)\circ f, this preserves display maps if hh is a display maps and these are closed under composition. f *f^* forms pullbacks along ff, and Π\Pi forms exponential objects. In particular for PP to preserve display maps it is sufficient that gg and hh are display maps.

A polynomial functor Σ hΠ gf *\Sigma_h\Pi_g f^* where gg (but not necessarily hh) is a display map restricted to display maps, one could call a dependent polynomial functor or better an inductive polynomial functor.

Initial algebras for polynomial functors, inductive families

A (weakly) initial algebra for an inductive polynomial functor we call an inductive family. An inductive family exists for all inductive polynomial functors.

Revision on February 28, 2013 at 01:20:10 by Stephan Alexander Spahn?. See the history of this page for a list of all contributions to it.