層・圏・トポス読書会 #5

7月11日に行われた第五回「層・圏・トポス  現代的集合像を求めて」勉強会にいってきました。
今回は随伴でハマりました
で、はまったところを考えてみました。随伴が普遍射を定めるというところの証明です。
以下の図が随伴を適当に表した図です。左側が圏A、右側が圏Bです。黒矢印が各圏での射で、赤矢印のFとUが関手です。図中の A、B、UA、FBは対象です。AとBが圏の名前とかぶってますが、あまり気にしない方向で。
それで、随伴とは HomA(FB, B) と HomB(FB, B) の間に自然な全単射があることと定義されます。図の青矢印の OA,B がその全単射で、射 a を 射 b に移していることをあらわしています。

で、自然な全単射の自然性の方ですが、

という図になります。
この図は元の図に任意の射 f と g (左下と右上)を付け足して、一回り大きな四角を作ったものです。大きな四角も長い青矢印 OA',B' で随伴になっています。そして射 f、g をそれぞれ関手 U と F で移してやると、左右に台形状の射が出来上がります。ここで、a' と b' は

a' = Fg ; a ; f
b' = g ; b ; Uf

とします。従って左右の台形はそれぞれ可換となります。
随伴の自然性は、射 a を動かして HomB(B', UA') に行く2つのルート

    随伴(OA,B)     gとUfではさむ
a ------------> b -------------> b'=g;b;Uf

    Fgとfではさむ             随伴(OA',B')
a ----------------> a'=Fg;a;f -------------> b'

がともに b' となり、等しくなることです。さらに同様にして 射 b をHomA(FB', A') に行く2つのルートが等しくなることも要請します。
図では随伴が既に成り立っているとして同じ b' で書きました。
この自然性を具体的に式で書いてみます。そのために、混乱を恐れずに新しい記法を導入します。
圏A の 射 a を随伴で 圏B の射に移したものを、右に行くイメージで、 a> とします。同様に 圏B の 射 b を随伴で 圏A の射に移したものを、左に行くイメージで、 b< とします*1。図の a と b では、

a> = b
b< = a
すなわち
a>< = a
b<> = b

が成り立っています。
この記法で、自然性を表現すると、

(Fg;a;f)> = g;a>;Uf
(g;b;Uf)< = Fg;b<;f

となります。特に、上の式で g = id としたものと、下の式で f = id としたものは、

(a;f)> = a>;Uf
(g;b)< = Fg;b<

となり、これは随伴が射の結合にどう影響するかを表している公式になっています。
で、問題の層・圏・トポス 78ページの図

         Fg                                                    f
  FB' --------> FB --------> A             FB --------> A  --------> A'
---------------------------------       ---------------------------------
          g                                                   Uf
   B' --------> B  --------> UA            B  --------> UA --------> UA'

ですが、この公式とちょうど一致するので、自然性を意図したものじゃないかと。

でまあ、自然性まで考えると、普遍射の可換性も言えます*2…よね?という話でした。

*1:>も<も、随伴で移せる射だけに定義されることに注意。

*2:謎の図式の解釈ができたから。