北海道苫小牧市出身の初老PGが書くブログ

永遠のプログラマを夢見る、苫小牧市出身のおじさんのちらしの裏

層・圏・トポス P80 定理8 (3)→(1)の証明

みなさん合宿を頑張ってるはずですので、こちらも対抗して前回の宿題を終わらせました。*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の対象と思っていい