12. 圏論の公理 (1):合成射の存在,およびその可換性
12
- 合成射の存在
- f :A から B に向かう射
- g :B から C に向かう射
- これらが存在するとき、必ず A から C に向かう射 g ° f が存在するべき
- 可換性
- f と g をそれぞれ使って、A から C に至ること
- g ° f を 1 つ使って、A から C に至ること
- これらは等しくなるべき
f g
g ° f
A B C
13. NG な例 ?
13
- in Scala 圏:
- length :長さを調べる関数
- isEven :偶数であるかを調べる関数
- isCamelCase :キャメルケースであるかを調べる関数
- このとき、始点?終点となる対象 (型) はそれぞれ一致しているが、
可換性が無いため、isCamelCase は合成射になっていない!
length isEven
isCamelCase
String Int Boolean
15. f ∈ Hom(A, B) ? ?a ∈ Hom(X, A), ?b ∈ Hom(X, B), b = f ° a
- 合成射の存在より、A から B に向かう射が 1 つでも存在すれば、
必ず X から B に向かう射が存在する ? Hom(X, B) の存在がいえる
- Hom(X, A) の任意の要素を、Hom(X, B) のある要素に対応づける、
自明な関数 f ° _ を考えることができる
15
X
B
A
圏 C 集合の圏 Sets
Hom(X, A)
Hom(X, B)f
f ° _
※ 合成射が必ず存在
16. 圏論の公理 (2):恒等射の存在,およびその単位律
16
- 恒等射の存在
- 任意の対象 X に関して、必ず X から X 自身に向かう射 idX
が存在するべき
- 単位律
- ?f:X から Y に向かう任意の射
- idX
° f , f ° idY
, および f のそれぞれが等しくなるべき
?f
idX
X
Y
X
Y
?f?f
idY
17. NG な例 ?
17
- in Scala 圏:
- increment ? 与えられた数を、1 増やして返す関数
- このとき、increment は Int から Int 自身に向かう射ではあるが、
恒等射になっていない! (例:increment ≠ increment ° increment)
Int
Int Int
increment
increment
increment
18. OK な例 ??♂
18
- in Scala 圏:
- identityInt
? 与えられた数を、そのまま返す関数
- このとき、identityInt
は恒等射の条件をみたす
∵ 任意の型 X からの任意の関数 f に対して、identityInt
° f = f
X
Int Int
identityInt
?f
?f
19. ?X ∈ Obj(C), Hom(X, X) ≠ ?
- 恒等射の存在より、任意の対象 X には恒等射 idX
が必ず備わる
- よって、Hom(X, X) には少なくとも 1 つは射が含まれる
(※ この事実は米田の補題を考える上でも重要となる)
19
X X
圏 C
Hom(X, X)
?X, ?idX
?
idX
集合の圏 Sets
20. - …については割愛します ?
- ざっくり言うと:
- f :A から B に向かう射
- g :B から C に向かう射
- h :C から D に向かう射
- このとき、(h ° g) ° f と h ° (g ° f) は等しくなるべき
- そうなるように合成演算子 ° を考えてね,と捉えても良い
圏論の公理 (3):合成射の結合律
20
23. 函手の記号的表現
- 圏 C から圏 D への函手を考える:
- 対象と対象の対応関係は、関数 F で表してみる
- 射と射の対応関係は、関数 mapF
で表してみる
(※ 数学的にはどちらも同じ記法で表してしまう場合が多いが、今回は分かりやすさを重視)
23
圏 D
X Y
f
F(X)
F(Y)
mapF
(f)
圏 C
24. 考察:函手と合成射 (1)
- 合成射に関するグラフ表現を、函手で移すことを考える:
- 対象 A, B, C :対象 F(A), F(B), F(C) に対応
- 射 f, g :射 mapF
(f), mapF
(g) に対応
- 合成射 g ° f :射 mapF
(g ° f) に対応
24
A
圏 D圏 C
B
C
F(B)
F(A) F(C)
f g mapF
(f) mapF
(g)
g ° f mapF
(g ° f)
25. - 合成射の存在より、mapF
(f) と mapF
(g) だけに着目しても、
これらの合成射 mapF
(g) ° mapF
(f) を考えることができる
- これは、mapF
(g ° f) とは別ものなのだろうか? ?
考察:函手と合成射 (2)
25
A
圏 D圏 C
B
C
F(B)
F(A) F(C)
f g mapF
(f) mapF
(g)
g ° f mapF
(g ° f)
mapF
(g) ° mapF
(f)
26. 函手の性質 (1):準同型性
- mapF
(g ° f) = mapF
(g) ° mapF
(f) となるように、函手は定めるべき
? このような性質を準同型性という
- 直感的には:
- ある圏の合成射が、別の圏でも合成射に移される,ということ
26
A
圏 D圏 C
B
C
F(B)
F(A) F(C)
f g mapF
(f) mapF
(g)
g ° f mapF
(g ° f) = mapF
(g) ° mapF
(f)
43. 共変 Hom 函手
- 任意の圏から集合の圏 Sets への函手であって,
- 対象 * を対象 Hom(X, *) へ移し,
- 射 f を射 f ° _ へ移す,そんな函手
43
?a
?b
?f, b = f ° a
Hom(X, A)
Hom(X, B)
f ° _
X
B
A
圏 C 集合の圏 Sets
44. Hom 函手と集合値函手の自然変換
- 圏 C から集合の圏 Sets への函手を 2 つ考える:
- 1 つめは、対象 X を固定した Hom 函手 :[ Hom(X, *) / f → f ° _ ]
- 2 つめは、適当な集合値函手 :[ F / mapF
]
- このとき、自然変換 θ = ?A. θA
: Hom(X, A) → F(A)
44
集合の圏 Sets圏 C
θA
θB
θC
A B C
F(A) F(B) F(C)X
Hom(X, A) Hom(X, B) Hom(X, C)
45. Hom 函手と集合値函手の、函手圏における Hom 集合
- ここで、函手圏 SetsC
で Hom 集合を考えたいが、表記が紛らわしい ?
- ? 函手圏での Hom 集合は、Nat( , ) のように表すとする
- 下図の函手圏 SetsC
で Hom 集合を考えた場合:
- Nat( [ Hom(X, *) / f → f ° _ ] , [ F / mapF
] ) = { α, β, γ }
45
α●
γ●
α●
γ●
Hom(X, *) / f → f ° _
函手圏 SetsC
F / mapF
α = ?X. αX
β = ?X. βX
γ = ?X. γX
集合の圏 Sets
β●
β●
β●
α●
γ●
F(A) F(B) F(C)
Hom(X, A) Hom(X, B) Hom(X, C)
46. "米田の補題" の主張
- 函手圏 SetsC
での Hom 集合もまた、集合の圏 Sets の対象
- 圏 C で固定した対象 X を、函手で移した F(X) もまた、集合の圏 Sets の対象
- ここで:
- Nat( [ Hom(X, *) / f → f ° _ ] , [ F / mapF
] ) ? F(X)
(※ これら 2 つの集合の要素が、それぞれ 1 対 1 に対応すること)
46
α●
γ●
α●
γ●
β●
β●
β●
α●
γ●
F(A) F(B) F(C)
Nat( [ Hom(X, *) / f → f ° _ ], [ F / mapF
] )
F(X)
※ 全単射が存在する
Hom(X, A) Hom(X, B) Hom(X, C)
集合の圏 Sets
51. 固定した対象 X を中心とした、圏 C のセッティング
- 固定した対象 X と、射で接続された対象たちをピックアップ
- e.g. A, B, C, ...
- このとき X 自身にも、恒等射 idX
による接続がある
- 各対象間には複数の射が存在しうるので、対象ごとに f*
, g*
, h*
, ... と表してみる
- e.g. X から A に伸びる射であれば、fA
, gA
, hA
, ...
51
圏 C
A B
X
X C
idX
52. X と A に着目した自然変換 (1)
- X と A を接続する射は、fA
, gA
, hA
, ... と複数ある
- ? ここでは fA
をピックアップし、それぞれの函手で移す
- ここで、自然変換の満たす可換図式から、以下の 2 つが等価:
- mapF
(fA
) ° θX
- θA
° (fA
° _)
52
圏 C
A B
X
X C
集合の圏 Sets
θX
θA
F(X) F(A)
Hom(X, X) Hom(X, A)
idX
fA
° _
mapF
(fA
)
fA
, gA
, hA
, ...
55. X と A に着目した自然変換 (4)
- したがって、下記の対応は、 Hom(X, A) から F(A) への関数 θA
を完全に定める
- mapF
(fA
)(αX
) = θA
( fA
)
- mapF
(gA
)(αX
) = θA
( gA
)
- mapF
(hA
)(αX
) = θA
( hA
)
- ...
55
圏 C
A B
X
X C
集合の圏 Sets
θX
θA
{ αX
} F(A)
Hom(X, A)
idX
fA
, gA
, hA
, ...
※ Hom(X, A) の要素 fA
, gA
, hA
, ... の行き先を全てカバー
{ idX
}
56. X と B に着目した自然変換
- 同様に、 Hom(X, B) から F(B) への関数 θB
も完全に定まる
- mapF
(fB
)(αX
) = θB
( fB
)
- mapF
(gB
)(αX
) = θB
( gB
)
- mapF
(hB
)(αX
) = θB
( hB
)
- ...
56
圏 C
A B
X
X C
集合の圏 Sets
θX
θB
{ αX
} F(B)
Hom(X, B)
idX
fB
, gB
, hB
, ...
※ Hom(X, B) の要素 fB
, gB
, hB
, ... の行き先を全てカバー
{ idX
}
57. X と C に着目した自然変換
- 同様に、 Hom(X, C) から F(C) への関数 θC
も完全に定まる
- mapF
(fC
)(αX
) = θC
( fC
)
- mapF
(gC
)(αX
) = θC
( gC
)
- mapF
(hC
)(αX
) = θC
( hC
)
- ...
57
圏 C
A B
X
X C
集合の圏 Sets
θX
θC
{ αX
} F(C)
Hom(X, C)
idX
fC
, gC
, hC
, ...
※ Hom(X, C) の要素 fC
, gC
, hC
, ... の行き先を全てカバー
{ idX
}
58. αX
= θX
(idX
) が定まれば、自然変換 θ が定まる
- 結局:
- * :圏 C の任意の対象
- f*
:X から * への任意の射
- これら全てに対して、mapF
(f*
)(αX
) = θ*
(f*
) が成り立つ
- この等式で任意性がある部分は、αX
の選び方だけ
58
圏 C
A B
X
X C
集合の圏 Sets
θX
θ*
{ αX
} F(*)
{ idX
} Hom(X, *)
idX
?f*
° _
mapF
(?f*
)