nLab differential category



Differential geometry

synthetic differential geometry


from point-set topology to differentiable manifolds

geometry of physics: coordinate systems, smooth spaces, manifolds, smooth homotopy types, supergeometry



smooth space


The magic algebraic facts




infinitesimal cohesion

tangent cohesion

differential cohesion

graded differential cohesion

singular cohesion

id id fermionic bosonic bosonic Rh rheonomic reduced infinitesimal infinitesimal & étale cohesive ʃ discrete discrete continuous * \array{ && id &\dashv& id \\ && \vee && \vee \\ &\stackrel{fermionic}{}& \rightrightarrows &\dashv& \rightsquigarrow & \stackrel{bosonic}{} \\ && \bot && \bot \\ &\stackrel{bosonic}{} & \rightsquigarrow &\dashv& \mathrm{R}\!\!\mathrm{h} & \stackrel{rheonomic}{} \\ && \vee && \vee \\ &\stackrel{reduced}{} & \Re &\dashv& \Im & \stackrel{infinitesimal}{} \\ && \bot && \bot \\ &\stackrel{infinitesimal}{}& \Im &\dashv& \& & \stackrel{\text{étale}}{} \\ && \vee && \vee \\ &\stackrel{cohesive}{}& \esh &\dashv& \flat & \stackrel{discrete}{} \\ && \bot && \bot \\ &\stackrel{discrete}{}& \flat &\dashv& \sharp & \stackrel{continuous}{} \\ && \vee && \vee \\ && \emptyset &\dashv& \ast }


Lie theory, ∞-Lie theory

differential equations, variational calculus

Chern-Weil theory, ∞-Chern-Weil theory

Cartan geometry (super, higher)

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels




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

The main intuition for differential categories, is that in a differential category morphisms ABA \rightarrow B must be interpreted as linear morphisms from AA to BB while morphisms !AB!A \rightarrow B must be interpreted as smooth morphisms from AA to BB. One can then differentiate these smooth morphisms from AA to BB. If we have f:!ABf:!A \rightarrow B, then we can obtain D(f):!AABD(f):!A \otimes A \rightarrow B which is smooth in the first variable and linear in the second variable. If we are in a monoidal closed category, we can alternatively view D(f)D(f) as a morphisms of type !A(AB)!A \rightarrow (A \multimap B) which associate smoothly to every point of AA the linear approximation of ff around this point.


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

The idea is that a coalgebra modality allows us to perform various operations on smooth morphisms.

  • If we start with f:!ABf:!A \rightarrow B and g:!ACg:!A \rightarrow C, we can “multiply” these two smooth morphisms together to obtain a smooth morphism !ABC!A \rightarrow B \otimes C defined as Δ;fg\Delta;f \otimes g.

  • If we start with f:ABf:A \rightarrow B which is a linear morphism, we can say that it is a very simple form of smooth morphism and obtain a morphism !AB!A \rightarrow B from ff defined as u;fu;f

  • If we start with a constant f:I!Af:I \rightarrow !A, we can say that is an even simpler form of smooth morphism and obtain a morphism !AB!A \rightarrow B from ff defined as ϵ;f\epsilon;f.

  • If we start with two smooth morphisms f:!ABf:!A \rightarrow B and g:!BCg:!B \rightarrow C, we can compose these two smooth morphisms to obtain a smooth morphism !AC!A \rightarrow C defined as m;!(f);gm;!(f);g.


A CMon-enriched symmetric monoidal category is a symmetric monoidal category 𝒞\mathcal{C} such that each hom-set 𝒞[A,B]\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.


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


Codifferential categories

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 𝒞 op\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)S(A) is to be interpreted as a mapping space of smooth functions with variables in AA.


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

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


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)S(A)Ad:S(A) \rightarrow S(A) \otimes A such that the following diagrams commute:

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.

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 11 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.


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

  • We define S(A)=Sym(A)S(A) = Sym(A), the symmetric algebra of the vector space AA.
  • It is a commutative algebra as usual.
  • The unit ASym(A)A \rightarrow Sym(A) of the monad is just the injection xxx \mapsto x.
  • The multiplication Sym(Sym(A))Sym(A)Sym(Sym(A)) \rightarrow Sym(A) of the monad is given on pure tensors by (x 1 (1) s... sx n 1 (1)) s... s(x 1 (p) s... sx n p (p))x 1 (1) s... sx n 1 (1)...x 1 (p) s... sx n p (p)(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)Sym(A)ASym(A) \rightarrow Sym(A) \otimes A is defined on pure tensors by x 1 s... sx n1kn(x 1 s... sx k1 sx k+1 s... sx n)x kx_{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,ZX,Y,Z is a basis of AA, then d(X 2+YZ)=2XX+YZ+ZYd(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 Vect_{\mathbb{R}}.

Differential categories vs codifferential categories

The deriving transformation in a codifferential category is a natural transformation of type !A!AA!A \rightarrow !A \otimes A. In the category of vector spaces with the exponential modality given by symmetric algebras, we have for example d(X 2+YZ)=2XX+YZ+ZYd(X^{2}+YZ) = 2X \otimes X + Y \otimes Z + Z \otimes Y.

It would seem more natural to have a deriving transformation of type !A!AA *!A \rightarrow !A \otimes A^{*} and to require the category to be *-autonomous. Thus, we would have d(X 2+YZ)=2XdX+YdZ+ZdYd(X^{2}+YZ) = 2X \otimes dX + Y \otimes dZ + Z \otimes dY. The concept of graded codifferential category can help to enlighten why the type !A!AA!A \rightarrow !A \otimes A is in fact more natural. If we start with an element of the (n+1) th(n+1)^{th} symmetric power S n+1AS_{n+1}A of AA, ie. an homogeneous polynomial of degree n+1n+1, the deriving transformation gives us as result an element of S nAAS_{n}A \otimes A and not of S nAA *S_{n}A \otimes A^{*}. There is an idea of “conservation of ressources”, if one starts with (n+1)(n+1) (symmetrized) elements of type AA, then a natural transformation must give as a result n+1n+1 elements (with a symmetrization performed on the nn first here) and not n1n-1 (here it would be nn elements together with a “minus” element in A *A^*).

If we wish to obtain a more natural typing, we need to use differential categories. In a differential category, the differential of a smooth function !AB!A \rightarrow B is given by d;f:!AABd;f:!{A} \otimes A \rightarrow B. If we are in a *-autonomous category, we can then represent it under the form a morphism !ABA *!A \rightarrow B \parr A^* using the dual tensor product \parr defined by AB=(A *B *) *A \parr B = (A^* \otimes B^*)^*.


The notion is due to:

following discussion of differential linear logic in:

The focus is more on codifferential categories in:

Last revised on May 24, 2023 at 19:16:14. See the history of this page for a list of all contributions to it.