Tangent bundles in differential lambda-categories

TL;DR

This paper explores tangent bundle structures within differential lambda-categories, establishing a canonical monad akin to tangent bundles in smooth manifolds, with implications for lambda-calculus semantics.

Contribution

It proves that differential lambda-categories naturally possess a canonical strong commutative monad similar to tangent bundles, extending the theory to broader cartesian differential categories.

Findings

Existence of a canonical strong commutative monad in differential lambda-categories

Construction resembles tangent bundles in smooth manifolds

Results extend to arbitrary cartesian differential categories

Abstract

Differential lambda-categories were introduced by Bucciarelli et al. as models for the simply typed version of the differential lambda-calculus of Ehrhard and Regnier. A differential lambda-category is a cartesian closed differential category of Blute et al. in which the differential operator is compatible with the closed structure. We prove that any differential lambda-category is equipped with a canonical strong commutative monad whose construction resembles that of the tangent bundle in the category of smooth manifolds. Most of the results of this note remain valid in an arbitrary cartesian differential category. Our emphasis on differential lambda-categories is motivated by the anticipated application of the theory developed in this note to the design and semantics of a lambda-calculus extended by the pushforward operator.