数学の基礎
圏と関手
圏とは、対象とその間の射を、結合律と単位律だけに従ってまとめたものである。関手とはそのような二つの世界の間の構造を保つ翻訳であり、「物がどう関係しているか」を固定すれば、対象自体は一意な同型を除いて決まることが分かる。
直観同じ形、違う衣装
翻訳者、グラフ、路線でつながる駅の網、「先に起こらなければならない」で結ばれた作業の集合——これらはすべて一つの骨格を共有している:いくつかのもの(対象)と、それらの間をつなぎ連結できる矢印である。圏はその骨格を精密にし、関手はそのような網をもう一つの網の中に、矢印の連結をすべて保ったまま描き直す方法である。
大学圏:対象、射、合成
定義: 圏
圏 とは、対象 の集まりと、各対に対する射の集合 、そして と を に送る合成規則、さらに各対象に対する恒等射 からなるものである。
二つの公理がこのデータを圏にする:合成が結合的である(、ゆえに矢印の連鎖はどこに括弧を置いても一つの明確な合成を持つ)こと、そして単位射が中立である(、ゆえに や と合成しても射は変わらない)ことである。
| 種類 | 射への作用 | 典型例 |
|---|---|---|
| 共変 | を に送る、同じ向き | リスト関手、忘却関手 |
| 反変 | を に送る、逆向き | 双対空間関手、前層Hom(-,A) |
発展関手と自然変換
関手 は、 の各対象 に の対象 を、各射 に射 を割り当て、合成と単位を保つ: かつ 。二つの関手 の間の自然変換 は、各対象 に における射 を割り当て、自然性四角形に従う:すべての に対して 。
と が共に の終対象である(すべての対象からそれぞれへの射がちょうど一つ存在する)とき、:両者の間に同型が存在し、それは の唯一の射である。双対の命題は始対象について成り立ち、同じ議論を候補錐の圏に適用すれば積についても成り立つ。
なぜ正しいのか?
この事実がなければ「終対象」や「積」が一意に定まらない——積の異なる構成(順序対か別の符号化か)は互換でなければならず、一意な同型を除いた一意性こそがそれらが「同じである」ことの正確な意味である。
証明
が終対象であるため、すべての対象——特に ——からそこへの射がちょうど一つ存在する。それを と呼ぶ。 が終対象であるため、対称的にちょうど一つの が存在する。
合成 を考える。 が終対象であるため、 の射はちょうど一つしかなく、 はそのような射の一つである。 も の射であるため、一意性から が強制される。
の終対象性を使った対称的な議論により、合成 も に等しくなければならない:。
両側逆射を持つ射は定義により同型であるから、 は逆射 を持つ同型 である。それが の唯一の射であるのは、 の終対象性がそもそもそのような射がちょうど一つしかないと述べているからである—— は最初から一意に決まっており、それが可逆であることが分かっただけである。
が関手であり、 が における逆射 を持つ同型であるとき、 は における同型であり、逆射は である。
なぜ正しいのか?
これが関手を信頼できる翻訳者にする理由である:関手は同値を誤って二つの本当に異なる対象に分解することは決してなく、対象を「同型を除いて」分類するという問いを関手は尊重する。
証明
と が互いに逆であるため、 かつ 。
最初の等式に を適用する。関手は合成を保つので ;関手は単位射を保つので 。これらを と組み合わせると が得られる。
同様に第二の等式に を適用する: かつ なので、 から が得られる。
この二つの式は、 が の両側逆射であることをまさに述べている。両側逆射を持つ射は同型であるから、 は逆射 を持つ同型であり、主張どおりである。
大学応用:関数型プログラミングとデータベース移行
主要な関数型言語がすべて `Functor` 型クラスを持つのは、リストや木、`Maybe`/`Option` のようなコンテナが、型と関数の圏上の関手であるからにほかならない:`fmap` は射に対する であり、関手則 、 はまさに上の公理である。`Monad` はさらに二つの自然変換(`return` と `join`)を用いて、自然性四角形に似た整合律を課すことで精緻化する。プログラミングの外では、David Spivakの関手的データ移行が、データベーススキーマを小さな圏(テーブルを対象、外部キーを射)としてモデル化し、スキーマ移行を二つのそのような圏の間の関手としてモデル化する。「データを正しく移動する」ことは文字通り「関手であること」を意味し、合成保存性により、中間スキーマを経由した移行が直接の移行と同じ結果を与えることが保証される。
例: リストに対する関手則の検証
リストに対する を、すべての要素に関数を適用するものとして定義する:。具体的なリスト に対し、、 で両方の関手則を検証せよ。
解答
法則一、:恒等関数を各要素に適用すると となり、これはまさに である。これはこのリストだけでなく任意のリストで成り立つ。各要素に「何もしない」を適用してもリストには何も起こらないからである。
法則二、:まず左辺を計算する。 なので、。
次に右辺:、続けて 。
両辺とも に等しく、この例で法則が確認された;一般的な証明は の代わりに を用いた同じ計算であり、 が要素を並べ替えたり落としたりすることが決してないからである。
例: 関手としてのスキーマ移行
スキーマ にはテーブル `Person` と `City` があり、外部キー `livesIn : Person -> City` を持つ。新しいスキーマ は `Person` を `Person` と `Contact` に分割し、`hasContact : Person -> Contact` と `livesIn2 : Contact -> City` を持つ。この移行を関手として記述し、合成保存が何をもたらすか説明せよ。
解答
各スキーマを圏としてモデル化する:対象はテーブル、射は自由に合成される外部キーである(したがって には生成子として合成 がある)。移行 は 、 を送り、射 を における合成射 に送る。
が関手であるためには単位射を単位射に送り(ここでは自明)、合成を尊重しなければならない: で から作られる外部キーの連鎖は、 から作られる同じ連鎖に、同じ順序で、飛ばしや並べ替えなしに写らなければならない。
これこそ「関手は合成を保つ」という定理がエンジニアにもたらすものである:古いスキーマで を介して を に結合するクエリがあるとき、各テーブルを翻訳し を二段階の経路に写してから結合を実行すれば、クエリ全体を一つの単位として翻訳した場合と同じ答えが得られる——テーブル単位で移行したデータは、クエリ単位で移行したデータと一致することが保証される。まさに であるからである。
どの二つの方程式が圏の二つの公理か?
反変関手は をどちら向きの射に送るか?
Spivakの関手的データ移行において、スキーマ移行は何に対応するか?
が二つの終対象の間の唯一の射であるとき、定理は について何を述べるか?
参考文献
- Saunders Mac Lane (1998). Categories for the Working Mathematician
- Emily Riehl (2016). Category Theory in Context
- David I. Spivak (2012). Functorial Data Migration · arXiv:1009.1166