Jean-Simon Lemay (University of Oxford): The Theory of Differential Categories

The theory of differential categories uses category theory to study the foundations of differentiation. Differential categories have been able to formalize various aspects of differentiation, from the very basic foundational aspects of differentiation to the more complex notions of differential geometry. In these lectures, we propose to introduce and summarize the theory of differential categories, as well as discuss interesting examples and applications. There will be three (possibly four) lectures:We will provide an overview introduction to the theory of differential categories. In particular, we will take a look at the "map of differential categories" and discuss how each stage of the theory of differential categories are connected.

We will also discuss the first stage differential categories, which are axiomatized by the basic algebraic foundations of differentiation and provide the categorical semantics of differential linear logic.

We will discuss Cartesian differential categories, which formalize the directional derivative and the theory of multivariable differential calculus over Euclidean spaces, and provide the categorical semantics of the differential lambda-calculus.We will discuss tangent categories, which formalize tangent bundle structure and the theory of smooth manifolds

(Bonus Lecture) Reverse differentiation is used in programming for efficient computations. We will discuss Cartesian reverse differential categories, a recent introduction to the theory of differential categories, which axiomatizes reverse differentiation, and their relationship to Cartesian differential categories, which axiomatize the forward derivative.