🔢 mathematics

Unbiasing symmetric monoidal categories in Lean

本文在 Lean 4 的 Mathlib 框架下，通过将对称幺半范畴扩展为有限集跨度 (2,1)-范畴的 Cat 值伪函子，并借助 Mac Lane 相干定理及 Kleisli 双范畴编码，形式化了对称幺半范畴的无偏化过程。

原作者： Robin Carlier

发布于 2026-03-03

📖 1 分钟阅读🧠 深度阅读

原作者： Robin Carlier

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

这篇论文讲述了一个关于**“如何让数学规则变得更灵活、更通用”**的故事，而且这个故事是在计算机程序（Lean 4）中完成的。

为了让你轻松理解，我们可以把这篇论文的核心内容想象成**“从‘双人舞’到‘大型团体操’的升级过程”**。

1. 背景：为什么我们需要“去偏见”（Unbiasing）？

想象一下，你正在教一个机器人做加法。

传统的做法（有偏见）： 你告诉机器人：“加法是两个人的事。先把 A 和 B 加在一起，得到结果，再把这个结果和 C 加在一起。”
- 这就好比 (A + B) + C。
- 如果你要加 D，你得先算 (A + B) + C，然后再 + D。
- 这种规则很死板，它强制规定了“谁先和谁结合”。虽然数学上我们知道 (A+B)+C 和 A+(B+C) 结果一样，但在计算机代码里，这种“结合顺序”是必须写死的。
现实的需求（无偏见）： 在现实生活中，比如计算一个班级所有学生的总分，或者计算一个群论公式，我们面对的是任意数量的数字（A, B, C, D... E, F...）。我们不需要规定“先加前两个，再加第三个”，我们想要一个能直接处理“这一堆”东西的通用规则。

这篇论文要做的，就是帮 Lean 4 这个数学证明助手，把“只能处理两个数相加”的死板规则，升级成“能处理任意多个数相加”的灵活规则。在数学界，这叫做对称幺半范畴（Symmetric Monoidal Categories）的“去偏见化”。

2. 核心挑战：混乱的舞步

在数学里，当你把两个东西“乘”在一起（比如张量积 $\otimes$ ），你不仅要考虑顺序，还要考虑它们交换位置时的规则（对称性）。

如果是两个东西：A ⊗ B 变成 B ⊗ A，这很简单。
如果是三个东西：(A ⊗ B) ⊗ C 变成 C ⊗ (B ⊗ A)，这就麻烦了。中间涉及很多“括号移动”和“交换位置”的步骤。

麦克莱恩（Mac Lane）的“相干性定理”就像是一个“万能翻译官”。它告诉我们：不管你怎么括号、怎么交换，只要起点和终点一样，中间所有的舞步（变换路径）最终都是等价的，只有一种“标准舞步”是唯一的。

这篇论文的难点在于： 以前 Lean 4 里的数学库（Mathlib）只记录了“双人舞”的规则。现在作者 Robin Carlier 要证明：我们可以利用“万能翻译官”，把“双人舞”的规则自动扩展成“百人团体操”的规则，并且保证在计算机里这个扩展是严格正确的。

3. 作者的解决方案：三个关键步骤

作者没有直接去硬算复杂的公式，而是用了三个巧妙的比喻和工具：

第一步：把“列表”变成“对称列表”（Symmetric Lists）

想象你有一堆积木。

普通列表： [红，蓝，绿]。顺序很重要，红在蓝前面就是红在蓝前面。
对称列表： 这是一堆积木，但顺序不重要，重要的是谁和谁在一起。如果你把“红”和“蓝”交换，它还是同一个“对称列表”。

作者首先证明了：在计算机里，我们可以用一种特殊的“对称列表”来完美地模拟“任意多个东西的乘积”。这就像是用乐高积木搭建了一个通用的模具，不管你要拼几个，都能放进去。

第二步：利用“柯西群”和“排列”做标签

这是论文中最硬核的数学部分，但我们可以这样理解：
作者给每一个“交换积木”的动作（比如把红和蓝交换）贴上了一个标签。

