技术摘要：在 Lean 中形式化抽象单纯复形与星形细分

问题陈述

单纯复形理论是代数和组合拓扑的基础，它是计算同调（homology）和亏格（genus）等不变量，以及通过离散 Morse 理论和塌缩算法研究同伦型的核心工具。虽然经典的定义通常依赖于在欧几里得空间中的几何嵌入（使用重心坐标和仿射独立性），但这类方法引入了额外的冗余数据，增加了形式化计算的复杂性。

作者指出 Lean 证明辅助生态系统中存在一个空白：虽然 mathlib 包含各种与单纯复形相关的形式化内容，但它们缺乏互连性，且目前不存在关于**星形细分（stellar subdivisions）**的现有形式化。此外，其他证明辅助工具（如 Rocq, ACL2）中的现有形式化过于偏向特定的计算应用（例如持久同调、Alexander 对偶），而非提供类似于 Alexander 和 Pachner 关于流形三角剖分定理的连贯组合基础。本文旨在 Lean 4 中建立一个纯组合性的框架，以支持对涉及星形细分、链路（links）和并（joins）之恒等式的严谨验证，同时保持与现有库内容的兼容性和可计算性。

方法论

作者采用了一种纯组合框架，将**抽象单纯复形（Abstract Simplicial Complexes）**定义为满足子集关系封闭的有限集合（面）的集合，而不依赖于任何环境几何空间。这种方法剥离了 mathlib 中 SimplicialComplex 结构所包含的几何条件（如仿射独立性、凸包交集），从而降低了开销并简化了类型签名。

关键的方法论选择包括：

• 类型转换与强制转换（Type-Casting and Coercions）： 为了处理改变底层顶点类型的操作（例如并、细分），作者定义了 SimplicialCoe 结构，它表示顶点集上的单射映射。这允许进行“无损”的重标记，而无需对环境类型进行全局双射。
• 利用不交并实现并运算： 为了在不假设顶点集不交的情况下定义两个复形的并 ($K \star L$)，作者利用乘积类型 $E \times k$（其中 $k$ 是一个非平凡半环）来索引面，从而有效地创建了顶点集的互不相交副本。
• 星形细分： 面 $s$ 的细分 $\sigma_s K$ 通过移除 $s$ 之星（star）的内部，并用 $s$ 之链路（link）、$s$ 之边界（boundary）与一个新的重心顶点 $x$ 的并来替换来实现。
• 形式化验证： 所有定义和定理均在 Lean 4 中实现。作者优先考虑保持可计算性并最小化假设，以促进未来与 mathlib 的集成。

核心贡献

本文提出了第一个在任何证明辅助工具中对星形细分进行的形式化。具体贡献如下：

1. 抽象单纯复形的形式化：

   • 定义了核心结构 AbstractSimplicialComplex 及其与几何 SimplicialComplex 实例之间的相互转换。
   • 形式化了态射（SimplicialMap）、同构（SimplicialIso）和强制转换（SimplicialCoe）。
   • 实现了标准操作：并集、交集、子复形和维数计算。

2. 子复形与操作的形式化：

   • 对链路 ($Lk(K, s)$)、**面边界** ($\partial s$)、**星** ($St(K, s)$)、星补（star complements）、锥（cones）和并 ($K \star L$) 的性质进行了严格的定义和证明。
   • 证明了并运算在同构/强制转换意义下的分配律、结合律和交换律。
   • 建立了展示这些操作如何与同构和强制转换相互作用的恒等式。

3. 星形细分的形式化：

   • 定义了星形细分 $\sigma_s K$ 和星形焊接（stellar weld，即逆操作）。
   • 定义了星形等价 ($K \cong_{st} L$) 为星形移动的传递闭包。
   • 证明了星形等价在单射类型强制转换下保持不变（定理 3.2），确保该等价关系对于顶点标记的变化具有鲁棒性。

4. 新定理与恒等式：

   • 推导了描述星形细分与链路之间相互作用的恒等式。值得注意的是，定理 3.9 确立了对于位于被细分面链路中的面 $t$，被细分复形中的 $t$ 之链路即为原链路的星形细分：$Lk(\sigma_s K, t) = \sigma_{s \setminus t}(Lk(K, t))$。
   • 作者指出，这一特定恒等式以及其他几个关于链路与细分“反交换性”的恒等式在文献中没有标准引用，是在形式化过程中推导出来的。

结果

该形式化成功验证了一系列在研究三角化流形时常用的恒等式：

• 链路保持： 如果面 $t$ 位于被细分的星之外，其链路保持不变 ($Lk(\sigma_s K, t) = Lk(K, t)$)。
• 并兼容性： 星形细分以特定方式在并运算上满足分配律，例如：$(\sigma_s K) \star L = \sigma_{s \sqcup \emptyset}(K \star L)$。
• 等价保持： 在单射类型强制转换下，星形等价保持不变，前提是目标类型为新重心标签提供了足够的“空间”。
• 代码量： 该项目目前包含约 14,000 行 Lean 代码，涵盖了定义、工具引理和证明。

重要性与声明

作者将这项工作定位为形式化 Alexander 定理和 Pachner 定理的基础性步骤，这两个定理指出，流形的三角剖分是同胚的，当且仅当它们可以通过一系列星形（或双星）移动相关联。

• 首创性： 本文声称是第一个在任何证明辅助工具中对星形细分进行形式化的工作。
• 桥接理论与计算： 通过采用组合框架，这项工作旨在使单纯复形理论更适用于计算技术和算法应用（例如在拓扑数据分析和像 Regina 这样的软件中）。
• 整理“民俗”知识： 作者认为，由于证明过程极其繁琐，许多组合拓扑中的技术恒等式已逐渐演变为“民俗”（folklore）状态。这种形式化起到了记录和验证这些结果的作用，确保其逻辑漏洞得到填补。
• 规模适度： 作者明确指出这只是“初步工作”。他们并不声称已经完成了 Pachner 定理的形式化，而是提供了必要的底层架构（细分、链路、并和等价关系）来完成此项工作。他们也承认，虽然他们隔离了组合方面的内容，但未来仍需工作以将这些结果与 mathlib 中的几何 SimplicialComplex 定义完全集成，并处理全复形（total complexes，即每个单元素均为面的复形）的复杂性。

这项工作强调了一种优先考虑可计算性和与 mathlib 兼容性的设计理念，旨在为 Lean 生态系统中组合拓扑的未来发展创建一个精简的基础。