🔢 mathematics

Unbiasing symmetric monoidal categories in Lean

この論文は、Mac ランズの結合性定理を形式化し、有限集合のスペインからなる (2,1)-圏への Cat 値擬関手として対称モノイダル圏を拡張することで、Lean 4 の Mathlib 環境において対称モノイダル圏の非偏倚化プロセスを形式化したものである。

原著者： Robin Carlier

公開日 2026-03-03

📖 1 分で読めます🧠 じっくり読む

CC BY 4.0

原著者： Robin Carlier

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

1. 問題：「順序」に縛られた数学の箱

まず、この研究が解決しようとしている問題を、**「レゴブロック」**で考えてみましょう。

数学の世界には、物をくっつける（積を取る）操作があります。例えば、レゴブロック A と B をくっつけて「AB」とします。

従来のやり方（バイアスあり）：
従来の数学の定義では、「A と B をくっつける」ことしか許されていませんでした。
「A, B, C をくっつける」場合でも、コンピュータは「まず A と B をくっつけて（AB）、それに C をくっつける（(AB)C）」という特定の順序でしか処理できません。
「B と C を先にくっつける（(BC)）」や「A, B, C を同時にくっつける」という考え方は、定義上存在しません。

問題点：
現実の数学（例えば、群論の公式や物理の計算）では、「A, B, C, D...」と何個でも並べて、順序やくっつけ方の順序（括弧の付け方）を気にせず、すべて同じ結果になるはずです。
しかし、従来の定義では「順序」や「括弧」に縛られて（バイアスがかかって）いるため、100 個のレゴブロックをくっつけるような複雑な計算を、1 回 1 回「2 個ずつくっつけていく」という面倒な手順でしか表現できませんでした。

2. 解決策：「魔法の箱」と「万能の翻訳機」

この論文の著者たちは、この「順序に縛られた箱」を、**「順序を気にしない魔法の箱」**に変えることに成功しました。

ステップ 1：レゴの「並べ替えルール」を証明する（コヒーレンス定理）

まず、著者たちは「レゴブロックを並べ替えても、実は同じ形になる」ということを、コンピュータに厳密に証明させました。

例え：
「A, B, C」を「B, A, C」に並べ替える操作や、「(A, B), C」を「A, (B, C)」に変える操作は、実はすべて「同じもの」だと証明しました。
これを数学用語では**「コヒーレンス定理（整合性の定理）」**と呼びますが、著者たちはこれを「対称リスト（Symmetric Lists）」という新しいデータ構造を使って、Lean 上で完璧に再現しました。
- 対称リストとは？
  単なる「リスト（順序付き）」ではなく、「中身が同じなら、順番が違っても同じリスト」として扱う、少し賢いリストです。

ステップ 2：「万能の翻訳機」を作る（偏関手）

次に、この「順序を気にしない魔法の箱」を、既存の「順序に縛られた箱」に翻訳する**「翻訳機」**を作りました。

例え：
従来の数学（順序あり）で書かれた複雑な式を、この翻訳機に通すと、自動的に「順序を気にしない魔法の箱」の形に変換されます。
これにより、ユーザーは「まず A と B をくっつけて、次に C を…」という面倒な手順を気にせず、「A, B, C をまとめてくっつけてください」という自然な指示だけで計算できるようになります。

3. 具体的な仕組み：「スパン」という橋渡し

この翻訳機を作るために、著者たちは**「スパン（Span）」**という概念を使いました。

スパンとは？
2 つの地点（集合）を、真ん中の「橋（共通部分）」でつなぐ図形です。
「A から B への道」を、単なる矢印ではなく、「A ← 橋 → B」という形で見ると、道順の入れ替えや組み合わせが非常に簡単になります。
論文の功績：
著者たちは、この「スパン」の構造を使って、有限集合（物の集まり）と、先ほどの「魔法の箱（対称モノイド圏）」をつなぐ**「橋」**を、Lean 上で初めて正確に組み立てました。

4. なぜこれが重要なのか？

この研究がなぜ画期的なのか、3 つのポイントでまとめます。

複雑な計算が楽になる：
これまで「順序」や「括弧」の処理に追われていた数学者やプログラマーは、これからは「何個の物をくっつけるか」だけを考えればよくなります。まるで、レゴブロックを「1 つずつ」ではなく「山ごと」に扱えるようになったようなものです。
未来の数学への架け橋：
現代の数学では、「無限次元」や「高次元」の概念（∞-圏など）が注目されています。これらの概念は、本質的に「順序を気にしない」性質を持っています。この研究は、従来の「順序あり」の数学と、最新の「高次元」の数学をつなぐ重要な接着剤の役割を果たします。
コンピュータ証明の信頼性向上：
Lean などのツールを使って数学を証明する際、この「アンバイアス化」があるおかげで、より複雑で現実的な定理（例えば、無限の和や、対称性を考慮した物理法則）を、人間が間違えずに証明できるようになります。