这些标签就像乐谱上的音符。
作者证明了：不管你怎么交换积木，只要最后积木的排列顺序变了，这个“乐谱”（标签）就能唯一地告诉你发生了什么。
这就像是在说：“只要我知道你最后把积木排成了什么样，我就能反推出你中间做了哪些交换动作，而且这个反推是唯一的。”
这解决了“怎么证明所有路径都等价”的问题。

第三步：把“跨度”（Spans）变成“矩阵”

这是最精彩的部分。

跨度（Span）： 想象你有两个集合，中间有一群“中间人”把它们连起来。这就像是一个桥梁。
作者发现： 如果我们把这些“桥梁”看作矩阵（就像 Excel 表格），那么：
- 把两个集合连起来，就像矩阵乘法。
- 把东西从一边传到另一边，就像矩阵里的数字在流动。
- 作者构建了一个**“万能转换器”**（伪函子），它能自动把“桥梁”的规则翻译成“积木”的规则。

比喻：
想象你在玩一个游戏，规则是“通过桥梁传递货物”。
以前，你只能一次传递两个箱子。
现在，作者发明了一个**“自动打包机”**（去偏见化过程）：

它把“桥梁”看作矩阵。
它把“货物”看作积木列表。
它利用“对称列表”的数学性质，自动计算出：如果我要把 100 个箱子从 A 运到 B，该怎么打包、怎么交换顺序。
最重要的是，它证明了这个打包过程是完美无缺的，不会漏掉任何细节，也不会产生矛盾。

4. 为什么这很重要？（对普通人的意义）

让数学软件更聪明： 以前，如果你想在 Lean 4 里写一个涉及“任意数量元素求和”或“任意数量张量积”的复杂公式，程序员得手动写很多繁琐的代码来规定顺序。现在，有了这个“去偏见化”工具，软件可以自动处理任意数量的元素，就像人类直觉一样自然。
连接“普通数学”和“高维数学”： 现代数学（特别是物理和计算机科学中的拓扑量子场论）经常需要处理“无限维”或“高维”的结构。这篇论文搭建了一座桥梁，把我们在二维平面上熟悉的“普通数学规则”，无缝升级到了高维空间。
为未来铺路： 作者提到，这是为了将来在计算机里形式化更高级的数学（比如 $\infty$ -范畴）做准备。就像为了造摩天大楼，必须先打好地基。这篇论文就是那个坚实的地基。

总结

Robin Carlier 的这篇论文，就像是一位**“数学翻译官”。
他手里拿着一本只有“双人舞”规则的旧字典（传统的对称幺半范畴定义）。
他利用“对称列表”（一种特殊的积木）和“矩阵乘法”（一种通用的计算逻辑），编写了一本“万能舞谱”**。
这本新字典告诉计算机：不要只盯着两个人怎么跳，要能指挥成千上万个人跳团体操，而且保证无论怎么跳，只要起点终点一样，中间的舞步就是和谐统一的。

这不仅让 Lean 4 这个数学证明助手变得更强大，也为未来人类探索更复杂的数学宇宙铺平了道路。

这是一份关于 Robin Carlier 论文《Unbiasing symmetric monoidal categories in Lean》（在 Lean 中消除对称幺半范畴的偏倚）的详细技术总结。

1. 研究背景与问题 (Problem)

核心问题：
在形式化数学库（如 Lean 的 Mathlib）中，对称幺半范畴（Symmetric Monoidal Categories, SMC）的传统定义是“有偏倚的”（biased）。

有偏倚定义： 仅包含二元张量积（ $\otimes: C \times C \to C$ ）、单位对象以及满足特定公理（如五边形公理、三角形公理、六边形公理）的自然同构（结合子、单位子、辫子）。
局限性： 这种定义在处理高阶 arity（即任意有限多个对象的张量积）时非常困难。例如，定义一个在任意有限集上求和的算子，或者定义自由交换幺半对象（Free Commutative Monoid Objects），需要证明结果不依赖于元素的枚举顺序或结合方式。
形式化挑战： 在依赖类型理论（如 Lean）中，对象相等性（propositional equality）的处理极其繁琐（即"DTT Hell"）。直接通过归纳法定义任意 arity 的张量积会导致大量的类型转换（casting）和复杂的证明义务。

