モノイド圏、豊饒圏、閉圏と内部ホム

他人の過去ネタを蒸し返し、自分用のメモにするエントリー。

[追記]トラックバック／コメント蘭で、色々なやりとりがありましたが、（この部分以外の）本文への修正や追加はしません。その代わり、「閉圏、弱いラムダ計算、弱い論理」で、似た話題を扱っています。[/追記]

たけをさんが、だいぶ前の彼のエントリーで次のようなことを述べています； 圏Cがデカルト閉（cartesian closed）なとき、“Yを（デカルト積の意味で）掛ける作用 (-)×Y” と “Yで累乗（べき、指数）する作用 (-)^Y” が互いに随伴なC上の自己関手になるわけですが、Hom_C(A×Y, B) と Hom_C(A, B^Y) の同型は集合圏での話であり、もとの圏Cの内部で同型が与えられるわけではない、と。

だがしかし、随伴による同型は、実はCの内部でもちゃんと定式化できるのです。Cのデカルト閉性（cartesian closedness）が、内部化を保証します。これは内部ホム（internal hom / hom object）という概念を使うのですが、内部ホムはけっこう難しい。事例から雰囲気を感じるのは容易なのだけど、ちゃんと定義するとめんどくさい！ そのめんどくさい感じをちょっくら説明します。が、めんどくさいことを律儀に実行するわけではありません。

内容：

目的は、圏の内部での同型

デカルト閉圏を少し一般化して、Cがモノイド閉圏（閉モノイド圏、あるいは単に閉圏ともいう）の状況で考えます。(-□-)がCのモノイド積（デカルト積とは限らない）、[-, -]が□の右随伴から定義される二項指数（exponential object）とすると、C内で次の同型が存在することを示したいのです。

• [A□X, B] ≒ [A, [X, B]] （≒はCの対象の同型を示す）

ホムを使った圏の定義

圏を、次の形で定義しておきます。

1. Uは対象の集合（Uの“大きさ”は気にしないことにする）。
2. A, B∈Uに対して集合Hom(A, B)が割り当てられている。(A, B)≠(C, D)ならば、Hom(A, B)∩Hom(C, D)は空。（Hom(A, B)は“大きすぎない”集合とする。）
3. 各A, B, C∈Uに対して、写像c_A,B,C:Hom(A, B)×Hom(B, C) → Hom(A, C) が割り当てられている。c = c_A,B,C は射の結合（合成）を与える写像である。
4. 各A∈Uに対して、写像u_A:{0} → Hom(A, A) が割り当てられている。u = u_A は、Hom(A, A)に含まれる恒等射 u(0)∈Hom(A, A) を指し示す（pointing）写像である。
5. c_A,B,Cとc_B,C,Dに関して結合法則、u_Aとc_A,A,B、u_Bとc_A,B,Bに関して単位法則が成立する。

(U, {Hom(A, B) | A, B∈U}, {c_A,B,C| A, B, C∈U}, {u_A | A∈U})という構造を圏C（対象に大文字英字を使ってしまったので、圏はイタリックにする）と呼びますが、いつもどおり、Uを|C|、Hom(A, B)をC(A, B)、c_A,B,C(f, g)をf;g、u_A(0)をid_Aなどと書くことにします。

このように定義しても、他の流儀による圏の定義と同じ圏概念が得られます。「(A, B)≠(C, D)ならば、Hom(A, B)∩Hom(C, D)は空」という条件を外しても、Hom'(A, B) := {(A, f, B) | f∈Hom(A, B)}と定義し直せば、dom, codなどをうまく定義できます。よって以下では、Hom(A, B)∩Hom(C, D)に関する仮定には言及しません。

対称モノイド圏

(C, □, I, σ)が対称モノイド圏（symmetric monoidal category）であるとは、

1. Cは、圏である。
2. □は、C×C→C という双関手（bifunctor; 二項関手）である。
3. Iは、Cの特定された対象である。
4. 各A, B∈|C|に、σ_A,B:A□B → B□A という射（AとBを取り替える射）が割り当てられている。
5. これらが、いくつかの法則を満たす。

めんどうなので、□に関する結合法則と単位法則は厳密に（on the noseで）成り立っているかのように扱います（実際にはそうでなくても）。ただし、A□B = B□A は仮定しなくて、同型σ_A,B: A□B → B□A を経由します。対称性（A□BとB□Aの同型）以外は厳密に成り立つ対称モノイド圏はpermutative圏と呼ぶようです。A□B = B□A も厳密に成立すれば、可換モノイド圏と呼ぶのが適当かもしれませんが、厳密に可換な例はあまり出てきませんね。

ここで対称モノイド圏の例をいくつか。アリキタリなものですが：

