在Lean中形式化抽象单纯复形和恒星细分
Formalizing Abstract Simplicial Complexes & Stellar Subdivisions in Lean
浏览论文内容
中文总结 AI 辅助
该研究在Lean证明助手中形式化抽象单纯复形和恒星细分，采用纯组合框架，给出相关态射、构造及操作的形式化，研究恒星细分与它们相互作用，还证明三角剖分流形相关恒等式，是恒星细分在证明助手中的首次形式化。
中文摘要 AI 辅助
单纯复形理论是拓扑学的基石，为计算不变量提供了精密工具。我们在Lean证明助手里对抽象单纯复形和恒星细分进行形式化。采用纯组合框架为研究组合拓扑中多种情形下的恒星细分理论提供连贯基础。具体给出抽象单纯复形间态射的形式化，复形上若干关键构造与操作如链和并，全面研究恒星细分与这些操作的相互作用。陈述并证明了三角剖分流形研究中常用的一些恒等式，如导出抽象单纯复形\(K\)及其恒星细分\(\sigma_s K\)中链之间的等价关系，包括标准文献中无参考的结果。据我们所知，这是在任何证明助手里对恒星细分的首次形式化。
英文摘要
The theory of simplicial complexes is a cornerstone of topology, offering a sophisticated tool for computing invariants. We present a formalization of abstract simplicial complexes and stellar subdivisions in the Lean proof assistant. We adopt a purely combinatorial framework in order to provide a cohesive foundation for studying the theory of stellar subdivisions as seen in many contexts of combinatorial topology. In particular, we provide formalizations of morphisms between abstract simplicial complexes; several crucial constructions and operations on complexes, such as links and joins; and perform a comprehensive study of how stellar subdivisions interact with these operations. We state and prove a number of identities commonly used in the study of triangulated manifolds, such as deriving equivalences between links in an abstract simplicial complex $K$ and in a stellar subdivision $σ_s K$, including results with no references in the standard literature. To our knowledge, this is the first formalization of stellar subdivisions in any proof assistant.
