Differential Category

A differential category (Blute, Cockett & Seely) axiomatises differentiation as categorical structure rather than as a limit of difference quotients. The Cartesian version equips a Cartesian left-additive category with a differential combinator sending to , the derivative of at the first argument in the direction of the second. Its axioms are exactly the laws of the Jacobian: linearity in the direction, the chain rule, the symmetry of mixed partials, and compatibility with products.

Property. The chain rule is a commuting diagram

The chain rule reads . Differentiation is a functor-like operation on the category, and the chain rule is its composition-preservation law. The linear-logic presentation instead places the structure on a comonad , as a deriving transformation on , so that differentiation becomes the infinitesimal shadow of the exponential modality. This derivation on traces back to Ehrhard–Regnier’s differential λ-calculus.

Example. Where the derivative already lives

Smooth maps between convenient vector spaces and polynomial maps with the formal derivative both carry a differential combinator. So does any model of synthetic differential geometry, where an infinitesimal object makes literally the slope read off . Kähler differentials give the algebraic-geometry instance.