1. 集合圏＋直積＋単元集合
2. アーベル群の圏＋（Z加群としての）テンソル積＋Z
3. K-ベクトル空間の圏＋K-テンソル積＋K
4. 圏の圏＋圏の直積＋単一対象と恒等だけの圏
5. （うんと小さい例）0以上の実数に順序で圏構造を入れて、足し算をモノイド積とする。これは厳密に可換なモノイド圏。

V-豊饒な圏

Vが対称モノイド圏だとして、Vにホムを持つような圏を次のように定義します。

1. Uは対象の集合。
2. A, B∈Uに対してVの対象Hom(A, B)が割り当てられている。
3. 各A, B, C∈Uに対して、Vの射c_A,B,C:Hom(A, B)□Hom(B, C) → Hom(A, C) が割り当てられている。
4. 各A∈Uに対して、Vの射u_A:I → Hom(A, A) が割り当てられている。
5. c_A,B,Cとc_B,C,Dに関して結合法則、u_Aとc_A,A,B、u_Bとc_A,B,Bに関して単位法則が（可換図式の意味で）成立する。

このような構造 (U, {Hom(A, B) | A, B∈U}, {c_A,B,C| A, B, C∈U}, {u_A | A∈U})を、Vで豊饒化された圏（V-enriched category）、あるいはV-豊饒圏、さらに短くV-圏などと呼びます。

Vとして前の節の例をとると、それぞれ：

1. 通常の圏の定義になる。
2. ホムセットに足し算が入り、圏の結合は足し算に対して分配的になる。つまり、射を自由に足し算できる圏。
3. ホムセットがK-ベクトル空間になり、圏の結合はK-双線形写像になる。K-線形圏と呼ぶこともあるらしい。
4. ホムセットが圏（ホム圏）になり、圏の結合は双関手になる。2-圏と呼ばれる。
5. この例のホムは、集合ではなくて“値”となる。点集合M上に「非負実数のモノイド圏」で豊饒化された圏は、Mに距離空間の構造を与える*1。ただし、a≧bのときにa→bという射があるとする。距離の対称性は仮定しない。

閉圏

対称モノイド圏(C, □, I, σ)が閉（closed）だとは、任意の対象X∈|C|による右からのモノイド積(-)□Xが右随伴を持つことです。(-)□X の右随伴を[X, -]と書くことにします。つまり、次の同型（集合の1：1対応）があります。

• C(A□X, B) ≒ C(A, [X, B]) （≒は集合の同型）

この同型（自然変換で与えられる）を、次の推論規則の形で使うことにします。

  f  : A□X → B
 -------------------[カリー化]
  f^ : A → [X, B]

  g : A → [X, B]
 -------------------[反カリー化]
  g~ : A□X → B

f^は「fのカリー化」、g~は「gの反カリー化」です。だいたいの感じとしては、f^(a) = λx.f(a, x)、g~(a, x) = (g(a))(x)。定義より、f^~ = f、g~^ = g ですね。

自分自身で豊饒化された圏

Cが閉じた（閉な）対称モノイド圏として、二項指数写像[-, -] : |C|×|C|→|C| が、C-豊饒化を与える状況を考えましょう。

1. A, B∈|C|に対してCの対象[A, B]が割り当てられている。
2. 各A, B, C∈|C|に対して、Cの射c_A,B,C:[A, B]□[B, C] → [A, C] が割り当てられている。
3. 各A∈|C|に対して、Cの射u_A:I → [A, A] が割り当てられている。
4. c_A,B,Cとc_B,C,Dに関して結合法則、u_Aとc_A,A,B、u_Bとc_A,B,Bに関して単位法則が（可換図式の意味で）成立する。

2つの引数を持つ写像[-, -]をホムだと考えて、結合を与える射（の族）c_A,B,Cと、恒等を割り当てる射（の族）u_Aを実際に作れば、|C|上のC-豊饒圏となります。まず、[A, B]の恒等を反カリー化します。

  id : [A, B] → [A, B]
 ------------------------[反カリー化]
  id~ : [A, B]□A → B

こうして作られたid~をevと名付けます（関数評価を意味するevaluationから）。感じとしては、id~(f, a) = (id(f))(a) ですから、ev(f, a) = f(a) ってことです。A, Bを明示するときはev_A,Bと書きます。ev':A□[A, B]→B を、σ;ev とし定義します。ここでσは、σ_{A, [A, B]}:A□[A, B]→[A, B]□A のことです。

さて、

 ev□id : ([A, B]□A)□[B, C] → B□[B, C] 
 ev' : B□[B, C]  → C
 -------------------------------[射の結合]
 ([A, B]□A)□[B, C] → C
 -------------------------------[□の結合性]
 [A, B]□(A□[B, C]) → C
 -------------------------------[□の対称性]
 [A, B]□([B, C]□A) → C
 -------------------------------[□の結合性]
 ([A, B]□[B, C])□A → C
 -------------------------------[カリー化]
  [A, B]□[B, C]→[A, C]

