synthetic differential geometry
Introductions
from point-set topology to differentiable manifolds
geometry of physics: coordinate systems, smooth spaces, manifolds, smooth homotopy types, supergeometry
Differentials
Tangency
The magic algebraic facts
Theorems
Axiomatics
Models
differential equations, variational calculus
Chern-Weil theory, ∞-Chern-Weil theory
Cartan geometry (super, higher)
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
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.
The main intuition for differential categories, is that in a differential category morphisms must be interpreted as linear morphisms from to while morphisms must be interpreted as smooth morphisms from to . One can then differentiate these smooth morphisms from to . If we have , then we can obtain 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 as a morphisms of type which associate smoothly to every point of the linear approximation of around this point.
A coalgebra modality in a symmetric monoidal category is given by a comonad and two natural transformations and such that for every , is a cocommutative comonoid in and this diagram commutes:
The idea is that a coalgebra modality allows us to perform various operations on smooth morphisms.
If we start with and , we can “multiply” these two smooth morphisms together to obtain a smooth morphism defined as .
If we start with which is a linear morphism, we can say that it is a very simple form of smooth morphism and obtain a morphism from defined as
If we start with a constant , we can say that is an even simpler form of smooth morphism and obtain a morphism from defined as .
If we start with two smooth morphisms and , we can compose these two smooth morphisms to obtain a smooth morphism defined as .
A CMon-enriched symmetric monoidal category is a symmetric monoidal category such that each hom-set is a commutative monoid (in Set) and 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 such that the following diagrams commute: …
The definition of a codifferential category is the formal dual of that of a differential category:
A codifferential category is a category equipped with structure such that its opposite category 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 is to be interpreted as a mapping space of smooth functions with variables in .
An algebra modality in a symmetric monoidal category is given by a monad and two natural transformations and such that for every , is a commutative monoid in 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 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.
It expresses that the differential of a vector, as a formal homogeneous polynomial of degree is more or less this vector.
It expresses that the second differential of a function is invariant by permutation of the two variables with respect to we differentiate successively.
If is a field, then is a codifferential category.
The free -ring monad on -vector spaces provides a structure of codifferential category on .
The deriving transformation in a codifferential category is a natural transformation of type . In the category of vector spaces with the exponential modality given by symmetric algebras, we have for example .
It would seem more natural to have a deriving transformation of type and to require the category to be *-autonomous. Thus, we would have . The concept of graded codifferential category can help to enlighten why the type is in fact more natural. If we start with an element of the symmetric power of , ie. an homogeneous polynomial of degree , the deriving transformation gives us as result an element of and not of . There is an idea of “conservation of ressources”, if one starts with (symmetrized) elements of type , then a natural transformation must give as a result elements (with a symmetrization performed on the first here) and not (here it would be elements together with a “minus” element in ).
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 is given by . If we are in a *-autonomous category, we can then represent it under the form a morphism using the dual tensor product defined by .
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,
Jean-Simon Lemay: Differential algebras in codifferential categories, Journal of pure and applied algebra (2019) (arXiv:1803.02304,
Last revised on May 24, 2023 at 19:16:14. See the history of this page for a list of all contributions to it.