An Ultrametric for Cartesian Differential Categories for Taylor Series Convergence

Cartesian differential categories provide a categorical framework for multivariable differential calculus and also the categorical semantics of the differential $\lambda$-calculus. Taylor series expansion is an important concept for both differential calculus and the differential $\lambda$-calculus. In differential calculus, a function is equal to its Taylor series if its sequence of Taylor polynomials converges to the function in the analytic sense. On the other hand, for the differential $\lambda$-calculus, one works in a setting with an appropriate notion of algebraic infinite sums to formalize Taylor series expansion. In this paper, we provide a formal theory of Taylor series in an arbitrary Cartesian differential category without the need for converging limits or infinite sums. We begin by developing the notion of Taylor polynomials of maps in a Cartesian differential category and then show how comparing Taylor polynomials of maps induces an ultrapseudometric on the homsets. We say that a Cartesian differential category is Taylor if maps are entirely determined by their Taylor polynomials. The main results of this paper are that in a Taylor Cartesian differential category, the induced ultrapseudometrics are ultrametrics and that for every map $f$, its Taylor series converges to $f$ with respect to this ultrametric. This framework recaptures both Taylor series expansion in differential calculus via analytic methods and in categorical models of the differential $\lambda$-calculus (or Differential Linear Logic) via infinite sums.