5 Polynomial Endofunctors

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 5.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}$

Proposition 5.0.2 Characterising property of Polynomial Endofunctors

✓

The data of a map into the polynomial applied to an object in $\mathbb {C}$

$\begin{tikzcd} \Ga & {\Poly{t} Y} \arrow[from=1-1, to=1-2] \end{tikzcd}$

corresponds to

$\begin{tikzcd} \Ga && {\Poly{t} Y} \\ & A \arrow["\phi", from=1-1, to=1-3] \arrow["\al"', dashed, from=1-1, to=2-2] \arrow["{t_* B^* Y}", from=1-3, to=2-2] \end{tikzcd}$

Applying the adjunction $A_{!} \dashv A^{*}$, this corresponds to

\[ \alpha : \Gamma \to A \quad \quad \text{ and } \quad \quad \]

$\begin{tikzcd} {B_! t^*\al} && {B \times Y} \\ & B \arrow["{\tilde{\phi}}", dashed, from=1-1, to=1-3] \arrow["{t^*\al}"', from=1-1, to=2-2] \arrow["{B^* Y}", from=1-3, to=2-2] \end{tikzcd}$

Applying the adjunction $t^{*} \dashv t_{*}$, this corresponds to

\[ \alpha : \Gamma \to A \quad \quad \text{ and } \quad \quad \]

$\begin{tikzcd} {\Ga \cdot \al := B_! t^*\al} && Y \arrow["{\beta}", dashed, from=1-1, to=1-3] \end{tikzcd}$

Henceforth we will write

\[ (\alpha , \beta ) : \Gamma \to P_{t} Y \]

for this map, since it is uniquely determined by this data. Furthermore, precomposition by $\sigma : \Delta \to \Gamma $, acts on such a pair by

$\begin{tikzcd} & \De \\ {} & \Ga & {\Poly{t} Y} \arrow["\si"', from=1-2, to=2-2] \arrow["{(\al \circ \si, \be \circ t^* \si)}", from=1-2, to=2-3] \arrow["{(\al, \be)}"', from=2-2, to=2-3] \end{tikzcd}$

and given a morphism $f : X \to Y$, the morphism $P_{t}{f}$ acts on such a pair by

$\begin{tikzcd} {} & \Ga & {\Poly{t} X} \\ && {\Poly{t}{Y}} \arrow["{(\al, \be)}", from=1-2, to=1-3] \arrow["{(\al, f \circ \be)}"', from=1-2, to=2-3] \arrow["{\Poly{t}{f}}", from=1-3, to=2-3] \end{tikzcd}$

Lemma 5.0.3

Use $R$ to denote the fiber product

$\begin{tikzcd} R & B \\ {\Poly{t} {Y}} & A \arrow["{\rho_\Term}", from=1-1, to=1-2] \arrow["{\rho_{\Poly{}}}"', from=1-1, to=2-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] \arrow["t", from=1-2, to=2-2] \arrow["{t_* B^* Y}"', from=2-1, to=2-2] \end{tikzcd}$

By the universal property of pullbacks and 5.0.2, The data of a map $\Gamma \to R$ corresponds to the data of $\beta : \Gamma \to B$ and $(t \circ \beta ,y) : \Gamma \to P_{t}{Y}$, or just $\beta : \Gamma \to B$ and $y : \Gamma \cdot t \circ \beta \to Y$

$\begin{tikzcd} \Ga \\ & R & B \\ & {\Poly{t} {Y}} & A \arrow["{(\be, y)}"{description}, from=1-1, to=2-2] \arrow["{(t \circ \be,y)}"', bend right, from=1-1, to=3-2] \arrow["\be", bend left, from=1-1, to=2-3] \arrow["{\rho_{\Poly{}}}", from=2-2, to=3-2] \arrow["{\rho_B}"{description}, from=2-2, to=2-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] \arrow["{t_* B^* Y}", from=3-2, to=3-3] \arrow["t"', from=2-3, to=3-3] \end{tikzcd}$

By uniqueness in the universal property of pullbacks and 5.0.2, Precomposition by a map $\sigma : \Delta \to \Gamma $ acts on such a pair by

$\begin{tikzcd} & \De \\ {} & \Ga & R \arrow["\si"', from=1-2, to=2-2] \arrow["{(\be\circ \si, y \circ t^* \si)}", from=1-2, to=2-3] \arrow["{(\be, y)}"', from=2-2, to=2-3] \end{tikzcd}$

Definition 5.0.4 Evaluation

Let $\, \mathsf{counit} \, : \rho _B \to B \to B^* Y$ denote the counit of the adjunction $f^* \dashv f_*$ at the object $B^* Y$, recalling that $\rho _B = t^* t_* B^* Y$. Then viewing the object $B^* Y$ in the slice as the object $Y \times B$ in the ambient category, we define $\mathsf{ev}_{} \, : R \to Y$ as the composition

$\begin{tikzcd} R & {Y \times B} & Y \\ B \arrow["\counit"', from=1-1, to=1-2] \arrow["\ev{}{}", bend left, from=1-1, to=1-3] \arrow["{\rho_B}"', from=1-1, to=2-1] \arrow["{\pi_Y}"', from=1-2, to=1-3] \arrow[from=1-2, to=2-1] \end{tikzcd}$

Lemma 5.0.5 Evaluation Computation

Suppose $(\beta ,y) : \Gamma \to R$, as in 5.0.3

\[ \beta : \Gamma \to B \quad \text{ and } \quad y : \Gamma \cdot t \circ \beta \to Y \]

Then the evaluation of $y$ at $\beta $ can be computed as

\[ \mathsf{ev}_{} \, \circ (\beta , y) = y \circ b \]

where

$\begin{tikzcd} \Ga \\ & {\Ga \cdot t \circ \be} & B \\ & \Ga & A \arrow["b"{description}, dashed, from=1-1, to=2-2] \arrow["\be"{description}, bend left, from=1-1, to=2-3] \arrow[Rightarrow, bend right, no head, from=1-1, to=3-2] \arrow["v"', from=2-2, to=2-3] \arrow["d", from=2-2, to=3-2] \arrow["t", from=2-3, to=3-3] \arrow["{t \circ \be}"', from=3-2, to=3-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] \end{tikzcd}$

and

$\begin{tikzcd} & \Ga \\ && R & {\Poly{t} {Y}} \\ Y & {Y \times B} & B & A \arrow["{(\be,y)}"{description}, from=1-2, to=2-3] \arrow["{(t \circ \be,y)}"{description}, bend left, from=1-2, to=2-4] \arrow["{y \circ b}"{description}, bend right, dashed, from=1-2, to=3-1] \arrow["{(y \circ b,\be)}"{description}, dashed, from=1-2, to=3-2] \arrow[from=2-3, to=2-4] \arrow["\counit"{description}, from=2-3, to=3-2] \arrow[from=2-3, to=3-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-3, to=3-4] \arrow["{t_* B^* Y}", from=2-4, to=3-4] \arrow["{\pi_Y}", from=3-2, to=3-1] \arrow["{\pi_B}"', from=3-2, to=3-3] \arrow["t"', from=3-3, to=3-4] \end{tikzcd}$

Proof ▶

It suffices to show $(\, \mathsf{counit} \, \circ (\beta , y)) = (y \circ b , \beta )$ instead.

\begin{align*} & \, \, \mathsf{counit} \, \circ (\beta , y) \\ = & \, \, \mathsf{counit} \, \circ (v \circ b, y \circ t^{*} d \circ t^{*} b) & \ref{evaluation_computation_diagram1} \\ = & \, \, \mathsf{counit} \, \circ (v, y \circ t^{*} d) \circ b & \ref{lem:R},\ref{evaluation_computation_diagram2}\\ = & \, \, \mathsf{counit} \, \circ t^{*} (t \circ \beta , y) \circ b & \ref{evaluation_computation_diagram3}\\ = & \, \overline{(t \circ \beta , y)} \circ b & \ref{evaluation_computation_diagram4}\\ = & \, (y, v) \circ b & \ref{evaluation_computation_diagram5} \\ = & \, (y \circ b, v \circ b)\\ = & \, (y \circ b, \beta )\\ \end{align*}

$\begin{tikzcd} {\Ga \cdot t \circ \be} & {\Ga \cdot t \circ \be \cdot t \circ \be} & {\Ga \cdot t \circ \be} & B \\ \Ga & {\Ga \cdot t \circ \be} & \Ga & A \arrow["{t^* b}", dashed, from=1-1, to=1-2] \arrow[bend left, Rightarrow, no head, from=1-1, to=1-3] \arrow[bend right, Rightarrow, no head, from=2-1, to=2-3] \arrow["d", from=1-1, to=2-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] \arrow["{t^* d}", dashed, from=1-2, to=1-3] \arrow[from=1-2, to=2-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3] \arrow["v", from=1-3, to=1-4] \arrow["d", from=1-3, to=2-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-3, to=2-4] \arrow["t", from=1-4, to=2-4] \arrow["b"', from=2-1, to=2-2] \arrow["d"', from=2-2, to=2-3] \arrow["{t \circ \be}"', from=2-3, to=2-4] \end{tikzcd}$

Figure 5.1 $t^{*} d \circ t^{*} b = \mathsf{id}_{\Gamma \cdot t \circ \beta }$

$\begin{tikzcd} \Ga \\ {\Ga \cdot t \circ \be} & R \arrow["b"', from=1-1, to=2-1] \arrow["{(v \circ b, y \circ t^{*} d \circ t^{*} b)}", from=1-1, to=2-2] \arrow["{(v, y \circ t^{*} d)}"', from=2-1, to=2-2] \end{tikzcd}$

Figure 5.2 $(v, y \circ t^{*} d) \circ b = (v \circ b, y \circ t^{*} d \circ t^{*} b)$

$\begin{tikzcd} {\Ga \cdot t \circ \be} & R & B \\ \Ga & {\Poly{t}{Y}} & A \arrow["{(v,y \circ t^* d)}", dashed, from=1-1, to=1-2] \arrow["v"{description}, shift left=3, bend left, from=1-1, to=1-3] \arrow["d"{description}, from=1-1, to=2-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] \arrow[from=1-2, to=1-3] \arrow[from=1-2, to=2-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3] \arrow["t", from=1-3, to=2-3] \arrow["{(t \circ \be, y)}"', from=2-1, to=2-2] \arrow["{t \circ \be}"{description}, shift right=3, bend right, from=2-1, to=2-3] \arrow["{t_* B^* Y}"', from=2-2, to=2-3] \end{tikzcd}$

$\begin{tikzcd} {\Ga \cdot t \circ \be} \\ \Ga & {\Poly{t}{Y}} \arrow["d"', from=1-1, to=2-1] \arrow["{(t \circ \be \circ d, y \circ t^* d)}", from=1-1, to=2-2] \arrow["{(t \circ \be, y)}"', from=2-1, to=2-2] \end{tikzcd}$

using 5.0.2, 5.0.3

Figure 5.3 $t^{*}(t \circ \beta , y) = (v, y \circ t^{*}d)$

$\begin{tikzcd} {t^*(t \circ \be)} && {} & {t \circ \be} \\ {t^* t_* B^* Y} & {B^*Y} & { t^{*} \dashv t_{*}} & {t_* B^* Y} & {t_* B^*Y} \arrow["{t^* (t \circ \be, y)}"', from=1-1, to=2-1] \arrow["{\overline{(t \circ \be,y)}}", dashed, from=1-1, to=2-2] \arrow[Rightarrow, no head, from=1-3, to=2-3] \arrow["{(t \circ \be, y)}"', from=1-4, to=2-4] \arrow["{(t \circ \be,y)}", from=1-4, to=2-5] \arrow["\counit"', from=2-1, to=2-2] \arrow["{\widetilde{\counit}}"', Rightarrow, no head, from=2-4, to=2-5] \end{tikzcd}$

Figure 5.4 $\, \mathsf{counit} \, \circ t^{*} (t \circ \beta , y) = \overline{(t \circ \beta , y)}$

$\begin{tikzcd} {\Ga \cdot t \circ \be} & {Y \times B} & {} & \Ga & {\Poly{t}{Y}} \\ B && {t^* \dashv t_*} & A \arrow["{(y,v)}", dashed, from=1-1, to=1-2] \arrow["{v = t^* (t \circ \be)}"', from=1-1, to=2-1] \arrow["{B^*Y}", from=1-2, to=2-1] \arrow[Rightarrow, no head, from=1-3, to=2-3] \arrow["{(t \circ \be,y)}", from=1-4, to=1-5] \arrow["{t \circ \be}"', from=1-4, to=2-4] \arrow["{t_*B^*Y}", from=1-5, to=2-4] \end{tikzcd}$

Figure 5.5 $\overline{(t \circ \beta , y)} = (y,v)$

Definition 5.0.6 Polynomial composition

Let $f : B \to A$ and $g : D \to C$. Define the polynomial composition $f \lhd g : Q \to P_{f}{C}$ as the composition of the two vertical maps in the following

$\begin{tikzcd} D & Q \\ C & R & B \\ & {\Poly{f}{C}} & A \arrow["g"', from=1-1, to=2-1] \arrow[from=1-2, to=1-1] \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-90}, draw=none, from=1-2, to=2-1] \arrow[from=1-2, to=2-2] \arrow["{f \PolyComp g}"{pos=0.1}, bend left, dashed, from=1-2, to=3-2] \arrow["{\ev{}{}}", from=2-2, to=2-1] \arrow[from=2-2, to=2-3] \arrow[from=2-2, to=3-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] \arrow["f", from=2-3, to=3-3] \arrow["{f_*B^*C}"', from=3-2, to=3-3] \end{tikzcd}$

Then the two functors

\[ P_{f \lhd g} \cong P_{f} \circ P_{g} \]

are naturally isomorphic.

Proof ▶

Definition 5.0.7 Mate

Suppose

$\begin{tikzcd} C && B \\ & A \arrow["\rho", from=1-1, to=1-3] \arrow["s"', from=1-1, to=2-2] \arrow["t", from=1-3, to=2-2] \end{tikzcd}$

Then we have a mate $\mu _{!} : \rho _{!} \circ s^{*} \Rightarrow t^{*}$. This is given by the universal property of pullbacks: given $f : x \to y$ in the slice $\mathbb {C}/ A$ we have

$\begin{tikzcd} \bullet & \bullet & X \\ \bullet & \bullet & Y \\ C & B & A \arrow["{\mu_{!x}}", from=1-1, to=1-2] \arrow[""{name=0, anchor=center, inner sep=0}, "{s^* f}"', from=1-1, to=2-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] \arrow[from=1-2, to=1-3] \arrow[""{name=1, anchor=center, inner sep=0}, "{t^* f}", from=1-2, to=2-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3] \arrow["f", from=1-3, to=2-3] \arrow["x", bend left = 70, from=1-3, to=3-3] \arrow["{\mu_{!y}}"', from=2-1, to=2-2] \arrow["{s^* y}"', from=2-1, to=3-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-1, to=3-2] \arrow[from=2-2, to=2-3] \arrow["{t^* y}"', from=2-2, to=3-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] \arrow["y", from=2-3, to=3-3] \arrow["\rho"', from=3-1, to=3-2] \arrow["t"', from=3-2, to=3-3] \arrow["{\mu_!}"{description}, shorten <=6pt, shorten >=6pt, Rightarrow, from=0, to=1] \end{tikzcd}$

By the calculus of mates we also have a reversed mate between the right adjoints $\mu ^{*} : t_{*} \to s_{*} \circ \rho ^{*}$. Explicitly $\mu ^{*}$ is the composition

$\begin{tikzcd} {t_*} & {s_* \rho^* \rho_! s^* t_*} & {s_* \rho^* t^* t_*} & {s_* \rho^*} \arrow["{\unit t_*}", from=1-1, to=1-2] \arrow["{s_* \rho^* \mu_! t_*}", from=1-2, to=1-3] \arrow["{s_* \rho^* \counit}", from=1-3, to=1-4] \end{tikzcd}$

Definition 5.0.8 Contravariant action of $P_{-}$ on a slice

Let $P_{-} : (\mathbb {C}/ A)^{\mathrm{op}} \to [\mathbb {C}, \mathbb {C}]$ be defined by taking $s \mapsto P_{s}$ on objects and act on a morphism by

$\begin{tikzcd} && B &&& {\Poly{t}} \\ A &&& {} & {} \\ && C &&& {\Poly{s}} \arrow["t"', from=1-3, to=2-1] \arrow["{\Star{\rho}}", from=1-6, to=3-6] \arrow[maps to, from=2-4, to=2-5] \arrow["\rho"', from=3-3, to=1-3] \arrow["s", from=3-3, to=2-1] \end{tikzcd}$

where

\[ {\rho }^{\star } := A_{!} (s_{*} \eta \circ \mu B^{*}) : P_{t} \to P_{s} \]

$\begin{tikzcd} [row sep = large] \catC \\ {\catC / C} & {\catC / B} \\ {\catC / A} \\ \catC \arrow[""{name=0, anchor=center, inner sep=0}, "{C^*}"', from=1-1, to=2-1] \arrow["{B^*}", from=1-1, to=2-2] \arrow["{s_*}"', from=2-1, to=3-1] \arrow["{\rho^*}"{description}, from=2-2, to=2-1] \arrow[""{name=1, anchor=center, inner sep=0}, "{t_*}", from=2-2, to=3-1] \arrow["{A_!}", from=3-1, to=4-1] \arrow["\eta"{description}, shorten <=9pt, shorten >=9pt, Rightarrow, from=2-2, to=0] \arrow["\mu"{description}, shorten <=2pt, Rightarrow, from=1, to=2-1] \arrow["{\Poly{s}}"', bend right = 70, from=1-1, to=4-1] \arrow["{\Poly{t}}", bend left = 100, shift left = 15, from=1-1, to=4-1] \end{tikzcd}$

where $\mu = \mu ^{*}$ is the mate from 5.0.7, and $\eta $ is the natural isomorphism given by pullback pasting.

Pointwise, this natural transformation acts on a pair $(\alpha , \beta ) : \Gamma \to P_{t}{X}$ by

$\begin{tikzcd} {} & \Ga & {\Poly{t} X} \\ && {\Poly{s}{X}} \arrow["{(\al, \be)}", from=1-2, to=1-3] \arrow["{(\al, \be \circ \al^* \rho)}"', from=1-2, to=2-3] \arrow["{\Star{\rho}_X}", from=1-3, to=2-3] \end{tikzcd}$

where $\alpha ^{*} \rho $ is defined as

$\begin{tikzcd} {\Ga \cdot_s \al} & C \\ {\Ga \cdot_t \al} & B \\ \Ga & A \arrow["{s^* \al}", from=1-1, to=1-2] \arrow["{\al^* \rho}"', dashed, from=1-1, to=2-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] \arrow["\rho", from=1-2, to=2-2] \arrow["{t^* \al}", from=2-1, to=2-2] \arrow[from=2-1, to=3-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-1, to=3-2] \arrow["t", from=2-2, to=3-2] \arrow["\al"', from=3-1, to=3-2] \end{tikzcd}$

We prove this now.

Proof ▶

Firstly ${\rho }^{\star }_{X} = A_{!} (s_{*} \eta _{X} \circ \mu _{B^{*}X})$, so the first component $\alpha : \Gamma \to A$ is preserved by ${\rho }^{\star }_{X}$ and it suffices to show, in $\mathbb {C}/ A$

$\begin{tikzcd} {} & \al & {t_* B^* X} \\ && {s_* C^* X} \arrow["{(\al, \be)}", from=1-2, to=1-3] \arrow["{(\al, \be \circ \al^* \rho)}"', from=1-2, to=2-3] \arrow["{s_{*} \eta_{X} \circ \mu_{B^{*}X}}", from=1-3, to=2-3] \end{tikzcd}$

By the adjunction $s^{*} \dashv s_{*}$, it suffices to show, in $\mathbb {C}/ C$

$\begin{tikzcd} {} & {s^* \al} & {s^*t_* B^* X} \\ && {C^* X} \arrow["{s^* (\al, \be)}", from=1-2, to=1-3] \arrow["{\overline{(\al, \be \circ \al^* \rho)}}"', from=1-2, to=2-3] \arrow["{\overline{s_{*} \eta_{X} \circ \mu_{B^{*}X}}}", from=1-3, to=2-3] \end{tikzcd}$

Now we calculate $\overline{s_{*} \eta _{X} \circ \mu _{B^{*}X}} = \eta _{X} \circ \overline{\mu _{B^{*}X}}$. So that our goal is to show

$\begin{tikzcd} {} & {s^* \al} & {s^*t_* B^* X} & {\rho^* B^*X} \\ && {C^* X} \arrow["{s^* (\al, \be)}", from=1-2, to=1-3] \arrow["{\overline{(\al, \be \circ \al^* \rho)}}"', from=1-2, to=2-3] \arrow["{\overline{\mu_{B^{*}X}}}", from=1-3, to=1-4] \arrow["{\eta_{X}}", "{\sim}"', outer sep = -1pt, from=1-4, to=2-3] \end{tikzcd}$

Since $\eta _{X}$ is an isomorphism between two limits of the same diagram, namely $X \times C \cong C_{!} C^{*} X \cong C_{!} \rho ^{*} B^{*} X$, it suffices to show that both $\overline{\mu _{B^{*}X}} \circ s^{*}(\alpha , \beta )$ and $\overline{(\alpha , \beta \circ \alpha ^{*} \rho )}$ are uniquely determined by the same two maps into $X$ and $C$.

By the characterising property of polynomial endofunctors (5.0.2) we calculate

\[ \overline{(\alpha , \beta \circ \alpha ^{*} \rho )} = (\beta \circ \alpha ^{*} \rho , s^{*} \alpha ) \]

$\begin{tikzcd} && {} &&& {} \\ \al & {s_* C^* X} && {s^* \al} & {C^* X} && {C_! s^* \al} & X \\ && {} &&& {} \arrow[Rightarrow, no head, from=1-3, to=3-3] \arrow[Rightarrow, no head, from=1-6, to=3-6] \arrow["{(\al, \be \circ \al^* \rho)}", from=2-1, to=2-2] \arrow["{\overline{(\al,\be \circ \al^* \rho)}}", from=2-4, to=2-5] \arrow["{(\be \circ \al^* \rho, s^* \al)}"', from=2-4, to=2-5] \arrow["{\be \circ \al^* \rho}"', from=2-7, to=2-8] \end{tikzcd}$

More formally, this means $\beta \circ \alpha ^{*} \rho : C_{!} s^{*} \alpha \to X$ and $s^{*} \alpha : C_{!} s^{*} \alpha \to C$ are the two maps that uniquely determine the map $C_{!} \overline{\alpha , \beta \circ \alpha ^{*} \rho } : C_{!} s^{*} \alpha \to X \times C$.

On the other hand,

$\begin{tikzcd} \al & {t_* B^* X} & {s_* \rho^* \rho_! s^*t_* B^*X} & {s_* \rho^* t^* t_* B^*X} & {s_* \rho* B^* X} \\ \\ {} &&&& {s^* \dashv s_*} \\ {s^* \al} & {s^*t_* B^* X} & {\rho^* \rho_! s^*t_* B^*X} & {\rho^* t^* t_* B^*X} & {\rho^* B^*X} \\ \\ {} &&&& {\rho_! \dashv \rho^*} \\ {\rho_! s^* \al} & {\rho_! s^*t_* B^* X} & { \rho_! s^*t_* B^*X} & { t^* t_* B^*X} & { B^*X} \\ {\Ga \cdot_s \al} & S && R & {X \times B} \\ \arrow["{(\al, \be)}", from=1-1, to=1-2] \arrow["{\unit_{t_* B^* X}}", from=1-2, to=1-3] \arrow["{{\mu_{B^{*}X}}}", bend right, from=1-2, to=1-5] \arrow["{s_* \rho^* \mu_! t_* B^*X}", outer sep = 5pt, from=1-3, to=1-4] \arrow["{s_* \rho^* \counit_{B^*X}}", outer sep = 5pt, from=1-4, to=1-5] \arrow[Rightarrow, no head, from=3-1, to=3-5] \arrow["{s^* (\al, \be)}", from=4-1, to=4-2] \arrow["{\overline{\unit_{t_* B^* X}}}", from=4-2, to=4-3] \arrow["{\overline{\mu_{B^{*}X}}}", bend right, from=4-2, to=4-5] \arrow["{\rho^* \mu_! t_* B^*X}", outer sep = 5pt, from=4-3, to=4-4] \arrow["{\rho^* \counit_{B^*X}}", outer sep = 5pt, from=4-4, to=4-5] \arrow[Rightarrow, no head, from=6-1, to=6-5] \arrow["{\rho_! s^* (\al, \be)}", from=7-1, to=7-2] \arrow["{\overline{\overline{\unit_{t_* B^* X}}}}", outer sep = 5pt, Rightarrow, no head, from=7-2, to=7-3] \arrow["{\mu_! t_* B^*X}", from=7-3, to=7-4] \arrow["{\counit_{B^*X}}", from=7-4, to=7-5] \arrow[Rightarrow, no head, from=7-1, to=8-1] \arrow[Rightarrow, no head, from=7-2, to=8-2] \arrow[Rightarrow, no head, from=7-4, to=8-4] \arrow[Rightarrow, no head, from=7-5, to=8-5] \end{tikzcd}$

The mate $\mu _{!}$ is calculated via the universal map into the pullback $R$ (dotted below).

$\begin{tikzcd} {\Ga \cdot_s \al} & {\Ga \cdot_t \al} & \Ga \\ S & R & {\Poly{t} X} \\ \quad C \quad & B & A \arrow[from=1-1, to=1-2] \arrow["{s^* (\al, \be)}"', from=1-1, to=2-1] \arrow["{s^* \al}"', bend right = 70, shift right = 4, from=1-1, to=3-1] \arrow[from=1-2, to=1-3] \arrow[from=1-2, to=2-2] \arrow["{(\al, \be)}", from=1-3, to=2-3] \arrow["\al", bend left = 70, shift left = 4, from=1-3, to=3-3] \arrow["{\mu_! t_* B^*X}"', dashed, from=2-1, to=2-2] \arrow["{s^* t_*B^* X}"', from=2-1, to=3-1] \arrow[from=2-2, to=2-3] \arrow["{t^* t_* B^* X}", from=2-2, to=3-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] \arrow["{t_* B^* X}", from=2-3, to=3-3] \arrow["\rho"', from=3-1, to=3-2] \arrow["t"', from=3-2, to=3-3] \end{tikzcd}$

Using the characterization of maps into $R$ from 5.0.3 we can calculate

\[ \mu _! t_* B^*X \circ s^* (\alpha , \beta ) = (\rho \circ s^{*} \alpha , \beta \circ t^{*}\alpha ^{*} s) \]

since the first component is simply the map $\Gamma \cdot _{s} \alpha \to B$ and the second component is the second component of the map

\[ (\alpha \circ \alpha ^{*} s, \beta \circ t^{*} \alpha ^{*} s) = (\alpha , \beta ) \circ \alpha ^{*} s : \Gamma \cdot _{s} \alpha \to P_{t}{X} \]

Then using 5.0.5

\begin{align} \label{polynomial_star_equation1} & \overline{\overline{\mu _{B^{*}X}} \circ s^{*}(\alpha , \beta )} \\ = \, & \, \mathsf{counit} \, _{B^{*} X} \circ \mu _! t_* B^*X \circ s^* (\alpha , \beta )\\ = \, & \, \mathsf{counit} \, _{B^{*} X} \circ (\rho \circ s^{*} \alpha , \beta \circ t^{*}\alpha ^{*} s)\\ = \, & (\beta \circ t^{*}\alpha ^{*} s \circ r, \rho \circ s^{*} \alpha ) \\ = \, & (\beta \circ \alpha ^{*} \rho , \rho \circ s^{*} \alpha ) \\ : \, \, & \Gamma \cdot _s \alpha \to X \times B \end{align}

where

$\begin{tikzcd} {\Ga \cdot_s \al} \\ & {\Ga \cdot_s \al \cdot_t \al \circ \al^*s} & B \\ & {\Ga \cdot_s \al} & A \arrow["r"', dashed, from=1-1, to=2-2] \arrow["{\rho \circ s^* \al}", bend left, from=1-1, to=2-3] \arrow[bend right, Rightarrow, no head, from=1-1, to=3-2] \arrow[from=2-2, to=2-3] \arrow[from=2-2, to=3-2] \arrow["t", from=2-3, to=3-3] \arrow["{\al \circ \al^* s}"', from=3-2, to=3-3] \end{tikzcd}$

and

$\begin{tikzcd} {\Ga \cdot_s \al} & {\Ga \cdot_s \al} & C \\ {\Ga \cdot_s \al \cdot_t \al \circ \al^*s} & {\Ga \cdot_t \al} & B \\ {\Ga \cdot_s \al} & \Ga & A \arrow[Rightarrow, no head, from=1-1, to=1-2] \arrow["r"', dashed, from=1-1, to=2-1] \arrow[bend right = 50, shift right = 7, Rightarrow, no head, from=1-1, to=3-1] \arrow["s", bend left = 50, from=1-3, to=3-3] \arrow["{s^* \al}", from=1-2, to=1-3] \arrow["{\al^* \rho}", from=1-2, to=2-2] \arrow["\rho", from=1-3, to=2-3] \arrow["{t^* \al^* s}"', dashed, from=2-1, to=2-2] \arrow[from=2-1, to=3-1] \arrow[from=2-2, to=2-3] \arrow[from=2-2, to=3-2] \arrow["t", from=2-3, to=3-3] \arrow["{\al*s}"', from=3-1, to=3-2] \arrow["\al"', from=3-2, to=3-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-1, to=3-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] \end{tikzcd}$

Moving back along the adjunction $\rho _{!} \dashv \rho ^{*}$ ?? tells us that

$\begin{tikzcd} {\Ga \cdot_s \al} & {} \\ && {X \times C} & C \\ & {} & {X \times B} & B \\ && X & 1 \arrow["{\overline{\mu_{B^{*}X}} \circ s^{*}(\al, \be)}"{description}, from=1-1, to=2-3] \arrow["{s^* \al}", bend left, from=1-1, to=2-4] \arrow["{\overline{\overline{\mu_{B^{*}X}} \circ s^{*}(\al, \be)}}"{description}, bend right, from=1-1, to=3-3] \arrow["{\be \circ \al^* \rho}"', bend right = 60, from=1-1, to=4-3] \arrow[from=2-3, to=2-4] \arrow[from=2-3, to=3-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-3, to=3-4] \arrow["\rho", from=2-4, to=3-4] \arrow[from=3-3, to=3-4] \arrow[from=3-3, to=4-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=3-3, to=4-4] \arrow[from=3-4, to=4-4] \arrow[from=4-3, to=4-4] \end{tikzcd}$

So that, as required, $\overline{\mu _{B^{*}X}} \circ s^{*}(\alpha , \beta )$ and $\overline{(\alpha , \beta \circ \alpha ^{*} \rho )}$ are uniquely determined by the same two maps into $X$ and $C$.

Definition 5.0.9 Covariant of $P_{-}$ on a cartesian square

We can also view taking polynomial endofunctors as a covariant functor on the category of arrows with cartesian squares as morphisms

\[ P_{-} : \mathsf{CartArr}(\mathbb {C}) \to [\mathbb {C}, \mathbb {C}] \]

where the action on a cartesian square is

$\begin{tikzcd} C && D &&& {\Poly{s}} \\ &&& {} & {} \\ A && B &&& {\Poly{t}} \arrow["\theta"', from=1-1, to=3-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=3-3] \arrow[""{name=0, anchor=center, inner sep=0}, "s"', from=1-3, to=1-1] \arrow["\rho", from=1-3, to=3-3] \arrow["{\Poly{\kappa}}", from=1-6, to=3-6] \arrow[maps to, from=2-4, to=2-5] \arrow[""{name=1, anchor=center, inner sep=0}, "t", from=3-3, to=3-1] \arrow["\kappa"', shorten <=9pt, shorten >=9pt, Rightarrow, from=0, to=1] \end{tikzcd}$

given by the whiskered natural transformations

$\begin{tikzcd} \catC & \catC \\ {\catC / D} & {\catC / B} \\ {\catC / C} & {\catC/A} \\ \catC & \catC \arrow[Rightarrow, no head, from=1-1, to=1-2] \arrow["{C^*}"', from=1-1, to=2-1] \arrow["{\eta^-1}"{description}, Rightarrow, from=1-1, to=2-2] \arrow["{\Poly{s}}"', shift right=5, bend right = 30, from=1-1, to=4-1] \arrow["{B^*}", from=1-2, to=2-2] \arrow["{\Poly{t}}", shift left=5, bend left = 30, from=1-2, to=4-2] \arrow["{s_*}"', from=2-1, to=3-1] \arrow["{\mu^{*-1}}"{description}, Rightarrow, from=2-1, to=3-2] \arrow["{\rho^*}"{description}, from=2-2, to=2-1] \arrow["{t_*}", from=2-2, to=3-2] \arrow["{C_!}"', from=3-1, to=4-1] \arrow["{\mu_!}"', shorten >=5pt, Rightarrow, from=3-1, to=4-2] \arrow["{\theta^*}", from=3-2, to=3-1] \arrow["{A_!}", from=3-2, to=4-2] \arrow[Rightarrow, no head, from=4-1, to=4-2] \end{tikzcd}$

Furthermore, the natural transformation $P_{\kappa }$ is cartesian. meaning each naturality square is a pullback square.

$\begin{tikzcd} && {\Poly{s}X} & {\Poly{t}X} \\ {} && {\Poly{s}Y} & {\Poly{t}Y} \arrow["{{\Poly{\kappa}}_Y}", from=1-3, to=1-4] \arrow["{\Poly{s} f}"', from=1-3, to=2-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-3, to=2-4] \arrow["{\Poly{s} f}", from=1-4, to=2-4] \arrow["{{\Poly{\kappa}}_Y}"', from=2-3, to=2-4] \end{tikzcd}$

The natural transformation $P_{\kappa }$ computes in the following way

$\begin{tikzcd} {\Ga \cdot _t \theta \circ \al} \\ & {\Ga \cdot _s \al} & D & B && \Ga \\ & \Ga & C & A && {\Poly{s} X} & {\Poly{t}{X}} \arrow["i"{description}, dashed, from=1-1, to=2-2] \arrow[from=1-1, to=2-4] \arrow[from=1-1, to=3-2] \arrow[from=2-2, to=2-3] \arrow[from=2-2, to=3-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] \arrow["\rho"{description}, from=2-3, to=2-4] \arrow["s"', from=2-3, to=3-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-3, to=3-4] \arrow["t", from=2-4, to=3-4] \arrow["{(\al, \be)}"', from=2-6, to=3-6] \arrow["{(\theta \circ \al, \be \circ i)}", from=2-6, to=3-7] \arrow["\al"', from=3-2, to=3-3] \arrow["\theta"', from=3-3, to=3-4] \arrow["{{\Poly{\kappa}}_X}"', from=3-6, to=3-7] \end{tikzcd}$

using the fact that $\Gamma \cdot _{s} \alpha $ and $\Gamma \cdot _{t} \theta \circ \alpha $ are limits of the same diagram.

Proof ▶

We can use the computation of ${P_{\kappa }}_{X}$ and $P_{s}{f}$ to show that the natural transformation $P_{\kappa }$ is cartesian. Essentially, the first component of a map $\Gamma \to P_{s}{X}$ is determined by its composition with $P_{s}{f}$ and its second component is determined by its composition with ${P_{\kappa }}_{X}$.

Corollary 5.0.10

If we have

$\begin{tikzcd} {D'} & {B'} \\ D & B \\ C & A \arrow[from=1-1, to=1-2] \arrow["{\rho_1}", from=1-1, to=2-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] \arrow["{q_1'}"', bend right, from=1-1, to=3-1] \arrow["{\rho_2}"', from=1-2, to=2-2] \arrow["{q_2'}", bend left, from=1-2, to=3-2] \arrow[from=2-1, to=2-2] \arrow["{q_1}", from=2-1, to=3-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-1, to=3-2] \arrow["{q_2}"', from=2-2, to=3-2] \arrow["\theta"', from=3-1, to=3-2] \end{tikzcd}$

then the two possible ways of obtaining composing the covariant and contravariant actions of $P_{-}$ form a (strictly commuting) pullback square in $[\mathbb {C}, \mathbb {C}]$.

$\begin{tikzcd} {\Poly{q_1}} & {\Poly{q_2}} \\ {\Poly{q_1'}} & {\Poly{q_2'}} \arrow["{\Poly{\kappa}}", from=1-1, to=1-2] \arrow["{\Star{\rho_1}}"', from=1-1, to=2-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] \arrow["{\Star{\rho_2}}", from=1-2, to=2-2] \arrow["{\Poly{\kappa'}}"', from=2-1, to=2-2] \end{tikzcd}$

Proof ▶

To check that it commutes and is a pullback, it suffices to do this pointwise, for some $X \in \mathbb {C}$. Then we simply unfold the computation for each of $P_{\kappa }$ and ${\rho }^{\star }$.