Chapter 42

14 表現可能関手

さのたけと
さのたけと
2021.06.02に更新

原文:4. Representable Functors

そろそろ集合について少し話してもいいころだ。数学者は集合論に愛憎絡まった感情を抱いている。集合は数学者にとってのアセンブリ言語だ---少なくともそうだった。圏論は集合論から距離をある程度置こうとする。例えば、全ての集合からなる集合は存在しないというのは既知の事実だが、全ての集合からなる圏\mathrm{Set}は存在する。いいことだ。他方、我々はある圏での2つの対象の間の射たちは集合をなすということを仮定している。その集合をHom集合とよんでいた。公正を期すために述べると、射たちが集合をなさないような圏論の一分野もある。そういうときは、射たちは集合のかわりにある別の圏をなす。そのような、Hom集合のかわりにHom対象を使う圏を 豊穣圏 とよぶ。しかしこの先、我々は古き良きHom集合を持つ圏だけを考えることにする。

集合というのは、圏論における対象を除けば最も無特徴なモノだ。集合は元を持つが、その要素たちについて大したことは分からない。もし有限集合を相手にしているなら、その元たちを数えることができる。順序数を使えば、無限集合についてもある意味で数えることができる。例えば、どちらも無限なのにも関わらず、自然数の集合は実数の集合よりも小さい。しかし、多分驚くだろうが、有理数の集合は自然数の集合と同じ大きさなのである。

その他には、集合に関する全ての情報は集合たちの間の関数にエンコードすることができる[1]---特に可逆な関数は同型とよばれる。あらゆる意味で、同型な集合たちは同一視できる。基礎論の数学者をお怒りを買う前に、同一であることと同型であることの違いは根本的に重要であることを説明させてほしい。実際、数学の最新の分野のHomotopy Type Theory (HoTT)では、これは重要な問題なのである。私がHoTTに言及しているのは、HoTTが計算からインスピレーションを得て作られた純粋数学だからであり、HoTTの主な提唱者であるVladimir Voevodskyは、定理証明器Coqの研究をしているときにHoTTの大きなひらめきを得たのだった。数学とプログラミングの相互作用はこのように両方向で起こるのである。

集合に関する重要な知恵は、異なる種類の集合同士を比較しても良いということである。例えば、与えられた自然変換の集合が何らかの射の集合と同型であると言ってもよい。なぜなら、集合は集合だからである。この場合の同型とは単に、片方の集合の全ての自然変換についてもう片方の集合の唯一の射があり、逆もまたそうであるという意味である。これらは互いにペアにすることができる。リンゴとミカンを比べることは、もしもそれらが異なる圏から来ているのならできないが、リンゴの集合とミカンの集合とを比べることはできる。しばしば、圏論の問題を集合論的な問題に変形することによって必要な直観が得られたり、価値ある定理を証明できたりすることさえある。

(和訳:@ashiato45

脚注
  1. 訳注: "all the information about sets can be encoded in functions between them" だが正直よくわからない。 ↩︎