Extracting an $\mathbb{N}$-filtered differential modality from a differential modality

Abstract

A differential modality is a comonad on an additive symmetric monoidal category $(\mathsf{C},\otimes ,I)$, whose underlying functor we denote $!:\mathsf{C}\to \mathsf{C}$, together with some additional structure including a differential operator $\partial :!A\otimes A\to !A$. A morphism $f:!A\to B$ is interpreted as a smooth function from $A$ to $B$. The notion of an $\mathbb{N}$-filtered differential modality is a variant in which a notion of degree is present. Instead of a single functor $!:\mathsf{C}\to \mathsf{C}$, we ask for a family of functors ${!}_{\le n}:\mathsf{C}\to \mathsf{C}$ where $n\in \mathbb{N}$. Now, a morphism $f:{!}_{\le n}A\to B$ is interpreted as a smooth function from $A$ to $B$, with degree less than $n$ for some notion of degree. We prove that under mild conditions, every differential modality on an additive symmetric monoidal category with underlying functor $!:\mathsf{C}\to \mathsf{C}$ yields an $\mathbb{N}$-filtered differential modality with underlying functors ${!}_{\le n}:\mathsf{C}\to \mathsf{C}$. A morphism $f:{!}_{\le n}A\to B$ corresponds to a polynomial map of degree less than $n$ from $A$ to $B$, in the sense that the $(n+1)$-th derivative of $f$ is $0$.

51 pages