技術要約：Leanにおける抽象単体複体および星状細分化の形式化

問題提起

単体複体の理論は、代数的および組合せ論的トポロジーの基礎であり、ホモロジーや種数を計算するための主要な道具であるとともに、離散モース理論や崩壊アルゴリズムを通じてホモトピー型を研究するための中心的な役割を果たす。古典的な定義は、しばしば（重心座標やアフィン独立性を用いた）ユークリッド空間への幾何学的埋め込みに依存するが、このようなアプローチは余分なデータをもたらし、形式的な計算を複雑にする。

著者らは、Leanの証明支援エコシステムにおけるギャップを特定している。mathlibには単体複体に関連する様々な形式化が含まれているものの、それらの相互接続性は欠けており、**星状細分化（stellar subdivisions）**の形式化は既存のものには存在しない。さらに、他の証明支援系（Rocq、ACL2）における既存の形式化は、アレクサンダーやパッハナーによる多様体の三角形分割に関する構造定理のような、組合せ論的な基礎を提供することよりも、特定の計算的応用（持続的ホモロジーやアレクサンダー双対など）に強く傾倒している。本論文は、既存のライブラリの内容との互換性を維持しつつ、計算可能性を担保しながら、星状細分化、リンク、およびジョインに関する構造的定理を厳密に検証できる、純粋に組合せ論的なフレームワークの必要性に対処するものである。

方法論

著者らは、抽象単体複体（Abstract Simplicial Complexes）を、（面としての）有限集合の集まりであり、部分集合関係に関して閉じているものとして定義する純粋に組合せ論的なフレームワークを採用する。これは、幾何学的な空間から独立しており、これにより、mathlibのSimplicialComplex構造に見られる幾何学的条件（アフィン独立性、凸包の交わり）を取り除き、オーバーヘッドを削減し、型シグネチャを簡素化する。

主要な方法論的選択は以下の通りである：

• 型キャストと強制（Type-Casting and Coercions）： ジョインや細分化のように、基礎となる頂点型を変更する操作を扱うために、著者らは頂点集合上の単射写像を表すSimplicialCoeを定義する。これにより、周囲の型に対する大域的な全単射を必要とせずに、「損失のない」ラベルの付け替えが可能になる。
• ジョインのための非交和： 頂点集合が互いに素であることを仮定せずに2つの複体のジョイン（$K \star L$）を定義するために、著者らは面のインデックスを作成するために積型 $E \times k$ （ここで $k$ は非自明な半環）を利用し、事実上、頂点集合の互いに素なコピーを作成する。
• 星状細分化： 面 $s$ の細分化 $\sigma_s K$ は、$s$ のスターの内部を取り除き、それを $s$ のリンク、$s$ の境界、および新しい重心頂点 $x$ のジョインで置き換えることによって、組合せ論的に定義される。
• 形式的検証： すべての定義と定理はLean 4で実装されている。著者らは、mathlibへの将来的な統合を容易にするため、計算可能性を優先し、仮定を最小限に抑えることを重視している。

主要な貢献

本論文は、いかなる証明支援系においても、星状細分化の最初の形式化を提示している。具体的な貢献は以下の通りである：

1. 抽象単体複体の形式化：

   • コア構造であるAbstractSimplicialComplexの定義、および幾何学的なSimplicialComplexインスタンスへの変換。
   • 射（morphisms）（SimplicialMap）、同型（isomorphisms）（SimplicialIso）、および強制（coercions）（SimplicialCoe）の形式化。
   • 標準的な操作（和集合、共通部分、部分複体、次元計算）の実装。

2. 部分複体および操作の形式化：

   • リンク（$Lk(K, s)$）、**面の境界**（$\partial s$）、**スター**（$St(K, s)$）、スター補集合、錐（cone）、およびジョイン（$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コードで構成されている。

意義と主張

著者らは、本研究を、多様体の三角形分割は、それらが一連の星状（またはビステラー）移動によって関連付けられている場合に限り、互いに同相であるというアレクサンダーおよびパッハナーの定理の形式化に向けた基礎的なステップとして位置付けている。

• 初となる成果： 本論文は、いかなる証明支援系においても、星状細分化の形式化として最初のものであると主張している。
• 理論と計算の架け橋： 組合せ論的なフレームワークを採用することで、本研究は、単体複体の理論を、計算的手法やアルゴリズム的応用（例：トポロジカル・データ解析やReginaのようなソフトウェア）により適したものにすることを目指している。
• フォークロアのカタログ化： 著者らは、組合せ論的トポロジーにおける多くの技術的な恒等式は、その証明の煩雑さゆえに「フォークロア（伝承）」的な地位に漂っていると主張している。この形式化は、これらの結果をカタログ化し検証することで、それらの論理的なギャップが埋められていることを保証するものである。
• 限定的な範囲： 著者らは、これが「初期段階の作業」であることを明示している。彼らはまだパッナーの定理を形式化したと主張しているわけではなく、そのために必要なインフラストラクチャ（細分化、リンク、ジョイン、および同値関係）を提供したのである。また、組合せ論的な側面を分離した一方で、これらをmathlibの幾何学的なSimplicialComplexの定義と完全に統合し、全複体（すべての単元集合が面であるもの）の複雑さを扱うためには、将来的な作業が必要であることも認めている。

この研究は、計算可能性とmathlibとの互換性を優先する設計思想を強調しており、Leanエコシステム内での組合せ論的トポロジーの将来的な発展のための合理化された基礎を構築することを目指している。