このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

米田埋め込みが強力すぎるので具体的計算が出来ない人になってしまう

Cデカルト閉圏だとしましょう。デカルト積とその単位(終対象)をそれぞれ、×、1 で表します。指数は BA、または [A, B] と書くことにします。

次のような指数法則は、形の上で自然に見えます(イコールは同型と解釈します)。

  1. A1 = A
  2. CA×B = (CA)B

例えば二番目の CA×B = (CA)B を確認するとしましょう。上付きは書くのが面倒なので、指数をブラケットで書くことにすれば、[A×B, C] = [B, [A, C]] です。カリー/ハワード対応があるので、指数法則は次の推論が妥当であることを意味しています。


A∧B ⊃ C
--------------
B ⊃ (A⊃C)


B ⊃ (A⊃C)
--------------
A∧B ⊃ C

あるいは、シーケントで書いて、A∧B ⊃ C ⇒ B ⊃ (A⊃C) と B ⊃ (A⊃C) ⇒ A∧B ⊃ C を示せばいいことになります。論理の証明図を書いて、それをデカルト閉圏Cで再解釈すれば、指数法則を与える具体的な同型が構成できるはずです。で、やってみると … 「アンレー?」とか嘆いて挫折。

具体的に構成できなくても(構成できるはずですけど)、米田の補題を使えば、同型であるという事実は示せてしまいます。XをCの任意の対象として、ホムセット C(X, [A×B, C]) と C(X, [B, [A, C]]) のあいだの同型を系統的に構成できれば、[A×B, C] と [B, [A, C]] が同型であることが従います。ホムセットの同型は、おおよそ次の手順で示せます。


C(X, [A×B, C])
------------------------
C(X×A×B, C)
------------------------
C(X×B×A, C)
------------------------
C(X×B, [A, C])
------------------------
C(X, [B, [A, C]])

ホムセット同型を作る手順を分析すれば、具体的な射の構成も分かるはずなのですが、ホムセット同型のほうがはるかに簡単に出来ます(少なくとも僕にとっては)。ホムセット同型が示せると「オーケイ、これでいいや」と思って、具体的な構成をそれ以上考える気力が失せます。いいんだか悪いんだか。


なぜ、ホムセット同型から対象の同型が言えるのでしょうか? その背景は米田の補題です。ここから先では、Cは単なる圏とします。圏C対象Aに対して、A~ を次のように定義します。

  • A~(X) = C(X, A)

ここで、XはCは任意の対象です。無名のラムダ変数'-'(ブランク)を使うと A~(-) = C(-, A) と書けます。A~ は、 (Cの対象) |→ 集合 という対応ですが、f:X→Y in C に対して、

  • A~(f):A~(Y) → A~(X)

という対応も定義できます。具体的には、u∈A~(Y) に対して、A~(f)(u) := f;u (手前にfを結合)とするだけです。A~ は、

  • Cの対象Xに、集合C(X, A) を対応させる。
  • Cの射 f:X→Y に、集合C(Y, A) から集合 C(X, A) への写像を対応させる。

そして関手性を持つので A~:CSet (反変) という関手となります。

さらに対象Aを動かすことにより、A |→ A~ は (Cの対象)→(CSet の反変関手) という対応になります。k:A→B があると、A~⇒B~ という自然変換をうまく定義できるので、(-)~ は、圏C → 関手圏[Cop, Set] という関手となります。

米田の補題は、米田埋め込みと呼ばれるこの関手 C → [Cop, Set] が充満忠実(full and faithful)であると主張します。つまり、次の2つの集合のあいだに(系統的な)同型があります。

  1. Cのホムセット C(A, B)
  2. 自然変換の集合 Nat(A~, B~: CopSet)

これから、Nat(A~, B~) のなかに自然同値が見つかれば、C(A, B) のなかに対応する同型射が存在することが保証されます。ときに、ホムセット C(A, B) より、自然変換の集合 Nat(A~, B~) のほうが見やすい/扱いやすいこともあるのです。そのようなときは、自然同値を構成できれば、具体的な射を示さなくても「オーケイ、これでいいや」となるわけです。