ナンプレ(数独)は難しさを定義するのが難しい

はじめに

私は先日、最新技術にキャッチアップするためにレベル別ナンプレ(数独) – 無料問題集 | パズル製作研究所(以下 puzzle.dev)というナンプレのサイトを構築しました。サイトでは自動生成した大量の問題の中から毎日難易度順に 13 問をランダムに出題しています。

以前、 CalcBlocks というサイトで計算ブロック・数字ブロック・ビルディングパズルなどのナンプレよりも自動生成が難しいパズルの自動生成をしていたのでナンプレサービスも簡単に作れるだろうと思ってました。

確かに、ナンプレの問題の自動生成はすぐにできました。でも、難易度別に問題を出し分けようとした時、問題に直面しました。

ナンプレの難しさって何で決まるんだ?

サイトを作り始めた頃は初期のヒントの数が少ないほど難しいと思っていましたが、これは間違いです。私はあまりにもナンプレのことを知らなさ過ぎました。

この記事は、以前の私と同様にナンプレというパズルの存在やルール位は知っているけど、解き方のテクニックなどについては詳しく知らない人向けにナンプレの奥深さを知ってもらいたくて書きました。
まず、初心者の多くが使う仮置きという解き方テクニックについて説明します。次に、世界一難しいナンプレの問題を作ろうとして失敗した話を紹介します。最後に、私がナンプレを解くテクニックを 13 個に整理してそれを使って難易度を定義した話をします。

仮置きは最強のテクニックだけど邪道です

puzzle.dev を作る前の私はナンプレについて

電車やバスでおじさんが解いてる時間をかけさえすれば簡単に解けるパズル

程度の認識でした。時間をかけさえすれば解くことができるというのは正しいです。仮置きと呼ばれるテクニックをひたすら繰り返せば原理的には解けます。
仮置きは以下のようなテクニックです。

  1. 数字が確定できるセルに数字をすべて入れる
  2. 数字が確定していないセルに入る可能性がある数字の中から適当に数字を入れる
  3. 1 と 2 をナンプレのルールと矛盾する、もしくは答えにたどり着くまで繰り返す
  4. ナンプレのルールと矛盾したら、2 に戻って別の数字を試す

仮置きはどんなナンプレの問題もこのテクニックだけで解くことができる最強で汎用性の高いテクニックです。ナンプレを解くプログラムを作成しろと言われたらほとんどのプログラマーはこのアルゴリズムを実装しようとするのではないでしょうか?
一方で、このアルゴリズムは、矛盾にたどり着いた場合にはさかのぼって別の数字を試すという BackTrack(引き戻し)が何度も発生するので紙の上で人が実行するのはほとんど不可能です。アプリ等で補助を受けても難しいし単なる運ゲーになってしまって楽しくありません。
これらの理由からナンプレ愛好家の間では仮置きは邪道と見なされています。

世界一難しいナンプレの問題の作成に失敗

10 年ほど前、世界一難しいナンプレの問題を作ったと数学者が発表したのち、その問題がすぐに基本的なテクニックのみを用いて解かれたことがありました。当時の様子は以下の記事で伺い知ることができます。

ここは推測なのですが、おそらく仮置きのアルゴリズムをベースに難しさを定義していたのではないかと思います。しかし、すでに述べたようにナンプレ愛好家は仮置きを使いません。特定のアルゴリズムを使ってコンピューターで解くのが難しくても、人間が簡単に解けるならその問題は難しいと言えるでしょうか。

私は当初、初期のヒントの数が少なければ少ないほど難しいのではないかと考えていましたが、初期のヒントの数が少なくても基本的なテクニックのみで解ける問題はたくさんあります。初期のヒントが少ない問題を作るのはとても難しいです。でも、人間が簡単に解けるならやはり難しい問題とは言えないと思います。
ちなみに、ナンプレの問題の初期のヒントの最小個数は 17個 であることが知られています。

大切なのは人間にとっての難しさです。

ナンプレを解くための 13 個のテクニック

人間にとっての難しさを定義するためには、ナンプレ愛好家の人たちがナンプレを解く時に使用しているテクニックについて十分によく理解する必要があります。
ナンプレを解くテクニックには大きく分けて 2 つの種類があります。

  • この空白のセルにはこの数字しか入らないと決めるテクニック
  • この空白のセルにはこの数字は入らないと決めるテクニック

ほとんどのナンプレ初心者の方は空白のセルに入る数字の候補を減らしていく 2 つ目の種類のテクニックを知らないために難しい問題を解くことができないと思います。
ナンバープレース(ナンプレ、数独)の解き方テクニック集 | パズル製作研究所 では下の 13 個のテクニックについて図を使いながら詳しく解説しました。

  1. ボードの領域で独り
  2. 数字別ボードの枠で独り
  3. 残り 2 席
  4. 3 人寄ればもんじゅの知恵
  5. 候補は独り
  6. 数字別ボードの行・列で独り
  7. 隠しレーザー
  8. 隠しコレーザー
  9. 2 国同盟
  10. n 国同盟
  11. 井形レーザー
  12. XY チェイン
  13. シンプルチェイン

13 個のテクニックは、私が書籍やネットで公開されているテクニックを調べて、それぞれについてそれは一体どういうテクニックなのか、他のテクニックとどう関係しているのか、新しいテクニックはないかなどを検討して整理した結果です(名前は適当です)。
例えばテクニック4 の 3 人寄ればもんじゅの知恵は私のオリジナルのテクニックです(私が知らないだけでどこかで解説されているかもしれません)。
他にもテクニック7 の隠しレーザーはよく知られたテクニックですが、そのテクニックを少し変更したテクニック8 の隠しコレーザーを説明しているサイトはほとんどありません。
テクニック 1 から 6 がこの数字しか入らないと決めるテクニックで、テクニック 7 以降がこの数字は入らないと決めるテクニックです。

AWS 上でランダムに作成した 4000 万問のナンプレの問題を実際に 13 個のテクニックを使用して解いたところ 99.5% の問題を解くことができました。逆に言うと、0.5% の問題は解くことができませんでした。
この結果から、私が解説したテクニックの集合は完全ではないにせよ十分に強力だと考えています。

ナンプレの難しさを定義する

人間にとっての難しさを定義する準備が整いました。
puzzle.dev では 13 個のテクニックを上で紹介した順で簡単なテクニックから難しいテクニックの順に並べています。その上で、より難しいテクニックを多く使わないと解けない問題の方が難しいと定義しています。

もう少し正確に定義します。
問題を解く場合には必ず簡単なテクニックから試します。もし、使えるテクニックが見つかればそのテクニックを使って、セルに入る数字を決めるか、セルに入る数字の候補を減らします。次は、再度最初のテクニックに戻って使えるテクニックを探します。これを繰り返します。
この手順にしたがって問題を解くと、それぞれのテクニックを使った回数が得られます。例えばテクニック 1 からテクニック 13 の順に使った回数を並べると次のようになります。
\begin{align*}
[21,24,0,0,1,0,0,0,0,0,0,0,0]
\end{align*}
これはある問題を解くのに、テクニック 1 を 21 回、テクニック 2 を 24 回、テクニック 5 を 1 回使ったことを表しています。どの順でテクニックを使ったかはわかりません。
難易度を決める際には先ほどのテクニックの使用回数を逆順に並べ替えた後で辞書式順序で比較します。例えば問題を解くのに使ったテクニックの回数が以下の 2 つの問題があったとします。
\begin{align*}
\text{問題} 1: [21,24,0,0,1,0,0,0,0,0,0,0,0] \\
\text{問題} 2: [21,22,1,1,0,1,0,0,0,0,0,0,0]
\end{align*}
この二つの問題の難しさを比較するためにこの数字の並び順をそれぞれ逆順に並べ替えます。
\begin{align*}
[0,0,0,0,0,0,0,0,1,0,0,24,21] \\
[0,0,0,0,0,0,0,1,0,1,1,22,21]
\end{align*}
この二つを辞書式順序で比較します。すると、
\begin{align*}
[0,0,0,0,0,0,0,0,1,0,0,24,21] \lt [0,0,0,0,0,0,0,1,0,1,1,22,21]
\end{align*}
となるので、この順序で大きい問題 2 が問題 1 より難しい問題であると判断します。
この難易度の決め方によって 「より難しいテクニックをより多く使っている問題の方が難しい問題である」 という気持ちを順序として表現することができます。

まだ発展・改良の余地はあるか?

puzzle.dev では、ナンプレの難易度の定義をより難しいテクニックを使わないと解けない問題の方が難しいと定義しましたが、これは唯一絶対正しい難易度の定義ではありません。例えば XY チェインやシンプルチェインの長さは現状一切考慮していませんが、チェインの長さが長い方が難しい問題になると思います。より人間の感覚に合うように難しさの定義も修正していく必要があります。

自動生成した問題のうち 0.5% の問題は 13 個のテクニックを利用しても解けません。13 個のテクニックを適用できない状況を詳しく分析することで新しいテクニックを発見できる可能性があります。新しいテクニックが見つかれば、難しさの定義も変える必要があります。

私が思いもつかないようなテクニックや、難易度の定義をみなさんが思いついてくれることを楽しみにしています。

おわりに

この記事を読んでナンプレの奥深さを知って楽しんでくれる人が増えると嬉しいです。

補足: 技術的な話

補足としてナンプレの問題の自動生成に用いた技術について簡単に解説します。

サイトを支える技術

サイトの構成には以下のフレームワークやサービスを使用しました。

サーバー側は AWS 上で APIGateway + Lambda のサーバーレスで構築しています。
ナンプレの問題の自動生成も Lambda 関数の組み合わせで実現し構成は全て Terraform で管理しています。

Sat Solver を利用した問題の自動生成

ここでは初期のヒントからナンプレのルールを満たす答えがただ一つに決まる問題を正当な問題と呼びます。
問題を自動生成するにあたりナンプレを解くプログラムは次の 2 種類必要です。

  • 人間が使うテクニックを使って問題を解くプログラム
  • 初期のヒントからナンプレのルールを満たす全ての答えを探索するプログラム

1 つ目のプログラムは自動生成した問題の難易度の判定に使用します。ただし、このプログラムは初期のヒントを満たす答えが複数個ある場合に、その一つしか見つけられない可能性があります。答えが複数個存在する問題は正当なナンプレの問題とみなされないので確実に判別して取り除く必要があります。また、上で述べたように、正当な問題であっても 0.5% の問題は解けません。正当な問題を解けない場合があると、初期のヒントとナンプレのルールを満たす答えがそもそも存在しないのか、単にこのプログラムで解けないだけなのか判別できません。よって、このプログラムだけで自動生成をすることはできません。

そこで 2 つ目のプログラムを用意します。このプログラムに必要な要件は次の 2 つです。

  • 正当な問題はすべて解くことができる
  • 初期のヒントとナンプレのルールを満たす答えを全て見つけることができる

puzzle.dev ではこれらの要件を満たすプログラムの実装に Sat Solver と呼ばれるソフトウェアを使用しています。

Sat Solver の使用場所

Sat Solver 自体について説明する前に Sat Solver の使用場所を下の図に従って説明します。

SatSolverの使用場所
SatSolverの使用場所
まず 1 のナンプレのルールを満たす数字の配置を探索する際に Sat Solver を使用しています。ちなみに、ナンプレのルールを満たす数字の配置は 6,670,903,752,021,072,936,960通りあるそうです(参考: ■数独の解は何通りか?: ガスコン研究所)。
次に、ヒントとなる数字を配置が点対称になるようにピックアップします。ヒントの配置が何かしらの対称性を持っているのはナンプレ業界の暗黙の了解でヒントの配置にこだわる人もいます。
最後に、もう一度 Sat Solver を使用してヒントとナンプレのルールを満たす全ての答えを探索します。図では赤い数字の位置が異なる 2 つの答えが見つかります。これは正当な問題ではないので、再度 2 のヒントのピックアップからやり直します。答えが 1 つしかない問題が見つかれば正当な問題として採用します。

Sat Solver とは

Sat Solver は充足可能性問題を高速に解くことに特化したプログラムです。
充足可能性問題とは、変数と、否定  \lnot、論理和  \lor、論理積  \land から構成される論理式を与えらえれた時に、論理式全体を True にするような変数の True もしくは False の割り当てが存在するかどうかを問う問題です。
私が使用した Sat Solver の実装のひとつ MiniSat は論理式を連言標準形で受け取ります。連言標準形は以下のように構成されます。

  • 変数  x,またはその否定  \lnot xリテラルと呼ぶ
  • リテラルを論理和  \lor で結合した論理式をと呼ぶ
  • 節を論理積  \land で結合した論理式を連言標準形と呼ぶ

例えば、以下の論理式は連言標準形の例です。
\begin{align*}
\lnot x_{0} \land (x_{1} \lor x_{2})
\end{align*}
この論理式に対しては
\begin{align*}
[ x_{0} \mapsto \rm{False},\, x_{1} \mapsto \rm{True},\, x_{2} \mapsto \rm{True}]
\end{align*}
などが論理式を充足する割り当てです。Sat Solver はこのような変数への割り当てを高速に求めます。
Sat Solver の実装について興味がある方は以下の書籍が参考になるでしょう。

ナンプレに限定すると、Sat Solver は上で説明した仮置きを高速に非常に効率よく実行していると考えられます。

ナンプレのルールを連言標準形で表現する

いくつかの用語を説明なしに使用するので用語の説明で確認してください。

ナンプレを Sat Solver で解くためにはナンプレのルールを連言標準形で表現する必要があります。ナンプレのルールを確認しておきます。

  1. 各セルには数字が 1 つ入ります。
  2. 各行には 1 から 9 の各数字が 1 度ずつ入ります。
  3. 各列には 1 から 9 の各数字が 1 度ずつ入ります。
  4. 太い線で囲まれた各 3x3 の枠内には 1 から 9 の各数字が 1 度ずつ入ります。
  5. 正解は1つだけです。

ルール 1 を連言標準形の形に変換します。
座標が (1, 1) のセルについて考えます。このセルには 1 から 9 の数字が 1 つ入ります。そこで、このセルの数字に対応する変数として 9 つの変数を用意します。
\begin{align*}
q_{1_{(1,1)}},\, q_{2_{(1,1)}},\, q_{3_{(1,1)}},\, q_{4_{(1,1)}},\, q_{5_{(1,1)}},\, q_{6_{(1,1)}},\, q_{7_{(1,1)}},\, q_{8_{(1,1)}},\, q_{9_{(1,1)}}
\end{align*}
この 9 つの変数の中で True が割り当てられた変数に対応する数字がこのセルに入ると解釈します。例えば、以下のような割り当てを Sat Solver がした場合は、数字の 3 がセルに入ると解釈します。
\begin{align*}
[ q_{1_{(1,1)}} \mapsto \rm{False},\, q_{2_{(1,1)}} \mapsto \rm{False},\, q_{3_{(1,1)}} \mapsto \rm{True},\, q_{4_{(1,1)}} \mapsto \rm{False},\, q_{5_{(1,1)}} \mapsto \rm{False},\\
q_{6_{(1,1)}} \mapsto \rm{False},\, q_{7_{(1,1)}} \mapsto \rm{False},\, q_{8_{(1,1)}} \mapsto \rm{False},\, q_{9_{(1,1)}} \mapsto \rm{False} ]
\end{align*}
変数の割り当ての中には、9 つの変数全てに False を割り当てたり複数個の変数に True を割り当てるものも存在するので、そのような割り当てを禁止する必要があります。
9 つの変数全てに False を割り当てる場合はこのセルに入る数字が 1 つもないのでルール 1 に反します。そこで、少なくとも 1 つの変数は True になるという論理式を Sat Solver に与える連言標準形に追加します。追加する論理式は以下の論理式です。
\begin{align*}
(q_{1_{(1,1)}} \lor q_{2_{(1,1)}} \lor q_{3_{(1,1)}} \lor q_{4_{(1,1)}} \lor q_{5_{(1,1)}} \lor q_{6_{(1,1)}} \lor q_{7_{(1,1)}} \lor q_{8_{(1,1)}} \lor q_{9_{(1,1)}})
\end{align*}
9 つの変数全てに False を割り当てるとこの論理式は False になります。すると Sat Solver は連言標準形で与えられた論理式を True にできないので、少なくとも 1 つの変数に True を割り当てます。
次に複数個の変数に True を割り当てることを禁止する論理式を追加します。
まず  q_{1_{(1,1)}} q_{2_{(1,1)}} で考えます。この 2 つの変数が同時に True になることを禁止するためには、2 つの変数に True が割り当てられた時にのみ False になる論理式を連言標準形に追加します。追加する論理式は以下の論理式です。
\begin{align*}
(\lnot q_{1_{(1,1)}} \lor \lnot q_{2_{(1,1)}})
\end{align*}
 q_{1_{(1,1)}} q_{2_{(1,1)}}が同時に True になることは禁止できたので、他の  {}_9 \mathrm{C} _2 - 1 = 35 通りの組み合わせについても論理式を追加します。
以上で、上の論理式と合わせて座標が (1, 1) のセルについてルール 1 の各セルには数字が 1 つ入るという条件を表現できました。
同様に残りの 80 個のセルについても変数と論理式を追加します。

次にルール 2 について考えます。
1 行目の数字の 1 に注目します。つまり、ルール 1 の場合と同様に 1 行目にあるセルの数字 1 に対応する 9 つの変数に注目します。
\begin{align*}
q_{1_{(1,1)}},\, q_{1_{(1,2)}},\, q_{1_{(1,3)}},\, q_{1_{(1,4)}},\, q_{1_{(1,5)}},\, q_{1_{(1,6)}},\, q_{1_{(1,7)}},\, q_{1_{(1,8)}},\, q_{1_{(1,9)}}
\end{align*}
1 行目に 数字の 1 は少なくとも 1 つ入ります。また複数回出てきてはいけません。この条件はルール 1 について考えた場合と同じです。
そこで以下の論理式を追加します。
\begin{align*}
(q_{1_{(1,1)}} \lor q_{1_{(1,2)}} \lor q_{1_{(1,3)}} \lor q_{1_{(1,4)}} \lor q_{1_{(1,5)}} \lor q_{1_{(1,6)}} \lor q_{1_{(1,7)}} \lor q_{1_{(1,8)}} \lor q_{1_{(1,9)}})
\end{align*}
また、 {}_9 \mathrm{C} _2 通りの組み合わせについて以下の論理式を追加します。
\begin{align*}
(\lnot q_{1_{(1,i)}} \lor \lnot q_{1_{(1,j)}})
\end{align*}
これで 1 行目の数字の 1 について、ちょうど 1 回入るという条件を表現できました。同様に、数字 2 から 9 についても追加します。同様に 2 行目から 9 行目についても条件を追加します。
以上でルール 2 を連言標準形に追加できました。

ルール 3 とルール 4 についてもルール 2 と同様に表現できます。
この状態で Sat Solver に可能な割り当てを求めさせると先に述べた 6,670,903,752,021,072,936,960 通りの配置のうちのどれかに対応する割り当てを返します。

ナンプレの問題を Sat Solver で解く

初期のヒントがすでに入っているナンプレの問題を Sat Solver で解くための手順を下の例を使って説明します。

Sat で解く問題例
Sat で解く問題例
問題例の座標が (1, 1) のセルを見ると数字の 6 が入っています。これは変数  q_{6_{(1,1)}} に True が割り当てられている状態だと考えます。
Sat Solver に対して  q_{6_{(1,1)}} に必ず True を割り当てるように強制するためにはナンプレのルールを表現する連言標準形に変数をそのまま追加します。
\begin{align*}
(\text{ナンプレのルールを表現する論理式}) \land q_{6_{(1,1)}}
\end{align*}
 q_{6_{(1,1)}} に False を割り当てると Sat Solver は連言標準形で与えられた論理式を True にできないので、必ず q_{6_{(1,1)}}に True を割り当てます。
同様に他のヒントについても対応する座標の対応する変数を連言標準形に追加していきます。
\begin{align*}
(\text{ナンプレのルールを表現する論理式}) \land q_{6_{(1,1)}} \land q_{5_{(1,2)}} \land q_{4_{(1,7)}} \land \dots \land q_{7_{(9,9)}}
\end{align*}
この論理式を True にする割り当てを Sat Solver が見つければ、それがこの問題の答えです。

答えが 1 つしかないことを Sat Solver で確認する

上の例題に対する論理式を True にする割り当てを探索すると下の答えが見つかります。

Sat で解く問題例の答え
Sat で解く問題例の答え
現状では、この数字の配置が初期のヒントと数独のルールを満たす答えの 1 つであるということしか確認できていません。これがただ 1 つの答えであることを確認する必要があります。そのために、問題を解いた時の論理式に見つけた答えに対応する割り当てを禁止する論理式を追加して再度 Sat Solver で問題を解きます。
追加する論理式は以下のようになります。
\begin{align*}
\lnot (q_{6_{(1, 1)}} \land q_{5_{(1,2)}} \land q_{9_{(1,3)}} \land \dots \land q_{3_{(9,8)}} \land q_{7_{(9,9)}})
\end{align*}
この論理式のままでは連言標準形の論理式に追加できないのでド・モルガンの法則を用いて以下のように変形します。
\begin{align*}
(\lnot q_{6_{(1, 1)}} \lor \lnot q_{5_{(1,2)}} \lor \lnot q_{9_{(1,3)}} \lor \dots \lor \lnot q_{3_{(9,8)}} \lor \lnot q_{7_{(9,9)}})
\end{align*}
この論理式は、見つけた答えに対応する割り当てと全く同じ割り当てをした場合にのみ False になります。Sat Solver に与える論理式は以下になります。
\begin{align*}
(\text{ナンプレのルールを表現する論理式}) \land (\text{ヒントに対応する論理式}) \land \\
(\lnot q_{6_{(1, 1)}} \lor \lnot q_{5_{(1,2)}} \lor \lnot q_{9_{(1,3)}} \lor \dots \lor \lnot q_{3_{(9,8)}} \lor \lnot q_{7_{(9,9)}})
\end{align*}
Sat Solver は論理式全体を True にするために先ほど見つけた割り当てとは違う割り当てを探索します。新たな割り当てが見つかれば答えが複数個存在することになるので、その問題は正当なナンプレの問題ではありません。新たな割り当てが見つからなければ正当な問題として採用します。

連言標準形への変換

Sat Solver は連言標準形の形の論理式しか受け付けてくれないので、解きたい問題を連言標準形の論理式に変換する必要があります。そこが難しいと感じた人も多いと思いますが、私はこの変換作業こそ面白いと感じます。ここでは変換の際に使えるテクニックを紹介します。
問題によっては、論理記号のならば  \Rightarrow を使って考えた方が考えやすい場合もあります。
\begin{align*}
X \Rightarrow Y
\end{align*}
は以下の論理式と同値なので変換は簡単にできます。
\begin{align*}
\lnot X \lor Y
\end{align*}
以下の論理式はどうでしょうか。
\begin{align*}
(X_{1} \wedge Y_{1})\vee (X_{2}\wedge Y_{2})\vee \dots \vee (X_{n}\wedge Y_{n})
\end{align*}
これを分配法則を用いて連言標準形の形に変換すると  2^{n} 個の節に変換されます。Sat Solver は非常に高速なのですが、節の数が多くなるとそれだけ計算に時間がかかるようになります。
実は、上の論理式を節の数が少ない論理的同値な論理式に変換する手法としてTseitin 変換という手法が知られています。
まずは、連言標準形の形にこだわらずに問題を論理式に変換した後でこれらの手法を用いて連言標準形に変換すると変換しやすくなります。

Sat Solver の応用例

ナンプレのルールは連言標準形に変換しやすい問題です。私はCalcBlocksを作成する際に以下のパズルも Sat Solver を用いて自動生成するプログラムを作成しています。
Sat Solver に習熟したい人はぜひこれらのパズルについても自動生成 + 答えの探索に挑戦してください。抽象的な問題を論理式に変換するとてもいい練習になります。

計算ブロック

  • 各行、各列には 1 から 4 の各数字が1度ずつ入ります。
  • 数字と演算子は各領域の和(+)、大きい数と小さい数の差(-)、積(×)、大きい数を小さい数で割った商(÷)、大きい数を小さい数で割った余り(%) を表しています。
  • 正解は 1 つだけです。

計算ブロック
計算ブロック

