Monoidal bicategories, linear logic and operads
幺半群二范畴、线性逻辑和操作数
基本信息
- 批准号:EP/V002325/2
- 负责人:
- 金额:$ 31.74万
- 依托单位:
- 依托单位国家:英国
- 项目类别:Research Grant
- 财政年份:2022
- 资助国家:英国
- 起止时间:2022 至 无数据
- 项目状态:未结题
- 来源:
- 关键词:
项目摘要
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.
当我们开始学习数学时,我们了解到对数字的乘法运算满足一些基本规则。其中一个称为结合性的规则说,对于任何三个数字a,b和c,如果我们将a和b相乘,然后将结果乘以c,或者如果我们将a乘以b和c的结果,我们得到相同的结果。这就产生了么半群的抽象代数概念,它是一个集合(在这种情况下是自然数的集合),它配备了一个二元运算(在这种情况下是乘法),是结合的,有一个单位(在这个例子中是数字1)。如果我们继续学习数学,我们会遇到一种新的乘法,不再是关于数字,而是关于集合,这就是众所周知的笛卡尔乘积。给定两个集合A和B,它们的笛卡尔乘积是集合A×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之间的一一对应,它们本质上是相同的。它相当于对象和它们之间的映射的集合(在这种情况下是它们之间的所有集合和函数的集合),它配备了一个乘法(在这种情况下是笛卡尔乘积),该乘法是结合的,并且具有直到同构的单位(在这种情况下是一元素集)。在20世纪60年代引入的么半群范畴,在数学(包括逻辑、代数和拓扑学)和理论计算机科学的几个领域中都非常重要。在逻辑和理论计算机科学中,它们与线性逻辑有关,在线性逻辑中,人们跟踪证明一项陈述所需的资源。这个项目是关于乘法这一抽象概念序列的下一步,这是由一元双范畴的概念给出的。在两个类别中,我们不仅有对象和地图,而且还有2-地图,这可以被认为是“地图之间的地图”,允许我们捕捉不同地图彼此之间的关系。在一元双范畴中,我们有一种方法来乘以它们的对象、映射和2-映射,受制于复公理。20世纪90年代引入的一元双分类比一元分类具有更大的应用潜力,因为它们允许我们跟踪更多的信息。我们试图通过提出一元双范畴理论来实现这一潜力。我们将证明有关它们的基本定理,发展与线性逻辑和理论计算机科学的新联系,并研究对代数和拓扑学感兴趣的例子。我们的工作通过一个重要的研究程序与代数联系在一起,这个程序被称为“范畴化”,它涉及到用基于范畴的结构(如么半群)替换基于集合的结构(如么半群),以获得更微妙的不变量。我们的工作通过操作符的概念链接到拓扑学,操作符是一种灵活的工具,用于描述代数结构,其中公理不是作为等式成立的,而是直到弱形式的同构。总体而言,该项目将把一元双范畴理论提高到一个新的水平,并促进数学和理论计算机科学之间的跨学科研究。
项目成果
期刊论文数量(3)
专著数量(0)
科研奖励数量(0)
会议论文数量(0)
专利数量(0)
Fixpoint constructions in focused orthogonality models of linear logic
线性逻辑聚焦正交模型中的不动点构造
- DOI:10.46298/entics.12302
- 发表时间:2023
- 期刊:
- 影响因子:0
- 作者:Fiore M
- 通讯作者:Fiore M
Strictifying Operational Coherences and Weak Functor Classifiers in Low Dimensions
低维下严格运算一致性和弱函子分类器
- DOI:10.48550/arxiv.2307.01498
- 发表时间:2023
- 期刊:
- 影响因子:0
- 作者:Miranda A
- 通讯作者:Miranda A
Fixpoint operators for 2-categorical structures
2 分类结构的不动点算子
- DOI:10.1109/lics56636.2023.10175688
- 发表时间:2023
- 期刊:
- 影响因子:0
- 作者:Galal Z
- 通讯作者:Galal Z
{{
item.title }}
{{ item.translation_title }}
- DOI:
{{ item.doi }} - 发表时间:
{{ item.publish_year }} - 期刊:
- 影响因子:{{ item.factor }}
- 作者:
{{ item.authors }} - 通讯作者:
{{ item.author }}
数据更新时间:{{ journalArticles.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ monograph.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ sciAawards.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ conferencePapers.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ patent.updateTime }}
Nicola Gambino其他文献
Kripke-Joyal forcing for type theory and uniform fibrations
- DOI:
10.1007/s00029-024-00962-2 - 发表时间:
2024-07-31 - 期刊:
- 影响因子:1.200
- 作者:
Steve Awodey;Nicola Gambino;Sina Hazratpour - 通讯作者:
Sina Hazratpour
Nicola Gambino的其他文献
{{
item.title }}
{{ item.translation_title }}
- DOI:
{{ item.doi }} - 发表时间:
{{ item.publish_year }} - 期刊:
- 影响因子:{{ item.factor }}
- 作者:
{{ item.authors }} - 通讯作者:
{{ item.author }}
{{ truncateString('Nicola Gambino', 18)}}的其他基金
Monoidal bicategories, linear logic and operads
幺半群二范畴、线性逻辑和操作数
- 批准号:
EP/V002325/1 - 财政年份:2021
- 资助金额:
$ 31.74万 - 项目类别:
Research Grant
Homotopy Type Theory: Programming and Verification
同伦类型理论:编程与验证
- 批准号:
EP/M01729X/1 - 财政年份:2015
- 资助金额:
$ 31.74万 - 项目类别:
Research Grant
相似海外基金
Linear logic, finiteness spaces and bicategories
线性逻辑、有限空间和二分类
- 批准号:
RGPIN-2022-03900 - 财政年份:2022
- 资助金额:
$ 31.74万 - 项目类别:
Discovery Grants Program - Individual
Monoidal bicategories, linear logic and operads
幺半群二范畴、线性逻辑和操作数
- 批准号:
EP/V002325/1 - 财政年份:2021
- 资助金额:
$ 31.74万 - 项目类别:
Research Grant
Monoidal bicategories, linear logic and operads
幺半群二范畴、线性逻辑和操作数
- 批准号:
EP/V002309/1 - 财政年份:2021
- 资助金额:
$ 31.74万 - 项目类别:
Research Grant