Homotopy Theory and its Applications

同伦理论及其应用

• 批准号: RGPIN-2018-04595
• 负责人: Kapulkin, Krzysztof
• 金额: $ 1.68万
• 依托单位: University of Western Ontario
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2018
• 资助国家: 加拿大
• 起止时间: 2018-01-01 至 2019-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=655076
• 关键词: 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年里已经被人们所知，但没有人能够构建这样一个映射的例子。这里提出的许多问题适合不同层次的学生，并为他们提供可以在进一步的学术工作和工业中使用的技能和经验。我们的许多具体目标涉及数学家和知识用户之间的合作，包括软件工程师和广播公司。总的来说，该提案采用了纯数学的核心技术，并研究了它们在这一领域之外的应用。