权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Homotopical Macrocosms for Higher Category Theory

高范畴理论的同伦宏观宇宙

基本信息

批准号：
2204304
负责人：
Emily Riehl
金额：
$ 39.97万
依托单位：
Johns Hopkins University
依托单位国家：
美国
项目类别：
Continuing Grant
财政年份：
2022
资助国家：
美国
起止时间：
2022-09-01 至 2025-08-31
项目状态：
未结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=2204304&HistoricalAwards=false
关键词：
Homotopical Macrocosms Higher Category Theory

项目摘要

Higher category theory is increasingly being used as the metatheory for new results in several areas of mathematics, creating a huge barrier to entry for mathematicians whose primary technical expertise lies in another field. Past joint work of the PI reimagined the foundations of infinite-dimensional category theory with the aim of simplifying proofs by replacing "analytic" methods, that rely on the combinatorics of a particular model of infinite-dimensional categories, with "synthetic" ones that apply in any model. One part of this project seeks to develop a computer-verifiable formal language that expresses only statements about infinite-dimensional categories that are invariant under change of model. Such a language would force users to "speak no evil" by guaranteeing that every statement they express is model-independent. This project connects to the plans to recast the theory of infinite-dimensional categories in a new proposed univalent foundation system for mathematics, in which homotopical uniqueness up to a contractible space of choices becomes genuine uniqueness, permitting streamlined definitions of fundamental concepts. Both of these projects will be undertaken in part with mentees of the PI at Johns Hopkins. In parallel, the PI has concrete plans to continue her expository and outreach work which include a new book (Elements of Infinity-Category Theory, joint with Verity), lectures directed at the general public, survey articles prepared for a variety of audiences, and efforts to improve access to advanced mathematics, such as her service on the Equity, Diversity, and Inclusion Advisory Board at the Banff International Research Station.The pioneers of homotopy type theory - the new proposed univalent foundation system - envisioned a computer-verifiable foundation for infinite-dimensional category theory, but some computational content is lost through the classical reasoning used in classical homotopy theory. With collaborators, the PI will develop a new model for classical homotopy theory in a particular category of cubical sets, in which cubical fibrations are required to be equivariant, respecting the symmetries of cubes defined by permuting their dimensions. A longer-term aim is to use similar methods to obtain cubical set based presentations of all infinity-topoi. A computer proof assistant based on equivariant cubical fibrations would have the correct classical semantics but would be able to restore the computational content to univalent mathematics. A final project explores homotopical macrocosms for higher category theory, aiming to prove that the collection of cartesian fibrations between (infinity,n)-categories assemble into a cartesian fibration of (infinity,n+1)-categories, which can be regarded as some sort of categorified hyperdoctrine for (infinity,n)-category theory. Results of this nature would establish a global lifting property against homotopy coherent diagrams that should aid further developments in (infinity,n)-category theory.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

高等范畴论越来越多地被用作若干数学领域新结果的元理论，这给那些主要技术专长在另一个领域的数学家创造了巨大的进入障碍。PI过去的合作工作重新构想了无限维范畴论的基础，目的是通过用适用于任何模型的“综合”方法取代依赖于无限维类别的特定模型的组合学的“解析”方法来简化证明。这个项目的一部分寻求开发一种计算机可验证的形式语言，这种语言只表达关于无限维类别的陈述，这些类别在模型变化下是不变的。这样的语言将通过保证用户表达的每个语句都是独立于模型的，从而迫使用户“不说坏话”。这个项目连接到在一个新的数学一元基础系统中重塑无限维范畴理论的计划，在这个系统中，同调唯一性直到选择的可收缩空间成为真正的唯一性，允许基本概念的流线型定义。这两个项目都将由约翰霍普金斯大学PI的学员参与。与此同时，PI有具体的计划继续她的解释性和外联性工作，包括一本新书（与Verity联合出版的《无限范畴理论的要素》），针对公众的讲座，为各种受众准备的调查文章，以及努力改善高等数学的获取，例如她在班夫国际研究站的公平、多样性和包容性咨询委员会的服务。同伦类型论的先驱者——新提出的一元基础体系——设想了无限维范畴论的计算机可验证基础，但经典同伦理论中使用的经典推理丢失了一些计算内容。与合作者一起，PI将开发一个新的经典同伦理论模型，该模型适用于特定类别的立方体集，其中立方体振动要求是等变的，尊重通过排列其维度定义的立方体的对称性。一个长期的目标是使用类似的方法来获得所有无穷拓扑的基于立方集的表示。基于等变立方振动的计算机证明助手将具有正确的经典语义，但能够将计算内容恢复为一元数学。最后一个项目探讨了高范畴论的同局部宏观，旨在证明（无穷，n）-范畴之间的笛卡尔纤曲集合可以组合成（无穷，n+1）-范畴的笛卡尔纤曲，这可以被视为（无穷，n）-范畴论的某种分类超论。这种性质的结果将建立对同伦相干图的整体提升性质，这将有助于（无穷，n）范畴理论的进一步发展。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。