目标：
实现“无偏倚”（Unbiasing）过程，即将一个标准的对称幺半范畴扩展为一个从有限集（或有限集的 Span 范畴）到范畴范畴（Cat）的伪函子（Pseudofunctor）。这使得可以直接处理任意有限多个对象的张量积及其相干性，而无需手动处理结合律和交换律的繁琐证明。

2. 方法论 (Methodology)

作者采用了一种基于**Mac Lane 相干性定理（Coherence Theorem）**的形式化策略，将对称幺半范畴的数据编码为从特定源范畴出发的伪函子。

2.1 核心工具：对称列表（Symmetric Lists）

定义： 作者将自由对称幺半范畴建模为“对称列表”范畴 $SList(J)$。
- 对象： $J$ 中元素的列表。
- 态射： 由交换生成元（swap）生成的，满足对称群关系的态射。
形式化难点： 在 HoTT（同伦类型论）中，这可以通过高归纳类型（HIT）直接定义。但在 Lean/Mathlib 的非 HoTT 环境中，作者必须手动构建由生成元和关系定义的范畴（Quiver -> Path Category -> Quotient Category）。
关键创新： 利用Coxeter 群（特别是 $A_n$ $A_{n}$ 型）来标记对称列表中的态射。
- 证明了 $SList(J)$ 中的态射与排列群（Permutation Groups）之间存在双射。
- 具体地，态射可以被唯一地标记为 $A_\infty$ 群（无限 Coxeter 群）中的元素，从而将范畴论问题转化为群论问题。

2.2 相干性定理的形式化 (The Coherence Theorem)

定理 1.3： 集合 $J$ 上的自由对称幺半范畴等价于 $J$ 上有限集与双射的范畴 $Core(Fin/J)$（赋予余积对称幺半结构）。
实现路径：
1. 形式化 Coxeter 群与排列群的关系。
2. 证明对称列表中的态射与排列一一对应（通过权重函数 $w$ ）。
3. 证明 $SList(J)$ 与自由对称幺半范畴等价。
4. 利用这一等价性，将任意对称幺半范畴中的计算转化为在“对称列表”上的通用计算。

2.3 伪函子与 Span 范畴

源范畴： 使用有限集的 Span 范畴（$Span(Fin)$）的“核心”（Pith，即只保留可逆 2-态射的部分）。
目标： 构造一个伪函子 $C^\otimes: Pith(Span(Fin)) \to Cat$ $C^{\otimes} : P i t h (S p an (F in)) \to C a t$ 。
- 将有限集 $J$ 映射到 $C^J$ （ $J$ 索引的 $C$ 中对象的乘积范畴）。
- 将 Span $A \xleftarrow{f} B \xrightarrow{g} K$ 映射到函子 $g_! f^*$ （其中 $f^*$ 是拉回， $g_!$ 是沿纤维的张量积）。
Pith-Beck-Chevalley 系统： 为了构造上述伪函子，作者定义了一种结构（Definition 3.2），包含两个伪函子（协变和反变）以及满足 Beck-Chevalley 条件的基变换同构。这利用了 Span 范畴中拉回方图的性质。

2.4 Kleisli 双范畴与通用公式

引入 Kleisli 双范畴 $K_{SList}$ 来编码对称幺半范畴的“通用公式”。
利用 Kleisli 双范畴的逆，将对称幺半范畴 $C$ 编码为 $K_{SList}^{op} \to Cat$ 的伪函子。
通过**对偶性（Duality）和多重集（Multisets）**的计算，证明了从 Span 范畴到 Kleisli 双范畴的映射是良定义的，且所有相干性条件（结合子、单位子等）在“线性”（无重复元素）情况下是唯一的，从而简化了证明。

