P87-88に書かれているのは、おおざっぱに言えば「-×Aの右随伴が存在 ⇔ ∀CについてC^Aやev_Cが存在」という話です。書籍だけではちょっと曖昧な部分があるのでフォローします。
題意
書籍では左辺はともかく右辺がちょっと曖昧です。マクレーン本や清水本から拾うと、以下のような感じです。
「∀C∈|C|, ∃C^A∈|C|, ∃ev_C∈C s.t. ∃1 hat(f)∈C, (hat(f)×id);ev_C = f」です*1。
証明
⇒は書籍の通りでほぼ十分です*2。⇐を見ます。
右随伴となる関手を構成
関手-^A を作ります。対象の対応は前提にあるC^AでOKです。後は射f:C1→C2の対応としてf^Aを作る必要がありますが、これは以下のように定義します。
- f^A = hat(ev_C1;f)
定義した-^Aが関手か
hatの一意性から、恒等射の保存と合成の保存が言えます。詳細は略。
右随伴となるか
Hom(B×A, C) ≃ Hom(B, C^A)の間の対応を作り、自然同型になるかみます。これは書籍にある通り、右向きφは f↦hat(f)で、左向きφ'は(f×id);ev_C↤fです。
この対応が全単射であること
φ￮φ' = id と φ'￮φ = id を言います。前者はhatの一意性から、後者は自明です。
この対応が自然であること
これも詳細は略しますが、2つの相関手Hom(-×A, -)とHom(-, -^A)について満たすべき可換図を書き、可換になることを確かめます。
φ'を使い、h∈Hom(-, -^A)から始めると楽です。-×Aは関手*3なんで、(f;g)×id = (f×id);(g×id) を使えます。後はhatとevの可換図と、f^Aの定義(最初に定義した)を使えばすぐ出ます。
まとめ
これで、Aに対して-^Aが作れ、この関手が-×A ⊣ -^Aとなることが言えたので、⇐を示したことになります。
