[infinite]-Lie Groups and Their [infinite]-Lie Algebras in Real Cohesive Homotopy Type Theory

实内聚同伦型理论中的[无穷]-李群及其[无穷]-李代数

• 批准号: 2888102
• 金额: --
• 依托单位: University of Nottingham
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2023
• 资助国家: 英国
• 起止时间: 2023 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2888102
• 关键词: infinite; Lie; Groups; Their; Algebras

Type theory has long been a cornerstone of theoretical computer science, providing the formal methods for programming language theory [10]. More recently, the development of homotopy type theory (HoTT) [9] has served as a bridge between pure mathematics and computer science, relating algebraic topology to computation. HoTT has been shown as the internal logic of all ([infinite], 1)-topoi [8], a large class of higher categories. Adding extra structure to this type theory, in particular in the form of modalities, gives a more specified mathematical setting to work in. Mike Shulman introduced cohesive HoTT to internalise the ideas of axiomatic cohesion, from Lawvere [3] and Schreiber [7], into type theory. These new structures allow us to access the "geometric" structure of a homotopy type, giving access to questions in differential topology and geometry. This effort is part of a larger project to translate the categorical foundations of modern physics presented by Schreiber [7], into the language of HoTT. In particular, supergravity, string theory and M-theory can be formulated in this way. This project will continue this effort, by focusing on the differential study of higher groups in cohesive HoTT, with an aim to simplify the existing presentation of higher Lie theory.

类型理论长期以来一直是理论计算机科学的基石，为编程语言理论提供了形式化方法[10]。最近，同伦类型理论（HoTT）[9] 的发展成为纯数学和计算机科学之间的桥梁，将代数拓扑与计算联系起来。 HoTT已被证明是所有([无穷],1)-topoi[8]这一一大类更高类别的内部逻辑。向这种类型的理论添加额外的结构，特别是以模态的形式，提供了更具体的数学设置。Mike Shulman 引入了内聚 HoTT 来内化公理内聚的思想，来自 Lawvere [3] 和 Schreiber [7]，进入类型理论。这些新结构使我们能够访问同伦类型的“几何”结构，从而解决微分拓扑和几何中的问题。这项工作是一个更大项目的一部分，该项目旨在将 Schreiber [7] 提出的现代物理学的分类基础翻译成 HoTT 语言。特别是，超引力、弦理论和M理论都可以用这种方式表述。该项目将继续这一努力，重点关注内聚 HoTT 中高级群的差异研究，旨在简化高级李理论的现有表述。