5つの圏の定義とCoqによる実装
はじめに
この記事では, 5つの圏の定義とCoqによる圏の実装を解説します.
記事内のCoqのソースコードにライブラリは必要ありません.
なお, 記事内のソースコードではポーランド記法(演算子を一番前に書く書き方)を使うので注意してください.
圏の定義と実装
定義を区別するために以降「～バージョン」という表現を使いますが, 本文内のみの用語であることに注意してください.
矢印バージョン
一番わかりやすいと思われる定義からします.
論理式$-:O,\ -\colon -\to -$と項$- \circ -$が次を満たすとき$(O,\to,\circ)$を圏とよぶ.
- $\forall X,\ Y,\ Z:O\ \forall f\colon X \to Y\ \forall g\colon Y \to Z\ g\circ f\colon X\to Z$
- $\forall W,\ X,\ Y,\ Z:O\ \forall f\colon W \to X\ \forall g\colon X \to Y\ \forall h\colon Y \to Z\ (h \circ g) \circ f = h \circ (g \circ f)$
- $\forall X:O\ \exists i\colon X\to X\ \\ ((\forall Y:O\ \forall f\colon X\to Y\ f \circ i = f) \wedge (\forall Y:O\ \forall f\colon Y\to X\ i \circ f = f))$
- $\forall X,\ Y,\ X',\ Y':O\ \forall f\colon X \to Y\ (f\colon X' \to Y' \Rightarrow(X = X' \wedge Y = Y'))$
$X:O$を「$X$は対象」と読み, $f\colon X\to Y$を「$f$は$X$から$Y$への射」と読む.
$\circ$を合成とよぶ.
以下, Coqによる実装です.
Definition category
(O : Set -> Prop) (M : Set -> Set -> Set -> Prop) (o : Set -> Set -> Set) :=
(forall f g X Y Z : Set, O X -> O Y -> O Z ->
M f X Y -> M g Y Z -> M (o g f) X Z) /\
(forall f g h W X Y Z : Set, O W -> O X -> O Y -> O Z ->
M f W X -> M g X Y -> M h Y Z -> o (o h g) f = o h (o g f)) /\
(forall X : Set, O X -> exists i : Set, M i X X /\
(forall f Y : Set, O Y -> M f X Y -> o f i = f) /\
(forall f Y : Set, O Y -> M f Y X -> o i f = f)) /\
(forall f X Y X' Y' : Set, O X -> O Y -> O X' -> O Y' ->
M f X Y -> M f X' Y' -> X = X' /\ Y = Y').
主な特徴
- 矢印を定義する必要がなく, イメージしやすい.
- 定義に必要なパラメーターが対象, 矢印, 合成の3つ.
1変数バージョン
合成$\circ$以外を1変数で圏を定義する方法です.
これは$f\colon X\to Y$を矢印$f$と, 矢印の根本$X$, 矢印の先$Y$の3つに分けて定義しているようなイメージです.
論理式$-:O,\ -:M$と項$- \circ -,\ D(-),\ C(-)$が次を満たすとき$(O,M,\circ,C,D)$を圏とよぶ.
- $\forall f:M\ D(f),\ C(f):O$
- $\forall f,\ g : M\ (C(f) = D(g) \Rightarrow (g \circ f:M \wedge D(g \circ f) = D(f) \wedge C(g \circ f) = C(g)))$
- $\forall f,\ g,\ h : M\ (C(f) = D(g) \Rightarrow (C(g) = D(h) \Rightarrow (h \circ g) \circ f = h \circ (g \circ f)))$
- $\forall x : O\ \exists i : M\ (D(i) = x \wedge C(i) = x \wedge\\ (\forall f : M\ (D(f) = x \Rightarrow f \circ i = f)) \wedge (\forall f : M\ (C(f) = x \Rightarrow i \circ f = f)))$
$X:O$を「$X$は対象」, $f:M$を「$f$は射」と読む.
$\circ$を「合成」, $D(f)$は「$f$の始域」, $C(f)$は「$f$の終域」とよぶ.
以下, Coqによる実装です.
Definition category_1
(O M : Set -> Prop) (o : Set -> Set -> Set) (D C : Set -> Set) :=
(forall f : Set, M f -> O (D f) /\ O (C f)) /\
(forall f g : Set, M f -> M g -> C f = D g ->
M (o g f) /\ D (o g f) = D f /\ C (o g f) = C g) /\
(forall f g h : Set, M f -> M g -> M h ->
C f = D g -> C g = D h -> o (o h g) f = o h (o g f)) /\
(forall x : Set, O x -> exists i : Set, M i /\ D i = x /\ C i = x /\
(forall f : Set, M f -> D f = x -> o f i = f) /\
(forall f : Set, M f -> C f = x -> o i f = f)).
主な特徴
- 定義に必要なパラメーターが対象, 射, 合成, 始域, 終域の5つ.
- 合成以外のパラメーターは1変数.
射のみ, 矢印バージョン
矢印バージョンから対象を消したバージョンです.
論理式$-\colon -\to -$と項$- \circ -$が次を満たすとき$(\to,\circ)$を圏とよぶ.
- $\forall x \forall y \forall z \forall f \colon x \to y\ \forall g \colon y \to z\ g \circ f \colon x \to z$
- $\forall w \forall x \forall y \forall z \forall f \colon w \to x\ \forall g \colon x \to y\ \forall h \colon y \to z\ (h \circ g) \circ f = h \circ (g \circ f)$
- $\forall x \forall y \forall f \colon x \to y\ (x \colon x \to x \wedge y \colon y \to y \wedge f \circ x = f \wedge y \circ f = f)$
- $\forall x \forall y \forall x' \forall y' \forall f \colon x \to y\ (f \colon x' \to y' \Rightarrow (x = x' \wedge y = y'))$
以下, Coqによる実装です.
Definition category_morphism
(M : Set -> Set -> Set -> Prop) (o : Set -> Set -> Set) :=
(forall f g x y z : Set,
M f x y -> M g y z -> M (o g f) x z) /\
(forall f g h w x y z : Set, M f w x ->
M g x y -> M h y z -> o (o h g) f = o h (o g f)) /\
(forall f x y : Set, M f x y ->
M x x x /\ M y y y /\ o f x = f /\ o y f = f) /\
(forall f x y x' y' : Set, M f x y -> M f x' y' -> x = x' /\ y = y').
主な特徴
- 矢印を定義する必要がなく, イメージしやすい.
- 定義に必要なパラメーターが矢印, 合成の2つ.
射のみ, 1変数バージョン
1変数バージョンから対象を消したバージョンです.
論理式$\ -:M$と項$- \circ -,\ D(-),\ C(-)$が次を満たすとき$(M,\circ,C,D)$を圏とよぶ.
- $\forall f,\ g : M\ (C(f) = D(g) \Rightarrow (g \circ f : M \wedge D(g \circ f) = D(f) \wedge C(g \circ f) = C(g)))$
- $\forall f,\ g,\ h : M\ (C(f) = D(g) \Rightarrow (C(g) = D(h) \Rightarrow (h \circ g) \circ f = h \circ (g \circ f)))$
- $\forall f : M\ (D(f),\ C(f) : M \wedge\\ D(D(f)) = D(f) \wedge C(D(f)) = D(f) \wedge\\ D(C(f)) = C(f) \wedge C(C(f)) = C(f) \wedge\\ f \circ D(f) = f \wedge C(f) \circ f = f)$
以下, Coqによる実装です.
Definition category_1_morphism
(M : Set -> Prop) (o : Set -> Set -> Set) (D C : Set -> Set) :=
(forall f g : Set, M f -> M g -> C f = D g ->
M (o g f) /\ D (o g f) = D f /\ C (o g f) = C g) /\
(forall f g h : Set, M f -> M g -> M h ->
C f = D g -> C g = D h -> o (o h g) f = o h (o g f)) /\
(forall f : Set, M f -> M (D f) /\ M (C f) /\
D (D f) = D f /\ C (D f) = D f /\
D (C f) = C f /\ C (C f) = C f /\
o f (D f) = f /\ o (C f) f = f).
主な特徴
- 定義に必要なパラメーターが射, 合成, 始域, 終域の4つ.
- 合成以外のパラメーターは1変数.
合成可能対バージョン
最後に, 合成可能対による対象なしの圏を定義します.
直感的には, 矢印の繋がりに注目した定義です.
論理式$C(-,-)$, 項$- \circ -$が次を満たすとき$(C,\circ)$を圏とよぶ.
- $\forall g\forall f(C(g,f) \Rightarrow \exists h\ C(g\circ f,h))$
- $\forall h \forall g \forall f((C(h,g) \wedge C(g,f)) \Rightarrow \\ (C(h,g\circ f) \wedge C(h \circ g, f) \wedge (h \circ g) \circ f = h \circ (g \circ f)))$
- $\forall h \forall g \forall f ((C(h,g) \wedge C(h \circ g,f)) \Rightarrow C(g,f))$
- $\forall h \forall g \forall f((C(g,f) \wedge C(h,g \circ f)) \Rightarrow C(h,g))$
- $\forall f((\exists h\ C(f,h)) \Rightarrow\\ \exists i \exists j(C(f,i) \wedge C(j,f) \wedge \\ (\forall g(C(g,i) \Rightarrow g \circ i = g)) \wedge (\forall g(C(i,g) \Rightarrow i \circ g = g)) \wedge \\ (\forall g(C(g,j) \Rightarrow g \circ j = g)) \wedge (\forall g(C(j,g) \Rightarrow j \circ g = g))))$
$C(g,f)$を「$g$と$f$は合成可能対」と読む.
$\circ$を「合成」とよぶ.
以下, Coqによる実装です.
Definition category_composable
(C : Set -> Set -> Prop) (o : Set -> Set -> Set) :=
(forall g f : Set, C g f -> exists h : Set, C (o g f) h) /\
(forall h g f : Set, C h g -> C g f ->
C h (o g f) /\ C (o h g) f /\ o (o h g) f = o h (o g f)) /\
(forall h g f : Set, C h g -> C (o h g) f -> C g f) /\
(forall h g f : Set, C g f -> C h (o g f) -> C h g) /\
(forall f : Set, (exists h : Set, C f h) ->
exists i j : Set, C f i /\ C j f /\
(forall g : Set, C g i -> o g i = g) /\ (forall g : Set, C i g -> o i g = g) /\
(forall g : Set, C g j -> o g j = g) /\ (forall g : Set, C j g -> o j g = g)).
主な特徴
- 定義に必要なパラメーターが合成可能対, 合成の2つ.
(射のみ)矢印バージョンの始域, 終域の well defined について
矢印バージョンの圏の定義には次の式が含まれていました.
$\forall X,\ Y,\ X',\ Y':O\ \forall f\colon X \to Y\ (f\colon X' \to Y' \Rightarrow(X = X' \wedge Y = Y'))$ …… ①
①は始域, 終域の well defined, つまり矢印の根本と先が一つに決まること意味しています.
①がないと始域, 終域が複数ある可能性があり, 他の定義との等価性を示すときに構造が戻らない, hom関手が定義できないなどの影響があります.
①が成り立つかわからない状況から, 順序対を使って①が成り立つように修正する方法もありますが, その場合, 矢印と合成の構造が変わり, 射が増えます.
射のみで圏が定義できる理由
矢印バージョンの圏の定義には次の式が含まれていました.
$\forall X:O\ \exists i\colon X\to X\ \\ ((\forall Y:O\ \forall f\colon X\to Y\ f \circ i = f) \wedge (\forall Y:O\ \forall f\colon Y\to X\ i \circ f = f))$ ......②
対象$X$について, ②に現れる$i$はただ一つ存在します.
この$i$を$X$の恒等射とよび, $1_X$と書きます.
対象がある圏では, 対象と恒等射の間に一対一対応があることを示せます.
たとえば, 単射性は次を示すことになります.
$\forall X,\ Y:O\ (1_X = 1_Y \Rightarrow X = Y)$
証明には始域, 終域の一意性①を使う必要があります.
これにより「恒等射を対象と思ってよい」というわけです.
対象も射も集合
矢印バージョンの圏の定義のCoqのソースコードを見ると次のように書かれているところがあります.
(O : Set -> Prop) (M : Set -> Set -> Set -> Prop) (o : Set -> Set -> Set)
forall f g X Y Z : Set, O X -> O Y -> O Z ->
M f X Y -> M g Y Z -> ...
実装は普通の一階述語論理+ZF(C)を想定していますから, (集合)$ : O$や(集合)$ \colon $(集合)$ \to $(集合)の形でなければ文法エラーです.
少し誤解を招く言い方をしなければいけなかったので, 対象が群のときを例にあげます.
整数全体$\mathbb{Z}$と整数のたし算$+_\mathbb{Z}$について, $\mathbb{Z}$と$+_\mathbb{Z}$は集合より順序対$(\mathbb{Z},+_\mathbb{Z})$は集合です.
よって$(\mathbb{Z},+_\mathbb{Z}):$群と書くことができます.
一方, 集合全体$\bf V$は集合ではないので$\bf V:$群は文法エラーとなり, 正しい間違い以前に, 意味のない文字列です.
圏の圏や関手圏などを考えるときに, 上記のような文法が効いて, 圏が「小さい」という概念を考えないといけない局面があります.
普段は圏が小さいなどを気にしなくても問題ないように感じるかもしれませんが, Coqのようなプログラミング言語で圏論をすると文法エラーで詰まるところが多いかもしれません.
オススメの定義
個人的には矢印バージョンか, 射のみ矢印バージョンをオススメしています.
直感的ですし, パラメーターも少ないので圏かどうかの確認も簡単です.
もちろん, どの定義を選ぶかは自由ですし, それぞれの定義が等価であることも示せます.
好みに合った定義を使ってください.