| Summary: | <p>The theory of differential categories uses category theory to provide the mathematical foundations of differentiation in both mathematics and computer science. Differential categories are successful because they capture both the classical limit definition of differentiation and the more algebraic synthetic definition of differentiation. As such, the theory of differential categories has been able to formalize various aspects of differential calculus, from the very basic foundational aspects of differentiation, such as the notion of derivations from commutative algebras, to the more complex notions of differential geometry, such as the tangent bundle of a smooth manifold. The theory of differential categories has a rich literature and has been used to study differentiation in a variety of fields from mathematics, such as commutative algebra and differential geometry, as well as computer science, such as in machine learning and differentiable programming languages. This thesis is split into three parts, each relating to the theory of differential categories. </p>
<p>The first part of this thesis addresses a long-standing problem amongst the differential category theory community. Differential categories can either be axiomatized in terms of a deriving transformation or in terms of a codereliction. It has long been known that coderelictions are equivalent to deriving transformations that satisfy an extra rule called the ∇-rule. However, by definition, not every deriving transformation needs to satisfy the ∇-rule. As such, this left open the question of whether for categorical models of differential linear logic, coderelictions and deriving transformations were distinct notions of differentiation. However, we show that for a monoidal coalgebra modality, it turns out that every deriving transformation automatically satisfies the ∇-rule and that, in fact, it is equivalent to the product rule. Therefore, for a monoidal coalgebra modality, there is a bijective correspondence between coderelictions and deriving transformations. Thus, there is only one notion of differentiation in linear logic.</p>
<p>The second part of this thesis introduces the notion of a linearizing combinator which abstracts linearization in the Abelian functor calculus. We explain how a linearizing combinator provides an alternative axiomatization of a Cartesian differential category. Indeed, every Cartesian differential category comes equipped with a canonical linearizing combinator obtained by differentiation at zero. Conversely, a differential combinator can be constructed when one has a system of partial linearizing combinators in each context. Thus, while linearizing combinators do provide an alternative axiomatization of Cartesian differential categories, an explicit notion of partial linearization is required. The ability to form a system of partial linearizing combinators from a total linearizing combinator, while not being possible in general, is possible when the setting is Cartesian closed.</p>
<p>The third part of this thesis introduces differential exponential maps in Cartesian differential categories, which generalize the exponential function e<sup>x</sup> from classical differential calculus. Every differential exponential map induces a commutative rig, which we call a differential exponential rig, and conversely, every differential exponential rig induces a differential exponential map. In particular, differential exponential maps can be defined without the need of limits, converging power series, or unique solutions of certain differential equations -- which most Cartesian differential categories do not necessarily have. That said, we do explain how every differential exponential map does provide solutions to certain differential equations, and conversely how in the presence of unique solutions, one can derivative a differential exponential map. </p>
<p>Each part of this thesis is an important result to the theory of differential categories. </p>
|
|---|