A Fibrational Theory of First Order Differential Structures

TL;DR

This paper introduces a fibrational categorical framework that unifies and simplifies the understanding of various differential structures, including forward and reverse derivatives, in a broad abstract setting.

Contribution

It provides a new fibrational approach to unify and analyze first-order differential structures across multiple categorical frameworks.

Findings

Unified fibrational perspective on differential categories

Simplified constructions in categorical differentiation

Clarified relationships between forward and reverse derivative structures

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.