大学数学基礎解説

文献あり

5つの圏の定義とCoqによる実装

圏論,Coq

904

はじめに

この記事では, 5つの圏の定義とCoqによる圏の実装を解説します.
記事内のCoqのソースコードにライブラリは必要ありません.
なお, 記事内のソースコードではポーランド記法(演算子を一番前に書く書き方)を使うので注意してください.

圏の定義と実装

定義を区別するために以降「～バージョン」という表現を使いますが, 本文内のみの用語であることに注意してください.

矢印バージョン

一番わかりやすいと思われる定義からします.

圏 [矢印バージョン]

論理式 $- : O, - : - \to -$ と項 $- \circ -$ が次を満たすとき $(O, \to, \circ)$ を圏とよぶ.

$\forall X, Y, Z : O \forall f : X \to Y \forall g : Y \to Z g \circ f : X \to Z$
$\forall W, X, Y, Z : O \forall f : W \to X \forall g : X \to Y \forall h : Y \to Z (h \circ g) \circ f = h \circ (g \circ f)$
$\forall X : O \exists i : X \to X ((\forall Y : O \forall f : X \to Y f \circ i = f) \land (\forall Y : O \forall f : Y \to X i \circ f = f))$
$\forall X, Y, X^{'}, Y^{'} : O \forall f : X \to Y (f : X^{'} \to Y^{'} \Rightarrow (X = X^{'} \land Y = Y^{'}))$

$X : O$ を「 $X$ は対象」と読み, $f : 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 : X \to Y$ を矢印 $f$ と, 矢印の根本 $X$ , 矢印の先 $Y$ の3つに分けて定義しているようなイメージです.

圏 [1変数バージョン]

論理式 $- : 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 \land D (g \circ f) = D (f) \land 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 \land C (i) = x \land (\forall f : M (D (f) = x \Rightarrow f \circ i = f)) \land (\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変数.

射のみ, 矢印バージョン

矢印バージョンから対象を消したバージョンです.

圏 [射のみ, 矢印バージョン]

論理式 $- : - \to -$ と項 $- \circ -$ が次を満たすとき $(\to, \circ)$ を圏とよぶ.

$\forall x \forall y \forall z \forall f : x \to y \forall g : y \to z g \circ f : x \to z$
$\forall w \forall x \forall y \forall z \forall f : w \to x \forall g : x \to y \forall h : y \to z (h \circ g) \circ f = h \circ (g \circ f)$
$\forall x \forall y \forall f : x \to y (x : x \to x \land y : y \to y \land f \circ x = f \land y \circ f = f)$
$\forall x \forall y \forall x^{'} \forall y^{'} \forall f : x \to y (f : x^{'} \to y^{'} \Rightarrow (x = x^{'} \land 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変数バージョンから対象を消したバージョンです.

圏 [射のみ, 1変数バージョン]

論理式 $- : M$ と項 $- \circ -, D (-), C (-)$ が次を満たすとき $(M, \circ, C, D)$ を圏とよぶ.

$\forall f, g : M (C (f) = D (g) \Rightarrow (g \circ f : M \land D (g \circ f) = D (f) \land 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 \land D (D (f)) = D (f) \land C (D (f)) = D (f) \land D (C (f)) = C (f) \land C (C (f)) = C (f) \land f \circ D (f) = f \land 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) \land C (g, f)) \Rightarrow (C (h, g \circ f) \land C (h \circ g, f) \land (h \circ g) \circ f = h \circ (g \circ f)))$
$\forall h \forall g \forall f ((C (h, g) \land C (h \circ g, f)) \Rightarrow C (g, f))$
$\forall h \forall g \forall f ((C (g, f) \land C (h, g \circ f)) \Rightarrow C (h, g))$
$\forall f ((\exists h C (f, h)) \Rightarrow \exists i \exists j (C (f, i) \land C (j, f) \land (\forall g (C (g, i) \Rightarrow g \circ i = g)) \land (\forall g (C (i, g) \Rightarrow i \circ g = g)) \land (\forall g (C (g, j) \Rightarrow g \circ j = g)) \land (\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 : X \to Y (f : X^{'} \to Y^{'} \Rightarrow (X = X^{'} \land Y = Y^{'}))$ …… ①

①は始域, 終域の well defined, つまり矢印の根本と先が一つに決まること意味しています.
①がないと始域, 終域が複数ある可能性があり, 他の定義との等価性を示すときに構造が戻らない, hom関手が定義できないなどの影響があります.

①が成り立つかわからない状況から, 順序対を使って①が成り立つように修正する方法もありますが, その場合, 矢印と合成の構造が変わり, 射が増えます.

射のみで圏が定義できる理由

矢印バージョンの圏の定義には次の式が含まれていました.

$\forall X : O \exists i : X \to X ((\forall Y : O \forall f : X \to Y f \circ i = f) \land (\forall Y : O \forall f : 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$ や(集合) $:$ (集合) $\to$ (集合)の形でなければ文法エラーです.
少し誤解を招く言い方をしなければいけなかったので, 対象が群のときを例にあげます.
整数全体 $Z$ と整数のたし算 $+_{Z}$ について, $Z$ と $+_{Z}$ は集合より順序対 $(Z, +_{Z})$ は集合です.
よって $(Z, +_{Z}) :$ 群と書くことができます.
一方, 集合全体 $V$ は集合ではないので $V :$ 群は文法エラーとなり, 正しい間違い以前に, 意味のない文字列です.