圏・関手・自然変換の定義
形式的に厳密であろうと努力した。その結果が以下の通り。
最後に小圏の圏、関手圏を定義する。
■圏の定義
圏は次の6つの成分で構成される。
(ob,mor,id,dom,cod,com)
(ob,mor,id,dom,cod,com)が圏であるとは、次の①～⑦を満たすもののことをいう。
①id∈Map(ob,mor)
②dom,cod∈Map(mor,ob)
③com∈Map({ (f,g) | f,g∈mor ∧ cod(f)=dom(g) }, mor)
④∀x(x∈ob ⇒ dom(id(x))=cod(id(x))=x)
⑤∀f(f∈mor ⇒ (com(id(dom(f)),f)=f ∧ com(f,id(cod(f)))=f))
⑥∀f∀g((f,g∈mor ∧ cod(f)=dom(g)) ⇒ (dom(com(f,g))=dom(f) ∧ cod(com(f,g))=cod(g)))
⑦∀f∀g∀h((f,g,h∈mor ∧ cod(f)=dom(g) ∧ cod(g)=dom(h)) ⇒ com(com(f,g),h)=com(f,com(g,h)))
圏の各成分の意味は次のように与えられる。
obは対象のクラス
morは射のクラス
idは対象の恒等射と呼ばれる射を与える写像
domは射の始域と呼ばれる対象を与える写像
codは射の終域と呼ばれる対象を与える写像
comは射の合成を与える写像
comは通常見られる射の合成の順序とは逆に与えている。ご注意。
com(f,g) = (g○f)
射の合成com、恒等射の与え方id、始域の与え方dom、終域の与え方codは圏ごとに与えられる属性なので、圏の定義で一括りにする。
hom := { ((x,y),{ f | f∈mor ∧ dom(f)=x ∧ cod(f)=y }) | x,y∈ob }
homはob×obからPow(mor)への写像になる。
homの性質
∀x∀y∀u∀v((x,y,u,v∈ob ∧ (x,y)≠(u,v)) ⇒ (hom(x,y) ∩ hom(u,v))=∅)
mor = Union({ hom(x,y) | x,y∈ob })
Cが圏のとき、次のようにして圏Cの6つの成分を表示する。
C = (ob[C], mor[C], id[C], dom[C], cod[C], com[C])
■集合圏
集合圏をSetと表記する。
ob[Set] := { X | Xは集合 }
mor[Set] := { (f,X,Y) | fは写像 ∧ X,Yは集合 ∧ Dom(f)=X ∧ Ran(f)⊆Y }
id[Set] := { (X,({ (x,x) | x∈X },X,X)) | Xは集合 }
dom[Set] := { ((f,X,Y),X) | fは写像 ∧ X,Yは集合 ∧ Dom(f)=X ∧ Ran(f)⊆Y }
cod[Set] := { ((f,X,Y),Y) | fは写像 ∧ X,Yは集合 ∧ Dom(f)=X ∧ Ran(f)⊆Y }
com[Set] := { (((f,X,Y),(g,Y,Z)),({ (x,z) | ∃y((x,y)∈f ∧ (y,z)∈g) },X,Z)) | f,gは写像 ∧ X,Y,Zは集合 ∧ Dom(f)=X ∧ Ran(f)⊆Y ∧ Dom(g)=Y ∧ Ran(g)⊆Z }
※Dom,Ranとdom,codは異なるもの
※射(f,X,Y)はfと略して使われることが頻繁にある
■単集合による圏
この圏はSingleton(a,f)と名付ける。
aとfは任意。
ob[Singleton(a,f)] := {a}
mor[Singleton(a,f)] := {f}
id[Singleton(a,f)] := {(a,f)}
dom[Singleton(a,f)] := {(f,a)}
cod[Singleton(a,f)] := {(f,a)}
com[Singleton(a,f)] := {((f,f),f)}
■空圏
この圏をEmptyと名付ける。
ob[Empty] := ∅
mor[Empty] := ∅
id[Empty] := ∅
dom[Empty] := ∅
cod[Empty] := ∅
com[Empty] := ∅
■関手の定義
関手は写像の対の構造をもつ。
C,Dを圏とする。
(F,F')がCからDへの関手とは、次の条件①～⑥をすべて満たすものである。
①F∈Map(ob[C],ob[D])
②F'∈Map(mor[C],mor[D])
③{ (F(x),F'(f)) | (x,f)∈id[C] } ⊆ id[D]
④{ (F'(f),F(x)) | (f,x)∈dom[C] } ⊆ dom[D]
⑤{ (F'(f),F(x)) | (f,x)∈cod[C] } ⊆ cod[D]
⑥{ ((F'(f),F'(g)),F'(h)) | ((f,g),h)∈com[C] } ⊆ com[D]
③～⑤について、左辺の対は右辺に含まれているので制限写像的になる。
⑥の左辺の定義域は④⑤より、
cod[D](F'(f))=F(cod[C](f))=F(dom[C](g))=dom[D](F'(g))
なので、com[D]の定義域に含まれている。
特記事項
関手は(F,F')という写像の対が正体なのだが、
G=(F,F')
と、まとめてしまって、
G(x)でxが対象の場合、Fの方が使われていて、
G(f)でfが射の場合、F'の方が使われてるという扱い方をされる。
以降、この方式を採用する。
そうしないと、たくさんの文字があふれて逆に分かり難くなる。
たいていのテキストでもそういう扱いがされるので慣れておいた方がいいと思う。
■自然変換の定義
C,Dを圏とする。
F,GをCからDへの関手とする。
tがFからGへの自然変換であるとは、次の条件①～③を満たすことである。
①t∈Map(ob[C], mor[D])
②∀x(x∈ob[C] ⇒ t(x)∈hom[D](F(x),G(x)))
③∀f∀x∀y(f∈hom[C](x,y) ⇒ com[D](t(x),G(f))=com[D](F(f),t(y)))
※homを使うとすっきりした表現になるので、そうした
※homからdom,codへ表現を変えたい場合、f∈hom(x,y) ⇔ (dom(f)=x ∧ cod(f)=y)
■小圏
ここに至り、小圏の圏、関手圏の構成が可能になる。
Cは小圏 :⇔ (Cは圏 ∧ ob[C],mor[C]は集合)
Cは局所小圏 :⇔ (Cは圏 ∧ ∀x∀y(x,y∈ob[C] ⇒ hom[C](x,y)は集合))
小圏全体 ⊆ 局所小圏全体 ⊆ 圏全体
という関係
Set,Grp,Ring,Top,Vect-Kは局所小圏
■小圏の圏
小圏の圏をCatと表示する。
ob[Cat] := { C | Cは小圏 }
mor[Cat] := { (F,C,D) | C,Dは小圏 ∧ FはCからDへの関手 }
id[Cat] := { (C,(({ (x,x) | x∈ob[C] },{ (f,f) | f∈mor[C] }),C,C)) | Cは小圏 }
dom[Cat] := { ((F,C,D),C) | C,Dは小圏 ∧ FはCからDへの関手 }
cod[Cat] := { ((F,C,D),D) | C,Dは小圏 ∧ FはCからDへの関手 }
com[Cat] := { ((((F,F'),C,D),((G,G'),D,E)),((com[Set](F,G),com[Set](F',G')),C,E)) | C,D,Eは小圏 ∧ (F,F')はCからDへの関手 ∧ (G,G')はDからEへの関手 }
※ここでは関手は写像の対で表示をしている
■関手圏
C,Dは圏とする。
関手圏Fun(C,D)はCからDへの関手全体を対象とする圏で、射は自然変換になる。
ob[Fun(C,D)] := { F | FはCからDへの関手 }
mor[Fun(C,D)] := { (t,F,G) | F,GはCからDへの関手 ∧ tはFからGへの自然変換 }
id[Fun(C,D)] := { (F,({ (x,id[D](F(x))) | x∈ob[C] },F,F)) | FはCからDへの関手 }
dom[Fun(C,D)] := { ((t,F,G),F) | F,GはCからDへの関手 ∧ tはFからGへの自然変換 }
cod[Fun(C,D)] := { ((t,F,G),G) | F,GはCからDへの関手 ∧ tはFからGへの自然変換 }
com[Fun(C,D)] := { (((t,F,G),(s,G,H)),({ (x,com[D](t(x),s(x))) | x∈ob[C] },F,H)) | F,G,HはCからDへの関手 ∧ tはFからGへの自然変換 ∧ sはGからHへの自然変換 }
小圏の圏Catは局所小圏になる。
Cが小圏、Dが局所小圏ならば、Fun(C,D)は局所小圏になる。
CもDも小圏のときは、Fun(C,D)は小圏になる。
一般の圏で、圏の圏や関手圏を扱うと集合論的に扱いが難しくなる。
以上
