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

点击翻译按钮获取中文摘要

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.