Category Theory for Programmersの2.1, 2.2の動画のノート
1.1, 1.2で説明されていた内容
オブジェクトとMorphism
Morphismは矢印
オブジェクトは、Morphismの始まりと終わりを表すもの
オブジェクトやMorphismに構造や属性はなく、原子のようなもの。
Composition
aからb, bからcの矢印が存在する時、
aからcへの矢印「g after f」が必ず存在する(。をafterと読む)
Category
オブジェクトと、矢印たちとその合成を定義する。マッピングテーブルのようなもの。
Identity
すべてのオブジェクトに、１つずつ、Identity Arrowが存在する。
Identity Arrowは、常にidと呼ばれる。
どの矢印とIdentity Arrowを合成しても、元の矢印になる。
Axiom
Left/right identity
矢印の左にあるIdentityをLeft identity
右側にあるIdentityをRight identityという。
この２つは違うもの。
Right identityの例
Associativity
h 。(g 。f) = (h 。g) 。f
Isomorphism
Functions that are both:
- Injective
- Surjective
Isomorphic functions are invertible
definition:
f 。g = id
g 。f = id
In Categorical language
e.g. f is an isomorphism if g exists
Domain, Codomain, Image, etc
Epimorphism
SurjectiveはGreekでEpic。
カテゴリーセオリーではEpimorphism。セットセオリーと違って、要素を使って定義することはできない。
なので、Epimorphismを、関数同士の関係のみを使って定義する。
上の図のように、fがEpimorphismでないとき、bからcへの関数が、fのイメージ外の要素について違う要素にマップする g1, g2として複数存在する余地がある。この場合にも、fのイメージからのマッピングについては同じなのでg1.f = g2.f となる。
\exists\ g_1,g_2,\ g_1 \ne g_2 \implies g1 \circ f = g2 \circ f
fがEpimorphismの場合には、b=fのイメージなので、bからcへの関数が複数存在することは起こりえない。
なのでbからcへのマッピング g は常に同じになる。これを使って、下のようにfがEpimorphismであることを定義できる。
\forall\ g_1,g_2,\ g1 \circ f = g2 \circ f \implies g_1 = g_2
Monomorphism
Injectiveは、GreekでMonic。
カテゴリーセオリーではMonomorphism。
Epimorphismと同じような感じで、オブジェクト群c上のオブジェクトzから、オブジェクト群a上のオブジェクトx1, x2への Morphism g1, g2を定義する。こうすると、f。g1とf。g2はどちらも、zをyにマップする。この場合に常にg1 = g2なればfは Monomorphism。以下が定義。
\forall g_1,g_2 \quad f \circ g_1 = f \circ g_2 \implies g_1=g_2
動画
Bartosz Milewski / Category Theory 2.1: Functions, epimorphisms
https://www.youtube.com/watch?v=O2lZkr-aAqk
Bartosz Milewski / Category Theory 2.2: Monomorphisms, simple types
https://www.youtube.com/watch?v=NcT7CGPICzo