Polynomial Functors in Lean4

3 Multivariate Polynomial Functors

Let \(\mathbb {C}\) be category with pullbacks and terminal object.

Definition 3.0.1 multivariable polynomial functor
#

A polynomial in \(\mathbb {C}\) from \(I\) to \(O\) is a triple \((i,p,o)\) where \(i\), \(p\) and \(o\) are morphisms in \(\mathbb {C}\) forming the diagram

\[ I \xleftarrow {i} E \xrightarrow {p} B \xrightarrow {o} J. \]

The object \(I\) is the object of input variables and the object \(O\) is the object of output variables. The morphism \(p\) encodes the arities/exponents.

Definition 3.0.2 extension of polynomial functors
#

The extension of a polynomial \(I \xleftarrow {i} B \xrightarrow {p} A \xrightarrow {o} J\) is the functor \(\mathrm{P}= o_! \, f_* \, i^* \colon \mathbb {C}/ I \to \mathbb {C}/ O\). Internally, we can define \(\mathrm{P}\) by

\[ \mathrm{P}\left(\left. X_i \ \middle \rvert \ i \in I \right.\right) = \left(\left. \sum _{b \in B_j} \prod _{e \in E_b} X_{s(b)} \ \middle \rvert \ j \in J \right.\right) \]

A polynomial functor is a functor that is naturally isomorphic to the extension of a polynomial.