まとめ

この論文は、**「数学のレゴブロックを、順序に縛られずに自由に組み立てられるようにする」**という、非常に実用的で美しい仕組みを、コンピュータの証明支援ソフト「Lean」の中に初めて実装したことを報告しています。

著者たちは、難しい数学の定理（マックレーンのコヒーレンス定理）を、**「対称リスト」という新しい言葉に翻訳し、それを「スパン」という橋を使って、既存の数学と未来の数学をつなぐ「万能翻訳機」**を作りました。

これにより、数学の世界は、より直感的で、複雑な構造を扱いやすいものへと進化しました。

論文「Unbiasing symmetric monoidal categories in Lean」の技術的概要

Robin Carlier によるこの論文は、Lean 4 証明支援系とその数学ライブラリ Mathlib において、**対称モノイド圏（symmetric monoidal categories）の「バイアス除去（unbiasing）」**を形式化したことを報告しています。対称モノイド圏の標準的な定義は二項演算（テンソル積）と結合律・単位律・対称性に関する同型射（コヒーレンス）に依存していますが、本論文はこれを任意の有限次数（高次アリティ）のテンソル積と、それらを一貫して扱う構造へと拡張する構成を構築しました。

以下に、問題設定、手法、主要な貢献、結果、および意義について詳細にまとめます。

1. 問題設定

背景

対称モノイド圏は、モノイドの圏論的一般化であり、テンソル積 $\otimes$ 、単位対象 $1 $、結合射$ \alpha $、単位射$ \lambda, \rho $、対称射$ \beta$ で定義されます。しかし、この「バイアス付き（biased）」な定義は、二項演算とそれらのコヒーレンス条件に限定されています。

課題

多くの数学的応用（例えば、有限群 $G$ の既約表現の次元の二乗和 $\sum (\dim \rho)^2 = |G|$ のような、任意の有限集合上の和や積）では、任意の有限次数の演算子が必要となります。

バイアス付き定義の限界: 二項演算を反復適用して高次演算を定義しようとすると、括弧の付け方（結合順序）や要素の順序（対称性）に依存した多数の同型射が生じます。これらが一意に定まることを保証するには、マックレーンのコヒーレンス定理（Mac Lane's coherence theorem）に依存する必要があります。
高次圏への拡張: 高次圏（ $(\infty, 1)$ -圏など）の理論では、対称モノイド構造は「有限集合のスパン（spans）の圏」からの擬関手（pseudofunctor）として記述されることが一般的です。既存の Lean/Mathlib の形式化は古典的なバイアス付き定義に基づいているため、この高次圏的な視点や、自由対称モノイド圏の構成、あるいは任意の次数のテンソル積を自然に扱うための「バイアス除去」が不可能でした。

2. 手法と構成

本論文は、以下の 3 つの主要なステップを経て、対称モノイド圏を「有限集合のスパンの (2,1)-圏（pith）」からの Cat 値擬関手として再構成しました。

2.1 対称リスト（Symmetric Lists）とコヒーレンス定理の形式化

まず、マックレーンのコヒーレンス定理を形式化するために、**対称リスト（Symmetric Lists）**という概念を導入しました。

対称リスト: 集合 $J$ 上の対称リスト $SList(J) $は、$ J$ の要素のリストを対象とし、隣接する要素の入れ替え（swap）を生成射とする圏です。これらは、対称群 $\Sigma_n$ のコクセター群 $A_n$ としての関係式（ $s_i^2=1$ , $s_i s_{i+1} s_i = s_{i+1} s_i s_{i+1}$ など）を反映しています。
Piceghello の結果の移植: Homotopy Type Theory (HoTT) で Piceghello が示した「自由対称モノイド圏は対称リストの圏に同値である」という結果を、Lean/Mathlib の非 HoTT 環境（通常の圏論）に移植しました。
同型の明確化: 対称リストの射と置換（permutations）の間の完全忠実な対応を形式化し、任意の射が一意な置換（およびそのラベル付け）によって特徴付けられることを証明しました（定理 2.8, 補題 2.9）。これにより、自由対称モノイド圏の構造が対称リストの圏 $SList(J)$ として具体的に記述可能になりました。

2.2 スパンの (2,1)-圏からの擬関手構成

次に、任意の対称モノイド圏 $\mathcal{C}$ から、有限集合のスパンの (2,1)-圏 $Pith(Span(Fin))$ への擬関手を構成します。

Pith-Beck-Chevalley システム: 擬関手を構成するための枠組みとして、 $U: \mathcal{C} \to \mathcal{B}$ と $V: \mathcal{C}^{op} \to \mathcal{B}$ の対（擬関手）と、引き戻し図式（pullback squares）に対するベック・チェバリー同型（base-change isomorphism）のデータを持つ「Pith-Beck-Chevalley システム」を定義しました。
スパンへの拡張: このシステムが与えられれば、スパンの (2,1)-圏（2-射が同型射のみである部分圏）からの一意な擬関手が構成できることを証明しました（定理 3.3）。これは、スパンの合成が引き戻しを通じて定義される性質を利用しています。

