💻 computer science

Delooping presented groups in homotopy type theory

本文在齐次类型论中利用生成集提出了呈现群的去循环的简化且计算高效的构造，并引入了用于分析所得高阶归纳类型的 2-多面体类型论框架，其中关键进展已在 Cubical Agda 中形式化。

原作者： Camil Champin, Samuel Mimram, Emile Oleon

发布于 2026-05-01

📖 1 分钟阅读☕ 轻松阅读

原作者： Camil Champin, Samuel Mimram, Emile Oleon

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你试图描述一个复杂的形状，比如一个甜甜圈或一个扭曲的结，但你只有一套用乐高积木搭建它的指令。在数学领域，特别是称为同伦类型理论的分支中，数学家将形状（称为“类型”）和构建它们的规则（称为“证明”）视为同一事物。

本文探讨一个具体挑战：如何构建一个能完美代表特定规则集合（即一个“群”）的“映射”（一个数学空间）？

在该理论中，“群”不仅仅是一串数字；它是一套移动指令。为了理解这些指令，数学家喜欢构建一个“类空间”。将类空间想象成一个游乐场，其中群的规则是唯一重要的事物。如果你站在游乐场中心并走一圈，你所走的路径就代表群中的一个元素。

以下是用简单类比对本文主要思想的分解：

1. 问题：游乐场太大了

通常，要为一个群构建这个游乐场，你有两种主要方法，但两者都像是在只需要一个小花园棚屋时却试图建造一座摩天大楼。

方法 A（主齐性空间）： 想象你拥有一个巨大的图书馆，里面收录了群作用于事物的每一种可能方式。你必须在那座图书馆中找到代表你那个群的特定“房间”。这很准确，但图书馆规模庞大且难以导航。
方法 B（高阶归纳类型）： 想象通过为群中的每一个可能动作添加一条新路径来建造游乐场。如果你的群有 1,000 个动作，你就必须画出 1,000 条路径。如果群是无限的，你就得永远画下去。这非常精确，但对于计算或证明相关事物来说却是一场噩梦。

2. 解决方案：使用“生成元”捷径

作者发现，如果你知道群的生成元（即能生成所有其他动作的少数基本动作），你就可以构建一个更小、更简单的游乐场。

类比： 想象你想描述如何在城市中行走。与其列出每一个街角（数量巨大），你只需列出主要路口（生成元）以及在这些路口转弯的规则。
结果：
- 更简单的主齐性空间： 与其查看整个图书馆，他们表明你只需查看“生成元的作用”。这就像只检查主要路口，而不是每一条街道。
- 更简单的游乐场： 与其为群中的每一个动作画一条路径，你只需为生成元画路径，然后添加“围栏”（关系），告诉你何时两条不同的路径实际上是相同的。
- 为何重要： 这使得游乐场小得多。计算机更容易进行计算，人类也更容易证明相关事物，因为需要检查的情况更少。

3. 工具：2-多图（蓝图）

为了管理这些更小的游乐场，作者引入了一种称为2-多图的工具。

类比： 将 2-多图想象成一张蓝图或食谱卡。
- 它列出了点（空间中的点）。
- 它列出了线（生成元动作）。
- 它列出了方块（说明“如果你走这条路，就等同于走那条路”的规则）。
蒂茨变换： 本文表明，你可以更改蓝图（添加一条新线或一条新规则），而无需改变游乐场的实际形状。这就像重写食谱以使用不同的食材，但最终做出完全相同的蛋糕。这使得数学家能够简化蓝图，直到它易于操作。

4. 凯莱图与复形：“差异”映射

最后，本文探讨了当你比较“自由群”游乐场（你可以在其中随意移动，没有规则）与“真实群”游乐场（规则适用）时会发生什么。

类比： 想象自由群是一片广阔的空旷场地。真实群则是同一块场地，但设有围栏和隧道，迫使你遵循特定路径。
凯莱图： 这是一张地图，精确显示“围栏”的位置。它突出了自由场地与真实群之间的差异。
凯莱复形： 这更进一步。它不仅显示围栏在哪里，还显示围栏中的“孔洞”。它可视化了规则如何相互作用。作者表明，该复形是群的“万有覆盖”，意味着它是群结构最详细、未折叠的版本。

总结

本文本质上是一份指南，教导当你已知基本构建块（生成元）时，如何构建一个更小、更高效的数学群模型。

不要建造整座城市； 只需建造主要路口和转弯规则。
使用蓝图（2-多图） 来组织这些规则并简化它们。
绘制“自由”版本与“真实”版本之间的差异，以理解群的隐藏结构（凯莱图）。

作者还将这些思想全部翻译成了一种计算机语言（Agda），证明了这些简化模型能正确运行，并可被计算机用于数学运算。

以下是 Champin、Mimram 和 Oleon 的论文《同伦类型论中呈现群的去循环》（Delooping Presented Groups in Homotopy Type Theory）的详细技术总结。

1. 问题陈述

在同伦类型论（HoTT）中，群可以通过两种方式表示：

外部方式：作为配备了满足公理的乘法、单位元和逆运算的集合。
内部方式：作为带基点的连通群胚 $A$ 的环路空间（ $\Omega A$ ）。类型 $A$ 被称为该群的去循环（delooping，记为 $BG$）。

虽然已知任何群都存在去循环，但对于任意群 $G$ 的标准构造往往会导致复杂的类型，难以进行计算或归纳推理。具体而言：

