论文标题

线性化合物

Linearizing Combinators

论文作者

Cockett, Robin, Lemay, Jean-Simon Pacaud

论文摘要

2017年,鲍尔(Bauer),约翰逊(Johnson),奥斯本(Osborne),里尔(Riehl)和泰伯(Tebbe)(比约(Bjort)(Bjort)表明,阿贝尔(Abelian)函子演算体提供了笛卡尔差异类别的示例。笛卡尔微分类别的定义基于一个差分组合器,该组合物直接从多变量计算中形式化了总导数。但是,在上述工作中,作者使用了善意的函子演算的技术来建立线性化过程,然后从中得出了差异组合器。这就提出了一个问题,即线性化与具有差异组合器的确切关系可能是什么。 在本文中,我们介绍了线性化组合器的概念,该组合物在Abelian Foundor演算中抽象线性化。然后,我们使用它来提供笛卡尔差异类别的替代公理化。每个笛卡尔差异类别都配备了通过零以零分化获得的规范线性化组合器。相反,当一个在每种情况下具有部分线性化组合器的系统时,可以构建一个差异组合器。因此,虽然线性化组合确实提供了笛卡尔微分类别的替代公理化,但需要明确的部分线性化概念。这与差分组合剂的情况相反,在差分组合的情况下,在存在总分化的情况下,部分分化是自动的。当设置为笛卡尔关闭时,可以从总线性化组合器中形成部分线性化组合器系统的能力。

In 2017, Bauer, Johnson, Osborne, Riehl, and Tebbe (BJORT) showed that the Abelian functor calculus provides an example of a Cartesian differential category. The definition of a Cartesian differential category is based on a differential combinator which directly formalizes the total derivative from multivariable calculus. However, in the aforementioned work the authors used techniques from Goodwillie's functor calculus to establish a linearization process from which they then derived a differential combinator. This raised the question of what the precise relationship between linearization and having a differential combinator might be. In this paper, we introduce the notion of a linearizing combinator which abstracts linearization in the Abelian functor calculus. We then use it to provide an alternative axiomatization of a Cartesian differential category. Every Cartesian differential category comes equipped with a canonical linearizing combinator obtained by differentiation at zero. Conversely, a differential combinator can be constructed à la BJORT 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. This is in contrast to the situation for differential combinators where partial differentiation is automatic in the presence of total differentiation. 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.

扫码加入交流群

加入微信交流群

微信交流群二维码

扫码加入学术交流群,获取更多资源