Monoidal bicategories, linear logic and operads

当我们开始学习数学时，我们学到数的乘法运算满足一些基本规则。其中一条规则被称为结合性，它说，对于任何三个数字a，B和c，如果我们将a和B相乘，然后将结果乘以c，或者如果我们将a乘以B和c的结果，我们会得到相同的结果。这导致了幺半群的抽象代数概念，幺半群是一个集合（在这种情况下是自然数的集合），配备了一个二元运算（在这种情况下是乘法），它是结合的，有一个单位（在这种情况下是数字1）。如果我们继续学习数学，我们会遇到一种新的乘法，不再是数字，而是集合，这被称为笛卡尔积。给定两个集合A和B，它们的笛卡尔积是集合A x B，其元素是有序对（a，B），其中a是A的元素，B是B的元素。从图形上看，两个集合的笛卡尔积是一个坐标由两个集合的元素给出的网格。该运算满足一些规则，类似于数字相乘的规则，但稍微微妙一点。例如，如果给定三个集合A、B和C，则集合A x（B x C）与集合（A x B）x C同构（而不是相等）。这里，同构意味着通过元素A x（B x C）与元素（A x B）x C之间的一一对应，它们本质上相同。这种构造导致了monoidal范畴的概念，它相当于对象和它们之间的映射的集合（在这种情况下是它们之间的所有集合和函数的集合），配备了乘法（在这种情况下是笛卡尔积），它是结合的，并且具有直到同构的单位（在这种情况下是单元素集合）。在60年代引入的Monoidal范畴在数学（包括逻辑、代数和拓扑）和理论计算机科学的几个领域中非常重要。在逻辑和理论计算机科学中，它们与线性逻辑有关，在线性逻辑中，人们跟踪证明一个陈述所需的资源。这个项目是关于乘法的抽象概念序列的下一步，这是由monoidal bicategory的概念给出的。在双范畴中，我们不仅有对象和映射，还有2-映射，这可以被认为是“映射之间的映射”，并允许我们捕捉不同映射之间的关系。在monoidal bicategory中，我们有一种方法来乘以他们的对象，映射和2-映射，服从复杂的公理。Monoidal bicategies，在90年代被引入，有着比Monoidal categories更大的应用潜力，因为它们允许我们跟踪更多的信息。我们试图通过推进monoidal bicategories理论来实现这一潜力。我们将证明关于它们的基本定理，发展与线性逻辑和理论计算机科学的新联系，并研究代数和拓扑学中感兴趣的例子。我们的工作通过一个重要的研究项目“范畴化”与代数相联系，该项目涉及用基于范畴的结构（如monoidal范畴）替换基于集合的结构（如monoidal范畴），以获得更微妙的不变量。我们的工作链接到拓扑通过的概念，一个操作，这是一个灵活的工具，用来描述代数结构中的公理不持有平等，而是到弱形式的同构。总的来说，这个项目将把monoidal bicategories的理论带到一个新的水平，并促进数学和理论计算机科学的跨学科研究。

When we begin to study mathematics, we learn that the operation of multiplication on numbers satisfies some basic rules. One of these rules, known as associativity, says that for any three numbers a, b and c, we get the same result if we multiply a and b and then multiply the result by c or if we multiply a by the result of multiplying b and c. This leads to the abstract algebraic notion of a monoid, which is a set (in this case the set of natural numbers) equipped with a binary operation (in this case multiplication) that is associative and has a unit (in this case the number 1). If we continue to study mathematics, we encounter a new kind of multiplication, no longer on numbers but on sets, which is known as Cartesian product. Given two sets A and B, their Cartesian product is the set A x B whose elements are the ordered pairs (a, b), where a is an element of A and b is an element of B. Pictorially, the Cartesian product of two sets is a grid with coordinates given by the elements of the two sets. This operation satisfies some rules, analogous to those for the multiplication of numbers, but a little more subtle. For example, if we are given three sets A, B and C, then the set A x (B x C) is isomorphic (rather than equal) to the set (A x B) x C. Here, being isomorphic means that we they are essentially the same by means of a one-to-one correspondence between the elements A x (B x C) and those of (A x B) x C. This construction leads to the notion of a monoidal category, which amounts to a collection of objects and maps between them (in this case the collection of all sets and functions between them) equipped with a multiplication (in this case the Cartesian product) that is associative and has a unit (in this case the one-element set) up to isomorphism. Monoidal categories, introduced in the '60s, have been extremely important in several areas of mathematics (including logic, algebra, and topology) and theoretical computer science. In logic and theoretical computer science, they connect to linear logic, in which one keeps track of the resources necessary to prove a statement. This project is about the next step in this sequence of abstract notions of multiplication, which is given by the notion of a monoidal bicategory. In a bicategory, we have not only objects and maps but also 2-maps, which can be thought of as "maps between maps" and allow us to capture how different maps relate to each other. In a monoidal bicategory, we have a way of multiplying their objects, maps and 2-maps, subject to complex axioms. Monoidal bicategories, introduced in the '90s, have potential for applications even greater than that of monoidal categories, as they allow us to keep track of even more information. We seek to realise this potential by advancing the theory of monoidal bicategories. We will prove fundamental theorems about them, develop new connections to linear logic and theoretical computer science and investigate examples that are of interest in algebra and topology. Our work connects to algebra via an important research programme known as "categorification", which is concerned with replacing set-based structures (like monoids) with category-based structures (like monoidal categories) in order to obtain more subtle invariants. Our work links to topology via the notion of an operad, which is a flexible tool used to describe algebraic structures in which axioms do not hold as equalities, but rather up to weak forms of isomorphism. Overall, this project will bring the theory of monoidal bicategories to a new level and promote interdisciplinary research within mathematics and with theoretical computer science.