Polynomial Functors in Lean4

2 Univaiate Polynomial Functors

In this section we develop some of the definitions and lemmas related to polynomial endofunctors that we will use in the rest of the notes.

Definition 2.0.1 Polynomial endofunctor
āœ“
#

Let \(\mathbb {C}\) be a locally Cartesian closed category (in our case, presheaves on the category of contexts). This means for each morphism \(t : B \to A\) we have an adjoint triple

\begin{tikzcd} 
    & {\catC / B} \\
    \\
    {} & {\catC / A}
    \arrow[""{name=0, anchor=center, inner sep=0}, "{t_*}", bend left, shift left=5, from=1-2, to=3-2]
    \arrow[""{name=1, anchor=center, inner sep=0}, "{t_!}"', bend right, shift right=5, from=1-2, to=3-2]
    \arrow[""{name=2, anchor=center, inner sep=0}, "{t^*}"{description}, from=3-2, to=1-2]
    \arrow["\dashv"{anchor=center}, draw=none, from=1, to=2]
    \arrow["\dashv"{anchor=center}, draw=none, from=2, to=0]
  \end{tikzcd}

where \(t^{*}\) is pullback, and \(t_{!}\) is composition with \(t\).

Let \(t : B \to A\) be a morphism in \(\mathbb {C}\). Then define \(P_{t} : \mathbb {C}\to \mathbb {C}\) be the composition

\[ P_{t} := A_{!} \circ t_{*} \circ B^{*} \quad \quad \quad \]
\begin{tikzcd} 
    \catC & {\catC / B} & {\catC / A} & \catC
    \arrow["{B^*}", from=1-1, to=1-2]
    \arrow["{t_*}", from=1-2, to=1-3]
    \arrow["{A_!}", from=1-3, to=1-4]
  \end{tikzcd}