nLab differential category

Idea

The notion of differential categories (Blute, Cocket & Seely 2006 is meant to provide categorical semantics for differential linear logic (Ehrhardt & Regnier 2009) which in turn is meant to be a syntactic proof-theoretic approach to differential calculus. In fact differential categories are slightly more general than the models of differential linear logic.

Differential categories

Definition

Definition

A CMon-enriched symmetric monoidal category is a symmetric monoidal category $\mathcal{C}$ such that each hom-set $\mathcal{C}[A,B]$ is a commutative monoid (in Set) and $- \otimes -$ as well as $-;-$ are bilinear ie. preserve sums and the zero in each variable.

Definition

A coalgebra modality? in a symmetric monoidal category $(\mathcal{C}, \otimes, I)$ is given by a comonad $(S,m,u)$ and two natural transformations $\epsilon:I \rightarrow S(A)$ and $\Delta:S(A) \otimes S(A) \rightarrow S(A)$ such that for every $A \in \mathcal{C}$, $(S(A), \Delta, \epsilon)$ is a cocommutative comonoid in $(\mathcal{C},\otimes,I)$ and this diagram commutes:

Definition

A differential category is a CMon-enriched symmetric monoidal category together with a coalgebra modality and a deriving transformation ie. a natural transformation $d:S(A) \otimes A \rightarrow S(A)$ such that the following diagrams commute: …

Examples

Codifferential categories

Definition

The definition of a codifferential category is the formal dual of that of a differential category:

A codifferential category is a category $\mathcal{C}$ equipped with structure such that its opposite category $\mathcal{C}^{op}$ is a differential category in the sense above (and vice versa).

The notion of codifferential categories is maybe more intuitively accessible because it involves monoids and monads instead of comonoids and comonads; but the formally dual notion of differential categories is closer to linear logic and differential linear logic with their comonadic modality.

In the following sequence of definitions, the object $S(A)$ is to be interpreted as a mapping space of smooth functions with variables in $A$.

Definition

An algebra modality in a symmetric monoidal category $(\mathcal{C}, \otimes, I)$ is given by a monad $(S,m,u)$ and two natural transformations $\eta:I \rightarrow S(A)$ and $\nabla:S(A) \otimes S(A) \rightarrow S(A)$ such that for every $A \in \mathcal{C}$, $(S(A), \nabla, \eta)$ is a commutative monoid in $(\mathcal{C},\otimes,I)$ and this diagram commutes:

The multiplication of the monad must be interpreted as the composition of smooth functions.

Definition

A codifferential category is a CMon-enriched symmetric monoidal category together with an algebra modality and a deriving transformation ie. a natural transformation $d:S(A) \rightarrow S(A) \otimes A$ such that the following diagrams commute:

• Leibniz rule:

It expresses that the differential of a product of two functions is the sum of the differential of the first function multiplied by the second one and the first function multiplied by the differential of the second one.

• Chain rule:

This diagram is the most tricky one. It expresses that the differential of the composition of two smooth functions is equal to the differential of the external function applied to the internal function multiplied by the differential of the internal function.

• Linear rule:

It expresses that the differential of a vector, as a formal homogeneous polynomial of degree $1$ is more or less this vector.

• Schwarz rule:

It expresses that the second differential of a function is invariant by permutation of the two variables with respect to we differentiate successively.

Examples

If $\mathbb{K}$ is a field, then $Vect_{\mathbb{K}}$ is a codifferential category.

• We define $S(A) = Sym(A)$, the symmetric algebra of the vector space $A$.
• It is a commutative algebra as usual.
• The unit $A \rightarrow Sym(A)$ of the monad is just the injection $x \mapsto x$.
• The multiplication $Sym(Sym(A)) \rightarrow Sym(A)$ of the monad is given on pure tensors by $(x_{1}^{(1)} \otimes_{s} ... \otimes_{s} x_{n_{1}}^{(1)}) \boxtimes_{s} ... \boxtimes_{s} (x_{1}^{(p)} \otimes_{s} ... \otimes_{s} x_{n_{p}}^{(p)}) \mapsto x_{1}^{(1)} \otimes_{s} ... \otimes_{s} x_{n_{1}}^{(1)} \otimes ... \otimes x_{1}^{(p)} \otimes_{s} ... \otimes_{s} x_{n_{p}}^{(p)}$. It is a kind of composition of polynomials.
• The deriving transformation $Sym(A) \rightarrow Sym(A) \otimes A$ is defined on pure tensors by $x_{1} \otimes_{s} ... \otimes_{s} x_{n} \mapsto \underset{1 \le k \le n}{\sum}(x_{1} \otimes_{s} ... \otimes_{s} x_{k-1} \otimes_{s} x_{k+1} \otimes_{s} ... \otimes_{s} x_{n}) \otimes x_{k}$. For instance, if $X,Y,Z$ is a basis of $A$, then $d(X^{2}+YZ) = 2X \otimes X + Y \otimes Z + Z \otimes Y$.

The free $\mathcal{C}^{\infty}$-ring monad on $\mathbb{R}$-vector spaces provides a structure of codifferential category on $Vect_{\mathbb{R}}$.

Commentary on the type of the deriving transformation

The deriving transformation in a codifferential category is a natural transformation of type $!A \rightarrow !A \otimes A$. As written before, in the example of vector spaces and symmetric algebras, we have thus $d(X^{2}+YZ) = 2X \otimes X + Y \otimes Z + Z \otimes Y$.

It could be more natural to have a deriving transformation of type $!A \rightarrow !A \otimes A^{*}$ and requiring the category to be *-autonomous. Thus, we would have $d(X^{2}+YZ) = 2X \otimes dX + Y \otimes dZ + Z \otimes dY$. However, the concept of graded codifferential category explains why the type $!A \rightarrow !A \otimes A$ is more natural.

Related concepts

• cartesian differential category

• differential cohesion

• tangent category, tangent (∞,1)-category

• tangent bundle category

References

The notion is due to:

• R. F. Blute, J. R. B. Cockett, and R. A. G. Seely: Differential categories. Math. Struct. Comput. Sci. 16(06), 1049–1083 (2006) (doi:10.1017/S0960129506005676)

• Richard Blute, Robin Cockett, Jean-Simon Lemay and Robert Seely, Differential categories revisited, Appl. Categ. Struct. 28, 171-235 (2020). (arXiv:1806.04804, doi:10.1007/s10485-019-09572-y)

following discussion of differential linear logic in:

• Thomas Ehrhard, Laurent Regnier: The differential lambda-calculus, Theor. Comput. Sci. 309 1 (2003) 1–41 (doi:10.1016/S0304-3975(03)00392-X)

• Thomas Ehrhard, Laurent Regnier: Differential interaction nets, Theor. Comput. Sci. 364 2 (2006) 166–195 (doi:10.1016/j.tcs.2006.08.003).

The focus is more on codifferential categories in:

• Jean-Simon Lemay: Why FHilb is Not an Interesting (Co)Differential Category, conference proceedings of QPL2019 (arXiv:1803.02304,

  doi:10.4202/EPTCS.318.2)

• Jean-Simon Lemay: Differential algebras in codifferential categories, Journal of pure and applied algebra (2019) (arXiv:1803.02304,

  doi:10.1016/j.jpaa.2019.01.005)