Cartesian Fermat Categories, a new class of Cartesian Differential Categories

Abstract: Cartesian differential categories (introduced by Blute, Cockett, and Seely) provide a categorical framework for differential calculus, and also provide the categorical foundations for the differential lambda calculus, differentiable programming, and certain automatic differentiation techniques used for machine learning. Another approach to the categorical foundations of differentiation are Fermat theories (introduced by Dubuc and Kock), which are Lawvere theories that have Hadamard’s Lemma as an axiom. It is already known that every Fermat theory is a Cartesian differential category. However, the definition of a Fermat theory is heavily dependent on 1) being a Lawvere theory and 2) being able to multiply maps, which are two things that are not assumed for Cartesian differential categories. In this talk, we will introduce Cartesian Fermat categories, the proper Fermat theory analogue of a Cartesian differential category, with the main result being that Cartesian Fermat category is a Cartesian differential category. This talk will also include a friendly introduction to Cartesian differential categories, and thus will be accessible to anyone, including newcomers, interested in differential categories.

This talk is based on joint work with Carlos Pascual Miralles.

Computer sciencecategory theorylogic

Audience: learners

( video )

Topos Institute Colloquium