みなさん合宿を頑張ってるはずですので、こちらも対抗して前回の宿題を終わらせました。*1
P80 3)から1)の証明で構成した関手Fは、射をどのように移すのか？
関手Fの構成方法
任意のBに対して、関手 B(B,U-):A→Sets を表現する対象を、FBとする。ここまではP80にある通り。
さて、B(B,U-) ≃ A(FB,-) を与える自然同型を、 φ_B,- とする。ここで、各コンポーネントφ_B,A は iso なので、 (φ_B,A)^-1 = φ_A,B と表記するものとする。
さらに後の簡単のために、η_B:B→U(FB) を η_B = φ_FB,B(id_FB) で定義する。
ここで、f:B→B' について、関手Fを、 Ff = φ_B,FB'(f;η_B') で定義すればよい。
ηやφ_B,Aの性質
ここからは泥臭いので、あまり読むことはお薦めしません(笑)。
性質1
B'を固定し、f:FB→Aについて考える*2。φ_B',- が自然同型なので、C(FB',FB)の要素g:FB'→FBについて可換図を考えると次が言える。
φ_A,B'(g;f) = φ_FB,B'(g);Uf
性質2
性質1で、特に B' = B、 g = id_FB の時を考えると、
φ_A,B(f) = η_B;Uf
Fが関手になることの証明
恒等射
これは定義より、以下の通り自明。
F(id_B) = φ_B,FB(η_B) = id_FB
結合則
f:B→B', f':B'→B'' とする。
φ_FB'',B(Ff;Ff') = η_B;U(Ff;Ff') ∵ 性質2 = η_B;UFf;UFf' ∵ Uは関手 = φ_FB',B(Ff);UFf' ∵ 性質2 = φ_FB',B(φ_B,FB'(f;η_B'));UFf' ∵ Fの定義 = f;η_B';UFf' = f;φ_FB'',B'(Ff') ∵性質2 = f;φ_FB'',B'(φ_B',FB''(f';η_B'')) ∵ Fの定義 = f;f';η_B'' ∵ Fの定義 = φ_FB'',B( φ_B,FB''(f;f';η_B'') ) = φ_FB'',B( F(f;f') ) ∵ Fの定義
この計算とφの単射性から、 Ff;Ff' = F(f;f') が言える。
F⟞Uの証明
φ_A,B が A(FB,-) ≃ B(B,U-) の随伴を与える自然同型となることを示す。
圏A×B^op の対象(A,B)と(A',B')と射(f, g)を考える。(f:A→A', g;B'→B)
自然同型を示す可換図が可換になるには、C(FB,A)の任意の要素 h:FB→Aについて、
φ_A',B'(Fg;h;f) = g;φ_A,B(h);Uf (左回り=右回り)
が成り立てばいい。ちまちま計算する。
φ_A',B'(Fg;h;f) = φ_FB,B'(Fg);U(h;f) ∵ h;fとFgに対して、性質1 = (g;η_B);U(h;f) ∵ Fの定義 = g;η_B;Uh;Uf ∵ Uは関手 = g;φ_A,B(h);Uf ∵ 性質2
よって、示された。 Q.E.D.
まとめ
基本的には、勉強会の中でやった 3)→2)→1) の流れと同じアイデアで、(2)をショートカットして証明してるだけです。普遍射の存在を経由しないので、一意性とか出て来ないのは多少わかりやすいかもしれませんが。
それにしても、このFの定義も証明も全然自明じゃないので、P80のようにごっそり省略しちゃあまずい気がします。それとも、我々の熟慮が足りず、もっと単純なことを見落としているのか・・・。
*1:モニャドセミナーの帰りに考えていたのはこの問題のことです。
*2:Fはまだ関手じゃないんで、FBはただの圏Aの対象と思っていい