主丛构造（使用 $G$ -集合）需要考察整个群的作用，导致类型庞大。
高阶归纳类型（HIT）构造（Eilenberg-MacLane 空间）通常需要对 $G$ 的每个元素定义一个环路，并对每对元素定义一条路径（乘法表），从而导致构造器的数量巨大。

作者旨在为呈现群（即由生成元和关系定义的群）开发更简单、计算效率更高的去循环构造。他们力求将所得类型的规模缩减至与呈现的组合复杂度相匹配，而非与完整的群结构相匹配。

2. 方法论

本文利用了 HoTT 的合成几何学，采用以下工具：

高阶归纳类型（HITs）：用于定义包含点、路径和高阶路径的空间。
截断（Truncation）：用于强制群胚性质（截断高阶同伦群）。
多图（Polygraphs）：一种适应于 HoTT 的重写论结构，用于系统地管理生成元和关系。
格罗滕迪克对偶与扁平化引理（Grothendieck Duality and Flattening Lemma）：用于关联纤维序列和全空间，从而能够计算核和连通分量。
形式化：所有结果均在 cubical Agda 证明助手中进行形式化。

3. 主要贡献与结果

A. 通过生成主丛实现的简化去循环（第 3 和 4 节）

作者改进了经典的主丛构造。他们不再使用所有 $G$ -集合（即具有整个群 $G$ 作用的集合）的类型，而是引入了 $X$ -集合（即具有生成集 $X$ 作用的集合）。

定理 15：如果群 $G$ 由集合 $X$ 生成，则主 $X$ -集合（源自主 $G$ -主丛）的连通分量是 $G$ 的一个去循环。
意义：该构造仅需生成元的作用，而非整个群的作用。
- 示例：对于循环群 $\mathbb{Z}$ ，标准的去循环是圆 $S^1$ 。作者表明，在自同态类型（ $\Sigma (A:U). (A \to A)$ ）中，后继函数（successor function）的连通分量是 $\mathbb{Z}$ 的一个去循环。这在某些上下文（如 UniMath）中避免了对 HIT 的需求，并简化了推理。

B. 通过高阶归纳类型实现的简化去循环（第 5 节）

作者为呈现群 $G = \langle X \mid R \rangle$ 提出了一种新的 HIT 构造。

**构造（$BP $）**：与每个群元素对应一个环路不同，类型$ $） * * ：与每个群元素对应一个环路不同，类型$ BP$ 包含：
- 一个点 $\star$ 。
- 每个生成元 $x \in X$ 对应一个环路 gen。
- 每个关系 $r \in R$ 对应一个 2-路径 rel。
- 一个群胚截断。
定理 24：$BP $是呈现群$ [P]$ 的一个去循环。
优势：与标准的 $K(G, 1)$ （需要为所有 $|G|$ 个元素定义环路）相比，这极大地减少了构造器的数量。它将类型论定义与标准的组合群论对齐，促进了归纳证明，使其能够镜像传统的群论论证（例如 Tietze 变换）。

C. 2-多图与内部推理（第 6 节）

为了形式化对这些 HIT 的操作，作者在 HoTT 中引入了 2-多图。

定义：一种由 0-胞（点）、1-胞（生成元）和 2-胞（关系）组成的结构。
呈现类型：他们将由 2-多图生成的类型定义为特定的 HIT。
Tietze 变换：他们定义了操作（T0, T1, T2），用于修改多图（添加/删除生成元或关系），同时保持所呈现的类型不变。
定理 29：Tietze 等价的 2-多图呈现相同的类型。
意义：这使得在 HoTT 内部能够操作群呈现，从而能够将呈现转换为计算上方便的形式（例如通过 Knuth-Bendix 完备化得到的收敛呈现），而无需改变底层的同伦类型。

D. 凯莱图与复形（第 7 节）

作者提供了凯莱图和复形的新型同伦解释。

凯莱图作为核：他们证明（定理 35），凯莱图 $C(X, G)$ $C (X, G)$ 是由呈现诱导的映射 $B\gamma^*: BX^* \to BG$ $B γ^{*} : B X^{*} \to B G$ 的核。
- $BX^*$ 是生成元上自由群的去循环。
- 纤维序列 $C(X, G) \to BX^* \to BG$ 编码了群的关系。
凯莱复形：他们将此扩展到 2 维，定义 凯莱复形 $CP $为映射$ B_2P \to BG $的核（其中$ B_2P$ 是去循环的 2-骨架）。
定理 40 和 43：凯莱复形是类型 $B_2P$ 的万有覆盖。
意义：这建立了经典群论几何对象（凯莱图/复形）与去循环的同伦结构之间的直接联系，衡量了自由群与呈现群之间的“缺陷”。

4. 意义与影响

计算效率：所提出的构造生成了具有显著更少构造器的类型，使其更易于在 Agda 等证明助手中进行计算和自动推理。
连接代数与拓扑：本文成功地将经典群论概念（生成元、关系、Tietze 变换、凯莱图）转化为 HoTT 的合成语言，允许进行类似于传统代数证明的“内部”证明。
元理论推理：通过使用 2-多图，作者提供了一个框架来推理 HIT 本身的结构，实现了保持同伦类型的变换。
未来工作的基础：本文为定义高维多图（ $n$ -多图）和高阶凯莱复形奠定了基础，这可能带来 HoTT 中群的自动一致性证明和高效的上同调计算。

总之，这项工作提供了一套工具，用于在同伦类型论中构建群去循环的“小”且“组合”模型，利用群呈现的特定结构来简化类型的定义及其推理过程。