A Fibrational Theory of First Order Differential Structures
Matteo Capucci, Geoffrey S. H. Cruttwell, Neil Ghani, Fabio Zanasi
TL;DR
This paper argues for a unifying fibrational framework to model first-order differential structure across multiple categorical formalisms (CDCs, gCDCs, RDCs, and tangent/reverse variants). By treating differentiation as a section of a suitably structured fibration with fibrewise additive monoids, it derives a uniform set of first-order axioms and constructions, clarifying how forward and reverse derivatives relate through dual fibrations (e.g., simple and lens fibrations). Key results include the characterization of CDCs and RDCs as sections of corresponding fibrations, the construction of cofree CDCs from linear objects, and the demonstration that linear differential data give rise to differential categories under the fibrational lens. The approach reveals how linearity and additivity interact in a broadly applicable setting, and it points toward higher-order and comprehension-based extensions to model richer differential-geometric structures. Overall, the work positions fibrations as a central organizing principle for differentiable structure in category theory, enabling uniform proofs and streamlined constructions across diverse models.
Abstract
We develop a categorical framework for reasoning about abstract properties of differentiation, based on the theory of fibrations. Our work encompasses the first-order fragments of several existing categorical structures for differentiation, including cartesian differential categories, generalised cartesian differential categories, tangent categories, as well as the versions of these categories axiomatising reverse derivatives. We explain uniformly and concisely the requirements expressed by these structures, using sections of suitable fibrations as unifying concept. Our perspective sheds light on their similarities and differences, as well as simplifying certain constructions from the literature.