2.3 クライスリ双圏（Kleisli Bicategory）と普遍性の利用

最後に、対称モノイド圏 $\mathcal{C}$ 自体を、上記のシステムを満たすデータとして解釈します。

相対擬モノードとクライスリ双圏: 対称リストの圏 $SList(J)$ を用いて、集合から自由対称モノイド圏を生成する相対擬モノード（relative pseudomonad）を定義し、そのクライスリ双圏 $K_{SList}$ を構成しました。
普遍性による解釈: 任意の対称モノイド圏 $\mathcal{C}$ は、 $K_{SList}$ の反対圏からの Cat 値擬関手 $C_K$ として解釈できます（Proposition 4.2）。これは、対称モノイド圏が自由対称モノイド圏上の擬代数（pseudoalgebra）であるという考え方に基づいています。
双対性と線形性: 対称リストの「線形性（重複要素がないこと）」を用いることで、スパンの双対性（transpose）とクライスリ双圏の双対性を整合させ、$Pith(Span(Fin)) $から$ K_{SList}^{op} $への擬関手$ \Lambda$ を構成しました（定理 4.12）。これにより、有限集合の集合論的構造（スパン）が、対称モノイド圏の普遍構造と完全に一致することが示されました。

3. 主要な結果

定理 1.1 (Main Theorem): 任意の対称モノイド圏 $(\mathcal{C}, \otimes, 1, \dots)$ に対して、有限集合のスパンの (2,1)-圏 $Pith(Span(Fin)) $から圏の圏$ Cat $への擬関手$ C_\otimes $が存在し、これは有限集合$ J $を$ J $個の$ \mathcal{C} $の直積$ \mathcal{C}^J $に、スパン$ A \xleftarrow{f} B \xrightarrow{g} J $を関手$ g_! f^*$ に写します。
- ここで $f^*$ は前合成、 $g_!$ はファイバーごとのテンソル積（直和）を取る関手です。
- この構成は、Lawvere 型の対称モノイド $(\infty, 1)$ -圏（Cranch の定義）の通常の圏論版を提供します。
コヒーレンス定理の形式化 (Theorem 1.3): 集合 $J$ 上の自由対称モノイド圏は、 $J$ 上の有限集合と全単射の圏 $Core(Fin/J)$（コクセター構造を備えた）にモノイド同値であることを証明しました。これは Piceghello の結果を Lean で完全に形式化したものです。
実装の規模: 約 12,500 行の Lean コード（コメント除く）で実装され、Mathlib の特定のコミットに基づいています。

4. 技術的貢献と意義

技術的貢献

Lean における高次圏的構造の構築: 従来の Lean/Mathlib には存在しなかった、スパンの双圏や、それらからの擬関手構成を初めて実装しました。
コヒーレンス定理の具体的な形式化: 抽象的な定理ではなく、対称リストと置換の具体的な対応（コクセター群 $A_\infty$ を介したラベリング）を用いて、コヒーレンスを計算可能にしました。
バイアス除去の完全な実装: 二項演算から出発し、任意の有限次数のテンソル積を自然に導出するプロセスを、証明支援系内で完全に構築しました。

学術的・実用的意義

高次圏理論への橋渡し: 対称モノイド圏をスパンの擬関手として記述することは、 $(\infty, 1)$ -圏論や無限圏理論における標準的な記法（Lurie の $\infty$ -operads や Cranch の Lawvere 型定義）との整合性を保ちます。Mathlib が将来的に高次圏理論を取り入れる際、この形式化が不可欠な基盤となります。
複雑な代数構造の扱い: 自由対称モノイド圏や、対称テンソル冪（symmetric tensor powers）など、高次アリティの演算を含む構成を、手作業で括弧や順序を管理することなく扱えるようになります。
計算機支援証明の拡張: 群論や表現論における複雑な公式（例： $\sum (\dim \rho)^2 = |G|$ ）の証明において、和や積の順序や結合順序に依存しない「バイアス除去された」操作を直接利用できるようになります。

5. 結論と将来の展望

本論文は、対称モノイド圏のバイアス除去を Lean 4 において初めて成功裏に形式化した画期的な成果です。これにより、Mathlib は単なる代数構造の定義を超え、高次圏論的な視点を取り入れた柔軟な枠組みへと進化しました。

今後の課題としては、

構築されたバイアス除去機構を用いた具体的な応用（対称テンソル冪の形式化など）の実装。
対称モノイド圏の圏と、スパンからの擬関手の圏との間の双圏同値（biequivalence）の完全な証明。
Mathlib への双圏論的インフラ（双圏の積、双圏同値など）の追加。
が挙げられています。これらは、より高度な数学的対象の形式化を可能にするための重要なステップです。