Linear Logic, Monoidal Categories and Abstract Models of Differentiation and Integration

我项目的目标是继续探索一元范畴的理论，特别是使用线性逻辑的技术。线性逻辑的模型是带有单元（满足若干自然性条件的内函子）的一元范畴。在以前的工作中，我们已经定义了微分范畴的概念。这些是线性逻辑的模型，有一个额外的算子，它允许微分态射。对于任何线性逻辑模型，我们都可以联想到第二个范畴，它的Kleisli范畴。对于微分范畴，这个范畴是光滑映射的范畴。相应的逻辑，微分线性逻辑，是由Ehrhard和Regnier引入的。这就为我们考虑抽象的微分理论提供了一个范畴和逻辑基础。******我们的微分范畴的概念和更传统的代数几何的Kahler模与交换代数相关的微分形式的概念之间有明显的关系。两者通常都将带有派生的模块关联到代数。但在微分范畴的情况下，新奇之处在于我们可以进一步表达微分规则，比如链式法则。然而微分范畴缺乏定义Kahler模的全称性质。******考虑到这一点，我们发展了Kahler范畴的概念它加入了一个适当的普适性概念并表明在非常一般的情况下，协微分范畴就是Kahler范畴。这项工作揭示了单细胞及其代数在Kahler理论中以前未被观察到的重要性。我们正在研究将描述光滑代数上同调的经典Hochschild-Kostant-Rosenberg定理扩展到Kahler范畴的集合。作为这项工作的一部分，有必要定义光滑单轴的概念，以类比于原始hkr定理的光滑代数。最后，我们正致力于将这些思想扩展到非对易环境，从非对易几何中汲取灵感。******从我们发展出来的逻辑和范畴的观点来考虑积分也是有意义的。其结果将类似于Rota-Baxter代数的多对象版本。Rota-Baxter代数是具有自同态的结合代数，它满足分部积分公式的抽象和推广。******在量子场论中的重整化相关的Connes-Kreimer Hopf代数中存在一个自然存在的Rota-Baxter算子。过去，在与Panangaden的联合工作中，我们证明了证明网（用于在线性逻辑中指定证明的图论语法）可以被解释为受费曼图启发的简单微积分中的形式算子。一个积分线性逻辑的概念，其中我们有一个Rota-Baxter算子的逻辑解释，可能证明对深化这种对应是有用的。

The goal of my project will be to continue to explore the theory of monoidal categories, especially using the techniques of linear logic. A model of linear logic is a monoidal category equipped with a monad (an endofunctor satisfying several naturality conditions). In previous work, we have defined the notion of differential category. These are models of linear logic with an additional operator which allows one to differentiate morphisms. To any model of linear logic, one can associate a second category, its Kleisli category. For differential categories, this category is a category of smooth maps. The corresponding logic, differential linear logic, was introduced by Ehrhard and Regnier. This then gives us a categorical and logical foundation for considering abstract theories of differentiation.******There is an evident relationship between our notion of differential category and the more traditional notion from algebraic geometry of a Kahler module of differential forms associated to a commutative algebra. Both canonically associate to an algebra a module equipped with a derivation. But in the case of differential categories, the novelty is that one can express further differentiation rules such as the chain rule. However differential categories lack the universal property defining Kahler modules. ******With this in mind, we developed the notion of Kahler category which adds in an appropriate notion of universality and showed that in a very general setting, codifferential categories are Kahler. This work revealed the previously unobserved importance of monads and their algebras in Kahler theory. We are looking into extending the classical Hochschild-Kostant-Rosenberg theorem characterizing the cohomology of smooth algebras to the setting of Kahler categories. As part of this work, it is necessary to define the notion of a smooth monad in analogy to the smooth algebras of the original HKR-theorem. FInally, we are working on an extension of these ideas to the noncommutative setting, drawing our inspiration from noncommutative geometry.******It also makes sense to consider the integral calculus from the logical and categorical viewpoint we have developed. The result would be something like a multi-object version of Rota-Baxter algebras. Rota-Baxter algebras are associative algebras with an endomorphism which satisfies an abstraction and generalization of the integration by parts formula. ******There is a naturally occurring Rota-Baxter operator in the Connes-Kreimer Hopf algebra associated to renormalization in quantum field theory. In the past, in joint work with Panangaden, we showed that proof nets, a graph-theoretic syntax for specifying proofs in linear logic, can be interpreted as formal operators in a simple calculus inspired by Feynman diagrams. A notion of integral linear logic in which we have a logical interpretation of a Rota-Baxter operator, may prove useful in deepening this correspondence.