3. 主要贡献 (Key Contributions)

首个形式化证明： 这是首次在 Lean/Mathlib 中完全形式化对称幺半范畴的“无偏倚”过程（Theorem 1.1）。
对称列表的完整形式化：
- 将 Piceghello 在 HoTT 中的工作移植到 Lean 的非 HoTT 框架。
- 建立了对称列表态射与 Coxeter 群元素及排列群之间的精确对应（Theorem 2.8, Corollary 2.9）。
- 解决了在非 HoTT 环境中处理生成元与关系定义范畴的复杂性。
Pith-Beck-Chevalley 系统的形式化：
- 定义并形式化了从 Span 范畴核心出发的伪函子构造所需的代数结构（Definition 3.3）。
- 证明了该结构足以生成所需的无偏倚伪函子。
Kleisli 双范畴的应用：
- 利用相对伪单子（Relative Pseudomonad）的 Kleisli 双范畴来分离“通用公式”与“具体实例化”。
- 证明了在对称幺半范畴中，高阶张量积的计算可以简化为多重集（Multiset）上的矩阵运算（Lemma 4.8, 4.9）。
代码实现：
- 提供了约 12.5k 行代码的完整形式化库。
- 依赖 Mathlib 的特定版本，使用了 Lean 4 的最新特性（如模块系统控制定义展开）。

4. 结果 (Results)

定理 1.1 (Main Result)： 给定一个对称幺半范畴 $C$ $C$ ，存在一个伪函子 $C^\otimes: Pith(Span(Fin)) \to Cat$ $C^{\otimes} : P i t h (S p an (F in)) \to C a t$ 。
- 该函子将有限集 $J$ 映射到 $C^J$ 。
- 将 Span 映射到张量积函子。
- 这实际上证明了 $C$ 可以被视为 Cranch 定义的 Lawvere 对称幺半 $(\infty, 1)$ -范畴的普通范畴版本。
相干性定理的强化： 证明了自由对称幺半范畴等价于 $SList(J)$，且态射完全由排列决定。
计算简化： 通过引入“线性”（Linear，即无重复元素）对称列表的概念，证明了在特定条件下（无重复元素），态射是唯一的（Subsingleton），从而极大地简化了相干性条件的验证。

5. 意义与未来工作 (Significance & Future Work)

意义：

连接普通范畴与高阶范畴： 这项工作为 Mathlib 中未来引入 $(\infty, 1)$ -范畴理论奠定了基础。它展示了如何将普通的对称幺半范畴自然地解释为高阶结构，无需重新定义基础数据。
解决高阶运算难题： 使得在形式化数学中定义和操作任意 arity 的张量积（如对称幂 $x^{\otimes n}$ ）成为可能，而无需手动处理复杂的结合律和交换律证明。
方法论示范： 展示了如何在依赖类型理论中通过“无偏倚”视角处理伪代数结构（Pseudoalgebraic structures），特别是利用相干性定理将复杂的范畴论问题转化为更易于处理的组合/群论问题。

未来工作：

应用形式化： 形式化对称张量幂（Symmetric Tensor Powers）和自由交换幺半对象。
双范畴基础设施： 完善 Mathlib 中的双范畴（Bicategory）理论，包括双等价（Biequivalence）、乘积保持等，以建立更严格的范畴等价关系。
高阶范畴整合： 将当前成果与 Mathlib 中正在进行的 $\infty$ -Cosmos 和 Riehl-Verity 理论项目对接，实现从普通范畴到 $(\infty, 1)$ -范畴的无缝转换。

总结：
这篇论文是形式化数学领域的一个重要里程碑。它不仅解决了对称幺半范畴在计算机辅助证明中的长期痛点（高阶运算的繁琐性），还通过精妙的数学构造（对称列表、Coxeter 群、Span 范畴）展示了如何在严格的类型理论中优雅地处理复杂的代数结构。这项工作为未来在 Lean 中进行更高级的代数几何和同伦论形式化铺平了道路。