ビルディングパズル

  • 高さが 1 から 4 のビルを上から見ています。
  • 各行、各列にはビルの高さを表す 1 から 4 の各数字が1度ずつ入ります。
  • 枠の外の数字はその方向から見えるビルの数を表しています。
  • 正解は 1 つだけです。

ビルディングパズル
ビルディングパズル

ナンバーリンク

  • 同じ数字どうしを 1 本の線でつなぎます。
  • それぞれの線は枝分かれしたり、交わったりしてはいけません。
  • それぞれのマスを通過する線は 1 本だけです。また空白のマスはありません。
  • 正解は1つだけです。

ナンバーリンク
ナンバーリンク

スリザーリンク

  • 点と点を線でつなぎ、全体で 1 つの閉じた輪をつくります。
  • 4 つの点で作られた正方形の中にある数字は、その正方形の辺に引く線の数を表しています。数字のない正方形には何本の線を引くかわかりません。
  • 線を交差させたり、枝分かれさせたりしてはいけません。
  • 正解は 1 つだけです。

スリザーリンク
スリザーリンク

対称性を用いた問題の複製

ナンプレの問題を 1 つ見つけた後で Sat Solver のように計算のコストが高い処理をせずに別のナンプレの問題を作ることは可能でしょうか?
ヒントの数字を好き勝手移動すると正解のない問題や正解が複数ある問題になる可能性があります。するともう一度 Sat Solver で確認する必要があります。一方で次の例のように、ヒントの数字全体を同時に 90 度回転した問題は、正解も 90 度回転したものになるので正当なナンプレの問題になります。

ガンマ変換
問題の 90 度回転
90 度の回転のように特定の規則に従ってヒントの数字を移動してできた問題は、再度チェックしなくても新しい問題として使えそうです。ではこのような移動にはどのようなものがいくつあるでしょうか?

わかりやすくするために 4 つの角に数字を振った正方形を考えます。この 4 つの数字を何らかの対称性に従って移動する方法には以下の方法があります。

対称変換リスト
対称変換リスト
それぞれの対称性に従った移動を次のように名付けます。

  • 点対称による移動は  \delta 変換
  • 線対称による上下移動は  \alpha 変換
  • 線対称よる右上と左下の数字の移動を  \beta 変換
  • 回転対称にる 90 度の回転移動を  \gamma 変換

図では 1 度の移動しか行なっていませんが続けて複数回の移動をする場合も考えます。この時、初めの配置から複数回の変換を行うことでたどり着くことができる数字の配置をすべて求めます。これは数学的には以下のように表現されます。

 \alpha,\beta,\gamma,\delta 変換によって生成される群の位数を求めよ

それぞれの変換の間には以下の等式が成り立ちます。変換を全く行わない場合を恒等変換と呼び  \bf{Id} で表します。
\begin{align*}
\alpha^{2} &= \bf{Id} \\
\beta^{2} &= \bf{Id} \\
\gamma^{4} &= \bf{Id} \\
\delta^{2} &= \bf{Id} \\
\gamma^{2} &= \delta \\
\alpha \beta &= \gamma \\
\beta \alpha &= \gamma^{3} \\
\alpha \gamma &= \beta \\
\gamma \alpha &= \gamma^{2} \beta = \beta \gamma^{2} \\
\beta \gamma &= \alpha \gamma^{2} = \gamma^{2} \alpha \\
\gamma \beta &= \alpha
\end{align*}

この等式を用いて全ての変換を  \alpha 変換と  \beta 変換だけで表すと以下の 8 つになります。
 \{ \bf{Id}, \alpha, \beta, \alpha \beta, \beta \alpha, \alpha \beta \alpha, \beta \alpha \beta, \alpha \beta \alpha \beta \}
それそれの変換に対応する数字の位置は以下の通りです。

変換に対応する数字の配置
変換に対応する数字の配置
結論として、1 つナンプレの問題が見つかるとその問題から追加で 7 つの問題を変換のコストだけで作成できます。
ただし、元の問題が正当なナンプレの問題であるときに、 \alpha 変換等を適用した後の問題も正当なナンプレの問題になっていることを証明しないといけません。正当なナンプレの問題が満たすべき論理式を正確に定義した上で証明をしてみてください。

大学数学の個別指導を始めます

はじめに

圏論に最短で入門する - 俺の Colimit を越えてゆけ の中で以下のように書きました。

数学にもともと興味があって数学科に進学した学生でも、大学以降で学ぶ数学についていけなくて挫折してしまう人は多いようです。私の考えでは、

  • 大学受験までの計算主体の数学から、大学以降の証明主体の数学への移行を明確に意識させること
  • 移行のためのトレーニングを積ませること

を学生が認識できる形で教育機会として大学が提供できていないことが原因なのではないかと考えています。

このブログを初めて以来、何人かの学生の方から数学の学習について相談を受けています。彼らと話をしているとどうも証明主体の数学の勉強を進める上での基礎が十分ではないように感じます。結果、数学の勉強の進め方、勉強の仕方に問題を抱えているように感じました。

私も数学の勉強を始めた当初は同じ問題を抱えていました。当時私が感じていた問題は次ようのなものです。

  • 何度も教科書を読み返して内容を記憶しようとはするのだけど、単なる暗記になってしまっていて理解した気になれない
  • 証明を読んでもその証明が本当に正しいのか自分で検証することができない
  • 練習問題を自分で解くことができないので、ほとんどの練習問題は解かずに飛ばし読みしてしまう
  • 練習問題を解いてみても、解答がないあるいは解答が一語一句自分の証明と一致していないと自分の証明が合っているのかどうか確信がもてない

大学の証明主体の数学に触れて、私と同じような問題を感じている人は多いのではないでしょうか。大学院に進みたいと思っていても、このような状態だと院試に合格できるかどうかも不安ですよね。

私もしばらくはこのような問題を感じながら勉強を続けていたのですが、あるきっかけによってこの問題を解決し、その後圏論を理解できる程度にまで数学を独学することができるようになりました。Steve Awodey の Category Theory を読む - 俺の Colimit を越えてゆけ を見ていただければ、教科書やネットの他のサイトには載っていない詳細な証明がなされているのが確認できると思います。それらの証明は私が自分で考えて構成したものであり、その正しさについても 100% 確信して書いています。みなさんにも私と同程度の能力を身につけてもらいたいと思っています。

そこで、昔の私と同じ問題を抱えている人に私の経験を伝えるために数学の個別指導を始めようと思います。一人でも多くの数学徒が数学の学習に関しての不安を解消し、数学を楽しめるようになることの一助になれれば幸いです。個別指導を始めようと思った一番の理由は、いよいよ私の貯金残高がやばくなってきたからです

個別指導を受けた結果あなたが得られるもの

突然ですが問題です。

ここに白いボールだけが入った袋があります。この袋から任意に一つボールを取り出した時、そのボールが白いことを証明しなさい。

問題を読んで何をしたらいいのかわからなかった人、あるいは、わかった風を装おうとして「定義より明らかだろjk」と思った人は私の個別指導を受けると学ぶところがあると思います。

大学数学の教科書では、定義や定理は上の問題のように自然言語で記述されています。数学の学習を進める際には、自然言語で書かれた定義や定理を論理式として表現し、許された手順のみを用いて具体的に証明を構成する必要があります。上の問題を読んで何をすればいいのかわからなかった人、「定義より明らかだろ」で済まそうとした人は数学書を読んでいる時にも、この必要な手順をこなさずにあたかも小説を読むかのように数学書を読んでいる可能性があります。

私の個別指導では、自然言語で書かれた定義や定理を論理式として表現し、許された手順のみを用いて具体的に証明を構成する能力を身につけるための指導をします。能力が身につけば、上の問題も実際に証明することができるようになります。

内容

はじめに基礎的な講義を行います。その後に、松坂の集合・位相入門もしくは代数系入門を用いて、定義、定理の証明、練習問題などを一つずつ証明しながら読み進めます。
書籍を通読することが目的ではなく、読むことを通して上の能力を身につけることが目的です。週 1 回、2–3 時間の講義で 6 ヶ月程度講義を受けてもらえば、上の能力は身につくと思います。

集合・位相入門

集合・位相入門

代数系入門

代数系入門

受講するかどうか悩んでいる人へ

ここまで読んでみて受講してみたいなと思っていても、値段も決して安くないし、本当に自分が求めている内容を教えてもらえるのだろうか?

と考えられていると思います。そこで、はじめの 1 日 2 時間分を体験授業ということで無料で受講可能にします。体験授業を受けてみて、続けて見ようかなと思った場合のみ引き続き受講していただきます。やっぱりやめておこうと思えば、お代をいただくことはありません。

ぜひお気軽に体験授業を受けてみてください。

詳細

対象

大学数学を先取りしたい高校生・大学生・社会人

場所

基本は京都市内の図書館やカフェ、セミナールームの予定です。
もし関東方面の方の希望が多ければ、曜日を限定して東京に私が行きます。関東方面の方で希望の方は、希望だけでもお伝えいただけると嬉しいです。

時給

7500 円/h 1 回 2 時間以上
複数人同時受講の場合は割引します

期間

週 1 回の場合は 6 ヶ月
週 2 回の場合は 3 ヶ月
計 50 時間程度

人数

複数人(1–3 人)の同時受講も可

連絡先

メールアドレス: takuya.0101 at gmail.com

補足

私は数学の研究者や数学科卒ではありません。私の最終学歴は東京大学情報理工学系研究科創造情報学専攻修士で、コンピュータ系の人です。
コンピュータ科学の研究に必要性を感じて数学の勉強を 30 歳を超えてから開始し、大学数学の学習時間は 5000 時間程度だと思います。よって、数学の特定の分野に関する専門知識を要求されても困ります。あくまでも、初心者よりは少しだけ数学の素養があるおじさんだと考えてください。

Steve Awodey の Category Theory を読む : Chapter 10

Steve Awodey の Category Theory を読む シリーズトップ

10.2 Monads and adjoints

Example 10.5

Exercise 6 と同様の表記を採用すると、任意の  f \colon X \to Y と任意の  U \in \mathcal{P}(X) に対して  \mathcal{P}(f)(U) = \left\{ f(x) \in Y \,\middle|\, x \in U \right\} と表せる。また任意の  \alpha \in \mathcal{PP}(X) に対して  \bigcup(\alpha) = \left\{ x \in X \,\middle|\, \exists U \in \alpha,\, x \in U \right\} と表せることに注意して以下を証明する。

 Lemma
\begin{equation}
(\mathcal{P}, \{-\}, \bigcup) \text{ is a monad on } {\bf{Sets}}. 
\end{equation}

 Proof.

  •  \eta \colon 1 \to \mathcal{P} が natural であること

任意の  f \colon X \to Y に対して以下の diagram を考える。
f:id:hitotakuchan:20161102131405p:plain

すると、任意の  x \in X に対して  \left( \mathcal{P}(f) \circ \eta_{X} \right)(x) = \left\{ f(x) \right\} = \left( \eta_{Y} \circ f \right)(x) が成り立つ。よって diagram は可換になる。

  •  \mu \colon \mathcal{PP} \to \mathcal{P} が natural であること

任意の  f \colon X \to Y に対して以下の diagram を考える。
f:id:hitotakuchan:20161102132128p:plain

任意の  \alpha \in \mathcal{PP}(X) に対して

\begin{align*}
\left( \mathcal{P}(f) \circ \mu_{X} \right)(\alpha) &= \mathcal{P}(f) \left( \left\{ x \in X \,\middle|\, \exists U \in \alpha,\, x \in U \right\} \right) \\
&= \left\{ f(x) \in Y \,\middle|\, \exists U \in \alpha,\, x \in U \right\}
\end{align*}

が成り立つ。一方、

\begin{align*}
\left( \mu_{Y} \circ \mathcal{PP}(f) \right)(\alpha) &= \mu_{Y} \left( \left\{ \mathcal{P}(f)(U) \,\middle|\, U \in \alpha \right\} \right) \\
&= \left\{ y \in Y \,\middle|\, \exists U' \in \left\{ \mathcal{P}(f)(U) \,\middle|\, U \in \alpha \right\},\, y \in U' \right\} \\
&= \left\{ y \in Y \,\middle|\, \exists U \in \alpha,\, y \in \mathcal{P}(f)(U) \right\} \\
&= \left\{ y \in Y \,\middle|\, \exists U \in \alpha,\, y \in \left\{ f(x) \in Y \,\middle|\, x \in U \right\} \right\} \\
&= \left\{ f(x) \in Y \,\middle|\, \exists U \in \alpha,\, x \in U \right\}
\end{align*}

が成り立つ。よって diagram は可換になる。

  • 結合則を満たすこと

任意の  X \in {\bf{Sets}} に対して以下の diagram が可換になることを示せばよい。
f:id:hitotakuchan:20161103072530p:plain

任意の  \beta \in \mathcal{PPP}(X) に対して

 \begin{align*}
\left( \mu_{X} \circ \mathcal{P}\mu_{X} \right)(\beta) &= \mu_{X} \left( \left\{ \mu_{X}(\alpha) \,\middle|\, \alpha \in \beta \right\} \right) \\
&= \left\{ x \in X \,\middle|\, \exists U \in \left\{ \mu_{X}(\alpha) \,\middle|\, \alpha \in \beta \right\},\, x \in U \right\} \\
&= \left\{ x \in X \,\middle|\, \exists \alpha \in \beta,\, x \in \mu_{X}(\alpha) \right\} \\
&= \left\{ x \in X \,\middle|\, \exists \alpha \in \beta,\, U \in \alpha,\, x \in U \right\}
\end{align*}

が成り立つ。一方、

 \begin{align*}
\left( \mu_{X} \circ \mu_{\mathcal{P}X} \right)(\beta) &= \mu_{X} \left( \left\{ U \in \mathcal{P}(X) \,\middle|\, \exists \alpha \in \beta,\, U \in \alpha \right\} \right) \\
&= \left\{ x \in X \,\middle|\, \exists U' \in \left\{ U \in \mathcal{P}(X) \,\middle|\, \exists \alpha \in \beta,\, U \in \alpha \right\},\, x \in U' \right\} \\
&= \left\{ x \in X \,\middle|\, \exists \alpha \in \beta,\, U \in \alpha,\, x \in U \right\}
\end{align*}

が成り立つので diagram は可換になる。

  • 単位則を満たすこと

任意の  X \in {\bf{Sets}} に対して以下の diagram が可換になることを示せばよい。
f:id:hitotakuchan:20161103074643p:plain

任意の  U \in \mathcal{P}(X) に対して左の triangle に関して

 \begin{align*}
\left( \mu_{X} \circ \eta_{\mathcal{P}X} \right)(U) &= \mu_{X} \left( \left\{ U \right\} \right) \\
&= \left\{ x \in X \,\middle|\, \exists U' \in \left\{ U \right\},\, x \in U' \right\} \\
&= U
\end{align*}

が成り立つ。次に右の triangle に関して

 \begin{align*}
\left( \mu_{X} \circ \mathcal{P}\mu_{X} \right)(U) &= \mu_{X} \left( \left\{ \left\{ x \right\} \,\middle|\, x \in U \right\} \right) \\
&= \left\{ x' \in X \,\middle|\, \exists U' \in \left\{ \left\{ x \right\} \,\middle|\, x \in U \right\},\, x' \in U' \right\} \\
&= \left\{ x \in X \,\middle|\, x \in U \right\} \\
&= U
\end{align*}

が成り立つので diagram は可換になる。

 \square

10.3 Algebras for a monad

Example 10.7

free monoid adjunction に対する monad を  (T, \eta, \mu) とすると、 {\bf{Mon}} \cong {\bf{Sets}}^{T} が成り立つことを示します。

 Lemma
 {\bf{Mon}} \cong {\bf{Sets}}^{T}

 Proof.
はじめに  \Phi \colon {\bf{Mon}} \to {\bf{Sets}}^{T} を定義する。
任意の monoid  (M, u_{M}, \cdot_{M}) に対して  \Phi\left( (M, u_{M}, \cdot_{M}) \right) = (M, \alpha) と定義する。ただし  \alpha \alpha( [ m_{1}, \dots , m_{n}] ) = m_1 \cdot_{M} \dots \cdot_{M} m_{n} を満たす関数とする。このとき書籍にあるように  (M, \alpha) T-algebra となる。
また任意の monoid homomorphism  h \colon (M, u_{M}, \cdot_{M}) \to (N, u_{N}, \cdot_{N}) に対して以下の diagram を考える。
f:id:hitotakuchan:20161106133829p:plain

任意の  [m_{1}, \dots, m_{n}] \in TM に対して  (\beta \circ Th)( [m_{1}, \dots, m_{n}] ) = h(m_{1}) \cdot_{N} \dots \cdot_{N} h(m_{n}) が成り立つ。一方、 (h \circ \alpha)([m_{1}, \dots, m_{n}]) = h(m_{1} \cdot_{M} \dots \cdot_{M} m_{n}) が成り立つが  h が monoid homomorphism であることから両者は等しい。
そこで  \Phi(h) = h \colon (M, \alpha) \to (N, \beta) で定義する。すると  \Phi が functor の条件を満たすことは明らかである。

次に  \Psi \colon {\bf{Sets}}^{T} \to {\bf{Mon}} を定義する。
任意の  (A, \alpha) に対して  u_{A} = \alpha([]) \cdot_{A} = \alpha([-,-]) とするとき、 \Psi\left( (A, \alpha) \right) = (A, u_{A}, \cdot_{A}) で定義する。このとき  (A, u_{A}, \cdot_{A}) が monoid となることを示す。
任意の  a,b,c \in A に対して
 \begin{align*}
a \cdot_{A} (b \cdot_{A} c) &= \alpha \left(  \left[ a, \alpha( [b, c] ) \right] \right) \\
&= \alpha \left( \left[ \alpha([a]), \alpha( [ b, c ] ) \right] \right) \\
&= ( \alpha \circ T\alpha) \left( \left[ [ a ], [b, c] \right] \right) \\
&= (\alpha \circ \mu) \left( \left[ [ a ], [b, c] \right] \right) \\
&= \alpha \left( [ a, b, c ] \right)
\end{align*}

一方、

 \begin{align*}
(a \cdot_{A} b) \cdot_{A} c &= \alpha \left( \left[ \alpha( [a, b]), c \right] \right) \\
&= \alpha \left( \left[ \alpha( [a, b]), \alpha([c]) \right] \right) \\
&= (\alpha \circ T\alpha) \left( \left[ [a, b], [c] \right] \right) \\
&= (\alpha \circ \mu) \left( \left[ [a, b], [c] \right] \right) \\
&= \alpha \left([a, b, c] \right)
\end{align*}

が成り立つので、 \cdot_{A} は結合則を満たす。また

 \begin{align*}
u_{A} \cdot_{A} a &= \alpha \left( \left[ \alpha([]), a \right] \right) \\
&= \alpha \left( \left[ \alpha([ ]), \alpha([a]) \right] \right) \\
&= (\alpha \circ T\alpha) \left( \left[ [ ], [a] \right] \right) \\
&= (\alpha \circ \mu) \left( \left[ [ ], [a] \right] \right) \\
&= \alpha ([a]) \\
&= a
\end{align*}

が成り立つ。同様に  a \cdot_{A} u_{A} = a が成り立つので  \cdot_{A} は 単位則を満たす。以上より  (A, u_{A}, \cdot_{A}) は monoid となる。
また任意の  h \colon (A, \alpha) \to (B, \beta) と任意の  a, b \in A に対して、

 \begin{align*}
h(a \cdot_{A} b) &= h \left( \alpha([ a,b]) \right) \\
&= (h \circ \alpha)([a, b]) \\
&= (\beta \circ Th)([a,b]) \\
&= h(a) \cdot_{B} h(b)
\end{align*}

が成り立ち、同様に  h(u_{A}) = u_{B} が成り立つので、 h は monoid homomorphism となる。そこで  \Psi(h) = h \colon (A, u_{A}, \cdot_{A}) \to (B, u_{B}, \cdot_{B}) とすれば  \Psi は明らかに functor の条件を満たす。

最後に、 \Psi \circ \Phi = 1_{\bf{Mon}} かつ  \Phi \circ \Psi = 1_{{\bf{Sets}}^{T}} が成り立つので  {\bf{Mon}} \cong {\bf{Sets}}^{T} が成り立つ。

 \square

10.4 Comonads and coalgebras

任意のadjoint pair  F \dashv U に対して unit を  \eta \colon 1_{\bf{C}} \to UF、counit を  \epsilon \colon FU \to 1_{\bf{D}} とするとき、 (G = FU, \epsilon, \delta = F\eta_{U}) が comonad となることを確認します。

 Lemma
 (G, \epsilon, \delta) \text{ is a comonad}.

 Proof.
10.2 節と同様に証明する。

  • coassociativity law が成り立つこと

任意の  f \colon X \to Y \in {\bf{C}} に対して  \eta が natural であることより、以下の diagram が可換になる。
f:id:hitotakuchan:20161107125109p:plain

 Y UFX f \eta_{X} で置き換えると、以下の diagram を得る。
f:id:hitotakuchan:20161107125424p:plain

 X UD として、全体に  F を適用すると以下の diagram を得る。
f:id:hitotakuchan:20161107125820p:plain

記号を置き換えると以下の diagram が可換となる。
f:id:hitotakuchan:20161107130311p:plain

  • counit law が成り立つこと

次の diagram が可換になることを示せばよいが、これは triangle identities より明らかである。
f:id:hitotakuchan:20161107131043p:plain

 \square

10.5 Algebras for endofunctors

Lemma 10.10

任意の endofunctor  P \colon \mathcal{S} \to \mathcal{S} に関して次の事柄が成り立つことを証明します。

 Lemma
 i \colon P(I) \to I \text{ is an initial } P\text{-algebra} \Rightarrow i \text{ is an isomorphism}.

 Proof.
 i が initial  P-algebra であることより、次の diagram が可換となるような  j \colon I \to P(I) がただ一つ存在する。
f:id:hitotakuchan:20161108142551p:plain

そこで以下の diagram を考える。
f:id:hitotakuchan:20161108142956p:plain

明らかに diagram は可換になるので、 i が initial であることより  i \circ j = 1_{I} が成り立つ。
そこでもう一度以下の diagram を考えると
f:id:hitotakuchan:20161108142551p:plain

 j \circ i = P(i) \circ P(j) = P(1_{I}) = 1_{P(I)} が成り立つ。よって  i は isomorphism である。

 \square

Corollary 10.13

任意の finite polynomial functor  P \colon {\bf{Sets}} \to {\bf{Sets}} \omega-colimit を保存することを証明します。

 Lemma
 P \text{ preserves } \omega \text{-colimits}.

 Proof.
index category  \omega に対しては
 \varinjlim_{n} \dashv \Delta_{n} \dashv \varprojlim_{n}

が成り立つこと、また、任意の集合  J に対しては

 \sum_{J} \dashv \Delta_{J} \dashv \prod_{J}

が成り立つことに注意する。
polynomial functor  P P(X) = \sum_{i \in I} C_{i} \times X^{B_{i}} で表すと、任意の  D \colon \omega \to \bf{Sets} に対して、証明するべきことは  P \left( \varinjlim_{n} D_{n} \right) = \sum_{I} C_{i} \times \left( \varinjlim_{n} D_{n} \right)^{B_{i}} \cong \varinjlim_{n} \left( \sum_{I} C_{i} \times D_{n}^{B_{i}} \right) = \varinjlim_{n} P(D_{n}) である。
任意の  X \in \bf{Sets} に対して
 \begin{align*}
\text{Hom}\left( \sum_{I} C_{i} \times \left( \varinjlim_{n} D_{n} \right)^{B_{i}}, X \right) &\cong \text{Hom} \left( C_{i} \times \left(\varinjlim_{n} D_{n} \right)^{B_{i}}, \Delta_{I} X \right) \\
&\cong \text{Hom} \left( \left(\varinjlim_{n} D_{n} \right)^{B_{i}}, \Delta_{I} X^{C_{i}} \right) \\
&\cong \text{Hom} \left( \varinjlim_{n} D_{n}^{B_{i}}, \Delta_{I} X^{C_{i}} \right) \\
&\cong \varprojlim_{n} \text{Hom} \left( D_{n}^{B_{i}}, \Delta_{I} X^{C_{i}} \right) \\
&\cong \varprojlim_{n} \text{Hom} \left( C_{i} \times D_{n}^{B_{i}}, \Delta_{I} X \right) \\
&\cong \varprojlim_{n} \text{Hom} \left( \sum_{I} C_{i} \times D_{n}^{B_{i}}, X \right) \\
&\cong \text{Hom} \left( \varinjlim_{n} \left( \sum_{I} C_{i} \times D_{n}^{B_{i}} \right), X \right) \\
\end{align*}

