自由群と随伴関手

やっと、自由群が随伴関手の例であることを確認できる所まで来た。まず Wikipedia の随伴関手の記事から自由群に関する部分を引用してみる。

自由群

自由群の構成は極めて普通の随伴による構成であり、上記の詳細の分かりやすくて便利な例である。
関手F : Grp ← Setは各集合YにYの要素の生成する自由群を対応させるものとし、関手G : Grp → Setは群Xにその台集合を対応させる忘却関手とする。以下に示すようにFはGの左随伴となる。

hom集合の随伴。自由群FYから群Xへの群準同型は正確に集合Yから集合GXへの写像に対応する。すなわち、FYからXへの射は生成元への作用により完全に決定される。この対応が自然同型であることも直接確認できる。よって(F,G)に対応するhom集合の随伴が得られた。

これも十分抽象的でわかりづらいので、整理してみる。まず集合の圏 Grp と群の圏 Set がある。また Grp の対象の群 X と Set の対象の集合 Y が取り出してある。また、関手 F を Grp の対象の集合とそれが生成する自由群とを対応させる関手とし、関手 G を群とその台集合を対応させる関手とする。つまり、

F : Set -> Grp
G: Grp -> Set

で両者は domain と codomain が逆になっている。ここで、集合 Y から集合 GX (群XのGの対象関数による像)への写像を f とする。

f : Y -> GX

このような関数の任意のもの f について、自由群の普遍性から、全ての a ∈ Y について、次の条件を満たす FY から G への準同型写像 f~ が一意的に決まる。

f~ a = f a

これは、自由群 FY は集合 Y の要素を生成元として全ての要素を生成できるので、準同型写像 f~ : FY -> G も集合Y の要素から決定できるからだ。φ : f |-> f~ が全単射であることの証明は省くがこれは全単射になる。したがって、

home(FY, X) ~= home(Y, GX)

となり、また、f~ a = f a から次の可換式が成り立つ。

Gf~F = f

したがって、関手 F と関手 G は随伴である。このとき、関手 F は関手 G の左随伴であり、関手 G は関手 F の右随伴である。

これから得られる随伴関手のイメージはつぎのようになるのではないだろうか。

圏 Set の世界と 圏 Grp の世界があり、Set の対象 Y は関手 F で Grp の対象 FY に写される。また、Grp の対象 X は関手 G によって Set の対象 GX に写される。そうして集合の世界の集合と集合の関係である写像 f : Y -> GX は群の世界の群と群の関係である準同型写像 f~ : FY -> Gに写される。

さらに射の可換性によって、集合の世界の対象が関手 F によって群の世界に写しだされ、処理を受けた後関手 G によって、集合の世界に移し戻された結果が、集合の世界の対応する変化と呼応している。

これが、具体的に何の役に立つのかと言われても答えられないが、集合の世界と群の世界の緊密な交流を随伴関手で行っているといえるのではないだろうか。参考までに、Wikipedia の随伴関手の記事をもう一つ引用する。

William Lawvereによる非常に一般的な解説[2]によると「構文と意味」は随伴である。つまり、Cを全ての論理(公理化)からなる集合とし、Dを全ての数学的構造からなる集合の冪集合とする。Cの各理論Tに対して、F(T)を公理Tを満たす構造全てからなる集合とし、各数学的構造の族Sに対して、G(S)はSの最小の公理化とする。このとき、F(T)がSの部分集合であることと、G(S)がTの論理的帰結であることは同値であり、「意味関手」Fは「構文関手」Gの左随伴である。

詳しいことは理解できなかったが、論理学における構文と意味との関係が随伴であることが証明されているらしい。構文の構造と数学的構造の関連性を問う意味論を、随伴によって厳密に記述できるという意味だろうか。

こうしてみると、圏論は数学的構造という掴み難いものに共通のパターンを与えるのに強力な働きをしているような気がする。これは、おそらくプログラミングの抽象化とも関連して将来的にはプログラミングをする上で重要な基礎知識になるのではないかと思えるが、そろそろ Haskell の実際のプログラミングに戻りたくなったので、圏論のシリーズはしばらくおしまいにする。知識が溜まって書きたくなったら再挑戦するかもしれない。
[PR]
by tnomura9 | 2014-08-31 12:07 | 圏論 | Comments(4)
Commented by 通りすがり at 2014-08-31 21:38 x
率直に言って、自由関手と忘却関手にはそれぞれそれ自体で十分
数学的実質があると思います。しかしその間の随伴性については
それらの発見?の後の後付けの装飾的知見にしか見えません。
また、上に引用された Lawvereの構文と意味の随伴性も同様です。
ずいぶん高尚に表現されていますが、それは論理学の初歩的知見の
後付けの、かつなんとも大仰な表現に過ぎません。たとえば、
構文と意味の随伴性から完全性定理が生み出されるというのなら
話は別ですが、そういう生産的な順序は決して起こらないのでは
ないでしょうか?
Commented by tnomura9 at 2014-09-01 07:23
通りすがりさん、コメントありがとうございました。
通りすがりさんが、随伴について問題にされていた意味がわかりました。圏論が単なる無用の抽象化なのか、数学を記述する言語にすぎないのか、あるいはなにか新しい発見につながる道具になるのか、あるいは集合論と同じように全ての概念の基礎になり得るのか重要なことだと思います。つまり、圏論に数学的構造についての今までの方法とは違う革新的な洞察があるかということの問題です。それについては、わたしにはコメントできるような知識はありません。ただ、私が、圏論に興味を持ったのは、Haskell の IO モナドに悩まされたからです。使い方の分かりにくさもですが、IO モナドでプログラムする事で自然に副作用が隔離されていく仕組みが不思議だったからです。これは数学とは直接の関係はないと思いますが、これに関する圏論の役割については、通りすがりさんはどう思われますか。
Commented by 通りすがり at 2014-09-01 15:49 x
まず、圏論は、数学言語として集合論や述語論理に代わるものには
なりえないでしょうね。圏論の教科書の叙述自体が基本的にそれらの
基礎言語に依存しています。

また圏論のexternalな(要素に言及しない)記法は、あくまで、
前提としてinternalな理解があってこそ成り立つ簡略記法というべき
ではないでしょうか?適当な例でないかもしれませんが、「A⊆B」は
「∀x.(x∈A⇒x∈B)」の簡略記法に過ぎず、それ単独では大した含蓄は
ありません。

> IO モナドでプログラムする事で自然に副作用が隔離
(tnomuraさんからご覧になっていい加減なことを書いてしまいますが)
あれのアイデアは、これまで純粋関数の型aと混同していたある種類の
型を本来そうあるべきだったIO(a)として型aとの関連は残しつつ独立
させた(それによって自ずと隔離もされた)というだけのことでは
ないのですか?他のモナドも同様ですね?
モナドは、21世紀初の関数プログラミング村に現れた一過性の現象と
いうことになるだろうと思っています。あんな変に小難しいものが
コンピュータサイエンスの将来に残るわけがないでしょう。そして
モナドなしでも、もっと簡単に同じことができるでしょうし。
Commented by tnomura9 at 2014-09-01 16:44
通りすがりさん、コメントありがとうございました。
随分頭がスッキリしたような気がします。現実的には Haskell のプログラミングをする際に IO モナドを避けて通ることはできないのですが、それ故圏論の勉強は続けたいと思いますが、コメントされたことを頭に置いて、本質的にはどういうものかという考えをしながら見てみます。
<< 篠原ともえ 自由群の準同型写像の作り方 >>