Synthetic perspectives on spaces and categories
空间和类别的综合视角
https://arxiv.org/pdf/2510.15795
摘要
最近发现的领域特定形式系统——特别是同伦类型论（homotopy type theory）和单纯类型论（simplicial type theory）——在一种原生地保持等价不变性的框架下，为研究空间与范畴提供了新的视角。在本文中，我们阐述了这些并行框架中的基本证明技术：包括对路径（paths）或箭头（arrows）上的归纳原理的描述，以及涉及全类（universes）的构造，这些全类要么是泛等的（univalent），要么是定向泛等的（directed univalent）。
1 引言
在过去几十年中，人们发展了多种形式体系，用于以一种原生“导出”或等价不变的方式处理空间或范畴 [35, 67, 50, 29, 46, 37, 27, 44]。
1.1 关于空间
就拓扑空间而言，我们所指的等价概念是弱同伦等价（weak homotopy equivalence），即一个映射 f:X→Y在路径连通分支以及所有同伦群上诱导出同构。尊重这一等价概念的构造，就是作用于同伦型（homotopy types）——即在弱同伦等价意义下的空间——之上的构造。这些同伦型也被称为 ∞-广群（∞-groupoids，源于 Grothendieck [36]）或“anima”（源于 Česnavičius、Clausen 与 Scholze [25, §11.1], [19, §1.2]）。在本文中，我们使用更熟悉的术语“空间”来指代这些等价的概念，但需注意：我们的“空间”并没有一个良好定义的底层集合；相反，空间中的一个“点”指的是从一个可缩空间出发的映射的同伦类，即路径连通分支集合中的一个元素。
本文第一部分的目标是提供一种关于空间的前瞻性观点，以捕捉同伦类型论与泛等基础（univalent foundations）的洞见——这是21世纪初发现的一种“构造性内涵类型论与抽象同伦论的惊人融合”[60]。同伦类型论可被视为一种空间的综合理论（synthetic theory of spaces），其中空间是原始概念，通常称为“（同伦）类型”。我们将介绍受该形式框架启发的记号、构造与证明方法，并将其置于一个可在传统基础中描述的具体语境中。
1.2 关于范畴
在范畴概念的诸多有趣变体中，本文聚焦于 (∞,1)-范畴——最初由 Boardman 与 Vogt [11] 引入，后由 Joyal [37] 进一步发展，并被 Lurie [44] 称为“∞-范畴”——它们是普通范畴的类比，将定义中所有的集合替换为上述意义下的空间。这可以理解为对普通范畴概念的“充实”（enrichment）：在箭头空间中引入态射之间的态射、态射之间的态射之间的态射，如此无限递归，分别被视为路径、同伦以及高阶同伦。然而，由于我们对空间的所有构造都要求是等价不变的，这也必须被理解为对原始概念的“弱化”（weakening）。在普通严格 1-范畴中，核心结构由其合成函数给出，对任意三个对象 x,y,z，该函数定义为：
此处，它表现为箭头的等价不变空间之间的一个映射；因此，态射 g:Y→Z与 f:X→Y的复合仅在“可缩的选择空间”意义下良好定义，这是通常要求“复合唯一确定”这一条件的同伦类比。在本文中，我们使用术语“范畴”指代 ∞-范畴，并在少数出现的场合使用术语“(严格) 1-范畴”指代普通概念。
由于我们的“范畴”是由“空间”构建而成（如 §1.1 所述），在空间的综合框架内发展范畴理论颇具吸引力。这避免了传统“解析式”范畴定义所固有的著名复杂性 [4, 8]。对于同伦类型论的形式系统，我们添加了一条满足严格区间公理的公理化有向箭头。在 §5 中，我们简要概述了我们设定中用于综合范畴理论的结构，该结构在文献中被称为单纯类型论 [55]。再次强调，我们预期的语义环境比我们的语言所暗示的更为一般。我们所有的构造不仅对上述描述的 ∞-范畴有意义，而且对所谓的内 ∞-范畴（internal ∞-categories）——即在任意 ∞-拓扑斯中定义的 ∞-范畴 [47, 48]——或甚至更一般的设定 [51] 也有意义。
1.3 纲要
我们本可以轻易地用对综合空间与综合范畴的形式框架——即同伦类型论与单纯类型论——更精确的描述来填满本文。然而，我们的计划是突出一些基本构造，这些构造同样可以在传统基础中展开。在每个平行设定中，我们探索新的归纳原理：具体而言，在 §3 中探讨路径归纳法（path induction），在 §6 中探讨箭头归纳法（arrow induction）；以及分别在 §4 和 §7 中使用的“泛等”（univalent）和“定向泛等”（directed univalent）全类。在 §8 中，我们将通过强调同事们关于综合空间、综合范畴及更广义的综合数学的持续工作来结束全文。
综合数学框架还有一个未在此处体现但激励本工作的额外优势：它们易于计算机形式化，因为在综合领域中的形式证明往往与其纸笔对应物更为贴近。特别是，同伦类型论中的定理——例如 §4.3 中提到的泛等性应用——已被多次形式化；而 §5–6 中出现的关于综合范畴的结果已在实现单纯类型论的计算机证明助手 RZK 中被形式化 [41, 42, 1]，这是首次且迄今为止唯一一次对高阶范畴论结果的形式化。该证明助手在论文 [55] 撰写时尚未存在，因此形式化工作是在事后进行的，旨在修正原始论文中 §6 所指出的错误。
2 一个非常便利的空间范畴
归纳法，此时只需指定常值路径的逆，而我们将常值路径的逆取为常值路径本身：
路径归纳法的完整原理在命题 3.3 所述版本的基础上沿两个方向进行了扩展。第一个扩展利用了 Quillen 模型结构满足 Frobenius 条件这一事实 [32]：平凡上纤维化（trivial cofibrations）在沿纤维化（fibrations）的拉回下是稳定的。沿一个纤维化进行拉回的操作可被理解为引入一种平凡的依赖关系，这被称为“弱化”（weakening）。路径归纳法的一个更一般版本指出：给定一个定义在路径空间经弱化后的纤维化上，要定义其一个截面，只需在常值路径构成的子空间上定义一个截面即可。
4 泛等全类
在 §4.1 中，我们构造了其点编码数学命题证明的空间，细节可参见 [59, §4]。在 §4.2 中，我们引入 Voevodsky 的泛等公理，并概述 Shulman [61] 提出的构造泛等全类的现代方法。在 §4.3 中，我们介绍几个标准应用，这些应用在教科书 [66, 58, 9] 中有更详细的描述。
4.2 构造泛等全类
前面的构造是在任意空间 A和 B的语境下定义的。这些构造可以被视为在语境 U×U中进行的，其中我们使用一个小空间的全类（universe）U来定义该语境。我们接下来的任务就是定义这个空间 U。
我们所寻求的既是一个小空间构成的空间 U，也是一个泛等族（universal family）(A)A:U的小空间，使得广义元素 A:Γ→U能够在语境 Γ中定义一族小空间：
小空间的普遍家族被称为对象分类器，类似于可以在任何基本1-拓扑中找到的子对象分类器。
根据Voevodsky [39]，宇宙是解决同伦类型理论中固有的一致性问题的基本成分（特别是，在1-范畴中，替换操作是定义到等价的），其中像拉回（4.6）这样的构造仅定义到同构，或者更糟，在（∞-）范畴中，像（4.6）这样的构造仅定义到等价。因此，我们构建宇宙作为（∞-）空间的严格1-范畴呈现，如定理2.2所示，并要求分类器拉回到1-范畴而不是（∞-）范畴。
天真地看，1-范畴的普遍性质（A）A,U表明它代表小空间家族。但这并不完全正确，因为具有替换作用的小空间家族定义了一个1-群组值伪函子，而不是一个严格的集合值函子；参见[54, §4.1]进行讨论。Shulman引入了一个纤维化结构的公理化概念[61, §3]，特别是定义了一个F值的1-群组伪函子。例子包括Quillen模型范畴中的拉回稳定的态射家族，但也包括“纤维化”的概念由附加结构编码的示例，而不是映射的简单属性。在具有Cisinski模型结构的Grothendieck 1-拓扑中，如定理2.2所示，任何满足大小条件的纤维化结构F——是小群组值的——并且一个局部性条件——局部可表示——允许一个宇宙U，具有一个映射ξU → F，它在适当意义上是一个“满射等价”[61, 5.10]。通过Yoneda引理，这些数据编码了一个纤维化（在纤维化结构F的意义上）覆盖U，定义了所需的普遍家族v: Ũ → U空间。
唯一性公理将路径（A ~ B）A,B:U在宇宙中的另一个普遍家族方面进行表征。考虑家族空间（A ≃ B）A,B:U编码普遍等价，如定理4.5所定义。通过构造，一个广义元素
4.3 唯一性的应用
唯一性意味着对于空间的合成语言是本地“派生的”，所有构造都尊重空间之间的等价性。空间上的构造可以解释为在宇宙U上定义一系列空间（Ex）X,U。根据定理3.8，空间X和Y之间的路径p：X ~ Y定义了一个传输函数trp：Ex → Ey。通过路径诱导的另一种应用，这个传输函数是一个等价性，因为在沿着常数路径传输的情况下这是真的，由恒等函数给出。通过唯一性，等价性X ≃ Y可以转换为路径X ~ Y，从而产生等价性Ex ≃ Ey。
宇宙还可以用来定义其他分类空间。然后使用唯一性通过一系列定理（称为结构识别原理[26, 2]）来表征它们的路径空间。
例4.8 对于任何自然数n，定义Finₙ := ΣX:U ||n ≃ X||为n元素空间的空间，即与n点上的离散空间等价的空间的子宇宙。这里，“||||”表示命题截断，意味着不记录明确的等价性n ≃ X的数据。由此可知，从Finₙ到U的自然投影是一个同伦单态。空间Finₙ自然地被视为一个基于空间，n：Finₙ作为基点。
通过唯一性公理，Finₙ是一个1-类型，其中所有同伦群在维度1以上消失。Finₙ中的路径等价于Finₙ中对象之间的路径；特别是，由于所有X,Y：Finₙ都等价于n，因此彼此等价，空间Finₙ是0-连通的，即，具有单一路径分量。通过唯一性，Finₙ中的路径X ~ Y等价于等价性X ≃ Y。由此可知，基于循环空间Ω(Finₙ) = n ~ n等价于等价性空间n ≃ n，更好地称为n元素上的对称群Σₙ。
如定理4.8所述，空间Finₙ是一个带有点的、0-连通的、1-类型的，其循环空间是离散空间Σₙ。因此，我们有替代符号BΣₙ := Finₙ，这更便于推广。
例4.9 对于离散群G，有一个标准的“解析”构造其分类空间，作为严格1-范畴的神经的几何实现，其中有一个对象的内胚是群G的元素。由于这种构造涉及左伴随（2.1），因此以某种方式建立在空间的普遍性质上。使用合成空间的语言，我们可以将BG构造为由X：U中的那些X：U跨越的空间，这些0-类型X配备了自由和传递的G-作用。要在基空间Γ上定义一个G-扭子族，只需定义一个映射X：Γ → BG。
例4.10 扩展定理4.9中引入的群视角，我们可以将群的空间定义为带点的、0-连通的、1-类型的空间。或者，我们可以定义群的空间，遵循标准定义：“一个群是一个离散空间，具有二元乘法，满足公理”，如我们在H-空间的更简单情况下所说明的。
通过唯一性，H-空间中的路径是通过H-空间同态的H-空间等价性；这是上述结构识别原理的一个实例。同样，在群中，路径是群同构[58]。
刚才描述的两种群空间——“具体”群由其分类空间BG编码，而“抽象”群由通常的集合论定义捕捉——是等价的。关于从分类空间的角度发展群论，参见[9]。
分类空间方法的一个优点是，它允许许多群论构造扩展到高阶群。如果a：A是任意空间A中的一个点，我们可以通过概括定理4.8中使用的构造来形成空间BAut(a) := Σx:A ||a ~ x||。这同样是一个带有点的空间，基点为a：BAut(a)，并且可以恢复更高自同构群Aut(a)作为Ω(BAut(a)) := a ~ a。如果A是一个(n + 1)-类型，那么BAut(a)也是如此，并且基于循环空间Aut(a)是n-截断的。这构建了一个(n + 1)-群组的例子，其中1-群组的概念恢复了离散空间自同构群的标准例子。特别地，我们可以形成与A：U相关联的BAut(A)，并立即从其定义中得出一个映射X → BAut(A)是X上空间的家族，其纤维等价于空间A。
一般来说，我们将高阶群定义为一个带有点的连通空间BG，其中G := ΩBG是高阶群的载体空间，BG是分类空间。具有未截断分类空间的群是∞-群，而具有(n + 1)-截断分类空间的群是(n + 1)-群。高阶群在空间X上的一个作用就是从BG到X：U的一个映射，将BG的基点发送到X：U。
因此，一个作用在空间X上的BG提供了一个在BG上的(Xz)z:BG空间族。这个作用的不变量和协变量由空间X^hG := Πz:BG Xz和X_hG := X//G := Σz:BG Xz分别给出。更详细的内容参见[14]。
5 合成范畴的语言
在合成范畴的语言中——在[55]中引入，现在通常称为简单同伦类型理论或简单类型理论——我们扩展了合成空间的语言，增加了一个满足严格区间公理的公理化有向区间2。那就是2配备了不同的元素0,1：2和一个二元谓词(x ≤ y)x,y:2，它是自反的、反对称的、传递的和全的，最小值为0，最大值为1。我们将对象2视为“行走箭头”，起点为0，终点为1。遵循Joyal证明严格区间理论的分类1-拓扑是简单集合的1-范畴[45, §VIII.8]，我们构建了一个“行走可组合对的箭头”3——我们将其识别为由谓词(y ≤ x)x,y:2雕刻出的正方形2×2的子空间——或者更一般地，“行走可组合序列的n个箭头”n+1，对于每个n ≥ 0。该语言还可用于构建面包含δᵢ：n → n + 1和退化映射σⱼ：n + 1 → n，定义余下对象：
我们可以将这种单纯形结构视为自由添加到在§2中引入的非常方便的空间范畴中，因此我们的基本语义设置是——一个严格1-范畴，其对象我们称之为单纯形空间。这又是一个∞-拓扑，特别是一个局部笛卡尔闭范畴，对于所有§2-4中的构造都是适用的。在sSet^Δop中，行走箭头被解释为离散嵌入的代表Δ¹，以及图中(5.1)的其他对象。实际上，按照惯例，我们重用为刚刚构造的行走箭头——Δ⁰:=1, Δ¹:=2, Δ²:=3等——在(5.1)右侧所示的单纯形符号。更一般地，我们将使用单纯形符号，如Δᵢ² ⊂ Δ²，用于离散嵌入的单纯形空间，即在离散空间中取值的单纯形对象。
警告5.2. 注意，用于定义路径空间分解的对象(3.1)与这里使用的单纯形空间Δ¹:=2不同：该对象是在非离散空间中取值的常数单纯形对象。因为定义常数路径子空间包含的映射ref是一个等价性，我们可以在此处使用A作为路径空间族在A上的总空间的等价表示。
为了尽可能具体，我们在接下来的内容中将提到“单纯形空间”，但合成范畴理论的语言语义更为一般，可以在任何∞-拓扑的单纯形对象范畴中解释[55, 69]。
6 箭头归纳
箭头归纳将传统范畴论中的Yoneda引理加以推广，后者描述了可表函子的“映出”泛性质。为使用更熟悉的语言，此处我们提及“范畴”，但本节中关于范畴的所有结果实际上适用于更一般的预范畴（precategory）情形，即仅满足定义5.4的结构。
对于范畴族的Yoneda引理，已有多种表述形式：最初由Street [65]提出，随后被[56, 57]推广至高阶范畴的语境，并由[55, 15, 70]进一步适配到合成范畴（synthetic categories）的框架中。
在此，我们呈现的是最容易解释的变体，而非最一般的形式：即针对一族∞-广群（∞-groupoids），它们在基底∞-范畴中的箭头上以协变函子方式变化。其他变体则考虑一族∞-范畴，其依赖关系可能混合协变与逆变。
6.1 协变族的箭头归纳
固定一个范畴 C 和元素 c : C，协变可表函子由单纯空间族 (Hom(c, x))_{x:C} 编码。该族具有一个特殊性质，即“协变性”，这意味着基底单纯空间中任意箭头 f: Hom(x, y) 唯一地提升为总空间中指定源点的箭头。
7 有向单值宇宙
单纯类型论是一个用于陈述和证明关于范畴的定理的有效形式系统[7]。但[55]中的原始表述并未提供构建合成范畴实例的任何技术。正如我们在§4.3中所见，有趣的合成空间实例可以从空间的普适族构建。
空间的普适协变族。在本节中，我们将简述一个类似的单纯空间普适协变族的构造。作为Voevodsky单值性原理的一个有向类比的结果，该普适协变族的基底是一个范畴。根据引理6.3，其纤维是群胚（groupoids），即按我们当前术语称为“空间”，因此这定义了空间的范畴，可用于构造其他有趣的例子。
在§7.1中，我们采用[61]的方法来构造一个有向单值宇宙——更一般地，在任何∞-拓扑中构造单纯对象范畴的严格1-范畴表示——并预览与Cavallo和Sattler即将合作的工作[17]中的结果。还有多种其他方法可用于构造空间或范畴的有向单值宇宙[49, 44, 40, 22, 68, 24, 33]。在§7.2中，我们简要概述其应用；更多内容请参见[24, 23, 33]。
7.1 构造有向单值宇宙
如§4.2所述，我们的目标是定义一个单纯空间的普适协变族，使得Γ索引的广义元素在上下文Γ中定义小单纯空间的协变族。我们在一个类型论模型拓扑的严格1-范畴（其中§5引入的1-范畴是基本例子）中工作；我们继续将泛型（纤维化）对象称为单纯空间。在该设定下，我们的协变族更常被称为左纤维化（left fibrations），即满足如下性质的映射ρ: E → B：在交换方块(6.2)中诱导出的到严格1-范畴拉回的映射是一个平凡纤维化。我们表明，结构恰当的左纤维化定义了一种纤维化结构的概念，该结构取值于小群胚且局部可表，因而存在一个单值的普适映射，满足定义4.7的条件。协变宇宙S具有类似于(4.6)的分类性质，这意味着任何小协变族都有一个“拉直”过程，得到一个函子A: Γ → S，其拉回恢复了“未拉直”的小群胚协变族
参见[17]以获取更多细节和证明，证明通用协变族是有向单值的。我们还建立了有向单值性的一个“更高”版本，定义了 S 中 n 个可组合箭头的单纯形空间与 S 上协变族之间 n 个可组合函数的单纯形空间之间的等价性。我们还展示了通用协变族中的函子作用是由函数复合给出的。
7.2 有向单值性的运用
有向单值性的高级版本可以用来提供合成范畴的第一个例子。
推论7.2 通用协变族的基定义了一个范畴。
一个有用的单值性结果，如在§4.3中提到的，是结构恒等原理，它描述了从宇宙中构建的各种分类空间的路径空间。同样，有向单值性意味着一个有向类比，我们可能称之为结构同态原理，它将宇宙中构建的各种分类范畴中的箭头识别为适当结构的同态[68, 33]。例如，在带基点空间的范畴
s. 中，箭头可以被识别为带基点函数。例7.3 我们可以通过以下方式定义 S 中的magma的单纯形空间：
8 展望
为了总结我们强调的正在进行的相关工作，我们涉及相关的想法。
8.1 计算同伦类型理论
虽然同伦类型理论现在几乎有十年的历史，但这种形式系统的精确性质仍在发展中。进一步创新的一个动机是恢复意向依赖类型理论的一些元理论性质，该理论作为构造数学的基础，满足规范性和归一化。在这样的系统中，证明建立具有某种性质的整数 n 的存在性——例如著名的Brunier的证明，即——可以被编译出来以计算 n 的值[12, 43]。这激发了同伦类型理论中各种立方体变体的研究[16]，尽管关于这些系统的精确同伦理论语义仍存在一些未解决的问题[5, 18]。
一个相关的目标是将表征恒等类型的等价性——如结构恒等原理给出的——转换为定义性等价性。这样一个系统，称为高等观测类型理论，目前正在由Altenkirch、Kaposi和Shulman开发，扩展了先前的内部参数化联合工作[3]，并有一个伴随的实验性证明助手NARVA。
8.2 多模态单纯形类型理论
关于不是等价不变的空间的定理不能在同伦类型理论中正确陈述或证明，原因在§4.3中讨论。同样，涉及不是函子或自然不能在单纯形类型理论中正确陈述或证明的范畴的构造，由引理5.6和6.5。因此，需要进一步的公理或扩展这个形式系统，以重新开发合成设置中的完整分析理论。
朝着这个目标的工作正在由Cisinski、Cossen、Nguyen和Walde [23]以及Gratzer、Weinberger和Buchholtz [33, 34]进行。后者项目通过各种模态扩展了单纯形类型理论，例如，可能区分上下文是范畴的还是群组的，并在某些情况下限制变量的使用。
8.3 合成数学
在欧几里得传统的合成数学正在经历一场复兴，这与计算机证明助手的最新进展有关，这些助手可以帮助在一个形式框架中训练的数学家学会在另一个[62]中推理。一个新提出的合成方法由Blechschmidt和Cherubini、Coquand以及Hutzler在Zariski拓扑的内部公理中提供，以便直接访问同伦类型理论中的更高同伦类型，以推理上同调[10, 21]。有类似的新提出的合成方法，旨在为轻量级凝聚集或即将由Barton和Commelin以及Cherubini、Coquand、Geerligs和Moeneclaey [20]开发的轻量级凝聚动物的高拓扑提供内部语言。
原文链接：https://arxiv.org/pdf/2510.15795
热门跟贴