が成り立つ。これらの同型射は adjoint pair の同型射であるから Chapter8 で証明した内容と合わせると  X に関して natural である。
よって米田の補題より  \sum_{I} C_{i} \times \left( \varinjlim_{n} D_{n} \right)^{B_{i}} \cong \varinjlim_{n} \left( \sum_{I} C_{i} \times D_{n}^{B_{i}} \right) が成り立つ。

 \square

参考書籍

Category Theory (Oxford Logic Guides)

Category Theory (Oxford Logic Guides)

  • 作者:Awodey, Steve
  • 発売日: 2008/01/10
  • メディア: ペーパーバック
圏論 原著第2版

圏論 原著第2版

Steve Awodey の Category Theory を読む : Chapter 9

Steve Awodey の Category Theory を読む シリーズトップ

9.1 Preliminary definition

Example 9.3

 F \colon {\bf{Pos}} \to \mathcal{C}{\bf{Pos}} F_{0}(P) = \left\{ U \subseteq P \ \middle| \ p' \leq p \in U \text{ implies } p' \in U \right\} で定義した時、 F が forgetful functor  U の left adjoint となることを証明します。はじめに  F_{0} の定義が well-defined であることを証明します。

 Lemma
 F_{0} \text{ is well-defined}.

 Proof.
任意の  P \in {\bf{Pos}} に対して  F_{0}(P) が cocomplete poset となることを示せばよい。 F_{0}(P) \subseteq を順序として入れると poset になることは明らかであるから、  F_{0}(P) が cocomplete になることを示す。
任意の index set  I に対して  \bigcup_{i \in I} U_{i} \in F_{0}(P) となることを示せばよい。任意の  a \in \bigcup_{i \in I} U_{i} と任意の  a' \leq a に対して  a \in \bigcup_{i \in I} U_{i} より  \exists i \in I,\ a \in U_{i} が成り立つ。 U_{i} \in F_{0}(P) であるから、 F_{0}(P) の定義より  a' \in U_{i} が成り立つ。よって  a' \in \bigcup_{i \in I} U_{i} が成り立つので  \bigcup_{i \in I} U_{i} \in F_{0}(P) が成り立つ。

 \square

次に、任意の  f \colon P \to Q \in {\bf{Pos}} に対して  F_{1}(f) を定義する必要があります。その前に、任意の  p \in P に対して  p\!\downarrow p\!\downarrow \,= \left\{ p' \in P \ \middle|\ p' \leq p \right\} と定義するとき、次のことが成り立つことを証明します。

 Lemma
 U \in F_{0}(P) \Rightarrow U = \bigcup_{p \in U} p\!\downarrow

 Proof.
任意の  a \in U に対して  a \in a\!\downarrow であるから  a \in \bigcup_{p \in U} p\!\downarrow が成り立つ。
逆に  a \in \bigcup_{p \in U} p\!\downarrow とすると  \exists p,\ a \in p\!\downarrow が成り立つので  a \leq p が成り立つ。すると  U \in F_{0}(P) であることから  a \in U が成り立つ。

 \square

上の事実をもとに、任意の  f \colon P \to Q \in {\bf{Pos}} と任意の  U \in F_{0}(P) に対して  F_{1}(f) F_{1}(f)(U) = F_{1}(f)\left( \bigcup_{p \in U} p\!\downarrow \right) = \bigcup_{p \in U} f(p)\!\downarrow で定義します。このとき  F_{1} が well-defined であることを証明します。

 Lemma
 F_{1} \text{ is well-defined}.

 Proof.
任意の  f \colon P \to Q と任意の  U \in F_{0}(P) に対して  F_{1}(f)(U) = \bigcup_{p \in U} f(p)\!\downarrow \in F_{0}(Q) となることを示せばよい。
任意の  q \in \bigcup_{p \in U} f(p)\!\downarrow と任意の  q' \leq q に対して、 \exists p \in U,\ q \in f(p)\!\downarrow が成り立つから、 q' \leq q なら  q' \in f(p)\!\downarrow となり  q' \in \bigcup_{p \in U} f(p)\!\downarrow が成り立つ。よって  \bigcup_{p \in U} f(p)\!\downarrow \in F_{0}(Q) である。

 \square

このとき、証明は省略しますが  F \colon {\bf{Pos}} \to \mathcal{C}{\bf{Pos}} は functor の条件 (a), (b), (c) を満たすので functor となります。

次に  F が forgetful functor  U の left adjoint となることを証明します。はじめに、任意の  f \colon P \to U(\mathcal{C}) に対して  \overline{f} \colon F(P) \to \mathcal{C} を任意の  U \in F(P) に対して  \overline{f}(U) = \bigvee_{p \in U} f(p) で定義します。このとき  \overline{f} が monotone かつ cocontinuous であることを証明します。

 Lemma
 \overline{f} \text{ is monotone and cocontinuous}.

 Proof.

  • monotone であること

