多范畴中的双映射：连接经典线性逻辑解释

本文探讨了多范畴理论与经典线性逻辑之间的深刻联系，特别是关注于解释经典线性逻辑的乘法片段的不同方法。在多范畴中，经典的线性逻辑模型通常建立在存在满足特定性质的多映射之上，如定义张量、par和否定运算。这些性质反映了多映射的普遍性，即它们能够处理不同类型的对象参数。 作者首先解释了这些通用性质如何可以通过一个单一的概念——参数化的polymap（泛多映射）来统一。polymap在多范畴中扮演着核心角色，它是经典多映射概念的概括，它能够适应输入和输出对象的变化。这种视角使得理解和处理多范畴中的复合性和结构变得更加直观。 接下来，文中引入了相对于多范畴的加细系统（严格的函子）的概念，即入卡多映射和出卡多映射，进一步细化了多映射的讨论。通过这种方式，泛多映射可以被视为更广泛情况下的特殊形式，这有助于澄清多范畴结构的底层原理。 多范畴的核心性质——可表示性与双分裂的概念紧密相连，即一个多范畴如果能在终端多范畴上实现双分裂，那么它就是可表示的。这个结果对于理解多范畴的内在特性及其与线性逻辑的对应关系至关重要。 最后，文章探讨了从多范畴和伪函子到MAdj（弱）2-多范畴的（弱）多范畴之间的Grothendieck对应，这是一种重要的构造工具。当这种对应被限制在双稳态情况下，它可以追溯到Shulman在MAdj中的近期工作，涉及Frobenius幺半群等概念。 本文深入研究了多范畴中解释线性逻辑的关键元素，包括多映射、泛性质、加细系统以及Grothendieck构造，这些都是理解计算理论和逻辑基础的重要组成部分。通过这些理论，作者揭示了多范畴与线性逻辑之间深刻的逻辑结构关联，为后续的理论研究和实际应用提供了坚实的数学基础。