Homotopy Theory and its Applications

同伦理论及其应用

• 批准号: RGPIN-2018-04595
• 负责人: Kapulkin, Krzysztof
• 金额: $ 1.68万
• 依托单位: University of Western Ontario
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2019
• 资助国家: 加拿大
• 起止时间: 2019-01-01 至 2020-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=679273
• 关键词: 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的一价公理）。依赖类型理论以前被研究过，因为它们适合大规模的计算机形式化（并且目前被许多大公司使用，包括英特尔和丰田），因此我们可以使用同伦理论来增强现有的软件。第三个主题“数学的形式化”的目标是研究由此产生的工具，因为我们将使用它们来形式化先前被证明是困难的几个结果。最后，在第四个主题“密码学”中，我们将研究同伦理论在密码学中的应用。具体地说，我们将尝试使用一个特殊的代数不变量，一个变量的上同环，来构造密码学上有用的多线性映射的例子。加密多线性地图的许多应用，包括广播加密、互联网投票和不可区分混淆，在过去的15年里已经为人所知，但没有人能够构建这样一个地图的例子。******这里提出的许多问题适合不同水平的学生，并为他们提供技能和经验，可以在他们进一步的学术工作和工业中使用。我们的许多具体目标涉及数学家和知识用户之间的合作，包括软件工程师，例如广播公司。总的来说，该提案以纯数学为中心，并研究了它们在纯数学领域之外的应用。