Homotopy Theory and its Applications

同伦理论及其应用

• 批准号: RGPIN-2018-04595
• 负责人: Kapulkin, Krzysztof
• 金额: $ 1.68万
• 依托单位: University of Western Ontario
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2020
• 资助国家: 加拿大
• 起止时间: 2020-01-01 至 2021-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=713158
• 关键词: Homotopy; Theory; its; Applications

Homotopy Theory is a branch of pure mathematics which uses algebraic invariants (such as the dimension) to tell two geometric objects apart. In recent years, tools coming from Homotopy Theory have been applied in other areas, both within mathematics (for instance, in algebra) and outside, for example, in mathematical physics and theoretical computer science. This Discovery Grant proposal explores several such applications and helps develop the general theory. In brief, the proposed research falls under four main themes. The first of these themes is Higher Category Theory, which aims to establish the general framework in which one can talk about homotopy theory, thus making the theory applicable to other areas. In this proposal, we explore possibilities of reshaping this framework in ways oriented towards computations and new applications, for instance in knot theory and geometric representation theory. The second theme, Homotopy Type Theory, investigates a newly discovered connection between homotopy theory and type theory, a logical system studied in theoretical computer science. This connection allows one to use dependent type theory to prove results in homotopy theory, while also use theorems from homotopy theory to suggest new principles of logic (such as Voevodsky's Univalence Axiom). Dependent type theories were previously studied due to their suitability for large scale computer formalization (and are currently used by many major corporations, including Intel and Toyota) and we can therefore use homotopy theory to enhance the existing software. The objectives of the third theme, Formalization of Mathematics, examine the resulting tools, as we will use them to formalize several results which had previously proven difficult. Finally, in the fourth theme, Cryptography, we will study applications of homotopy theory to cryptography. Specifically, we will attempt to use a particular algebraic invariant, the cohomology ring of a variety, to construct examples of cryptographically useful multilinear maps. Many applications of cryptographic multilinear maps, including broadcast encryption, internet voting, and indistiguishability obfuscation, have been known for the past 15 years, yet no one was able to construct an example of such a map. Many of the problems proposed here are suitable for students at different levels and equip them with the skills and experience that can be used both in their further academic work and in industry. Many of our specific objectives involve collaboration between mathematicians and knowledge users, including software engineers and, for example, broadcast companies. Altogether the proposal takes techniques central to pure mathematics and investigates their applications outside this realm.

同型理论是纯数学的一个分支，它使用代数不变性（例如维度）将两个几何对象分开。近年来，来自同型理论的工具已在数学（例如，代数）和外部（例如数学物理学和理论计算机科学）中应用。该发现赠款提案探讨了几种此类应用，并有助于发展一般理论。简而言之，拟议的研究属于四个主要主题。 这些主题中的第一个是更高的类别理论，旨在建立一个可以谈论同质理论的一般框架，从而使该理论适用于其他领域。在此提案中，我们探讨了以针对计算和新应用的方式重塑该框架的可能性，例如结理论和几何表示理论。第二个主题是同质类型理论，研究了同义理论与类型理论之间的新发现的联系，这是一个在理论计算机科学中研究的逻辑系统。这种连接使人们可以使用依赖类型理论证明结果具有同义理论，同时也使用同型理论的定理来提出逻辑的新原理（例如Voevodsky的Univalence Axiom）。由于其适用于大规模计算机形式化（当前由包括英特尔和丰田在内的许多主要公司使用），因此先前研究了依赖类型的理论，因此我们可以使用同义理论来增强现有软件。第三个主题的目标，数学的形式化，检查结果工具，因为我们将使用它们正式化几个以前证明困难的结果。最后，在第四个主题（密码学）中，我们将研究同质理论对密码学的应用。具体而言，我们将尝试使用特定的代数不变式，即一种多种多样的共同体学环来构建密码有用的多线性图的示例。在过去的15年中，人们已经知道了许多密码多线性地图的应用程序，包括广播加密，互联网投票和不可忽视的混淆，但没有人能够构建此类地图的示例。 这里提出的许多问题适合不同级别的学生，并配备了可以在其进一步的学术工作和行业中使用的技能和经验。我们的许多特定目标涉及数学家和知识用户之间的合作，包括软件工程师以及广播公司。该提案完全将纯粹数学的核心技术赋予了核心，并在此领域之外调查了其应用。