こうして得られた最後の射 [A, B]□[B, C]→[A, C] をc_A,B,Cとします。感じとしては次のようです。

 ((f, a), g) |→ (f(a), g)
 (b, g) |→ g(b)
 -------------------------------[射の結合]
 ((f, a), g) |→ g(f(a))
 -------------------------------[(-, -)の結合性]
 (f, (a, g)) |→ g(f(a))
 -------------------------------[(-, -)の対称性]
 (f, (g, a)) |→ g(f(a))
 -------------------------------[(-, -)の結合性]
 ((f, g), a) |→ g(f(a))
 -------------------------------[カリー化]
  (f, g) |→ λa.g(f(a))

また、次の手順で得られた射をu_Aと名付けます。

 I□A → A （左単位性）
 ----------------------[カリー化]
  I→[A, A]

 (0, a) |→ a （左単位性）
 ----------------------[カリー化]
  0 |→ λa.a

以上の |C|, {[A, B] | A, B∈|C|}, {c_A,B,C | A, B, C∈|C|}, {u_A | A∈|C|} が、|C|上のC-豊饒圏を定義していることは、根気よく定義を確認していけば分かります（定義を正確に述べてないけど(苦笑)）。Cからこの手順で作られたC-豊饒圏を、Cそのものとは区別して/C/と書くことにします（標準的な記法ではないです）。

内部化という不思議な現象

もとの閉圏CとC-豊饒圏/C/は、まー、だいたい同じようなものです。しかし、/C/では、そのホムである/C/(A, B)がCの対象として認識できる点は大きな違いです。

感じをつかむための例えとして、Cのなかに生物が棲んでいるとしましょう。彼らは、Cの個々の対象A, Bなどを認識できます。Cの個々の射（例えば f:A→B）もちゃんと認識します。しかし、ホム集合C(A, B)を見ることはできません。彼らには集合認識能力がないので、“AからBへの射の全体”を把握することはできないのです。

ホム集合C(A, B)は、外部からCを眺める我々には見えてますが、C内に棲む生物には認識不可能な超越的な存在です。しかし、対象AとBから作った[A, B]は中に棲む彼らにも見えます（だって、Cの対象だもの）。ev_A,B:[A, B]□A→B とか c_A,B,C:[A, B]□[B, C]→[A, C] なども見えます。[A, B] = /C/(A, B) でしたから、C-豊饒圏/C/の様子はC内部から認識と観測が可能なのです。

中に棲む生物たちも、/C/の対象、ホム、結合、恒等などの概念を、あたかも我々がCを外から眺めるように認識・観測できるわけです。そこで問題は、我々が C(A□X, B)≒C(A, [X, B])という随伴性を外から（集合概念を使って）認識できるように、中の生物は /C/(A□X, B)≒/C/(A, [X, B]) という、「随伴性の内部化バージョン」を認識できるか？ ということです。

これは、C内の射（集合間の写像ではありません！）で、/C/(A□X, B)と/C/(A, [X, B])の同型を与えるものがあるか？ という問題です。実際の答は肯定的であり、次が成立します。

• [A□X, B] ≒ [A, [X, B]] （≒はC内での同型）

どうすればいいのか？

C内に確実に存在する射とか自然変換達をうまく組み合わせて、[A□X, B] → [A, [X, B]] という同型射（可逆射）を具体的に構成できればいいのですが、これはなかなか難しいようです*2。Cがデカルト閉なら、型付きラムダ計算の結果を翻訳して具体的構成ができるかもしれません（僕はやったことありません）。

Borceuxの教科書（Handbook）には、超越的な証明が載っています。ようするに、「存在しないはずがない！」（よって存在する）という論法でして、「はい、これがそうですよ」と射を作って目の前に見せてくれるものではありません（けど、面白い方法です）。

ところで、我々の問題意識は、C内の生物が [A□X, B] ≒ [A, [X, B]] という同型を認識できるか？ でした。言い方を変えれば、同型を与える射を彼らは見つけられるか？ です。超越的な証明だと、彼らの作業を肩代わりして実行するのではなくて、「見つけられないわけはない」ことを示します。こうすると、C内の生物は、C内をくまなく探すという点では超越的というか猛烈な能力を持っていることを仮定することになります。つまりコイツらは、C内に閉じ込められているくせに、その内部世界においては全知全能なわけね。世界の外に出られない神様？ -- 変なヤツらだ。

内部的な随伴性の超越的な証明は今度（いつか分からない）紹介します、たぶん。米田の補題が活躍しますよ。

[追記]トラックバック／コメント蘭で、色々なやりとりがありましたが、（この部分以外の）本文への修正や追加はしません。その代わり、「閉圏、弱いラムダ計算、弱い論理」で、似た話題を扱っています。[/追記]

*1:この例は、Lawvereの1973年の論文のもので、有名ですね。

*2:難しくないかもしれないけど、僕は全然思いつかなかったです。