圏論を公理的に扱うには

質問

圏のはじめの定義において対象のcollection、射のcollectionという若干曖昧な言い方がなされるのが普通だと思います。
圏の対象、set全体やgroup全体はproper classになり一階述語論理で書かれた集合論の公理では記述できないことが書籍などでは書かれており、また圏論の解説などで量化記号(∀∃など)を使っているのも見ません。
しかし圏論を公理的に定式化できなければそれも問題だと思うので、公理的な扱いができるとも思っているのですが、それはどういうように行われているのでしょう。
また集合論が数学の基礎づけになっているというのと同じような意味で、圏論がいろいろな数学を展開する場を与えてくれると考えられると感じるのですが、一つ一つの具体的な圏、Set、Group、Top、Htpyなどは圏論全体の枠組みの中でどのようにして導入されるのでしょうか。圏の具体例として急に外から与えられているようにみえるのですが...(たとえば、群全体なるものがどこかで想定されていて圏の定義を満たしていることは確認されるように記述されているように感じます)

おそらく公理的な集合論と圏論との関係がわかっていないための混乱なのですが、圏論はどのように形式的に定まっているものなのでしょうか。

回答No.1

tmpname

classのZFCでの扱い方は、適当な本を見れば載っています。

例をあげると、例えばGroupというのはZFCの枠組みではかけないけど、「AはGroupのobjectである」というのはZFCの枠組みで書ける。というのは、「GはGroupのobjectである」というのは、「Gは群である」ということで、これを表す論理式φ(G)はZFCの中で書ける。同様に「fはGroupのarrowである」というのは、「fは何かの群準同型写像である」ということで、これを表す論理式ψ(f)もZFCで書ける。そこでGroupと書いた時は、この2つの論理式φ、ψのペアの略号と見做せば良い。

関手も同様に扱えます。例えば、忘却関手: Group → Setについては、「Gは集合で、SはGの台集合である」という論理式χ(G, S)を考えている、と思えばよい。χ(G, S)に当てはまる<G,S>のペア全体というのは集合論の枠組みからはずれるけど、χはZFCでかける。

一般に、classというのは、それに対応する何らかのZFCで書ける論理式を「visualizeしたもの」です。