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.

同伦论是纯数学的一个分支，它使用代数不变量(如维度)来区分两个几何对象。近年来，来自同伦理论的工具已经被应用于其他领域，包括数学内部(例如，代数)和外部，例如，数学物理和理论计算机科学。这份探索奖助金提案探索了几个这样的应用，并帮助发展了一般理论。简而言之，本研究分为四个主题。*第一个主题是高等范畴理论，旨在建立一个可以谈论同伦理论的一般框架，从而使该理论适用于其他领域。在这个建议中，我们探索了以面向计算和新应用的方式重塑这个框架的可能性，例如在纽结理论和几何表示理论中。第二个主题，同伦类型理论，研究了同伦理论和类型理论之间新发现的联系，类型理论是理论计算机科学中研究的一个逻辑系统。这种联系允许人们使用从属类型理论来证明同伦理论中的结果，同时也可以使用同伦理论中的定理来提出新的逻辑原理(例如沃沃茨基的单叶公理)。以前研究依赖类型理论是因为它们适合大规模计算机形式化(目前许多大公司都在使用，包括英特尔和丰田)，因此我们可以使用同伦理论来增强现有的软件。第三个主题--数学的形式化--的目标是审查所产生的工具，因为我们将使用它们来正式化以前被证明是困难的几个结果。最后，在第四个主题密码学中，我们将研究同伦理论在密码学中的应用。具体地说，我们将尝试使用一种特殊的代数不变量，即簇的上同调环，来构造密码上有用的多线性映射的例子。密码多线性地图的许多应用，包括广播加密、互联网投票和不可分辨混淆，在过去的15年里已经为人所知，但还没有人能够构建这样的地图的例子。这里提出的许多问题适用于不同水平的学生，并使他们获得可以在进一步的学术工作和工业中使用的技能和经验。我们的许多具体目标涉及数学家和知识用户之间的合作，包括软件工程师和广播公司。总之，该提案采用了纯数学的核心技术，并研究了它们在这一领域之外的应用。