任意の  U' \subseteq U に対して  \bigvee_{p' \in U'} f(p') \leq \bigvee_{p \in U} f(p) を示せばよい。任意の  p' \in U' に対して  p' \in U であるから、 f(p') \leq \bigvee_{p \in U} f(p) が成り立つので colimit の UMP より  \bigvee_{p' \in U'} f(p') \leq \bigvee_{p \in U} f(p) が成り立つ。

  • cocontinuous であること

任意の index set  I に対して  \overline{f}\left( \bigcup_{i \in I} U_{i} \right) = \bigvee_{i \in I} \overline{f}(U_{i}) が成り立つことを示せばよい。定義よりこれは  \bigvee_{a \in \bigcup_{i \in I} U_{i}} f(a) = \bigvee_{i \in I} \bigvee_{a \in U_{i}} f(a) と同値である。
任意の  a \in \bigcup_{i \in I} U_{i} に対して  f(a) \leq \bigvee_{i \in I} \bigvee_{a \in U_{i}} f(a) が成り立つので、colimit の UMP より  \bigvee_{a \in \bigcup_{i \in I} U_{i}} f(a) \leq \bigvee_{i \in I} \bigvee_{a \in U_{i}} f(a) が成り立つ。
一方、任意の  i \in I と任意の  a \in U_{i} に対して  f(a) \leq \bigvee_{a \in \bigcup_{i \in I} U_{i}} f(a) が成り立つので、colimit の UMP より  \bigvee_{i \in I} \bigvee_{a \in U_{i}} f(a) \leq \bigvee_{a \in \bigcup_{i \in I} U_{i}} f(a) が成り立つ。

 \square

次に  \eta \colon 1_{\bf{Pos}} \to U \circ F \eta_{P}(p) = p\!\downarrow で定義します。このとき  \eta が natural transformation になることを証明します。

 Lemma
 \eta \text{ is a natural transformation}.

 Proof.
任意の  f \colon P \to Q に対して以下の diagram が可換になることを示せばよい。
f:id:hitotakuchan:20160902093405p:plain
これは任意の  p \in P に対して  f(p)\!\downarrow\, = \bigcup_{p' \in p\downarrow} f(p')\!\downarrow が成り立つことと同値である。

  • only if case

 q \in f(p)\!\downarrow とすると、 q \leq f(p) が成り立つ。すると  p \in p\!\downarrow であるから  q \in \bigcup_{p' \in p\downarrow} f(p)\!\downarrow となる。

  • if case

 q \in \bigcup_{p \in p\downarrow} f(p)\!\downarrow とすると、ある  p' \in p\!\downarrow が存在して  q \in f(p')\!\downarrow が成り立つ。  f は monotone であるから  q \leq f(p') \leq f(p) が成り立つので、 q \in f(p)\!\downarrow が成り立つ。

 \square

 Lemma
 U(\overline{f}) \circ \eta_{P} = f

 Proof.
任意の  p \in P に対して  \bigvee_{p' \in p\downarrow} f(p') = f(p) となることを示せばよい。
 p \in p\!\downarrow より  f(p) \leq \bigvee_{p' \in p\downarrow} f(p') となることは明らかである。逆に、任意の  p' \in p\!\downarrow とすると  p' \leq p であり、 f が monotone であるから  f(p') \leq f(p) が成り立つ。よって colimit の UMP より  \bigvee_{p' \in p\!\downarrow} f(p') \leq f(p) が成り立つ。

 \square

最後に  \overline{f} の唯一性について証明する。

 Lemma
 \forall g \colon F(P) \to \mathcal{C},\ U(g) \circ \eta_{P} = f \Rightarrow g = \overline{f}

 Proof.
任意の  U \in F(P) に対して  U = \bigcup_{p \in U} p\!\downarrow が成り立つことと  g が cocontinuous であることに注意すると、
\begin{align*}
g(U) &= g\left( \bigcup_{p \in U} p\!\downarrow \right) \\
&= \bigvee_{p \in U} g(p\!\downarrow) \\
&= \bigvee_{p \in U} f(p) \\
&= \overline{f}(U)
\end{align*}
が成り立つ。

 \square

9.2 Hom-set definition

 \eta_{C} = \phi(1_{FC}) で定義された  \eta \colon 1_{\bf{C}} \to U \circ F が natural transformation であることを証明します。

 Lemma
 \eta \text{ is a natural transformation}.

 Proof.
任意の  h \colon C' \to C に対して以下の diagram が可換になることを示せばよい。
f:id:hitotakuchan:20160905110844p:plain
 \phi が natural であることから以下の diagram が可換になることに注意すると、
f:id:hitotakuchan:20160905112152p:plain
\begin{align*}
UF(h) \circ \eta_{C'} &= UF(h) \circ \phi_{C', FC'}(1_{FC'}) \\
&= \left( UF(h)_{\ast} \circ \phi_{C', FC'} \right)(1_{FC'}) \\
&= \left( \phi_{C', FC} \circ F(h)_{\ast} \right)(1_{FC'}) \\
&= \phi_{C', FC}\left( F(h) \right) \\
&= \phi_{C', FC} \left( 1_{FC} \circ F(h) \right) \\
&= \left( \phi_{C', FC} \circ F(h)^{\ast} \right)(1_{FC}) \\
&= \left( h^{\ast} \circ \phi_{C, FC} \right)(1_{FC}) \\
&= \phi_{C, FC}(1_{FC}) \circ h \\
&= \eta_{C} \circ h
\end{align*}
が成り立つ。

 \square

9.4 Order adjoints

この節で出てくる例は、adjoint functor の domain も codomain も Preorder set を圏と見なしたものなので、任意の対象間には高々一つの写像しか存在しません。
よって同型射が natural になることは自明に成り立つのでその証明は省略されています。

Example 9.12

こちらの記事でも言及したのですが、ここの記述は正確ではありません。ただし位相空間に詳しくない方は飛ばして構いません。

書籍にあるように dual image function を  f_{\ast}(U) = \left\{ b \in B \,\middle|\, f^{-1}(b) \subseteq U \right\} と定義した場合、 f_{\ast} \colon \mathcal{P}(A) \to \mathcal{P}(B) は確かに  f^{-1} の right adjoint になります。これは、 f^{-1}(V) \subseteq U \Rightarrow V \subseteq f_{\ast}(U) かつ  V \subseteq f_{\ast}(U) \Rightarrow f^{-1}(V) \subseteq U が成り立つことを確認すればいいです。

問題はその次で、 f^{-1} を開集合に制限して  f^{-1} \colon \mathcal{O}(B) \to \mathcal{O}(A) とした場合にも  f_{\ast} f^{-1} の right adjoint になるという記述です。というのも  U を任意の  A の開集合とした時に  f_{\ast}(U) は必ずしも  B の開集合とはならないからです。よって  f_{\ast} f^{-1} の right adjoint にはなり得ません。

そこで  {\it{Sheaves\ in\ Geometry\ and\ Logic}} という書籍を参照すると、そこでは dual image function を以下のように定義しています。
 f_{\ast}(U) = \bigcup \left\{ V \in \mathcal{O}(B) \,\middle|\, f^{-1}(V) \subseteq U \right\}
この定義を用いると、任意の  A の開集合  U に対して  f_{\ast}(U) B の開集合になり  f^{-1} の right adjoint になることが証明できます。一方で開集合に制限しない  f^{-1}
\colon \mathcal{P}(B) \to \mathcal{P}(A) に対しては right adjoint になりません。

以上の二つの定義とその結果が、ここの記述ではごちゃ混ぜになっています。上で述べたことを是非自分で確認してみてください。

9.5 Quantifiers as adjoints

Figure 9.1 の説明がわかりにくいかもしれないので補足しておきます。ちなみに Figure 9.1 にある  \phi \psi の誤りです。
Figure 9.1 の左下を原点として、水平方向を  x 軸、垂直方向を  y 軸とします。また  x 上の任意の領域  R に対して  \pi^{-1}(R) によって生成される長方形をそのまま  \pi^{-1}(R) と書くことにします。さらに斜線で塗られた領域を、領域  \psi と呼ぶことにします。

 \frac{\exists y. \psi(x,y) \dashv \phi(x)}{\psi(x,y) \dashv \phi(x)}

  • 上から下に読む場合

 \phi(x) を満たす  x 軸上の領域  R \exists y. \psi(x,y) を満たす  x 軸上の領域、つまり Figure 9.1 の  \exists \psi と書かれた領域を含むのであれば、 \pi^{-1}(R) は領域  \psi を含むと読みます。

  • 下から上に読む場合

 \psi(x) を満たす  x 軸上の領域  R に対して  \pi^{-1}(R) が領域  \psi を含むのであれば、 R \exists \psi を含むと読みます。

同様に
 \frac{\phi(x) \dashv \psi(x,y)}{\phi(x) \dashv \forall y. \psi(x,y)}

  • 上から下に読む場合

 \phi(x) を満たす  x 軸上の領域  R に対して  \pi^{-1}(R) が領域  \psi に含まれるならば、 R \forall \psi に含まれると読みます。

  • 下から上に読む場合

 \phi(x) を満たす  x 軸上の領域  R \forall \psi に含まれるのであれば、 \pi^{-1}(R) は領域  \psi に含まれると読みます。

9.6 RAPL

Proposition 9.16

ここでは  {F_{!}}_{1} の定義と  F_{!} が functor になることの証明、 {F^{\ast}}_{1} の定義と  F^{\ast} が functor になることの証明が省略されています。
さらに natural isomorphism であることを示すところで、isomorphism であることは示されていますが、natural であることの証明が省略されています。 E に関して natural になることは Chapter 8 で確認しましたが  P に関して natural になることは確認していないので、ここで確認しておきます。

 Lemma
 F_{!} \text{ is a functor}.

 Proof.

  •  {F_{!}}_{1} の定義

任意の natural transformation  \theta \colon P \to Q に対して次の diagram を考える。
f:id:hitotakuchan:20160915131833p:plain
ここで任意の  h \colon (x', C') \to (x, C) \in \int\!P に対して  \phi_{P} \circ i_{h} = i_{(x', C')} \psi_{P} \circ i_{h} = i_{(x, C)} \circ F(h) である。
 i_{\left( \theta_{C}(x), C \right)} F \circ \pi(x,C) \overset{1_{FC}}{\to} F \circ \pi \left( \theta_{C}(x), C \right) \overset{i_{\left( \theta_{C}(x), C \right)}}{\to} \coprod_{\int\!Q} F \circ \pi(z,C) の合成である。
また  \theta が natural であるから  \left( Q(h) \circ \theta_{C} \right)(x) = \left( \theta_{C'} \circ P(h) \right)(x) = \theta_{C'}(x') が成り立つことから  h h \colon \left( \theta_{C'}(x'), C' \right) \to \left( \theta_{C}(x), C \right) \in \int\!Q となることに注意する。すると
\begin{align*}
c_{Q} \circ \left[ i_{\left( \theta_{C}(x), C \right)} \right] \circ \phi_{P} \circ i_{h} &= c_{Q} \circ i_{\left( \theta_{C'}(x'), C' \right)} \\
&= c_{Q} \circ \phi_{Q} \circ i_{h} \\
&= c_{Q} \circ \psi_{Q} \circ i_{h} \\
&= c_{Q} \circ i_{\left( \theta_{C}(x), C \right)} \circ F(h) \\
&= c_{Q} \circ \left[ i_{\left( \theta_{C}(x), C \right)} \right] \circ \psi_{P} \circ i_{h}
\end{align*}
が成り立つ。よって coproduct の UMP と colimit の UMP より diagram を可換にする写像  {F_{!}}_{1}(\theta) \colon \varinjlim_{\int\!P} F \circ \pi(x,C) \to \varinjlim_{\int\!Q} F \circ \pi(z, C) がただ一つ存在する。これを  {F_{!}}_{1}(\theta) と定義する。

  •  F_{!} が functor であること

 {F_{!}}_{1}(\theta \colon P \to Q) \colon {F_{!}}_{0}(P) \to {F_{!}}_{0}(Q) となるから  F_{!} は functor の条件 (a) を満たす。
 {F_{!}}_{1}(1_{P}) は上の diagram の  \theta 1_{P} で置き換えると、colimit の UMP より  {F_{!}}_{1}(1_{P}) = 1_{{F_{!}}_{0}(P)} が成り立つことがわかる。よって  F_{!} は functor の条件 (b) を満たす。
 {F_{!}}_{1}(\theta' \circ \theta) \left[ i_{\left( \theta'_{C}(z), C \right)} \right] \circ \left[ i_{\left( \theta_{C}(x), C \right)} \right] = \left[ i_{\left( (\theta' \circ \theta)_{C}(x), C \right)} \right] が成り立つので colimit の UMP より  {F_{!}}_{1}(\theta' \circ \theta) = {F_{!}}_{1}(\theta') \circ {F_{!}}_{1}(\theta) が成り立つ。よって  F_{!} は functor の条件 (c) を満たす。

 \square

次に  F^{\ast} が functor であることを証明します。

 Lemma
 F^{\ast} \text{ is a functor}.

 Proof.

  • 任意の  E \in \mathcal{E} に対して  F^{\ast}(E) が functor であること

任意の  h \colon C' \to C に対して  {F^{\ast}(E)}_{1}(h) \colon \text{Hom}(FC, E) \to \text{Hom}(FC', E) {F^{\ast}(E)}_{1}(h) = F(h)^{\ast} で定義する。
 {F^{\ast}(E)}_{1}(h \colon C' \to C) \colon {F^{\ast}(E)}_{0}(C) \to {F^{\ast}(E)}_{0}(C') となるので  F^{\ast}(E) は functor の条件 (a) を満たす。
 {F^{\ast}(E)}_{1}(1_{C}) = F(1_{C})^{\ast} = 1_{F(C)}^{\ast} = 1_{\text{Hom}(FC, E)} = 1_{{F^{\ast}(E)}_{0}(C)} が成り立つので  F^{\ast}(E) は functor の条件 (b) を満たす。
 {F^{\ast}(E)}_{1}(h \circ h') = F(h \circ h')^{\ast} = F(h')^{\ast} \circ F(h)^{\ast} = {F^{\ast}(E)}_{1}(h') \circ {F^{\ast}(E)}_{1}(h) が成り立つ。よって  F^{\ast}(E) は functor の条件 (c) を満たす。

  •  F^{\ast} が functor であること

任意の  f \colon E \to E' に対して  {F^{\ast}}_{1}(f) を任意の  C \in {\bf{C}} に対して  {F^{\ast}}_{1}(f)_{C} = f_{\ast} で定義する。
f:id:hitotakuchan:20160916132529p:plain
任意の  h \colon C' \to C と任意の  g \colon FC \to E に対して  \left( F^{\ast}(E')(h) \circ f_{\ast} \right)(g) = f \circ g \circ F(h) = \left( f_{\ast} \circ F^{\ast}(E)(h) \right)(g) が成り立つので、上の diagram は可換になる。よって  {F^{\ast}}_{1}(f) は natural transformation である。
このとき  {F^{\ast}}_{1}(f \colon E \to E') \colon {F^{\ast}}_{0}(E) \to {F^{\ast}}_{0}(E') が成り立つので  F^{\ast} は functor の条件 (a) を満たす。
 {F^{\ast}}_{1}(1_{E}) = 1_{{F^{\ast}}_{0}(E)} は定義より明らか。よって  F^{\ast} は functor の条件 (b) を満たす。
 {F^{\ast}}_{1}(f' \circ f)_{C} = (f' \circ f)_{\ast} = f'_{\ast} \circ f_{\ast} = {F^{\ast}}_{1}(f')_{C} \circ {F^{\ast}}_{1}(f)_{C} = \left( {F^{\ast}}_{1}(f') \circ {F^{\ast}}_{1}(f) \right)_{C} が成り立つので、 F^{\ast} は functor の条件 (c) を満たす。

 \square

最後に  \text{Hom}(P, F^{\ast}(E)) \cong \text{Hom}(F_{!}(P), E) P に関して natural であることを証明します。
 \text{Hom}(\varinjlim_{j \in J} yC_{j}, F^{\ast}(E)) \cong \varprojlim_{j \in J} \text{Hom}(yC_{j}, F^{\ast}(E)) の場合は  \text{Hom}(\varinjlim_{j \in J} FC_{j}, E) \cong \varprojlim_{j \in J} \text{Hom}(FC_{j}, E) の場合と同様に示せるので、 \eta \colon \text{Hom}(\varinjlim_{j \in J} FC_{j}, E) \cong \varprojlim_{j \in J} \text{Hom}(FC_{j}, E) が natural であることの証明のみを示します。それ以外の箇所は Chapter 8 で示した証明と同様に証明できるので省略します。 \eta の定義は Chapter8 の 8.7 節の証明を参照してください。

 Lemma
 \eta \text{ is a natural transformation}.

 Proof.
任意の  \theta \colon Q \to P について考える。 \eta が natural であるためには以下の diagram が可換になることを示す必要がある。
f:id:hitotakuchan:20160916140213p:plain
しかし diagram の右の写像がどのような写像なのか明らかではない。そこで以下の diagram を考える。
f:id:hitotakuchan:20160916141840p:plain
ここで  \theta が natural であることから、任意の  h \colon (z', C') \to (z, C) in \int\!Q h \colon \left( \theta_{C'}(z'),C' \right) \to \left( \theta_{C}(z), C \right) となることに注意しておく。すると
\begin{align*}
\pi_{h} \circ \phi_{Q} \circ \left< \pi_{\left( \theta_{C}(z), C \right)}(-) \right>_{(z,C) \in \int\!Q} \circ e_{P} &= \pi_{(z',C')} \circ \left< \pi_{\left( \theta_{C}(z), C \right)}(-) \right>_{(z,C) \in \int\!Q} \circ e_{P} \\
&= \pi_{\left( \theta_{C'}(z'), C' \right)} \circ e_{P} \\
&= \pi_{h} \circ \phi_{P} \circ e_{P} \\
&= \pi_{h} \circ \psi_{P} \circ e_{P} \\
&= F(h)^{\ast} \circ \pi_{\left( \theta_{C}(z), C \right)} \circ e_{P} \\
&= F(h)^{\ast} \circ \pi_{(z,C)} \circ \left< \pi_{\left( \theta_{C}(z), C \right)}(-) \right>_{(z,C) \in \int\!Q} \circ e_{P} \\
&= \pi_{h} \circ \psi_{Q} \circ \left< \pi_{\left( \theta_{C}(z), C \right)}(-) \right>_{(z,C) \in \int\!Q} \circ e_{P}
\end{align*}
が成り立つので、product の UMP と limit の UMP より diagram を可換とする唯一つの  \overline{\theta} が存在する。

次に  \pi_{(z,C)} \circ e_{Q} \circ \overline{\theta} \circ \eta_{P} = \pi_{(z,C)} \circ e_{Q} \circ \eta_{Q} \circ F_{!}(\theta)^{\ast} を示す。すると product の UMP と  e_{Q} が monic であることから  \overline{\theta} \circ \eta_{P} = \eta_{Q} \circ F_{!}(\theta)^{\ast} が成り立つ。
任意の  f \colon \varinjlim_{(x,C)} F \circ \pi(x,C) \to E に対して
\begin{align*}
\left( \pi_{(z,C)} \circ e_{Q} \circ \overline{\theta} \circ \eta_{P} \right)(f) &= \left( \pi_{\left( \theta_{C}(z), C \right)} \circ e_{P} \circ \eta_{P} \right)(f) \\
&= \left( \pi_{\left( \theta_{C}(z), C \right)} \circ \left< - \circ i_{(x,C)} \right>_{(x,C) \in \int\!P} \circ c_{P}^{\ast} \right)(f) \\
&= f \circ c_{P} \circ i_{\left( \theta_{C}(z), C \right)} \\
&= f \circ c_{P} \circ \left[ i_{\left( \theta_{C}(z), C \right)} \right] \circ i_{(z,C)}
\end{align*}
が成り立つ。一方、
\begin{align*}
\left( \pi_{(z,C)} \circ e_{Q} \circ \eta_{Q} \circ F_{!}(\theta)^{\ast} \right)(f) &= \left( \pi_{(z,C)} \circ \left< - \circ i_{(z,C)} \right>_{(z,C) \in \int\!Q} \circ c_{Q}^{\ast} \circ F_{!}(\theta)^{\ast} \right)(f) \\
&= f \circ F_{!}(\theta) \circ c_{Q} \circ i_{(z,C)}
\end{align*}
が成り立つ。これは  F_{!}(\theta) の定義より等しい。よって  \eta は natural isomorphism である。

 \square

最後にこのように定義した  F_{!} に対して  F_{!}(yC) \cong FC が成り立つことを証明します。

 Lemma
 F_{!}(yC) \cong FC

 Proof.
 \int\!yC において  (1_{C},C) は terminal object になるので、任意の  (f, C') \in \int\!yC に対して  F(f) \colon F \circ \pi(f, C') \to F \circ \pi(1_{C},C) が存在する。このことに注意すると、任意の natural transformation  \phi \colon F \circ \pi \to \Delta E に対して次の左の diagram は可換となる。
f:id:hitotakuchan:20161005121121p:plain
また任意の  \psi \colon F \circ \pi(1_{C},C) \to E が存在して同様に diagram を可換にするとすると、上の右の diagram が可換になることより  \psi = \phi_{(1_{C}, C)} が成り立つ。
よって colimit の UMP より  F_{!}(yC) = \varinjlim_{(f,C) \in \int\!yC} F \circ \pi(f,C) \cong F \circ \pi(1_{C}, C) = FC が成り立つ。

 \square

9.7 Locally cartesian closed categories

Proposition 9.20

はじめに、任意の  f \colon A \to B に対して  \sum_{f} \dashv f^{\ast} \dashv \prod_{f} が成り立つとき、 \sum_{f} \circ\, f^{\ast} \dashv \prod_{f} \circ\, f^{\ast} が成り立つことを確認してください。
 \sum_{f} \dashv f^{\ast} \dashv \prod_{f} の二つの natural isomorphism を合成すればいいです。

次に  !_{A} \colon A \to \ast に対して  \sum_{!_{A}} \circ\, !_{A}^{\ast} A \times - となることは Proposition 5.14 で確認しました。すると  A \times - の right adjoint は  (-)^{A} に unique up to isomorphism で決まるので、 B^{A} = (\prod_{!_{A}} \circ\, !_{A}^{\ast})(B) で定義すればよいことがわかります。

次に証明なしに出てくる "a slice of a slice is a slice" の確認をしておきます。

 Lemma
 \text{a slice of a slice is a slice}.

 Proof.
f:id:hitotakuchan:20161021121200p:plain
任意の  X,Y \in \mathcal{E} と任意の  f \colon X \to Y について  \left( \mathcal{E} / Y \right) /\, f \cong \mathcal{E} / X となることを示す。
はじめに functor  \Phi \colon \left( \mathcal{E} / Y \right) /\, f \to \mathcal{E} / X を定義する。
任意の  a' \colon a \to f \in \left( \mathcal{E} / Y \right) /\, f に対して  \Phi_{0}(a') = a' と定義すると、 a' \colon A \to X であるから  a \in \mathcal{E} / X となる。
また任意の  h \colon a' \to b' \in \left( \mathcal{E} / Y \right) /\, f に対して  \Phi_{1}(h) = h と定義すると、 h b' \circ h = a' を満たすので  h \in \mathcal{E} / X となる。
このとき、 \Phi_{1} \left(h \colon (a' \colon a \to f) \to (b' \colon b \to f) \right) = h \colon (a' \colon A \to X) \to (b' \colon B \to X) = h \colon \Phi_{0}(a') \to \Phi_{0}(b') が成り立つので、 \Phi は functor の条件 (a) を満たす。
次に  \Phi_{1}(1_{a'}) = 1_{a'} = 1_{\Phi_{0}(a')} が成り立つので  \Phi は functor の条件 (b) を満たす。
最後に  \Phi_{1}(h' \circ h) = h' \circ h = \Phi_{1}(h') \circ \Phi_{1}(h) が成り立つので  \Phi は functor の条件 (c) を満たす。

次に functor  \Psi \colon \mathcal{E} / X \to \left( \mathcal{E} / Y \right) /\, f を定義する。
任意の  a' \colon A \to X \in \mathcal{E} / X に対して  \Psi_{0} \Psi_{0}(a') = a' \colon (f \circ a') \to f で定義する。明らかに  \Psi_{0}(a') \in \left( \mathcal{E} / Y \right) /\, f である。
また任意の  h \colon a' \to b' \in \mathcal{E} / X に対して  \Psi_{1}(h) = h と定義すると、 h f \circ b' \circ h = f \circ a' を満たすので、 \Psi_{1}(h) = h \colon \Psi_{0}(a') \to \Psi_{0}(b') となり functor の条件 (a) を満たす。
次に  \Psi_{1}(1_{a'}) = 1_{a'} = 1_{\Psi_{0}(a')} が成り立つので  \Psi は functor の条件 (b) を満たす。
最後に  \Psi_{1}(h' \circ h) = h' \circ h = \Psi_{1}(h') \circ \Psi_{1}(h) が成り立つので  \Psi は functor の条件 (c) を満たす。

以上のように定義した  \Phi \Psi に対して  \Psi \circ \Phi = 1 かつ  \Phi \circ \Psi = 1 が成り立つことは明らかであるから、 \left( \mathcal{E} / Y \right) /\, f \cong \mathcal{E} / X が成り立つ。

 \square

任意の  f \colon (a \colon A \to X) \to (b \colon B \to X) \in \mathcal{E}/X に対して composition functor  \sum_{f} \colon (\mathcal{E}/X)/\,a \to (\mathcal{E}/X)/\,b を考えます。
上の同型射を用いると  \sum_{f}' \colon \mathcal{E}/A \to \mathcal{E}/B が構成できます。 \mathcal{E} が locally cartesian category なら、 \sum_{f}' に対して right adjoint  {f^{\ast}}' \prod_{f}' が構成できます。よって再び同型射を用いることで  \sum_{f} に対して right adjoint を構成できるので  \mathcal{E}/X も locally cartesian category になります。

逆の  \text{2} \Rightarrow \text{1} の証明は exponential が突然出てきて難しいですね。 \mathcal{F} を使った置き換えがなぜ必要なのかもよくわかりません。また1対1に対応するとは書かれていますが、それが  Y p に対して natural であることの証明は省略されています。

 Lemma
 F^{\ast} \dashv \prod_{F}

 Proof.
f:id:hitotakuchan:20161021133911p:plain
任意の  F \colon A \to B の composition functor の right adjoint  F^{\ast} は pullback functor である。よって上の図のように任意の  Y \colon C \to B \in \mathcal{E}/B に対して  F^{\ast}(Y) = \pi_{2} \in \mathcal{E}/A となる。 Y F \mathcal{E} における射であるから  Y \times F \mathcal{E} の object のように記述するのはおかしいが、 \mathcal{E}/B においては  F \circ \pi_{2} = Y \circ \pi_{1} は確かに  Y \times F となるのでこのように記述している。このとき  \pi_{1} \pi_{2} は実際に  \mathcal{E}/B において projection function になっている。

以上の注意を元に、任意の  Y \colon C \to B p \colon X \to A に対して  \theta_{Y,p} \colon \text{Hom} \left( F^{\ast}(Y), p \right) \to \text{Hom}\left(Y, \prod_{F}(p) \right) を定義する。
任意の  l \colon F^{\ast}(Y) \to p に対して以下の diagram を考える。
f:id:hitotakuchan:20161021135558p:plain
 l l \colon F \circ \pi_{2} \to F \circ p \in \mathcal{E}/B と考えると  l \colon Y \times F \to F \circ p と見なせる。 \mathcal{E}/B は cartesian closed であるので exponential の UMP より  \exists !\, \widetilde{l} \colon Y \to {F \circ p}^{F} が存在する。 p p \colon F \circ p \to F \in \mathcal{E}/B と見なせることに注意して以下の pullback diagram in  \mathcal{E}/B を考える。
f:id:hitotakuchan:20161021141034p:plain
すると、 \epsilon \circ (p^{F} \times 1) \circ (\widetilde{l} \times 1) = p \circ \epsilon \circ (\widetilde{l} \times 1) = p \circ l = \pi_{2} が成り立つ。一方、
 \epsilon \circ ( \widetilde{\pi_{2}} \times 1) \circ (! \times 1) = \pi_{2} \circ (! \times 1) = \pi_{2} が成り立つので exponential の UMP より  p^{F} \circ \widetilde{l} = \widetilde{\pi_{2}} \circ ! が成り立つ。よって pullback の UMP より  \exists !\, m \colon Y \to \prod_{F}(p) が存在する。そこで  \theta_{Y,p}(l) = m で定義する。これは各 UMP により well-defined である。

次に  \theta^{-1}_{Y,p} \colon \text{Hom}\left(Y, \prod_{F}(p) \right) \to \text{Hom} \left( F^{\ast}(Y), p \right) を定義する。
任意の  m \colon Y \to \prod_{F}(p) \in \mathcal{E}/B に対して、上の diagram において  n \circ m を考える。すると exponential の UMP より  \exists !\, \overline{n \circ m} \colon Y \times F \to F \circ p が存在する。この  \overline{n \circ m} \overline{n \circ m} \colon \pi_{2} \to p \in \mathcal{E}/A とみなして、 \theta^{-1}_{Y,p}(m) = \overline{n \circ m} で定義する。
f:id:hitotakuchan:20161021143437p:plain

 \theta^{-1}_{Y,p} \theta_{Y,p} の逆射になるので、 \theta_{Y,p} は isomorphism である。次に natural であることを示す。

  •  \theta_{Y,p} Y に関して natural であること

任意の  h \colon Y' \to Y \in \mathcal{E}/B に対して Two-pullback Lemma より以下の diagram が可換になる。
f:id:hitotakuchan:20161024130748p:plain
すると  h' h' \in \mathcal{E}/A とみなすことができる。そこで次の左の diagram を考える。
f:id:hitotakuchan:20161024140733p:plain
任意の  l \colon F^{\ast}(Y) \to p に対して、 (h^{\ast} \circ \theta_{Y,p})(l) = \theta_{Y,p}(l) \circ h が成り立つ。一方、 (\theta_{Y',p} \circ h'^{\ast})(l) = \theta_{Y', p}(l \circ h') が成り立つ。
 \theta_{Y,p}(l) \circ h に対して  \theta の定義より、 \epsilon \circ \left( n \circ \theta_{Y,p}(l) \circ h \times 1 \right) = \epsilon \circ \left( n \circ \theta_{Y,p}(l) \times 1 \right) \circ ( h \times 1) = l \circ (h \times 1) が成り立つ。同様に \theta_{Y', p}(l \circ h') に対して  \epsilon \circ n \circ \theta_{Y', p}(l \circ h') = l \circ h' が成り立つ。
Two-pullback Lemma による diagram より上の右の diagram は可換になる。よって  h \times 1 = h' が成り立つので、exponential の UMP と pullback の UMP より  \theta_{Y,p}(l) \circ h = \theta_{Y', p}(l \circ h') が成り立つ。

  •  \theta_{Y,p} p に関して natural であること

任意の  h \colon (p \colon X \to A) \to (p' \colon X' \to A) \in \mathcal{E}/A に対して Two-pullback Lemma より以下の diagram が可換になる。
f:id:hitotakuchan:20161024140052p:plain
そこで次の diagram を考える。
f:id:hitotakuchan:20161024140723p:plain
任意の  l \colon F^{\ast}(Y) \to p に対して、 ( {h^{F}}'_{\ast} \circ \theta_{Y,p})(l) = {h^{F}}' \circ \theta_{Y,p}(l) が成り立つ。一方、 (\theta_{Y,p'} \circ h_{\ast})(l) = \theta_{Y,p'}(h \circ l) が成り立つ。
上の Two-pullback Lemma による diagram と  \theta の定義より
\begin{align*}
\epsilon \circ \left( n' \circ {h^{F}}' \circ \theta_{Y,p}(l) \times 1 \right) &= \epsilon \circ \left( h^{F} \circ n \circ \theta_{Y,p}(l) \times 1 \right) \\
&= h \circ \epsilon \circ \left( n \circ \theta_{Y,p}(l) \times 1 \right) \\
&= h \circ l
\end{align*}
が成り立つ。一方、 \epsilon \circ \left( n' \circ \theta_{Y, p'}(h \circ l) \times 1 \right) = h \circ l が成り立つ。よって exponential の UMP と pullback の UMP より  {h^{F}}' \circ \theta_{Y,p}(l) = \theta_{Y,p'}(h \circ l) が成り立つ。

以上より  \theta は natural isomorphism である。

 \square

Lemma 9.23

ここでは  \Psi \colon {\bf{Sets}}^{(y/P)^{\text{op}}} \to {\bf{Sets}}^{{\bf{C}}^{\text{op}}}/P を定義し、 1 \simeq \Psi \circ \Phi かつ  1 \simeq \Phi \circ \Psi を示す必要があります。
はじめに  \Psi を定義するために、任意の  G \in {\bf{Sets}}^{(y/P)^{\text{op}}} に対して functor  \coprod G \colon {\bf{C}}^{\text{op}} \to {\bf{Sets}} を定義します。

 Lemma
  \coprod G \text{ is a functor}.

 Proof.
任意の  C \in {\bf{C}} に対して1つ目の成分が  C であるような  \int_{\bf{C}} P の object の集合を  \mathcal{L}_{C} と表す。このとき  (\coprod G)(C) = \coprod_{(C,x) \in \mathcal{L}_{C}} G( (C,x)) で定義する。
次に任意の  f \colon C' \to C に対して、 yf \colon yC' \to yC は任意の  x \colon yC \to P に対して  yf \colon x \circ yf \to x \in \int_{\bf{C}} P となる。すると  G(yf) G(yf) \colon G( (C,x)) \to G( (C', x \circ yf)) となることに注意して、 (\coprod G)(f) = \left[ i \circ G(yf) \right]_{(C,x) \in \mathcal{L}_{C}} \colon \coprod_{(C,x) \in \mathcal{L}_{C}} G( (C,x)) \to \coprod_{(C',x') \in \mathcal{L}_{C'}} G( (C',x')) で定義する。
このとき  \coprod G が functor の条件をみたすことは coproduct の UMP により明らかである。

 \square

本当に  \coprod G が functor の条件を満たすか確認してください。
次にこの  \coprod G を用いて  \Psi(G) \Psi(G) \colon \coprod G \to P で定義する。このとき  \Psi が functor となることを示す。

 Lemma
  \Psi \text{ is a functor}.

 Proof.
任意の  (C,x) \in \int_{\bf{C}} P と任意の  l \in G( (C,x)) に対して  (\coprod G)(C) の要素を  ( (C,x), l) で表すとすると、 \Psi(G) (\Psi(G))_{C}( (C,x), l) = x_{C}(1_{C}) で定義する。このとき  \Psi(G) が natural transformation であることを示す。
f:id:hitotakuchan:20161027142513p:plain
任意の  f \colon C' \to C \in {\bf{C}} と任意の  ( (C,x), l) \in (\coprod G)(C) に対して  \left( P(f) \circ \Psi(G)_{C} \right)( (C,x), l) = P(f)(x_{C}(1_{C})) が成り立つ。一方米田の補題より
\begin{align*}
\left( \Psi(G)_{C'} \circ (\coprod G)(f) \right)( (C,x), l) &= \Psi(G)_{C'}\left( (C', x \circ yf), G(yf)(l) \right) \\
&= (x \circ yf)_{C}(1_{C}) \\
&= P(f)(x_{C}(1_{C}))
\end{align*}
が成り立つので、上の diagram は可換となり  \Psi(G) \in {\bf{Sets}}^{{\bf{C}}^{\text{op}}}/P となる。

次に、任意の  \theta \colon G \to G' に対して  {\Psi(\theta)}_{C} \colon (\coprod G)(C) \to (\coprod G')(C) {\Psi(\theta)}_{C} = \left[ i \circ \theta_{(C,x)} \right]_{(C,x) \in \mathcal{L}_{C}} で定義する。このとき  \Psi(\theta) が natural であることを示す。
f:id:hitotakuchan:20161028105839p:plain
任意の  f \colon C' \to C と任意の  ( (C,x), l) \in (\coprod G)(C) に対して
 \left( (\coprod G')(f) \circ \Psi(\theta)_{C} \right) \left( ( (C,x), l) \right) = (\coprod G')(f)\left( ( (C, x), \theta_{(C,x)}(l)) \right) = \left( (C', x \circ yf),  \left( G'(yf) \circ \theta_{(C,x)} \right)(l) \right)
一方
 \left( \Psi(\theta)_{C'} \circ (\coprod G)(f) \right)\left( ( (C,x), l) \right) = \Psi(\theta)_{C'} \left( ( (C', x \circ yf), G(yf)(l) ) \right) = \left( ( C', x \circ yf), \left( \theta_{(C',x \circ yf)} \circ G(yf) \right)(l) \right)
が成り立つ。これらは  \theta が natural であることより等しい。上の左の diagram は可換であるので  \Psi(\theta) は natural である。

また任意の  ( ( C,x), l) \in (\coprod G)(C) に対して
 \left( \Psi(G')_{C} \circ \Psi(\theta)_{C} \right)\left( ( (C,x), l) \right) = x_{C}(1_{C}) = \Psi(G)_{C} \left( ( (C,x), l) \right)
が成り立つので、 \Psi(\theta) \colon \Psi(G) \to \Psi(G') \in {\bf{Sets}}^{{\bf{C}}^{\text{op}}}/P となる。

 \Psi が functor の条件をみたすことは coproduct の UMP 等により明らかである。

 \square

 Lemma
 1 \simeq \Psi \circ \Phi

 Proof.
natural isomorphism  \phi \colon 1 \to \Psi \circ \Phi を構成すればよい。
任意の  q \colon Q \to P と任意の  C \in {\bf{C}} に対して  (\Psi \circ \Phi)(q)(C) \colon \coprod_{(C,x) \in \mathcal{L}_{C}} \text{Hom}(x,q) \to PC となることに注意して、 {\phi_{q}}_{C} \colon QC \to \coprod_{(C,x) \in \mathcal{L}_{C}} \text{Hom}(x,q) を任意の  l \in QC に対して  {\phi_{q}}_{C}(l) = ( ( C, q \circ \widetilde{l}), \widetilde{l}) で定義する。ただし  \widetilde{l} \colon yC \to Q は米田の補題により一意に定まる  \widetilde{l}_{C}(1_{C}) = l を満たす natural transformation とする。

任意の  ( (C, x), m) \in \coprod_{(C,x) \in \mathcal{L}_{C}} \text{Hom}(x,q) に対して  {\phi_{q}}_{C}^{-1}\left( ( (C,x), m) \right) = m_{C}(1_{C}) {\phi_{q}}_{C}^{-1} を定義すれば、明らかに  {\phi_{q}}_{C} は isomorphism となる。

 \phi_{q} C に関して natural であることを示す。
任意の  f \colon C' \to C に対して以下の diagram を考える。
f:id:hitotakuchan:20161028121845p:plain
任意の  l \in QC に対して
 \left( \left( \coprod \Phi(q) \right)(f) \circ {\phi_{q}}_{C} \right)(l) = ( (C', q \circ \widetilde{l} \circ yf), \widetilde{l} \circ yf)
が成り立つ。一方、 \left( {\phi_{q}}_{C'} \circ Q(f) \right)(l) = ( (C', q \circ \widetilde{Q(f)(l)}), \widetilde{Q(f)(l)}) が成り立つ。 (\widetilde{l} \circ yf)_{C}(1_{C}) = Q(f)(l) が成り立つので両者は等しい。よって diagram は可換となる。

この  \phi_{q} に対して以下の diagram が可換になることは明らかなので、
f:id:hitotakuchan:20161028123226p:plain
 \phi_{q} \colon q \to (\Psi \circ \Phi)(q) \in {\bf{Sets}}^{{\bf{C}}^{\text{op}}}/P となる。

最後に任意の  \theta \colon q \to q' に対して以下の diagram を考える。
f:id:hitotakuchan:20161028124537p:plain
任意の  l \in QC に対して
 \left( (\Psi \circ \Phi)(\theta)_{C} \circ {\phi_{q}}_{C} \right)(l) = ( \Psi \circ \Phi)(\theta)_{C}( ( (C, q \circ \widetilde{l}), \widetilde{l}) ) = ( ( C, q \circ \widetilde{l}), \theta \circ \widetilde{l})
が成り立つ。一方、 ( {\phi_{q'}}_{C} \circ \theta_{C})(l) = ( (C, q' \circ \widetilde{\theta_{C}(l)}), \widetilde{\theta_{C}(l)}) が成り立つ。
ところが  (\theta \circ \widetilde{l})_{C}(1_{C}) = \theta_{C}(l) が成り立つので、両者は等しい。よって上の diagram は可換となる。

以上より  \phi は natural isomorphism である。

 \square

 Lemma
 1 \simeq \Phi \circ \Psi

 Proof.
natural isomorphism  \psi \colon 1 \to \Phi \circ \Psi を構成すればよい。
任意の  G \in {\bf{Sets}}^{(y/P)^{\text{op}}} と任意の  (C,x) \in y/P に対して  {\psi_{G}}_{(C,x)} \colon G(C,x) \to \text{Hom}\left( x, \Psi(G) \right) を次のように定義する。
任意の  l \in G(C,x) に対して  ( (C,x), l) ( (C,x), l) \in \coprod_{(C,x) \in \mathcal{L}_{C}} G(C,x) つまり  ( (C,x), l) \in (\coprod G)(C) であるから米田の補題より一意に対応した  \widetilde{l} \colon yC \to \coprod G が得られる。

この  \widetilde{l} に対して以下の diagram を考える。
f:id:hitotakuchan:20161028144902p:plain
任意の  f \colon C' \to C に対して米田の補題と  \coprod G の定義より、
\begin{align*}
\left( \Psi(G)_{C'} \circ \widetilde{l}_{C'} \right)(f) &= \Psi(G)_{C'}( (C', x \circ yf), G(yf)(l)) \\
&= (x \circ yf)_{C'}(1_{C'}) \\
&= P(f) \left( x_{C'}(1_{C'}) \right) \\
&= x_{C'}(f)
\end{align*}
が成り立つので、上の diagram は可換になる。よって  \widetilde{l} \colon x \to \Psi(G) となるので  {\psi_{G}}_{(C,x)}(l) = \widetilde{l} と定義する。

次に  \psi_{G} が isomorphism であることを示す。
 {\psi_{G}}_{(C,x)}^{-1} \colon \text{Hom}\left( x, \Psi(G) \right) \to G(C,x) を次のように定義する。
任意の  m \colon x \to \Psi(G) に対して、 m m \colon yC \to \coprod G と見なせるので米田の補題より  ( (C, x'), \overline{m}) が一意に存在して  m_{C}(1_{C}) = ( ( C, x'), \overline{m}) を満たす。このとき  m x = \Psi(G) \circ m をみたすことから  x = x' が成り立つ。よって  \overline{m} \in G(C,x) である。
そこで  {\psi_{G}}_{(C,x)}^{-1}(m) = \overline{m} と定義すると、米田の補題より  {\psi_{G}}_{(C,x)} の逆射となり  {\psi_{G}}_{(C,x)} は isomorphism となる。

次に  \psi_{G} が natural であることを示す。
任意の  yf \colon (C',x') \to (C,x) に対して次の diagram を考える。
f:id:hitotakuchan:20161028195553p:plain
任意の  l \in G( (C,x)) に対して  (yf^{\ast} \circ {\psi_{G}}_{(C,x)})(l) = \widetilde{l} \circ yf が成り立つ。一方  \left( {\psi_{G}}_{(C',x')} \circ G(yf) \right)(l) = \widetilde{G(yf)(l)} が成り立つ。
今、 (\widetilde{l} \circ yf)_{C'}(1_{C'}) = \widetilde{l}(f) = ( ( C', x \circ yf), G(yf)(l)) \widetilde{G(yf)(l)}_{C'}(1_{C'}) = ( (C', x'), G(yf)(l)) が成り立ち両者は等しいので、米田の補題より diagram は可換となる。よって  \psi_{G} は natural である。

最後に  \psi が natural であることを示す。
任意の  \theta \colon G \to G' と任意の  (C,x) に対して次の diagram を考える。
f:id:hitotakuchan:20161028195604p:plain
任意の  l \in G( (C,x)) に対して  \left( (\Phi \circ \Psi)(\theta)_{(C,x)} \circ {\psi_{G}}_{(C,x)} \right)(l) = (\Phi \circ \Psi)(\theta)_{(C,x)}(\widetilde{l}) = \Psi(\theta) \circ \widetilde{l} が成り立つ。一方  \left( {\psi_{G'}}_{(C,x)} \circ \theta_{(C,x)} \right)(l) = \widetilde{\theta_{(C,x)}(l)} が成り立つ。
 \left( \Psi(\theta) \circ \widetilde{l} \right)_{C}(1_{C}) = \Psi(\theta)_{C}( ( (C,x), l)) = ( (C,x), \theta_{(C,x)}(l)) \widetilde{\theta_{(C,x)}(l)}_{C}(1_{C}) = ( (C,x), \theta_{(C,x)}(l)) が成り立つので、米田の補題より上の diagram は可換となる。

以上より  \psi は natural isomorphism である。

 \square

9.8 Adjoint functor theorem

Theorem 9.29

書籍にある Solution set condition が微妙に間違ってます。書籍にある通り論理式で表現すると
 \forall X \in {\bf{X}},\ \exists I,\ \exists (S_{i})_{i \in I},\ \forall C \in {\bf{C}},\ \forall f \colon X \to UC,\ \exists i \in I,\ \exists \phi \colon X \to US_{i},\ \exists \overline{f} \colon S_{i} \to C,\ f = U(\overline{f}) \circ \phi
となりますが、正しくは
 \forall X \in {\bf{X}},\ \exists I,\ \exists (S_{i})_{i \in I},\ \exists (\phi_{i} \colon X \to US_{i})_{i \in I},\ \forall C \in {\bf{C}},\ \forall f \colon X \to UC,\ \exists i \in I,\ \exists \overline{f} \colon S_{i} \to C,\ f = U(\overline{f}) \circ \phi_{i}
となります。

こちらの条件でないと、Theorem 9.29 の証明の中で Lemma 9.30 を使用することができません。

参考書籍

Category Theory (Oxford Logic Guides)

Category Theory (Oxford Logic Guides)

  • 作者:Awodey, Steve
  • 発売日: 2008/01/10
  • メディア: ペーパーバック
圏論 原著第2版

圏論 原著第2版

Steve Awodey の Category Theory を読む : Chapter 8

Steve Awodey の Category Theory を読む シリーズトップ

8.3 The Yoneda lemma

書籍の lemma 8.2 の証明は contravariant 版の米田の埋め込みに関する証明ですが、covariant 版の米田の埋め込みに対しても同様の lemma が成立します。
つまり  y \colon {\bf{C}}^{\text{op}} \to {\bf{Sets}}^{\bf{C}} を 任意の  C \in {\bf{C}} に対して  yC = \text{Hom}_{\bf{C}}(C, -) \colon {\bf{C}} \to {\bf{Sets}}、任意の  f \colon C \to D に対して  yf = \text{Hom}_{\bf{C}}(f, -) \colon \text{Hom}_{\bf{C}}(D, -) \to \text{Hom}_{\bf{C}}(C, -) で定義します。
このとき lemma 8.2 と同様に、任意の  C \in {\bf{C}} と任意の  F \in {\bf{Sets}}^{\bf{C}} に対して  \text{Hom}(yC, F) \cong FC が成立し、 y は埋め込みになります。
証明自体は書籍にある lemma 8.2 の証明とほとんど同じなので省略します。理解の確認のためにこちらの証明を書籍を見ながらやってみるといいと思います。

8.4 Applications of the Yoneda lemma

 y \left( (A^{B})^{C} \right) \cong y \left( A^{(B \times C)} \right)

 \text{Hom} \left( X, (A^{B})^{C} \right) \cong \text{Hom}(X \times C, A^{B}) \text{Hom}(X \times C, A^{B}) \cong \text{Hom} \left( (X \times C) \times B, A \right) \text{Hom} \left( X \times (B \times C), A \right) \cong \text{Hom} \left( X, A^{(B \times C)} \right) に関しては transpose を取る対応なので、exponential の UMP より同型となります。

 Lemma
\[ \text{Hom} \left( (X \times C) \times B, A \right) \cong \text{Hom} \left( X \times (B \times C), A \right) \] Proof.
同型射として  \left< \left<\pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right>^{\ast} \colon \text{Hom} \left( (X \times C) \times B, A \right) \to \text{Hom} \left( X \times (B \times C), A \right) \left< \pi_{X} \circ \pi_{X \times C}, \left< \pi_{B}, \pi_{C} \circ \pi_{X \times C} \right> \right>^{\ast} \colon \text{Hom} \left( X \times (B \times C), A \right) \to \text{Hom} \left( (X \times C) \times B, A \right) を取る。
このとき、任意の  f \colon (X \times C) \times B \to A に対して  \left( \left< \pi_{X} \circ \pi_{X \times C}, \left< \pi_{B}, \pi_{C} \circ \pi_{X \times C} \right> \right>^{\ast} \circ \left< \left<\pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right>^{\ast} \right)(f) = f を示せばよい。つまり   \left< \left<\pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \circ \left< \pi_{X} \circ \pi_{X \times C}, \left< \pi_{B}, \pi_{C} \circ \pi_{X \times C} \right> \right> = 1_{(X \times C) \times B} を示せばよい。
\[
\begin{align*}
& \pi_{X} \circ \pi_{X \times C} \circ \left< \left<\pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \circ \left< \pi_{X} \circ \pi_{X \times C}, \left< \pi_{B}, \pi_{C} \circ \pi_{X \times C} \right> \right> \\
&= \pi_{X} \circ \left< \pi_{X} \circ \pi_{X \times C}, \left< \pi_{B}, \pi_{C} \circ \pi_{X \times C} \right> \right> \\
&= \pi_{X} \circ \pi_{X \times C}
\end{align*}
\]\[
\begin{align*}
& \pi_{C} \circ \pi_{X \times C} \circ \left< \left<\pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \circ \left< \pi_{X} \circ \pi_{X \times C}, \left< \pi_{B}, \pi_{C} \circ \pi_{X \times C} \right> \right> \\
&= \pi_{C} \circ \pi_{B \times C} \circ \left< \pi_{X} \circ \pi_{X \times C}, \left< \pi_{B}, \pi_{C} \circ \pi_{X \times C} \right> \right> \\
&= \pi_{C} \circ \pi_{X \times C}
\end{align*}
\]\[
\begin{align*}
& \pi_{B} \circ \left< \left<\pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \circ \left< \pi_{X} \circ \pi_{X \times C}, \left< \pi_{B}, \pi_{C} \circ \pi_{X \times C} \right> \right> \qquad \\
&= \pi_{B} \circ \pi_{B \times C} \circ \left< \pi_{X} \circ \pi_{X \times C}, \left< \pi_{B}, \pi_{C} \circ \pi_{X \times C} \right> \right> \\
&= \pi_{B}
\end{align*}
\]
が成り立つので、product の UMP より   \left< \left<\pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \circ \left< \pi_{X} \circ \pi_{X \times C}, \left< \pi_{B}, \pi_{C} \circ \pi_{X \times C} \right> \right> = 1_{(X \times C) \times B} が成り立つ。
任意の  g \colon X \times (B \times C) \to A に対して  \left( \left< \left<\pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right>^{\ast} \circ \left< \pi_{X} \circ \pi_{X \times C}, \left< \pi_{B}, \pi_{C} \circ \pi_{X \times C} \right> \right>^{\ast} \right)(g) = g の証明も同様である。

 \square

次にそれぞれの同型射に関して、それが natural transformation であることを証明します。

 Lemma
\[ transpose \colon \text{Hom} \left( -, (A^{B})^{C} \right) \to \text{Hom}( - \times C, A^{B}) \text{ is a natural transformation}. \] Proof.
f:id:hitotakuchan:20160715153254p:plain
任意の  f \colon X' \to X g \colon X \to (A^{B})^{C} に対して
\[
\begin{align*}
(f \times 1_{C})^{\ast}(\overline{g}) &= \overline{g} \circ (f \times 1_{C}) \\
&= \epsilon \circ (g \times 1_{C}) \circ (f \times 1_{C}) \\
&= \epsilon \circ \left( (g \circ f) \times 1_{C} \right) \\
&= \overline{g \circ f} \\
&= \overline{f^{\ast}(g)}
\end{align*}
\]

 \square

 Lemma
\[ transpose \colon \text{Hom}( - \times C, A^{B}) \to \text{Hom} \left( (- \times C) \times B, A \right) \text{ is a natural transformation}. \] Proof.
f:id:hitotakuchan:20160715153305p:plain
任意の  f \colon X' \to X g \colon X \times C \to A^{B} に対して
\[
\begin{align*}
\left( (f \times 1_{C}) \times 1_{B} \right)^{\ast}(\overline{g}) &= \overline{g} \circ \left( (f \times 1_{C}) \times 1_{B} \right) \\
&= \epsilon \circ (g \times 1_{B}) \circ \left( (f \times 1_{C}) \times 1_{B} \right) \\
&= \epsilon \circ \left( (g \circ (f \times 1_{C}) \times 1_{B} \right) \\
&= \overline{g \circ (f \times 1_{C})} \\
&= \overline{(f \times 1_{C})^{\ast}(g)}
\end{align*}
\]

 \square

 Lemma
\[ \left< \left<\pi_{-}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right>^{\ast} \colon \text{Hom} \left( (- \times C) \times B, A \right) \to \text{Hom} \left( - \times (B \times C), A \right) \text{ is a natural transformation}. \] Proof.
f:id:hitotakuchan:20160715153316p:plain
任意の  f \colon X' \to X g \colon \left( (X \times C) \times B \right) \to A に対して
\[
\begin{align*}
\left( (f \times 1_{B \times C})^{\ast} \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right>^{\ast} \right)(g) &= g \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \circ (f \times 1_{B \times C}) \\
&= g \circ \left( (f \times 1_{C}) \times 1_{B} \right) \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \\
&= \left( \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right>^{\ast} \circ \left( (f \times 1_{C}) \times 1_{B} \right)^{\ast} \right)(g)
\end{align*}
\]
が成り立つことを示せばよい。これはつまり
  \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \circ (f \times 1_{B \times C}) =  \left( (f \times 1_{C}) \times 1_{B} \right) \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right>
を示せばよい。
\[
\begin{align*}
\pi_{X} \circ \pi_{X \times C} \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \circ (f \times 1_{B \times C}) &= \pi_{X} \circ (f \times 1_{B \times C}) \\
&= f \circ \pi_{X}
\end{align*}
\]\[
\begin{align*}
\pi_{X} \circ \pi_{X \times C} \circ \left( (f \times 1_{C}) \times 1_{B} \right) \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> &= \pi_{X} \circ (f \times 1_{C}) \circ \pi_{X \times C} \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \\
&= f \circ \pi_{X} \circ \pi_{X \times C} \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \\
&= f \circ \pi_{X}
\end{align*}
\]
\[
\begin{align*}
\pi_{C} \circ \pi_{X \times C} \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \circ (f \times 1_{B \times C}) &= \pi_{C} \circ \pi_{B \times C} \circ (f \times 1_{B \times C}) \\
&= \pi_{C} \circ \pi_{B \times C}
\end{align*}
\]\[
\begin{align*}
\pi_{C} \circ \pi_{X \times C} \circ \left( (f \times 1_{C}) \times 1_{B} \right) \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> &= \pi_{C} \circ (f \times 1_{C}) \circ \pi_{X \times C} \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \\
&= \pi_{C} \circ \pi_{X \times C} \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \\
&= \pi_{C} \circ \pi_{B \times C}
\end{align*}
\]
\[
\begin{align*}
\pi_{B} \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \circ (f \times 1_{B \times C}) &= \pi_{B} \circ \pi_{B \times C} \circ (f \times 1_{B \times C}) \\
&= \pi_{B} \circ \pi_{B \times C}
\end{align*}
\]\[
\begin{align*}
\pi_{B} \circ \left( (f \times 1_{C}) \times 1_{B} \right) \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> &= \pi_{B} \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \\
&= \pi_{B} \circ \pi_{B \times C}
\end{align*}
\]
以上が成り立つことと product の UMP より   \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> \circ (f \times 1_{B \times C}) =  \left( (f \times 1_{C}) \times 1_{B} \right) \circ \left< \left< \pi_{X}, \pi_{C} \circ \pi_{B \times C} \right>, \pi_{B} \circ \pi_{B \times C} \right> が成り立つ。

 \square

 Lemma
\[ transpose \colon \text{Hom} \left( - \times (B \times C), A \right) \to \text{Hom}( -, A^{B \times C}) \text{ is a natural transformation}. \] Proof.
f:id:hitotakuchan:20160715153323p:plain
任意の  f \colon X' \to X g \colon X \times (B \times C) \to A に対して
\[
\begin{align*}
\overline{f^{\ast}(\widetilde{g})} &= \overline{\widetilde{g} \circ f} \\
&= \epsilon \circ ( \widetilde{g} \circ f \times 1_{B \times C}) \\
&= \epsilon \circ (\widetilde{g} \times 1_{B \times C}) \circ (f \times 1_{B \times C}) \\
&= g \circ (f \times 1_{B \times C}) \\
&= (f \times 1_{B \times C})^{\ast}(g)
\end{align*}
\]
が成り立つので、exponential の UMP より  f^{\ast}(\widetilde{g}) = \widetilde{(f \times 1_{B \times C})^{\ast}(g)} が成り立つ。

 \square

Proposition 8.6

上の証明と同様に証明できるので省略しますが、ここでは covariant 版の米田の埋め込みが使われていることに注意してください。

8.5 Limits in categories of diagrams

Proposition 8.7

ここでは  \varprojlim_{i \in J}{F_{i}} \colon {\bf{C}}^{\text{op}} \to {\bf{Sets}} が functor であること。またそれが  {\bf{Sets}}^{{\bf{C}}^{\text{op}}} において limit となることの証明が省略されています。これらの事柄を確認しておきましょう。証明を考える前に Proposition 5.21 を復習して、任意の small category  J と任意の functor  F \colon J \to  {\bf{Sets}}^{{\bf{C}}^{\text{op}}} に関して  F の limit が具体的にどのように構成されるかを再度確認しておいてください。

 Lemma
\[ \left( \varprojlim_{i \in J} F_{i} \right) \text{ is a functor}. \] Proof.
任意の  C \in {\bf{C}} に対して  \left( \varprojlim_{i \in J}{F_{i}} \right)(C) = \varprojlim_{i \in J} (F_{i}C) で定義する。
次に任意の  f \colon C' \to C に対して次の diagram を考える。ただし  \phi,\psi などは Proposition 5.21 と同様に定義されているとする。
f:id:hitotakuchan:20160722162832p:plain
このとき任意の  \alpha \colon i \to j に対して  F(\alpha) が natural transformation であるから以下の diagram が可換となる。
f:id:hitotakuchan:20160722163817p:plain
このことに注意すると
\[\begin{align*}
\pi_{\alpha} \circ \psi \circ \left< F_{i}(f) \circ \pi_{i} \right>_{i \in J} \circ e_{C} &= F(\alpha)_{C'} \circ \pi_{i} \circ \left< F_{i}(f) \circ \pi_{i} \right>_{i \in J} \circ e_{C} \\
&= F(\alpha)_{C'} \circ F_{i}(f) \circ \pi_{i} \circ e_{C} \\
&= F_{j}(f) \circ F(\alpha)_{C} \circ \pi_{i} \circ e_{C} \\
&= F_{j}(f) \circ \pi_{\alpha} \circ \psi \circ e_{C} \\
&= F_{j}(f) \circ \pi_{\alpha} \circ \phi \circ e_{C} \\
&= F_{j}(f) \circ \pi_{j} \circ e_{C} \\
&= \pi_{\alpha} \circ \phi \circ \left< F_{i}(f) \circ \pi_{i} \right>_{i \in J} \circ e_{C}
\end{align*}\]
が成り立つので、product の UMP より  \psi \circ \left< F_{i}(f) \circ \pi_{i} \right>_{i \in J} \circ e_{C} = \phi \circ \left< F_{i}(f) \circ \pi_{i} \right>_{i \in J} \circ e_{C} が成り立つ。よって equalizer の UMP より diagram を可換とするような  f' \colon \varprojlim_{i \in J} F_{i}C \to \varprojlim_{i \in J} F_{i}C' がただ一つ存在する。
そこで   \left( \varprojlim_{i \in J} F_{i} \right)(f) = f' と定義する。


 \left( \varprojlim_{i \in J} F_{i} \right)(f) \colon \varprojlim_{i \in J} F_{i}C \to \varprojlim_{i \in J} F_{i}C' = \left( \varprojlim_{i \in J} F_{i} \right)(C) \to \left( \varprojlim_{i \in J} F_{i} \right)(C') より  \left( \varprojlim_{i \in J} F_{i} \right) は functor の条件 (a) を満たす。
次に equalizer の UMP より  \left( \varprojlim_{i \in J} F_{i} \right)(1_{C}) = 1_{\left( \varprojlim_{i \in J} F_{i} \right)(C)} が成り立つので、 \left( \varprojlim_{i \in J} F_{i} \right) は functor の条件 (b) を満たす。
最後に任意の  f \colon C' \to C g \colon C'' \to C' に対して、
\[\begin{align*}
\pi_{i} \circ e_{C''} \circ \left( \varprojlim_{i \in J} F_{i} \right)(f \circ g) &= \pi_{i} \circ \left< F(f \circ g) \circ \pi_{i} \right>_{i \in J} \circ e_{C} \\
&= F(g) \circ F(f) \circ \pi_{i} \circ e_{C} \\
&= \pi_{i} \circ \left< F(g) \circ \pi_{i} \right>_{i \in J} \circ \left< F(f) \circ \pi_{i} \right>_{i \in J} \circ e_{C} \\
&= \pi_{i} \circ e_{C''} \circ \left( \varprojlim_{i \in J} F_{i} \right)(g) \circ \left( \varprojlim_{i \in J} F_{i} \right)(f)
\end{align*}\]
が成り立つので、product の UMP と equalizer の UMP より  \left( \varprojlim_{i \in J} F_{i} \right)(f \circ g) = \left( \varprojlim_{i \in J} F_{i} \right)(g) \circ \left( \varprojlim_{i \in J} F_{i} \right)(f) が成り立つ。よって  \left( \varprojlim_{i \in J} F_{i} \right) は functor の条件 (c) を満たす。

 \square

次に  \theta_{i} \colon \left( \varprojlim_{i \in J} F_{i} \right) \to F_{i} を任意の  C \in {\bf{C}} に対して  {\theta_{i}}_{C} = \pi_{i} \circ e_{C} で定義します。ここで  e_{C} は上で  \left( \varprojlim_{i \in J} F_{i} \right) を定義する際に出てきたものとします。このとき  \left( \left( \varprojlim_{i \in J} F_{i} \right), (\theta_{i})_{i \in J} \right) F の limit となることを証明します。

 Lemma
\[ \left( \left( \varprojlim_{i \in J} F_{i} \right), (\theta_{i})_{i \in J} \right) \text{ is a cone of diagram } F. \] Proof.
はじめに  \theta_{i} が natural transformation となることを示す。
任意の  f \colon C' \to C に対して以下の diagram が可換になることを示せばよい。
f:id:hitotakuchan:20160722180440p:plain
\[\begin{align*}
{\theta_{i}}_{C'} \circ \left( \varprojlim_{i \in J} F_{i} \right)(f) &= \pi_{i} \circ e_{C'} \circ \left( \varprojlim_{i \in J} F_{i} \right)(f) \\
&= \pi_{i} \circ \left< F_{i}(f) \circ \pi_{i} \right>_{i \in J} \circ e_{C} \\
&= F_{i}(f) \circ \pi_{i} \circ e_{C} \\
&= F_{i}(f) \circ {\theta_{i}}_{C}
\end{align*}\]
よって  \theta_{i} は natural transformation である。

次に任意の  \alpha \colon i \to j に対して
\[\begin{align*}
F(\alpha)(C) \circ {\theta_{i}}_{C} &= F(\alpha)(C) \circ \pi_{i} \circ e_{C} \\
&= \pi_{\alpha} \circ \psi \circ e_{C} \\
&= \pi_{\alpha} \circ \phi \circ e_{C} \\
&= \pi_{j} \circ e_{C} \\
&= {\theta_{j}}_{C}
\end{align*}\]
が成り立つので  \left( \left( \varprojlim_{i \in J} F_{i} \right), (\theta_{i})_{i \in J} \right) は diagram  F の cone である。

 \square

最後に  \left( \varprojlim_{i \in J} F_{i} \right) が limit であることを証明する。

 Lemma
\[ \left( \varprojlim_{i \in J} F_{i} \right) \text{ is a limit of diagram } F. \] Proof.
f:id:hitotakuchan:20160723133652p:plain
 \left( G, (\eta_{i})_{i \in J} \right) を diagram  F の任意の cone とする。このとき Proposition 5.21 の議論にあるように、任意の  C \in {\bf{C}} に対して  \phi \circ \left< {\eta_{i}}_{C} \right>_{i \in J} = \psi \circ \left< {\eta_{i}}_{C} \right>_{i \in J} が成り立つので、 e_{C} \circ \mu_{C} = \left< {\eta_{i}}_{C} \right>_{i \in J} を満たす  \mu_{C} \colon G(C) \to \left( \varprojlim_{i \in J} F_{i} \right)(C) がただ一つ存在する。このとき  \mu \colon G \to \left( \varprojlim_{i \in J} F_{i} \right) が natural transformation となることを示す。
f:id:hitotakuchan:20160723133707p:plain
任意の  f \colon C' \to C と任意の  i \in J に対して
\[\begin{align*}
\pi_{i} \circ e_{C'} \circ \mu_{C'} \circ G(f) &= \pi_{i} \circ \left< {\eta_{i}}_{C'} \right>_{i \in J} \circ G(f) \\
&= {\eta_{i}}_{C'} \circ G(f) \\
&\underset{\eta_{i} \text{ is natural}}{=} F_{i}(f) \circ {\eta_{i}}_{C} \\
&= \pi_{i} \circ \left< F_{i}(f) \circ \pi_{i} \right>_{i \in J} \circ e_{C} \circ \mu_{C} \\
&= \pi_{i} \circ e_{C'} \circ \left( \varprojlim_{i \in J} F_{i} \right)(f) \circ \mu_{C}
\end{align*}\]
が成り立つので、product の UMP と equalizer の UMP より  \mu_{C'} \circ G(f) = \left( \varprojlim_{i \in J} F_{i} \right)(f) \circ \mu_{C} が成り立つ。

次に任意の  \nu \colon G \to \left( \varprojlim_{i \in J} F_{i} \right) が cone  \left( G, (\eta_{i})_{i \in J} \right) から cone  \left( \left( \varprojlim_{i \in J} F_{i} \right), (\theta)_{i \in J} \right) への写像とすると任意の  C \in {\bf{C}} と任意の  i \in J に対して  \pi_{i} \circ e_{C} \circ \mu_{C} = {\theta_{i}}_{C} \circ \mu_{C} = {\eta_{i}}_{C} が成り立つので、product の UMP と equalizer の UMP より  \nu_{C} = \mu_{C} が成り立つ。よって  \left( \varprojlim_{i \in J} F_{i} \right) は diagram  F の limit である。

 \square

8.6 Colimits in categories of diagrams

Proposition 8.10

証明が省略されている箇所がいくつかあるので補っておきます。
任意の  x \in P(C) に対して米田の補題によって対応する natural transformation をここでは  \theta_{x} と書くことにします。米田の補題の証明を見返して  \theta_{x} の定義を再確認してください。
はじめに任意の  h \colon (x', C') \to (x, C) に対して  \theta_{x} \circ yh = \theta_{x'} が成り立つことを証明します。

 Lemma
\[ \theta_{x} \circ yh = \theta_{x'} \] Proof.
f:id:hitotakuchan:20160728135800p:plain
任意の  C'' \in {\bf{C}} と任意の  f \colon C'' \to C' に対して
\[\begin{align*}
\left( (\theta_{x})_{C''} \circ yh \right)(f) &= P(h \circ f)(x) \\
&= \left( P(f) \circ P(h) \right)(x) \\
&= P(f)(x') \\
&= (\theta_{x'})_{C''}(f)
\end{align*}\]

 \square

次に  \theta \colon P \to Q \theta_{C}(x) = (\theta_{(x,C)})_{C}(1_{C}) で定義するとき、 \theta \circ \theta_{x} = \theta_{(x,C)} が成り立つことを証明します。

 Lemma
\[ \theta \circ \theta_{x} = \theta_{(x,C)} \] Proof.
f:id:hitotakuchan:20160729171552p:plain
任意の  g \colon C'' \to C に対して、 Q が cocone であることより上の右の diagram が可換になることに注意すると
\[\begin{align*}
\left( \theta_{C''} \circ (\theta_{x})_{C''} \right)(g) &= \theta_{C''} \left( P(g)(x) \right) \\
&= \left( \theta_{\left( P(g)(x), C'' \right)} \right)_{C''}(1_{C''}) \\
&= \left( (\theta_{(x, C)})_{C''} \circ \text{Hom}(-, g) \right)(1_{C''}) \\
&= (\theta_{(x, C)})_{C''}(g)
\end{align*}\]
が成り立つ。

 \square

次に  \theta が natural transformation であることを証明します。

 Lemma
\[ \theta \text{ is a natural transformation}. \] Proof.
f:id:hitotakuchan:20160909101920p:plain
任意の  f \colon C' \to C と任意の  x \in PC に対して、 \theta_{(x, C)} が natural transformation であるから上の右の diagram が可換になることに注意すると
\[\begin{align*}
\left( Q(f) \circ \theta_{C} \right)(x) &= \left( Q(f) \circ ( \theta_{(x, C)})_{C} \right)(1_{C}) \\
&= \left( (\theta_{(x,C)})_{C'} \circ \text{Hom}(f, -) \right)(1_{C}) \\
&= (\theta_{(x,C)})_{C'}(f)
\end{align*}\]
が成り立つ。一方先程の証明と同様に  \theta_{\left( P(f)(x), C' \right)} = \theta_{(x, C)} \circ yf が成り立つことに注意すると
\[\begin{align*}
\left( \theta_{C'} \circ P(f) \right)(x) &= (\theta_{\left( P(f)(x), C' \right)})_{C'}(1_{C'}) \\
&= \left( (\theta_{(x, C)})_{C'} \circ \text{Hom}(-, f) \right)(1_{C'}) \\
&= (\theta_{(x, C)})_{C'}(f)
\end{align*}\]
が成り立つ。

 \square

最後に  \theta が unique に決まることを証明します。

 Lemma
\[ \forall \varphi \colon P \to Q,\ \forall C,\ \forall x \in PC,\ \varphi \circ \theta_{x} = \theta_{(x, C)} \Rightarrow \varphi = \theta \] Proof.
任意の  x \in PC に対して
\[\begin{align*}
\varphi_{C}(x) &= \left( \varphi_{C} \circ (\theta_{x})_{C} \right)(1_{C}) \\
&= (\varphi \circ \theta_{x})_{C}(1_{C}) \\
&= (\theta_{(x,C)})_{C}(1_{C}) \\
&= \theta_{C}(x)
\end{align*}\]
が成り立つので  \varphi = \theta である。

 \square

8.7 Exponentials in categories of diagrams

ここでは  \theta_{j} \times B が cocone となることの証明が省略されていますが、これは簡単なので確認しておいてください。
次の  \theta_{C} が isomorphism であることを証明する箇所で  A_{j},B が集合であるとみなしてよいという点がわかりにくいかもしれません。
Propostiion 8.7 や 8.8 の議論から functor category においては limit や colimit は pointwise に定義されるのでした。そこで  \theta_{C} \colon \left( \varinjlim_{j}(A_{j} \times B) \right) (C) \to \left( (\varinjlim_{j} A_{j}) \times B \right)(C) の domain と codomain を展開すると  \theta_{C} \colon \varinjlim_{j} \left( A_{j}(C) \times B(C) \right) \to \left( \varinjlim_{j} A_{j}(C) \right) \times B(C) となります。 A_{j}(C) B(C) は集合です。そこで、 (C) の部分を書くのを省略して(記号を乱用して)  A_{j}, B を初めから集合とみなして考えましょうということです。

書籍では covariant 版の米田の補題を用いて  \varinjlim_{j}(A_{j} \times B) \cong (\varinjlim_{j} A_{j}) \times B を証明するという方針がとられています。証明では同型射であることは示されていますが、 X に関して natural であることの証明が省略されているので、これを補っておきます。

 \text{Hom} \left( \varinjlim_{j}(A_{j} \times B), X \right) \cong \varprojlim_{j} \text{Hom} (A_{j} \times B, X)

まず、任意の  X に対して  \text{Hom} \left( \varinjlim_{j}(A_{j} \times B), X \right) \cong \varprojlim_{j} \text{Hom} (A_{j} \times B, X) を証明します。

 Lemma
\[ \text{Hom} \left( \varinjlim_{j}(A_{j} \times B), X \right) \cong \varprojlim_{j} \text{Hom} (A_{j} \times B, X) \] Proof.
Proposition 5.21 の議論から colimit は以下の diagram によって具体的に構成される。
f:id:hitotakuchan:20160804114324p:plain
Corollary 5.27 より contravariant representable functor によって全ての colimit は limit に移されることに注意して以下の diagram を考える。
f:id:hitotakuchan:20160804121117p:plain
ここで  (- \times B) \circ A A \times B と表すとすると、 \phi',\ \psi' はそれぞれ  \pi_{\alpha} \circ \phi' = \pi_{i},\ \pi_{\alpha} \circ \psi' = (A \times B)(\alpha)^{\ast} \circ \pi_{j} を満たす。

  •  \theta_{X} の定義

任意の  f \colon \varinjlim_{i} (A_{i} \times B) \to X に対して、 (\phi^{\ast} \circ e^{\ast})(f) = f \circ e \circ \phi = f \circ e \circ \psi = (\psi^{\ast} \circ e^{\ast})(f) が成り立つ。よって  f \circ e \circ i_{i} = f \circ e \circ \phi \circ i_{\alpha} = f \circ e \circ \psi \circ i_{\alpha} = f \circ e \circ i_{j} \circ (A \times B)(\alpha) が成り立つことに注意すると、
\[\begin{align*}
(\pi_{\alpha} \circ \phi' \circ \left< - \circ i_{i} \right>_{i \in J} \circ e^{\ast})(f) &= \pi_{i} \circ \left< f \circ e \circ i_{i} \right>_{i \in J} \\
&= f \circ e \circ i_{i} \\
&= f \circ e \circ i_{j} \circ (A \times B)(\alpha) \\
&= (A \times B)(\alpha)^{\ast} \circ \pi_{j} \circ \left< f \circ e \circ i_{i} \right>_{i \in J} \\
&= (\pi_{\alpha} \circ \psi' \circ \left< - \circ i_{i} \right>_{i \in J} \circ e^{\ast})(f)
\end{align*}\]
が成り立つ。よって product の UMP と equalizer の UMP より  e' \circ \theta_{X} = \left< - \circ i_{i} \right>_{i \in J} \circ e^{\ast} を満たすただ一つの  \theta_{X} が存在する。

  •  \theta_{X}^{-1} の定義

任意の  g \in \varprojlim_{i} \text{Hom} \left( (A_{i} \times B), X \right) に対して、 \left( \phi^{\ast} \circ \left[ \pi_{i}(-) \right]_{i \in J} \circ e' \right)(g) = \left[ \pi_{i} \left( e'(g) \right) \right]_{i \in J} \circ \phi であることに注意すると、
\[\begin{align*}
\left[ \pi_{i} \left( e'(g) \right) \right]_{i \in J} \circ \phi \circ i_{\alpha} &= \left[ \pi_{i} \left( e'(g) \right) \right]_{i \in J} \circ i_{i} \\
&= \pi_{i} \left( e' (g) \right) \\
&= (\pi_{\alpha} \circ \phi' \circ e')(g)
\end{align*}\]
同様に、
\[\begin{align*}
\left[ \pi_{i} \left( e'(g) \right) \right]_{i \in J} \circ \psi \circ i_{\alpha} &= \left[ \pi_{i} \left( e'(g) \right) \right]_{i \in J} \circ i_{j} \circ (A \times B)(\alpha) \\
&= \pi_{j} \left( e'(g) \right) \circ (A \times B)(\alpha) \\
&= (\pi_{\alpha} \circ \psi' \circ e')(g)
\end{align*}\]
が成り立つ。よって  \phi' \circ e' = \psi' \circ e' であるから、coproduct の UMP と equalizer の UMP より  e^{\ast} \circ \theta_{X}^{-1} = [ \pi_{i}(-) ]_{i \in J} \circ e' を満たすただ一つの  \theta_{X}^{-1} が存在する。

  •  \theta_{X} が isomorphism であること

 \left< - \circ i_{i} \right>_{i \in J} \circ \left[ \pi_{i}(-) \right]_{i \in J} = 1_{\prod_{i} \text{Hom} \left( (A_{i} \times B), X \right)} \left[ \pi_{i}(-) \right]_{i \in J} \circ \left< - \circ i_{i} \right>_{i \in J} = 1_{\text{Hom} \left( \coprod_{i}(A_{i} \times B), X \right)} が成り立つことは product の UMP、coproduct の UMP より容易に証明できる。
よって equalizer の UMP より  \theta_{X}^{-1} \circ \theta_{X} = 1_{\text{Hom} \left( \varinjlim_{i} (A_{i} \times B), X \right)} かつ  \theta_{X} \circ \theta_{X}^{-1} = 1_{\varprojlim_{i} \text{Hom} \left( (A_{i} \times B), X \right)} が成り立つので、 \theta_{X} は isomorphism である。

 \square

次に  \theta_{X} \colon \text{Hom} \left( \varinjlim_{j}(A_{j} \times B), X \right) \to \varprojlim_{j} \text{Hom} \left( (A_{j} \times B), X \right) が natural in X であることを証明します。任意の  h \colon X \to Y に対して  \varprojlim_{i} \text{Hom}\left( (A_{i} \times B), h \right) がどのように定義されるかは Proposition 8.7 の証明を参照してください。

 Lemma
\[ \theta \text{ is a natural transformation}. \] Proof.
f:id:hitotakuchan:20160804141626p:plain
任意の  h \colon X \to Y と任意の  f \colon \varinjlim_{i} (A_{i} \times B) \to X に対して、
\[\begin{align*}
\left( \pi_{i} \circ e'_{Y} \circ \varprojlim_{i} \text{Hom} \left((A_{i} \times B), h \right) \circ \theta_{X} \right)(f) &= \left( \pi_{i} \circ \left< \text{Hom}\left( (A_{i} \times B), h \right) \circ \pi_{i} \right>_{i \in J} \circ e'_{X} \circ \theta_{X} \right)(f) \\
&= \left( \text{Hom} \left( (A_{i} \times B), h \right) \circ \pi_{i} \circ \left< - \circ i_{i} \right>_{i \in J} \circ e^{\ast} \right)(f) \\
&= h \circ f \circ e \circ i_{i}
\end{align*}\]
一方で
\[\begin{align*}
(\pi_{i} \circ e'_{Y} \circ \theta_{Y} \circ h_{\ast})(f) &= \left( \pi_{i} \circ \left< - \circ i_{i} \right>_{i \in J} \circ e^{\ast} \circ h_{\ast} \right) (f) \\
&= h \circ f \circ e \circ i_{i}
\end{align*}\]
が成り立つ。よって product の UMP と  e'_{Y} が monic であることより  \theta は natural transformation となる。

 \square

 \varprojlim_{j} \text{Hom} \left( (A_{i} \times B), X \right) \cong \varprojlim_{j} \text{Hom} (A_{i}, X^{B})

任意の  i \in J に対して  \text{Hom} \left( (A_{i} \times B), X \right) \cong \text{Hom}(A_{i}, X^{B}) は exponential の UMP より成り立ちます。このとき、 \varprojlim_{j} \text{Hom} \left( (A_{i} \times B), X \right) \cong \varprojlim_{j} \text{Hom} (A_{i}, X^{B}) が成り立つことは自明でしょうか?
証明は上の証明とほとんど同じなので概略だけ示しておきます。

 Lemma
\[ \varprojlim_{j} \text{Hom} \left( (A_{i} \times B), X \right) \cong \varprojlim_{j} \text{Hom} (A_{i}, X^{B}) \] Proof.
f:id:hitotakuchan:20160805111721p:plain
上の証明と同様に diagram を可換とするような  \theta_{X} \theta_{X}^{-1} が equalizer の UMP よりただ一つ存在する。
 \left< \widetilde{\pi_{i}(-)} \right>_{i \in J} \left< \overline{\pi_{i}(-)} \right>_{i \in J} は明らかに逆射となるので equalizer の UMP により  \theta_{X} は isomorphism である。

 \square

次に  \theta が natural transformation となることを証明します。任意の  h \colon X \to Y に対して  h^{B} \colon X^{B} \to Y^{B} がどのように定義されるのか Proposition 6.7 の証明をみて再確認してください。

 Lemma
\[ \theta \text{ is a natural transformation}. \] Proof.
f:id:hitotakuchan:20160805114221p:plain
任意の  f \in \varprojlim_{i} \text{Hom} \left( (A_{i} \times B), X \right) に対して、
\[\begin{align*}
\left( \pi_{i} \circ e'_{Y} \circ \varprojlim_{i} \text{Hom} (A_{i}, h^{B}) \circ \theta_{X} \right)(f) &= \left( \pi_{i} \circ \left< \text{Hom}(A_{i}, h^{B}) \circ \pi_{i}(-) \right>_{i \in J} \circ e'_{X} \circ \theta_{X} \right)(f) \\
&= \left( \text{Hom}(A_{i}, h^{B}) \circ \pi_{i} \circ \left< \widetilde{\pi_{i}(-)} \right>_{i \in J} \circ e_{X} \right)(f) \\
&= h^{B} \circ \widetilde{\pi_{i} \left( e_{X}(f) \right)}
\end{align*}\]
が成り立つ。また、
\[\begin{align*}
\left( \pi_{i} \circ e'_{Y} \circ \theta_{Y} \circ \varprojlim_{i} \text{Hom} \left( (A_{i} \times B), h \right) \right)(f) &= \left( \pi_{i} \circ \left< \widetilde{ \pi_{i}(-) } \right>_{i \in J} \circ e_{Y} \circ \varprojlim_{i} \text{Hom} \left( (A_{i} \times B), h \right) \right)(f) \\
&= \left( \widetilde{ \pi_{i}(-) } \circ \left< \text{Hom} \left( (A_{i} \times B), h \right) \circ \pi_{i}(-) \right>_{i \in J} \circ e_{X} \right)(f) \\
&= \widetilde{h \circ \pi_{i} \left( e_{X}(f) \right)}
\end{align*}\]
が成り立つ。一方
\[\begin{align*}
eval_{Y} \circ \left( h^{B} \circ \widetilde{\pi_{i} \left( e_{X}(f) \right)} \times 1_{B} \right) &= eval_{Y} \circ ( h^{B} \times 1_{B}) \circ \left( \widetilde{ \pi_{i} \left( e_{X}(f) \right)} \times 1_{B} \right) \\
&= h \circ eval_{X} \circ \left( \widetilde{ \pi_{i} \left( e_{X}(f) \right)} \times 1_{B} \right) \\
&= h \circ \pi_{i} \left( e_{X}(f) \right)
\end{align*}\]
が成り立つので、exponential の UMP と product の UMP より  \varprojlim_{i} \text{Hom} (A_{i}, h^{B}) \circ \theta_{X} = \theta_{Y} \circ \varprojlim_{i} \text{Hom} \left( (A_{i} \times B), h \right) が成り立つ。

 \square


上の証明でわかるように natural transformation になることの証明が非常に面倒です。より簡単な証明はないのでしょうか?
今考えている圏が  {\bf{Sets}} であることを利用すると、もっと直接的に  \varinjlim_{j}(A_{j} \times B) \cong (\varinjlim_{j} A_{j}) \times B を示すことができます。

 Lemma
\[ \varinjlim_{j}(A_{j} \times B) \cong (\varinjlim_{j} A_{j}) \times B \] Proof.
ここでは  \coprod_{i} (A_{i} \times B) の要素を  \left( i, (a_{i}, b) \right) と表します。 u \colon \coprod_{i} (A_{i} \times B) \to \left( \coprod_{i} A_{i} \right) \times B u\left( \left( i, (a_{i}, b) \right) \right) = \left( (i, a_{i}), b \right) で定義する。すると  u が isomorphism となることは明らかである。このとき以下の diagram を考える。
f:id:hitotakuchan:20160808100525p:plain
任意の  \left( \alpha, (a_{i}, b) \right) \in \coprod_{\alpha \colon i \to j} (A_{i} \times B) に対して  (e' \circ u \circ \phi) \left( \alpha, (a_{i}, b) \right) = (e' \circ \phi') \left( (\alpha, a_{i}), b \right) = (e' \circ \psi') \left( (\alpha, a_{i}), b \right) = (e' \circ u \circ \psi) \left( \alpha, (a_{i}, b) \right) が成り立つので coequalizer の UMP より diagram を可換とする  \theta がただ一つ存在する。同様に  \theta^{-1} がただ一つ存在して、 u が isomorphism であるから coequalizer の UMP より  \theta は isomorphism となる。

 \square

Theorem 8.14

証明するべきことは  y(A \times B) \cong yA \times yB y(A^{B}) \cong yA^{yB} です。

 Lemma
\[ y(A \times B) \cong yA \times yB \] Proof.
natural isomorphism  \theta \colon y(A \times B) \to yA \times yB を構成すればよい。任意の  C \in {\bf{C}} に対して  \theta_{C} \colon \text{Hom}(C, A \times B) \to \text{Hom}(C,A) \times \text{Hom}(C, B) を任意の  h \colon C \to A \times B に対して  \theta_{C}(h) = (\pi_{A} \circ h, \pi_{B} \circ h) で定義する。すると product の UMP より  \theta_{C} は isomorphism となる。
次にこの  \theta C に関して natural であることを示す。
f:id:hitotakuchan:20160809104348p:plain
任意の  f \colon C' \to C と任意の  h \colon C \to A \times B に対して、 \left( (f^{\ast} \times f^{\ast}) \circ \theta_{C} \right)(h) = (\pi_{A} \circ h \circ f, \pi_{B} \circ h \circ f) = (\theta_{C'} \circ f^{\ast})(h) が成り立つ。

 \square

 Lemma
\[ y(A^{B}) \cong yA^{yB} \] Proof.
任意の  C \in {\bf{C}} に対して
\[\begin{align*}
y(A^{B})(C) = \text{Hom}(C, A^{B}) &\cong \text{Hom}(C \times B, A) \\
&= yA(C \times B) \\
&\cong \text{Hom} \left( y(C \times B), yA \right) \\
&\cong \text{Hom} ( yC \times yB, yA ) = yA^{yB}(C)
\end{align*}\]
が成り立つので、この isomorphism を  \theta_{C} とする。このとき  \theta C に関して natural であることを示せばよい。
その証明は今までの証明と同様なので省略する。

 \square

Theorem 8.14 は contravariant 版の米田の埋め込みに対しての定理ですが、covariant 版の米田の埋め込みに関してはどのようなことが成り立つでしょうか?考えて、証明してみてください。

8.8 Topoi

Proposition 8.18

書籍で  u_{C} の定義が与えられていますが、この表記はわかりにくいです。より正確には、 \theta \colon U \rightarrowtail E とすると任意の  e \in E(C) に対して  u_{C}(e) = \left\{ f \colon D \to C \ \middle|\ \exists y \in U(D),\ E(f)(e) = \theta_{D}(y) \right\} と定義されます。
このとき、 u_{C}(e) が sieve となること、つまり precomposition に対して閉じていることを確認する必要があります。さらに pullback condition に関しても証明する必要があります。

 Lemma
\[ u_{C}(e) \text{ is a sieve}. \] Proof.
任意の  g \colon F \to D と任意の  f \in u_{C}(e) に対して、 \exists y' \in U(F) が存在して  E(f \circ g)(e) = \theta_{F}(y') となることを示せばよい。
 f \in u_{C}(e) より、 \exists y \in U(D) が存在して  E(f)(e) = \theta_{D}(y) が成り立つ。 一方で  \theta が natural transformation であることより  E(g) \circ \theta_{D} = \theta_{F} \circ U(g) が成り立つことに注意すると、 E(f \circ g)(e) = \left( E(g) \circ E(f) \right)(e) = \left( E(g) \circ \theta_{D} \right)(y) = \left( \theta_{F} \circ U(g) \right)(y) = \theta_{F} \left( U(g)(y) \right) が成り立つ。
よって  y' = U(g)(y) とすれば、 f \circ g \in u_{C}(e) となるので  u_{C}(e) は sieve である。

 \square

 Lemma
\[ t \colon 1 \to \Omega \text{ is a subobject classifier}. \] Proof.
任意の  (X, \phi, \psi) u \circ \phi = t \circ \psi を満たすとする。このとき natural transformation  \exists \alpha \colon X \to U がただ一つ存在して  \phi = \theta \circ \alpha を満たすことを示せばよい。
任意の  C \in {\bf{C}} と任意の  x \in X(C) に対して  t_{C} が total sieve であることより、 1_{C} \colon C \to C \in u_{C} \left( \phi(x) \right) が成り立つ。言い換えると  \exists y \in U(C) が存在して  E(1_{C}) \left( \phi(x) \right) = \phi(x) = \theta_{C}(y) が成り立つ。そこで  \alpha_{C}(x) = y と定義する。このとき  \phi_{C}(x) = (\theta_{C} \circ \alpha_{C})(x) が成り立つ。

次に、任意の  f \colon C' \to C に対して
\[\begin{align*}
\theta_{C'} \circ U(f) \circ \alpha_{C} &= E(f) \circ \theta_{C} \circ \alpha_{C} \\
&= E(f) \circ \phi_{C} \\
&= \phi_{C'} \circ X(f) \\
&= \theta_{C'} \circ \alpha_{C'} \circ X(f)
\end{align*}\]
が成り立つ。 \theta_{C'} は monic であるから、 U(f) \circ \alpha_{C} = \alpha_{C'} \circ X(f) が成り立つ。よって  \alpha は natural transformation である。

最後に  \beta \colon X \to U を diagram を可換とするような natural transformation であるとする。
すると任意の  x \in X(C) に対して  \theta_{C} \left( \beta_{C}(x) \right) = \phi_{C}(x) = \theta_{C} \left( \alpha_{C}(x) \right) が成り立つが、 \theta_{C} は monic であるから、 \beta_{C}(x) = \alpha_{C}(x) となる。よって  \beta = \alpha となる。

 \square

参考書籍

Category Theory (Oxford Logic Guides)

Category Theory (Oxford Logic Guides)

圏論 原著第2版

圏論 原著第2版

圏論の入門書籍・入門資料まとめ

はじめに

圏論が数学のみならず幅広い自然科学の分野で利用されるに従って、これから専門的に圏論を学習したいという人がますます増えてくると予想されます。
また Haskell 等の関数型言語を勉強する中で、圏論について専門的に勉強するまではいかないけどどのような学問なのか知っておきたい、という人もいるでしょう。
以前は圏論について知ろうと思うと初見殺しとして有名な 圏論の基礎 や英語の専門書しか利用できなかったのですが、最近では圏論について日本語で読める書籍が揃ってきました。
また、教科書的なものに限らず読み物的な書籍も幾つか出版されています。

現状でも圏論について書かれた書籍はたくさんあると思います。また、ネット上にもたくさんの圏論に関する解説ブログや資料があります。それらを全て読んで紹介することは不可能なので、ここでは以下のような基準 (必ずしも厳密ではない) を設けた上で、私の独断で入門書・入門資料として適切と思われるものを選択してみました。

  • 圏論への入門を意図して書かれたものであること
  • 内容にある程度以上の信頼性があること
  • ロジックやトポロジー等の数学の専門分野の知識を前提とせず、圏論そのものを主題としているもの

初めはリストアップするだけになりますが、ここで紹介している書籍や資料に関しては詳しく読んだ上で書評を随時アップデートしていきます。

このまとめが、これから圏論に入門しようとしている人のよい道標になれば幸いです。

読み物

圏論の歩き方

圏論の歩き方

今読んでいます。読み次第書評を書きます。

数学教室 πの焼き方: 日常生活の数学的思考

数学教室 πの焼き方: 日常生活の数学的思考

専門書籍

Conceptual Mathematics: A First Introduction to Categories

Conceptual Mathematics: A First Introduction to Categories

この本は本当に数学の素養が一切ない人向けに書かれた圏論の入門書です。数学の素養がなくても理解できる例を導入することから始まり、圏論の基本的な概念の導入まで書かれています。
ただし後半にいくほどに出てくる圏論の概念自体が難しくなっていくので、学習曲線が急になり次第に理解できなくなっていくと思います。Part Ⅳ あたりまで読んだら次の Awodey 本などに移行してもっと厳密な数学の証明スタイルに馴染んでいく必要があると思います。
一方で数学の素養がある人にとっては、ほとんど自明な話が延々と続いてやっと面白いと思う事柄が出てきたら終了するという感じになって物足りなさを感じると思います。流し読みするくらいの感じでいいと思います。


Category Theory (Oxford Logic Guides)

Category Theory (Oxford Logic Guides)

圏論 原著第2版

圏論 原著第2版

入門書の中では日本語で読める唯一の書籍です。
2017 年 1 月 29 日に下の ベーシック圏論 普遍性からの速習コース が発売されました。
数学の素養を持たない人でも読めるようにと書かれていますが、集合論や位相論の知識は前提としていると思われます。ラムダ計算やロジックの例がたくさん出てくることから、計算機科学や論理学の知識があるとより読みやすいでしょう。
内容は定義、例、定理、証明という数学の専門書のスタイルで書かれています。証明は厳密で埋めないといけない行間はあまりないです。ですが、数学の素養がないとやはり証明を理解するのも難しいと思うので、私のこちらの記事などを参照して自分がこの本を読む準備ができているか確認してみてください。

ベーシック圏論 普遍性からの速習コース

ベーシック圏論 普遍性からの速習コース

Basic Category Theory (Cambridge Studies in Advanced Mathematics)

Basic Category Theory (Cambridge Studies in Advanced Mathematics)

すでに数学の素養があるのであれば、Awodey 本よりこちらの方がおすすめだという人もいます。私は詳しく読んでいないので、読んだら感想を追記します。


Category Theory for Computing Science (Prentice-hall International Series in Computer Science)

Category Theory for Computing Science (Prentice-hall International Series in Computer Science)

こちらも入門書としての評価は高いです。Fibration や Topos に章が割かれておりここまで紹介した書籍の中では一番専門的な内容になっていると思います。
目次の内容からはそこまで計算機科学に特化しているようには見えません。
PDF が以下で配布されています。
http://www.math.mcgill.ca/triples/Barr-Wells-ctcs.pdf


Category Theory for the Sciences (MIT Press)

Category Theory for the Sciences (MIT Press)

最近話題の関手データモデルの考案者 David Spivak による圏論の入門書です。Chapter 5 で関手データモデルも紹介されています。
関手データモデルについては詳しく勉強したいのですが、圏論の入門書としては少し物足りない感じがします。
この書籍は無料で PDF 版が以下で配布されています。
http://math.mit.edu/~dspivak/teaching/sp13/CT4S.pdf

より専門的な内容のもの

圏論の勉強をしていて分からないことがあったら一番最初に参照するサイトです。
ただし現在の圏論の最先端の知識を用いて極めて一般的、抽象的に定義などが書かれているため、検索でたどり着いたもののこれじゃない感を感じることがよくあります。
このサイトの記述、内容が理解できるようになったらその時点でかなりの圏論マスターじゃないかと思います。私はほとんど理解できません。


Category Theory in Context (Aurora: Dover Modern Math Originals)

Category Theory in Context (Aurora: Dover Modern Math Originals)

Chapter 6 のタイトルが All Concepts are Kan Extensions とあるので圏論の基礎と同程度の内容かと思います。ページ数が少なめで簡潔な記述になっています。すでに数学の素養のある人向けだと思います。
PDF が以下で配布されています。
http://www.math.jhu.edu/~eriehl/context.pdf


Categories for the Working Mathematician (Graduate Texts in Mathematics)

Categories for the Working Mathematician (Graduate Texts in Mathematics)

圏論の基礎

圏論の基礎

Awodey 本を読んだ後、あるいはホモロジー代数などを勉強したあとなら普通に読めるようです。私はまだ読んでませんが、読める気がします。
私が数学を勉強する前にこの本を読んだ時の絶望感は半端じゃありませんでした。数学の素養がない状態では間違ってもこの本で圏論に入門しようなどとは思わない方がいいと思います。
ですがこれから圏論を専門的に研究したり、利用していこうと思うのであれば、Awodey 本の内容では物足りなくて、この本を読んでやっと圏論の基礎を身につけたという段階のようです。
頑張って読みましょう。私も読みます。


Toposes, Triples and Theories (Grundlehren der mathematischen Wissenschaften)

Toposes, Triples and Theories (Grundlehren der mathematischen Wissenschaften)

上で紹介した Category Theory for Computing Science (Prentice-hall International Series in Computer Science) の著者らによる書籍です。タイトルにある Triples というのはモナドのことです。
PDF が以下で配布されています。
http://www.tac.mta.ca/tac/reprints/articles/12/tr12.pdf


Handbook of Categorical Algebra: Volume 1, Basic Category Theory: 001 (Encyclopedia of Mathematics and its Applications)

Handbook of Categorical Algebra: Volume 1, Basic Category Theory: 001 (Encyclopedia of Mathematics and its Applications)

Handbook of Categorical Algebra: Volume 3, Sheaf Theory: 003 (Encyclopedia of Mathematics and its Applications)

Handbook of Categorical Algebra: Volume 3, Sheaf Theory: 003 (Encyclopedia of Mathematics and its Applications)

twitter 上で圏論初心者を圏論上級者が殴る際に使われる武器。
Topos の話題が多いので数理論理学の人向けでしょうか。

終わりに

現在数学の素養が全くない状態でこれから圏論を専門的に勉強していきたいと考えている人が、いきなり圏論の勉強を始めても全く理解できないと思います。
そのような人が数学の何から勉強すればいいのか、どのような順序で勉強をすれば最短で圏論が理解できるようになるのかは以下の記事が参考になると思います。
www.orecoli.com

そんなに1から勉強している余裕はなくてとにかく圏論の書籍を読み始めたいという人には以下の記事が参考になると思います。
上で紹介した Awodey 本の副読本的な内容で書籍で省略されている証明や練習問題を中心に詳細な証明をしています。
www.orecoli.com


ここに挙げたものが全てではないですし、もっといいと思うものがあればコメント欄で教えて頂けると嬉しいです。

Steve Awodey の Category Theory を読む : Chapter 7

Steve Awodey の Category Theory を読む シリーズトップ

7.5 Examples of natural transformations

Exercise 9

任意の  U \subseteq B に対して  f^{\ast} \colon \mathcal{P}(B) \to \mathcal{P}(A) f^{\ast}(U) = \left\{ a \in A \ \middle| \ f(a) \in U \right\} と表すことができます。
同様に任意の  V \subseteq \mathcal{P}(A) に対して  f^{\ast\ast} \colon \mathcal{PP}(A) \to \mathcal{PP}(B) f^{\ast\ast}(V) = \left\{ U \in \mathcal{P}(B) \ \middle|\ f^{\ast}(U) \in V \right\} と表されます。

 Lemma
\[ \eta \colon 1_{\bf{Sets}} \to \ast\ast \text{ is a natural transformation}. \] Proof.
任意の集合  A, B と任意の  f \colon A \to B に対して  f^{\ast\ast} \circ \eta_{A} = \eta_{B} \circ f が成り立つことを示せばよい。
任意の  a \in A に対して
\[
\begin{align*}
(f^{\ast\ast} \circ \eta_{A})(a) &= f^{\ast\ast} \left( \left\{ U \subseteq A \ \middle| \ a \in U \right\} \right) \\
&= \left\{ V \in \mathcal{P}(B) \ \middle| \ f^{\ast}(V) \in \left\{ U \subseteq A \ \middle| \ a \in U \right\} \right\} \\
&= \left\{ V \subseteq B \ \middle| \ a \in f^{-1}(V) \right\} \\
&= \left\{ V \subseteq B \ \middle| \ f(a) \in V \right\} \\
&= (\eta_{B} \circ f)(a)
\end{align*}
\]
が成り立つので、 \eta は natural transformation である。

 \square

7.6 Exponentials of categories

Proposition 7.13

書籍では、写像に対して片方の引数を固定した bifunctor を適用するとき  F(A, \beta) のように記述されていますが、これは厳密には  F_{1}(1_{A}, \beta) の意味であるということを確認しておきましょう。

 Lemma
\[ \epsilon \colon \text{Fun}({\bf{C}},{\bf{D}}) \times {\bf{C}} \to {\bf{D}} \text { is functorial}. \] Proof.
 \epsilon_{0} を任意の  F \in \text{Fun}({\bf{C}},{\bf{D}})_{0} と任意の  C \in {\bf{C}}_{0} に対して  \epsilon_{0}(F,C) = F(C) で定義する。また  \epsilon_{1} を任意の  \theta \colon F \to G \in \text{Fun}({\bf{C}},{\bf{D}})_{1} と任意の  f \colon C \to C' \in {\bf{C}}_{1} に対して  \epsilon_{1}(\theta, f) = G(f) \circ \theta_{C} で定義する。このとき bifunctor lemma より  \epsilon が functor となることを示す。

初めに  F \in \text{Fun}({\bf{C}},{\bf{D}})_{0} を固定すると、任意の  C \in {\bf{C}}_{0} と任意の  f \colon C \to C' \in {\bf{C}}_{1} に対して  \epsilon_{0}(F,C) = F(C) \epsilon_{1}(1_{F}, f) = F(f) \circ 1_{F(C)} = F(f) が成り立つ。よって  F が functor であることより  \epsilon(F, -) は functor である。

次に  C \in {\bf{C}}_{0} を固定すると、任意の  F \in \text{Fun}({\bf{C}},{\bf{D}})_{0} と任意の  \theta \colon F \to G \in \text{Fun}({\bf{C}},{\bf{D}})_{1} に対して  \epsilon(-, C)_{1}(\theta) = \epsilon_{1}(\theta, 1_{C}) = \theta_{C} \colon F(C) \to G(C) = \theta_{C} \colon \epsilon(-, C)_{0}(F) \to \epsilon(-,C)_{0}(G) が成り立つ。よって  \epsilon(-,C) は functor の条件 (a) を満たす。
また  \epsilon(-,C)_{1}(1_{F}) = \epsilon(1_{F}, 1_{C}) = 1_{FC} = 1_{\epsilon(-,C)_{0}(F)} が成り立つので  \epsilon(-,C) は functor の条件 (b) を満たす。
任意の  \theta' \colon G \to H \in \text{Fun}({\bf{C}},{\bf{D}})_{1} に対して  \epsilon(-,C)_{1}(\theta' \circ \theta) = H(1_{C}) \circ \theta'_{C} \circ \theta_{C} = \epsilon(-,C)_{1}(\theta') \circ \epsilon(-,C)_{1}(\theta) が成り立つので  \epsilon(-,C) は functor の条件 (c) を満たす。

 \epsilon が interchage law を満たすことは下の等しい diagram が可換になることと同値であるが、これは  \theta が natural transformation であることから自明である。

f:id:hitotakuchan:20160602133842p:plain

 \square

 Lemma
\[ \forall F \colon {\bf{X}} \times {\bf{C}} \to {\bf{D}},\, \exists \tilde{F} \colon {\bf{X}} \to \text{Fun}({\bf{C}}, {\bf{D}}),\, \epsilon \circ (\tilde{F} \times 1_{\bf{C}}) = F \] Proof.
 \tilde{F} \colon {\bf{X}} \to \text{Fun}({\bf{C}} を任意の  X \in {\bf{X}}_{0} と任意の  f \colon X \to X' \in {\bf{X}}_{1} に対して \tilde{F}_{0}(X) = F(X,-) \tilde{F}_{1}(f) = \left( F(f, 1_{C}) \right)_{C \in {\bf{C}}_{0}} で定義する。
このとき  \tilde{F}(f) が natural transformation になることは、任意の  C, C' \in {\bf{C}}_{0} と任意の  g \colon C \to C' に対して以下の diagram が可換になることと同値であるが、これは  F が functor であることより成り立つ。

f:id:hitotakuchan:20160603120017p:plain

次に  \tilde{F} が functor になることを示す。
上の議論より  \tilde{F}_{1}(f \colon X \to X') \colon \tilde{F}_{0}(X) \to \tilde{F}_{0}(X') となるので  \tilde{F} は functor の条件 (a) を満たす。
次に  \tilde{F}_{1}(1_{X}) = \left( F(1_{X}, 1_{C}) \right)_{C \in {\bf{C}}_{0}} = 1_{\tilde{F}_{0}(X)} であるから  \tilde{F} は functor の条件 (b) を満たす。
最後に  \tilde{F}_{1}(f' \circ f) = \left( F(f' \circ f, 1_{C}) \right)_{C \in {\bf{C}}_{0}} = \left( F(f', 1_{C}) \right)_{C \in {\bf{C}}_{0}} \circ \left( F(f, 1_{C}) \right)_{C \in {\bf{C}}_{0}} = \tilde{F}_{1}(f') \circ \tilde{F}_{1}(f) が成り立つので  \tilde{F} は functor の条件 (c) を満たす。

最後に  \epsilon_{0} \circ (\tilde{F} \times 1_{\bf{C}})_{0}(X, C) = \epsilon_{0}(F(X, -), C) = F_{0}(X,C) \epsilon_{1} \circ (\tilde{F} \times 1_{\bf{C}})_{1}(f, g) = \epsilon_{1}(\tilde{F}(f), g) = F(1_{X'}, g) \circ F(f, 1_{C}) = F_{1}(f, g) が成り立つので  \epsilon \circ (\tilde{F} \times 1_{\bf{C}}) = F が成り立つ。

 \square

 Lemma
\[ \forall G \colon {\bf{X}} \to \text{Fun}({\bf{C}}, {\bf{D}}),\, \widetilde{\left( \epsilon \circ (G \times 1_{\bf{C}}) \right)} = G \] Proof.
任意の  X \in {\bf{X}}_{0} と任意の  C \in {\bf{C}}_{0} に対して  \widetilde{\left( \epsilon \circ (G \times 1_{\bf{C}}) \right)}_{0}(X)(C) = \epsilon \circ (G \times 1_{\bf{C}})(X, C) = G(X)(C) が成り立つ。
また任意の  g \in {\bf{C}}_{1} に対して  \widetilde{\left( \epsilon \circ (G \times 1_{\bf{C}}) \right)}_{0}(X)(g) = \epsilon \circ (G \times 1_{\bf{C}})(1_{X}, g) = G(X)(g) \circ G(1_{X})_{C} = G(X)(g) が成り立つ。
次に任意の  f \colon X \to X' \in {\bf{X}}_{1} に対して   \widetilde{\left( \epsilon \circ (G \times 1_{\bf{C}}) \right)}_{1}(f) = \left( \left( \epsilon \circ (G \times 1_{\bf{C}}) \right)(f, 1_{C}) \right)_{C \in {\bf{C}}_{0}} = \left( \epsilon \circ \left( G(f), 1_{C} \right) \right)_{C \in {\bf{C}}_{0}} = \left( G(f)_{C} \right)_{C \in {\bf{C}}_{0}} = G(f) が成り立つ。
以上より  \widetilde{\left( \epsilon \circ (G \times 1_{\bf{C}}) \right)} = G が成り立つ。

 \square

7.8 Monoidal categories

Exercise 18

 \bf{C} が finite product を持つとき  ({\bf{C}}, \times, {\bf{1}}) が monoidal category になることを証明します。
初めに  \alpha \alpha = \left( \left< \left< \pi_{A}, \pi_{B} \circ \pi_{B \times C} \right>, \pi_{C} \circ \pi_{B \times C} \right> \right)_{(A,B,C) \in {\bf{C}} \times {\bf{C}} \times {\bf{C}}} で定義します。また  \lambda \lambda = \left( \pi_{A} \colon {\bf{1}} \times A \to A \right)_{A \in {\bf{C}}} で定義し、同様に  \rho を定義します。
このとき  \alpha \lambda \rho が natural isomorphism となることを証明します。

 Lemma
\[ \alpha \text{ is a natural isomorphism}. \] Proof.

  • 任意の  A,B,C に対して  \alpha_{ABC} が isomorphism であること

 \alpha_{ABC}^{-1} \alpha_{ABC}^{-1} = \left< \pi_{A} \circ \pi_{A \times B}, \left< \pi_{B} \circ \pi_{A \times B}, \pi_{C} \right> \right> で定義する。
 \pi_{A} \circ \alpha_{ABC}^{-1} \circ \alpha_{ABC} = \pi_{A} \circ \pi_{A \times B} \circ \alpha_{ABC} = \pi_{A} \circ \left< \pi_{A}, \pi_{B} \circ \pi_{B \times C} \right> = \pi_{A}
 \pi_{B} \circ \pi_{B \times C} \circ \alpha_{ABC}^{-1} \circ \alpha_{ABC} = \pi_{B} \circ \pi_{A \times B} \circ \alpha_{ABC} = \pi_{B} \circ \left< \pi_{A}, \pi_{B} \circ \pi_{B \times C} \right> = \pi_{B} \circ \pi_{B \times C}
 \pi_{C} \circ \pi_{B \times C} \circ \alpha_{ABC}^{-1} \circ \alpha_{ABC} = \pi_{C} \circ \alpha_{ABC} = \pi_{C} \circ \pi_{B \times C}
が成り立つので product の UMP より  \alpha_{ABC}^{-1} \circ \alpha_{ABC} = 1_{A \times (B \times C)} が成り立つ。
同様に
 \pi_{A} \circ \pi_{A \times B} \circ \alpha_{ABC} \circ \alpha_{ABC}^{-1} = \pi_{A} \circ \pi_{A \times B}
 \pi_{B} \circ \pi_{A \times B} \circ \alpha_{ABC} \circ \alpha_{ABC}^{-1} = \pi_{B} \circ \pi_{B \times C} \circ \alpha_{ABC}^{-1} = \pi_{B} \circ \pi_{A \times B}
 \pi_{C} \circ \alpha_{ABC} \circ \alpha_{ABC}^{-1} = \pi_{C} \circ \pi_{B \times C} \circ \alpha_{ABC}^{-1} = \pi_{C}
が成り立つので product の UMP より  \alpha_{ABC} \circ \alpha_{ABC}^{-1} = 1_{(A \times B) \times C} が成り立つ。
よって  \alpha_{ABC} は isomorphism である。

  •  \alpha が natural transformation であること

任意の  f \colon A \to A', g \colon B \to B', h \colon C \to C' に対して以下の diagram が可換になればよい。
f:id:hitotakuchan:20160608145327p:plain

 \pi_{A'} \circ \pi_{A' \times B'} \circ \left( (f \times g) \times h \right) \circ \alpha_{ABC} = \pi_{A'} \circ (f \times g) \circ \pi_{A \times B} \circ \alpha_{ABC} = f \circ \pi_{A} \circ \left< \pi_{A}, \pi_{B} \circ \pi_{B \times C} \right> = f \circ \pi_{A}
 \pi_{A'} \circ \pi_{A' \times B'} \circ \alpha_{A'B'C'} \circ \left(f \times (g \times h) \right) = \pi_{A'} \circ \left( f \times (g \times h) \right) = f \circ \pi_{A}

 \pi_{B'} \circ \pi_{A' \times B'} \circ \left( (f \times g) \times h \right) \circ \alpha_{ABC} = \pi_{B'} \circ (f \times g) \circ \pi_{A \times B} \circ \alpha_{ABC} = g \circ \pi_{B} \circ \left< \pi_{A}, \pi_{B} \circ \pi_{B \times C} \right> = g \circ \pi_{B} \circ \pi_{B \times C}
 \pi_{B'} \circ \pi_{A' \times B'} \circ \alpha_{A'B'C'} \circ \left( f \times (g \times h) \right) = \pi_{B'} \circ \pi_{B' \times C'} \circ \left( f \times (g \times h) \right) = \pi_{B'} \circ (g \times h) \circ \pi_{B \times C} = g \circ \pi_{B} \circ \pi_{B \times C}

 \pi_{C'} \circ \left( (f \times g) \times h \right) \circ \alpha_{ABC} = h \circ \pi_{C} \circ \alpha_{ABC} = h \circ \pi_{C} \circ \pi_{B \times C}
 \pi_{C'} \circ \alpha_{A'B'C'} \circ \left( f \times (g \times h) \right) = \pi_{C'} \circ \pi_{B' \times C'} \circ \left( f \times (g \times h) \right) = \pi_{C'} \circ (g \times h) \circ \pi_{B \times C} = h \circ \pi_{C} \circ \pi_{B \times C}

が成り立つので product の UMP より  \left((f \times g) \times h \right) \circ \alpha_{ABC} = \alpha_{A'B'C'} \circ \left( f \times (g \times h) \right) が成り立つ。

 \square

 Lemma
\[ \lambda \text{ is a natural isomorphism}. \] Proof.

  • 任意の  A に対して  \lambda_{A} が isomorphism であること

terminal object  \bf{1} への写像を  \bf{1} で表すとすると以下の diagram より  \pi_{A} \circ \left< {\bf{1}}, 1_{A} \right> = 1_{A} が成り立つ。
f:id:hitotakuchan:20160608151255p:plain

一方、 \pi_{A} \circ \left< {\bf{1}}, 1_{A} \right> \circ \pi_{A} = \pi_{A} が成り立つので、以下の diagram は可換になる。
f:id:hitotakuchan:20160608151412p:plain

よって product の UMP より  \left< {\bf{1}}, 1_{A} \right> \circ \pi_{A} = 1_{A} が成り立つ。以上より  \lambda_{A} = \pi_{A} は isomorphism である。

  •  \lambda が natural transformation であること

任意の  f \colon A \to A' に対して  \pi_{A'} \circ (1_{\bf{1}} \times f) = f \circ \pi_{A} が成り立つので、 \pi_{A} は natural transformation である。

 \square

 \rho の場合も同様に証明できます。
次に2つの diagram が可換になることを証明します。3つ目の diagram は初めの2つの diagram の可換性から証明できるので省略します。
diagram に現れる  \alpha_{ABC \times D}, \alpha_{A \times BCD}, \alpha_{AB \times CD} に関して  \alpha の定義より以下のことが成り立つことを確認しておきます。
 \alpha_{ABC \times D} = \left< \left< \pi_{A}, \pi_{B} \circ \pi_{B \times (C \times D)} \right>, \pi_{C \times D} \circ \pi_{B \times (C \times D)} \right>
 \alpha_{A \times BCD} = \left< \left< \pi_{A \times B}, \pi_{C} \circ \pi_{C \times D} \right>, \pi_{D} \circ \pi_{C \times D} \right>
 \alpha_{AB \times CD} = \left< \left< \pi_{A}, \pi_{B \times C} \circ \pi_{(B \times C) \times D} \right>, \pi_{D} \circ \pi_{(B \times C) \times D} \right>

 Lemma
\[ \forall A,B,C,D,\ \alpha_{A \times BCD} \circ \alpha_{ABC \times D} = (\alpha_{ABC} \times 1_{D}) \circ \alpha_{AB \times CD} \circ (1_{A} \times \alpha_{BCD}) \] Proof.
\[
\begin{align*}
\pi_{A} \circ \pi_{A \times B} \circ \pi_{(A \times B) \times C} \circ \alpha_{A \times BCD} \circ \alpha_{ABC \times D} &= \pi_{A} \circ \pi_{A \times B} \circ \left< \pi_{A \times B}, \pi_{C} \circ \pi_{C \times D} \right> \circ \alpha_{ABC \times D} \\
&= \pi_{A} \circ \pi_{A \times B} \circ \alpha_{ABC \times D} \\
&= \pi_{A} \left< \pi_{A}, \pi_{B} \circ \pi_{B \times (C \times D)} \right> \\
&= \pi_{A}
\end{align*}
\]\[
\begin{align*}
\pi_{A} \circ \pi_{A \times B} \circ \pi_{(A \times B) \times C} \circ (\alpha_{ABC} \times 1_{D}) \circ \alpha_{AB \times CD} \circ (1_{A} \times \alpha_{BCD}) &= \pi_{A} \circ \pi_{A \times B} \circ \alpha_{ABC} \circ \pi_{A \times (B \times C)} \circ \alpha_{AB \times CD} \circ (1_{A} \times \alpha_{BCD}) \\
&= \pi_{A} \circ \left< \pi_{A}, \pi_{B \times C} \circ \pi_{(B \times C) \times D} \right> \circ (1 \times \alpha_{BCD}) \\
&= \pi_{A} \circ (1 \times \alpha_{BCD}) \\
&= \pi_{A}
\end{align*}
\]
\[
\begin{align*}
\pi_{B} \circ \pi_{A \times B} \circ \pi_{(A \times B) \times C} \circ \alpha_{A \times BCD} \circ \alpha_{ABC \times D} &= \pi_{B} \circ \pi_{A \times B} \circ \left< \pi_{A \times B}, \pi_{C} \circ \pi_{C \times D} \right> \circ \alpha_{ABC \times D} \\
&= \pi_{B} \circ \pi_{A \times B} \circ \alpha_{ABC \times D} \\
&= \pi_{B} \circ \left< \pi_{A}, \pi_{B} \circ \pi_{B \times (C \times D)} \right> \\
&= \pi_{B} \circ \pi_{B \times (C \times D)}
\end{align*}
\]\[
\begin{align*}
\pi_{B} \circ \pi_{A \times B} \circ \pi_{(A \times B) \times C} \circ (\alpha_{ABC} \times 1_{D}) \circ \alpha_{AB \times CD} \circ (1_{A} \times \alpha_{BCD}) &= \pi_{B} \circ \pi_{A \times B} \circ \alpha_{ABC} \circ \pi_{A \times (B \times C)} \circ \alpha_{AB \times CD} \circ (1_{A} \times \alpha_{BCD}) \\
&= \pi_{B} \circ \pi_{B \times C} \circ \left< \pi_{A}, \pi_{B \times C} \circ \pi_{(B \times C) \times D} \right> \circ (1_{A} \times \alpha_{BCD}) \\
&= \pi_{B} \circ \pi_{B \times C} \circ \pi_{(B \times C) \times D} \circ (1_{A} \times \alpha_{BCD}) \\
&= \pi_{B} \circ \pi_{B \times C} \circ \alpha_{BCD} \circ \pi_{B \times (C \times D)} \\
&= \pi_{B} \circ \pi_{B \times (C \times D)}
\end{align*}
\]
\[
\begin{align*}
\pi_{C} \circ \pi_{(A \times B) \times C} \circ \alpha_{A \times BCD} \circ \alpha_{ABC \times D} &= \pi_{C} \circ \left< \pi_{A \times B}, \pi_{C} \circ \pi_{C \times D} \right> \circ \alpha_{ABC \times D} \\
&= \pi_{C} \circ \pi_{C \times D} \circ \alpha_{ABC \times D} \\
&= \pi_{C} \circ \pi_{C \times D} \circ \pi_{B \times (C \times D)}
\end{align*}
\]\[
\begin{align*}
\pi_{C} \circ \pi_{(A \times B) \times C} \circ (\alpha_{ABC} \times 1_{D}) \circ \alpha_{AB \times CD} \circ (1_{A} \times \alpha_{BCD}) &= \pi_{C} \circ \alpha_{ABC} \circ \pi_{A \times (B \times C)} \circ \alpha_{AB \times CD} \circ (1_{A} \times \alpha_{BCD}) \\
&= \pi_{C} \circ \pi_{B \times C} \circ \left< \pi_{A}, \pi_{B \times C} \circ \pi_{(B \times C) \times D} \right> \circ (1_{A} \times \alpha_{BCD}) \\
&= \pi_{C} \circ \pi_{B \times C} \circ \pi_{(B \times C) \times D} \circ (1_{A} \times \alpha_{BCD}) \\
&= \pi_{C} \circ \pi_{B \times C} \circ \alpha_{BCD} \circ \pi_{B \times (C \times D)} \\
&= \pi_{C} \circ \pi_{C \times D} \circ \pi_{B \times (C \times D)}
\end{align*}
\]
\[
\begin{align*}
\pi_{D} \circ \alpha_{A \times BCD} \circ \alpha_{ABC \times D} &= \pi_{D} \circ \pi_{C \times D} \circ \alpha_{ABC \times D} \\
&= \pi_{D} \circ \pi_{C \times D} \circ \pi_{B \times (C \times D)}
\end{align*}
\]\[
\begin{align*}
\pi_{D} \circ (\alpha_{ABC} \times 1_{D}) \circ \alpha_{AB \times CD} \circ (1_{A} \times \alpha_{BCD}) &= \pi_{D} \circ \alpha_{AB \times CD} \circ (1_{A} \times \alpha_{BCD}) \\
&= \pi_{D} \circ \pi_{(B \times C) \times D} \circ (1_{A} \times \alpha_{BCD}) \\
&= \pi_{D} \circ \alpha_{BCD} \circ \pi_{B \times (C \times D)} \\
&= \pi_{D} \circ \pi_{C \times D} \circ \pi_{B \times (C \times D)}
\end{align*}
\]
以上と product の UMP より  \alpha_{A \times BCD} \circ \alpha_{ABC \times D} = (\alpha_{ABC} \times 1_{D}) \circ \alpha_{AB \times CD} \circ (1_{A} \times \alpha_{BCD}) が成り立つ。

 \square

 Lemma
\[ \forall A,\ (\rho_{A} \times 1_{A}) \circ \alpha_{A{\bf{1}}A} = 1_{A} \times \lambda_{A} \] Proof.
 A \times A から  A への projection を  \pi_{1}, \pi_{2} で表すと、
 \pi_{1} \circ (\rho_{A} \times 1_{A}) \circ \alpha_{A{\bf{1}}A} = \pi_{1} \circ \pi_{A \times {\bf{1}}} \circ \alpha_{A{\bf{1}}A} = \pi_{A}
 \pi_{1} \circ (1_{A} \times \lambda_{A}) = \pi_{A}

 \pi_{2} \circ (\rho_{A} \times 1_{A}) \circ \alpha_{A{\bf{1}}A} = \pi_{A} \circ \alpha_{A{\bf{1}}A} = \pi_{A} \circ \pi_{{\bf{1}} \times A}
 \pi_{2} \circ (1_{A} \times \lambda_{A}) = \pi_{A} \circ \pi_{{\bf{1}} \times A}

が成り立つので product の UMP より  (\rho_{A} \times 1_{A}) \circ \alpha_{A{\bf{1}}A} = 1_{A} \times \lambda_{A} が成り立つ。

 \square

7.9 Equivalence of categories

Proposition 7.26

(2 implies 1) の証明の中で  E \colon {\bf{D}} \to {\bf{C}} を定義するために、任意の  D \in {\bf{D}}_{0} に対して  E(D) \in {\bf{C}}_{0} を選ぶ箇所で選択公理を仮定しています。

7.10 Examples of equivalence

Proposition 7.28

arrow  f \colon A \rightharpoondown B (U_{f} \subseteq A, f) と表すことにします。すると  {\bf{Par}} における写像の結合は  (U_{g}, g) \circ (U_{f}, f) = (f^{-1}(U_{g}), g \circ f) と表せます。

 Lemma
\[ {\bf{Par}} \text{ is a category}. \] Proof.
f:id:hitotakuchan:20160613142238p:plain
任意の  (U_{f}, f),(U_{g}, g), (U_{h}, h) に対して  (U_{h}, h) \circ \left( (U_{g}, g) \circ (U_{f}, f) \right) = (U_{h}, h) \circ \left( f^{-1}(U_{g}), g \circ f \right) = \left( (g \circ f)^{-1}(U_{h}), h \circ (g \circ f) \right) \left( (U_{h}, h) \circ (U_{g}, g) \right) \circ (U_{f}, f) = \left( g^{-1}(U_{h}), h \circ g \right) \circ (U_{f}, f) = \left( f^{-1} \left( g^{-1}(U_{h}) \right), (h \circ g) \circ f \right) が成り立つ。
 (g \circ f)^{-1}(U_{h}) = (f^{-1} \circ g^{-1})(U_{h}) h \circ (g \circ f) = (h \circ g) \circ f が成り立つので、 (U_{h}, h) \circ \left( (U_{g}, g) \circ (U_{f}, f) \right) = \left( (U_{h}, h) \circ (U_{g}, g) \right) \circ (U_{f}, f) が成り立つ。

f:id:hitotakuchan:20160613142252p:plain
また  (B, 1_{B}) \circ (U_{f}, f) = \left( f^{-1}(B), 1_{B} \circ f \right) = (U_{f}, f) (U_{f}, f) \circ (A, 1_{A}) = \left( 1_{A}^{-1}(U_{f}), f \circ 1_{A} \right) = (U_{f}, f) が成り立つ。

 \square

 Lemma
\[ F \colon {\bf{Par}} \to {\bf{Sets}}_{\ast} \text{ is a funcotr}. \] Proof.
書籍のように  F を定義すると、任意の  f \colon A \rightharpoondown B に対して  F(f) \colon F(A) \to F(B) となるので、 F は functor の条件 (a) を満たす。
次に  1_{A} \colon A \rightharpoondown A = (A, 1_{A}) であることに注意して、
\[
F(1_{A})(x) = F \left( (A, 1_{A}) \right)(x) =
\begin{cases}
x & \text{if } x \in A \\
\ast & \text{otherwise}
\end{cases}
\]
これは  1_{A_{\ast}} = 1_{F(A)} と等しい。よって  F は functor の条件 (b) を満たす。
最後に任意の  (U_{f}, f) \colon A \rightharpoondown B (U_{g}, g) \colon B \rightharpoondown C に対して
\[
F\left( (U_{g},g) \circ (U_{f}, f) \right)(x) =
\begin{cases}
(g \circ f)(x) & x \in f^{-1}(U_{g}) \\
\ast & \text{otherwise}
\end{cases}
\]
である。一方
\[
\begin{align*}
\left( F\left( (U_{g}, g) \right) \circ F \left( (U_{f}, f) \right) \right)(x) &= F \left( (U_{g}, g) \right) \circ
\begin{cases}
f(x) & x \in U_{f} \\
\ast & \text{otherwise}
\end{cases} \\
&=
\begin{cases}
g \left( f(x) \right) & f(x) \in U_{g} = x \in f^{-1}(U_{g}) \\
\ast & \text{otherwise}
\end{cases}
\end{align*}
\]
よって  F\left( (U_{g},g) \circ (U_{f}, f) \right) = F\left( (U_{g}, g) \right) \circ F \left( (U_{f}, f) \right) が成り立つので  F は functor の条件 (c) を満たす。

 \square

 Lemma
\[ G \colon {\bf{Sets}}_{\ast} \to {\bf{Par}} \text{ is a functor}. \] Proof.
書籍のように  G を定義すると、任意の  f \colon (A, a) \to (B, b) に対して  G(f) \colon G\left( (A, a) \right) \to G \left( (B, b) \right) となるので  G は functor の条件 (a) を満たす。
次に  G(1_{(A,a)}) = \left( A - 1_{A}^{-1}(a), 1_{A} \middle|_{A - 1_{A}^{-1}(a)} \right) = (A - \{ a \}, 1_{A - \{a \}}) = 1_{G\left( (A, a) \right)} が成り立つので  G は functor の条件 (b) を満たす。
最後に任意の  f \colon (A,a) \to (B, b) g \colon (B, b) \to (C, c) に対して
 G(g \circ f) = \left( A - (g \circ f)^{-1}(c), (g \circ f) \middle|_{A - (g \circ f)^{-1}(c)} \right)
 G(g) \circ G(f) = \left( B - g^{-1}(c), g \middle|_{B - g^{-1}(c)} \right) \circ \left( A - f^{-1}(b), f \middle|_{A - f^{-1}(b)} \right) = \left( f^{-1} \left( B - g^{-1}(c) \right), (g \circ f) \middle|_{f^{-1} \left( B - g^{-1}(c) \right)} \right)
が成り立つ。一方で
\[
\begin{align*}
x \in A - (g \circ f)^{-1}(c) &\iff x \in A \land g\left( f(x) \right) \neq c \\
&\iff x \in A \land f(x) \in B - g^{-1}(c) \\
&\iff x \in f^{-1} \left( B - g^{-1}(c) \right)
\end{align*}
\]
が成り立つので、 G(g \circ f) = G(g) \circ G(f) となり  G は functor の条件 (c) を満たす。

 \square

 Lemma
\[ G \circ F = 1_{\bf{Par}} \] Proof.
 (G \circ F)_{0}(A) = G( A \cup \{\ast\}) = (A \cup \{\ast\}) - \{\ast\} = {1_{\bf{Par}}}_{0}(A) が成り立つ。
一方  (G \circ F)_{1}(U_{f}, f) = G(f_{\ast}) = (U_{G(f_{\ast})}, f_{\ast}) となるが、 U_{G(f_{\ast})} = (A \cup \{\ast\}) - f_{\ast}^{-1}(\ast) = U_{f} が成り立つので、 (U_{G(f_{\ast})}, f_{\ast}) = (U_{f}, f) となる。よって  (G \circ F)_{1} = {1_{\bf{Par}}}_{1} が成り立つ。

 \square

 Lemma
\[ F \circ G \simeq 1_{{\bf{Sets}}_{\ast}} \] Proof.
任意の  (A, a) に対して  \theta_{(A,a)} \colon (A,a) \to \left((A - a) \cup \{\ast\}, \ast \right) を以下のように定義する。
\[
\theta_{(A,a)}(x) =
\begin{cases}
x & x \neq a \\
\ast & x = a
\end{cases}
\]

  •  \theta_{(A,a)} が isomorphism であること

 \theta_{(A,a)} が surjective であることは明らかである。
任意の  x, y \in A に対して  \theta_{(A,a)}(x) = \theta_{(A,a)}(y) とする。まず  \theta_{(A,a)}(x) = x とする。このとき  \theta_{(A,a)}(y) = \ast とすると  \ast \in A となり  \ast \notin A と矛盾する。 \theta_{(A,a)}(y) = y とすると  x = y となり  \theta_{(A,a)} は injective である。
次に  \theta_{(A,a)}(x) = \ast とする。このとき  \theta_{(A,a)}(y) = \ast とすると  x = a = y となり  \theta_{(A,a)} は injective である。 \theta_{(A,a)}(y) = y とすると  \ast \in A となり  \ast \notin A と矛盾する。以上より  \theta_{(A,a)} は injective である。

  •  \theta が natural であること

f:id:hitotakuchan:20160618141711p:plain
任意の  f \colon (A,a) \to (B,b) に対して
\[
(F \circ G)(f) =
\begin{cases}
f(x) & x \in A - f^{-1}(b) \\
\ast & \text{otherwise}
\end{cases}
\]
と表せる。
初めに  \left( (F \circ G)(f) \circ \theta_{(A,a)} \right)(a) = \ast = (\theta_{(B,b)} \circ f)(a) が成り立つ。
次に任意の  x \neq a \in f^{-1}(b) に対して  \left( (F \circ G)(f) \circ \theta_{(A,a)} \right)(x) = \ast (\theta_{(B,b)} \circ f)(x) = \theta_{(B, b)}(b) = \ast が成り立つ。
最後に任意の  x \in A - f^{-1}(b) に対して  \left( (F \circ G)(f) \circ \theta_{(A,a)} \right)(x) = f(x) = (\theta_{(B,b)} \circ f)(x) が成り立つ。
以上より  \theta は natural isomorphism である。

 \square

Example 7.29

 Lemma
\[ \Phi \text{ is a functor}. \] Proof.
f:id:hitotakuchan:20160621150317p:plain
書籍のように  \Phi \left( (A_{i})_{i \in I} \right) = \pi_{(A_{i})} \colon \coprod_{i \in I} A_{i} \to I で定義する。このとき、任意の  i \in I に対して任意の  a_{i} \in A_{i} i に対応させる constant map を  c_{i} \colon A_{i} \to I とすると、 \pi_{(A_{i})} \circ i_{A_{i}} = c_{i} が成り立つ。
次に任意の  (f_{i} \colon A_{i} \to B_{i})_{i \in I} に対して  \Phi \left( (f_{i}) \right) を次のように定義する。任意の  i \in I に対して  \widetilde{f} \circ i_{A_{i}} = i_{B_{i}} \circ f_{i} を満たす  \widetilde{f} \colon \coprod_{i \in I} A_{i} \to \coprod_{i \in I} B_{i} が coproduct の UMP よりただ一つ存在する。この  \widetilde{f} と任意の  i \in I に対して  \pi_{(B_{i})} \circ \widetilde{f} \circ i_{A_{i}} = \pi_{(B_{i})} \circ i_{B_{i}} \circ f_{i} = c_{i} \circ f_{i} = c_{i} が成り立つ。一方  \pi_{(A_{i})} \circ i_{A_{i}} = c_{i} であるから coproduct の UMP より  \pi_{(B_{i})} \circ \widetilde{f} = \pi_{(A_{i})} が成り立つ。そこで  \Phi \left( (f_{i}) \right) = \widetilde{f} と定義する。

初めに、 \Phi \left( (f_{i}) \colon (A_{i}) \to (B_{i}) \right) = \widetilde{f} \colon \Phi \left( (A_{i}) \right) \to \Phi \left( (B_{i}) \right) となるので  \Phi は functor の条件 (a) を満たす。
次に  \Phi (1_{(A_{i})}) = 1_{\coprod_{i \in I}(A_{i})} = 1_{\Phi \left( (A_{i}) \right)} となるので  \Phi は functor の条件 (b) を満たす。
最後に  \widetilde{g \circ f} の定義より  \widetilde{g \circ f} \circ i_{A_{i}} = i_{C_{i}} \circ g_{i} \circ f_{i} が成り立つ。一方で  \widetilde{g} \circ \widetilde{f} \circ i_{A_{i}} = \widetilde{g} \circ i_{B_{i}} \circ f_{i} = i_{C_{i}} \circ g_{i} \circ f_{i} が成り立つ。よって coproduct の UMP より  \Phi(g \circ f) = \Phi(g) \circ \Phi(f) が成り立ち、  \Phi は functor の条件 (c) を満たす。

 \square

 Lemma
\[ \Psi \text{ is a functor}. \] Proof.
任意の  \alpha \colon A \to I に対して  \Psi(\alpha) = \left( \alpha^{-1}(i) \right)_{i \in I} で定義する。また任意の  f \colon \alpha \to \beta と任意の  i \in I に対して  f_{i} = f\vert_{\alpha^{-1}(i)} とする。すると  \alpha = \beta \circ f より  \alpha^{-1}(i) = (f^{-1} \circ \beta^{-1})(i) \iff f \left( \alpha^{-1}(i) \right) = \beta^{-1}(i) が成り立つので、 f_{i} \colon \alpha^{-1}(i) \to \beta^{-1}(i) となる。そこで  \Psi(f) \Psi(f) = (f_{i})_{i \in I} で定義する。

 \Psi(f \colon \alpha \to \beta) = (f_{i})_{i \in I} \colon \left( \alpha^{-1}(i) \right)_{i \in I} \to \left( \beta^{-1}(i) \right)_{i \in I} = (f_{i})_{i \in I} \colon \Psi(\alpha) \to \Psi(\beta) が成り立つので  \Psi は functor の条件 (a) を満たす。
次に  \Psi(1 \colon \alpha \to \alpha) = \left( 1 \middle|_{\alpha^{-1}(i)} \right)_{i \in I} = 1_{\left( \alpha^{-1}(i) \right)_{i \in I}} = 1_{\Psi(\alpha)} が成り立つので  \Psi は functor の条件 (b) を満たす。
最後に  \Psi( g \circ f \colon \alpha \to \gamma ) = \left( g \circ f \middle|_{\alpha^{-1}(i)} \right)_{i \in I} = \left( g \middle|_{\beta^{-1}(i)} \right)_{i \in I} \circ \left( f \middle|_{\alpha^{-1}(i)} \right)_{i \in I} = \Psi(g) \circ \Psi(f) が成り立つので  \Psi は functor の条件 (c) を満たす。

 \square

 Lemma
\[ 1_{{\bf{Sets}}^{I}} \overset{\sim}{\to} \Psi \circ \Phi \] Proof.
任意の  (A_{i})_{i \in I} に対して  (\Psi \circ \Phi) \left( (A_{i})_{i \in I} \right) = \left( \left\{ (i, a) \, \middle| \,  a \in A_{i} \right\} \right)_{i \in I} であることに注意する。
 \theta_{(A_{i})} \colon (A_{i})_{i \in I} \to \left( \left\{ (i, a) \, \middle| \, a \in A_{i} \right\} \right)_{i \in I} を任意の  a \in A_{i} に対して  (\theta_{(A_{i})})_{i}(a) = (i,a) で定義する。
f:id:hitotakuchan:20160623155650p:plain

任意の  (f_{i}) \colon (A_{i})_{i \in I} \to (B_{i})_{i \in I} と任意の  i \in I a \in A_{i} に対して  \left( \Psi \circ \Phi \left( (f_{i}) \right) \circ \theta_{(A_{i})} \right)_{i}(a) = \left( i, f(a) \right) \left( \theta_{(B_{i})} \circ (f_{i}) \right)_{i}(a) = \left( i, f(a) \right) が成り立つ。 \theta_{(A_{i})} は明らかに isomorphism であるから、 \theta \colon 1_{{\bf{Sets}}^{I}} \to \Psi \circ \Phi は natural isomorphism である。

 \square

 Lemma
\[ 1_{{\bf{Sets}}/I} \overset{\sim}{\to} \Phi \circ \Psi \] Proof.
任意の  \alpha \colon A \to I に対して  (\Phi \circ \Psi)(\alpha) = \pi_{\left(\alpha^{-1}(i) \right)} \colon \coprod_{i \in I} \alpha^{-1}(i) \to I であることに注意する。
 \eta_{\alpha} \colon \alpha \to (\Phi \circ \Psi)(\alpha) を任意の  a \in A に対して  \eta_{\alpha}(a) = \left( \alpha(a),  a \right) で定義する。このとき  \alpha(a) = (\pi_{\left( \alpha^{-1}(i) \right)} \circ \eta_{\alpha})(a) が成り立つのでこれは well-defined である。
次に  \eta_{\alpha}^{-1} \colon (\Phi \circ \Psi)(\alpha) \to \alpha を任意の  i \in I に対して  \eta_{\alpha}^{-1} \left( i, a \in \alpha^{-1}(i) \right) = a で定義すると、 \pi_{\left( \alpha^{-1}(i) \right)} = \alpha \circ \eta_{\alpha}^{-1} が成り立つのでこれは well-defined である。
このとき明らかに  \eta_{\alpha}^{-1} \circ \eta_{\alpha} = 1_{\alpha} かつ  \eta_{\alpha} \circ \eta_{\alpha}^{-1} = 1_{(\Phi \circ \Psi)(\alpha)} が成り立つので  \eta_{\alpha} は isomorphism である。
f:id:hitotakuchan:20160623163037p:plain

任意の  f \colon \alpha \to \beta と任意の  a \in A に対して  \left( (\Phi \circ \Psi)(f) \circ \eta_{\alpha} \right)(a) = \left( (\Phi \circ \Psi)(f) \right) \left( \alpha(a), a \right) = \left( \alpha(a), f(a) \right) (\eta_{\beta} \circ f)(a) = \left( (\beta \circ f)(a), f(a) \right) = \left( \alpha(a), f(a) \right) が成り立つ。よって  \eta \colon 1_{{\bf{Sets}}/I} \to \Phi \circ \Psi は natural isomorphism である。

 \square

Lemma 7.33

lemma 7.33 は証明したかったのですが、私に Boolean Algebra に関する素養がないため証明できませんでした。
わかりやすい証明をご存知の方はコメント欄なので教えてください。

参考書籍

Category Theory (Oxford Logic Guides)

Category Theory (Oxford Logic Guides)

圏論 原著第2版

圏論 原著第2版