はじめに
こんにちは。SREの神谷です。
この記事では簡単な圏を作ってみます。
前回のおさらい
前回の記事で述べたように、2026年の抱負は圏論をSREに活用することです。
抱負の達成に向けて3ステップで進めると宣言しました。
- 圏論の様々な概念を学ぶ
- SREに関連する様々な概念を圏論の概念と関連付ける
- 圏論をSREに活用する
また、キーワードが2つあり、積極的に活用することも述べました。
- ソフトウェアエンジニアリング（Lean）
- カン拡張
今回やること
ステップ1「圏論の様々な概念を学ぶ」として簡単な圏を作ってみます。
Leanを使います。
カン拡張は今回は使いません。
Leanを使うモチベーション
圏論をSREに活用するにあたって心配なことがあります。数学的に間違えてしまうことです。課題があるとき、どのように解決すべきでしょうか？SREであれば、ソフトウェアエンジニアリングを使うべきでしょう。つまり、ソフトウェアエンジニアリングによって、数学的に正しいことを保証すれば良いのです。Leanは、この目的にぴったりです。Leanはプログラミング言語であり、かつ定理証明支援系でもあるからです。Leanでエラーが出なければ、数学的に正しいことが証明されたことになります。我々は、ソフトウェアエンジニアとしてエラーが出ないようにコーディングすることに専念すれば良いのです。
ゴール設定
今回は初めてLeanを使うので、簡単な例に取り組みます。簡単な圏の例で Lean の mathlib4 というライブラリの Category の instance を定義します。エラーが出ないように定義できれば、圏であることが証明できたことになります。それが今回のゴールです。
Leanの使い方
Lean 4 Web にアクセスするとブラウザ上で簡単に試すことができます。
今回のソースコード込みのリンクを貼っておきます。Leanソースコードリンク
リンクを開くと画面が左右に分割され、左側にソースコード、右側にメッセージが表示されます。
例えば
#eval 1 + 1と入力すると右側に2と表示されます。
このように対話的に開発・証明作業ができます。
ゴールの達成
ソースコード込みのリンクを開くと、左側のソースコードの中に
instance : Category TwoObj whereが含まれています。また、右側にエラーは表示されていません。つまり Category の instance をエラーを発生させずに定義するという今回のゴールが達成できています！
この後は、ソースコードを抜粋しながら説明をしていきます。
圏を作ってみる
書籍『はじめての圏論 ブンゲン先生の現代数学入門』の「はじめに」によると
「圏論」の基本的なアイデアは、単に「モノとモノを矢印でつなぐ」というシンプルなものです。
ということで、ふたつのモノを矢印でつないで圏を作ってみましょう。
絵で書くとこんな感じです。
graph LR A --> B
「A → B」をイメージしづらい方は、例えば千代田線「・・・→乃木坂→赤坂→国会議事堂前→・・・」から「赤坂→国会議事堂前」を抜き出したものだと考えてください。
graph LR A[赤坂] --> B[国会議事堂前]
「A → B」の例として、千代田線の他に、組織における上下関係（部下 → 上司）、自然数の大小関係0 ≦ 1、集合と関数f:X → Yなどでも構いません。何かしら関連があるモノたちであれば何でも良いです。
対象
では、Leanで圏を作ってみましょう。まずはモノの準備です。圏論ではモノのことを対象（object）といいます。
inductive TwoObj | A | BここでLeanではinductiveを列挙型のように使うことができます。
射
次に矢印を作ります。圏論では矢印のことを射（morphism）といいます。
inductive TwoHom : TwoObj → TwoObj → Type | a_to_b : TwoHom A B | id_a : TwoHom A A | id_b : TwoHom B B射の定義をもとに、はじめに書いた絵を書き直しておきましょう。
千代田線の図も載せておきます。
id_aとid_bは恒等射（identity morphism）と呼ばれます。恒等射は、直感的には何もしない矢印です。千代田線の例では「赤坂→赤坂」がid_aに相当します。
圏
対象と射の準備ができたので、いよいよ圏（category）を作ります。
instance : Category TwoObj where Hom X Y := TwoHom X Y id X := ... comp f g := ... id_comp := ... comp_id := ... assoc := ...なお…の部分を省略しています。
恒等射
idの省略した…の部分は、このようになっています。対象A, Bそれぞれの恒等射をid_a, id_bと定めています。冒頭の例ではA（赤坂）の恒等射をid_a（赤坂→赤坂）と定めています。
id X := match X with | A => id_a | B => id_b合成
compの省略した…の部分は、このようになっています。
comp（合成、Composition）は直感的には矢印をつなげることに相当します。
comp f g := match f, g with | id_a, id_a => id_a | id_a, a_to_b => a_to_b | a_to_b, id_b => a_to_b | id_b, id_b => id_bまずid_a, id_a => id_aはid_aとid_aの合成をid_aと定めています。
冒頭の例では2つの矢印id_a（赤坂→赤坂）とid_a（赤坂→赤坂）をつなげるとid_a（赤坂→赤坂）になると定めています。
graph LR A2[A] -- id_a --> A3[A] A2[A] -- id_a --> A A -- id_a --> A3[A]
graph LR A2[赤坂] -- id_a[赤坂->赤坂] --> A3[赤坂] A2[赤坂] -- id_a[赤坂->赤坂] --> A[赤坂] A -- id_a[赤坂->赤坂] --> A3[赤坂]
次にid_a, a_to_b => a_to_bはid_aとa_to_bの合成をa_to_bと定めています。
冒頭の例では2つの矢印id_a（赤坂→赤坂）とa_to_b（赤坂→国会議事堂前）をつなげるとa_to_b（赤坂→国会議事堂前）になると定めています。
graph LR A2[A] -- id_a --> A A2[A] -- a_to_b --> B A -- a_to_b --> B
graph LR A2[赤坂] -- id_a[赤坂->赤坂] --> A[赤坂] A2[赤坂] -- a_to_b[赤坂->国会議事堂前] --> B[国会議事堂前] A[赤坂] -- a_to_b[赤坂->国会議事堂前] --> B[国会議事堂前]
残りの2つa_to_b, id_b => a_to_bとid_b, id_b => id_bも同様です。
左単位律
id_compは左単位律です。恒等射を左から合成しても射は変わりません。
例えばid_a, a_to_b => a_to_bはa_to_bに左から恒等射id_aを合成してもa_to_bのままです。
左単位律を確認しましょう。
/-## 左単位律 `id_comp` の確認左から恒等射を合成しても，射は変わりません。つまり `𝟙 X ≫ f = f` が成り立ちます。-/example {X Y : TwoObj} {f : X ⟶ Y} : 𝟙 X ≫ f = f := by -- ここにカーソルを置くと図が表示されます。 exact Category.id_comp fここでXとYは任意のTwoObj、fはXからYへの射、𝟙 XはXの恒等射です。
例えばXをA, YをB, fをa_to_b, 𝟙 Xをid_aと考えるとわかりやすいかもしれません。
この場合は上の図と同じになります。千代田線の例ではid_a（赤坂→赤坂）を左からa_to_b（赤坂→国会議事堂前）に合成してもa_to_b（赤坂→国会議事堂前）のまま変わらないということです。
Lean 4 Web の画面で-- ここにカーソルを置くと図が表示されます。の部分にカーソルを置いてみてください。右側に図が表示されるはずです。
Commutative Diagram（可換図式）は対象を四角、射を（四角いラベル付きの）矢印で表します。
この可換図式は𝟙 X ≫ f = fを意味しています。≫は合成の記号です。
左上から右下に行くとき、右に行ってから下に行く（𝟙 X ≫ f）のと、右斜め下に直接行く（f）のが同じ（=）ということです。
千代田線の例ではid_a（赤坂→赤坂）のあとでa_to_b（赤坂→国会議事堂前）するのと、直接a_to_b（赤坂→国会議事堂前）するのは同じ（=）ということです。
String Diagram（ストリング図）は対象を線、射を四角で表します。ストリング図では恒等射は省略されます。
右単位律
comp_idは右単位律です。恒等射を右から合成しても射は変わりません。左右が入れ替わっているだけで、左単位律とほぼ同様です。
結合律
assocは結合律です。合成の括弧の付け方を変えても，射は変わりません。 つまり (f ≫ g) ≫ h = f ≫ (g ≫ h) が成り立ちます。
可換図式はこのようになります。左上から右下に行くとき、右に行ってから下に行く（(f ≫ g) ≫ h）のと、右斜め下に直接行く（f ≫ (g ≫ h)）のが同じ（=）ということです。
冒頭の例では３つの射id_a（赤坂→赤坂）、a_to_b（赤坂→国会議事堂前）、id_b（国会議事堂前→国会議事堂前）を合成するとき
id_a（赤坂→赤坂）、a_to_b（赤坂→国会議事堂前）を先に合成してからid_b（国会議事堂前→国会議事堂前）を合成するa_to_b（赤坂→国会議事堂前）、id_b（国会議事堂前→国会議事堂前）を先に合成してからid_a（赤坂→赤坂）、を合成する
の2つが同じだということです。
graph LR A -- id_a --> A2[A] A2[A] -- a_to_b --> B B -- id_b --> B2[B]
graph LR A[赤坂] -- id_a[赤坂->赤坂] --> A2[赤坂] A2[赤坂] -- a_to_b[赤坂->国会議事堂前] --> B[国会議事堂前] B[国会議事堂前] -- id_b[国会議事堂前->国会議事堂前] --> B2[国会議事堂前]
ストリング図はこのようになります。ストリング図では括弧は図に反映されません。
個人的な圏論のイメージ
個人的には、圏論は落ち物パズルと似ていると思います。
ブロックをつなげて消すのは、射を合成して恒等射を消すのと似ています。
合成でつなげるだけだと長くなってしまうばかりですが、左単位律、右単位律、結合律があることで短く整理できます。
例えば
graph LR A -- id_a --> A2[A] A2[A] -- a_to_b --> B B -- id_b --> B2[B]
はid_aとid_bを消すことができます。
graph LR A2[A] -- a_to_b --> B
スッキリしましたね！
今回は簡単な圏でしたが、今後、もっと複雑な圏で、矢印をつなげて消して爽快感を味わいたいです。
まとめ
今回は対象が2つ、非恒等射が１つの簡単な圏をLeanで作ってみました。
また、ストリング図や可換図式を表示しました。
次回以降、ステップ2「SREに関連する様々な概念を圏論の概念と関連付ける」に取り組みます。
カン拡張も使いたいです。
参考資料
- 書籍『はじめての圏論 ブンゲン先生の現代数学入門』
- Web『Lean by Example』
- Web『mathlib4』