「第4章 自然変換」を見ていきます。コンマ圏のところまでは、どうやれば良いのかわからないのでそのままの書き方で書いていくことにします。
第4章 自然変換
①自然変換の定義1
、
を圏
から
への関手とします。
このとき、 から
への 自然変換
は
の各対象
に
の射
を対応させる。
に対して
が成り立つ。
というものを言います。このとき と書きます。
を
の
成分と呼びます。
図式は同じようには描けないのですが描いておきます。
および
を関手
の間の自然変換とするとき、これらの合成を
と定義すると、自然変換
となります。この合成は結合律、単位律を満たします。
圏 から圏
への関手を対象とし、それらの間の自然変換を射とする圏を、圏
から圏
への関手圏と呼び、
と書きます。
関手圏の射として同型射であるような自然変換を自然同値と呼びます。また、関手圏の対象として同型であるような関手を自然同値であると言います。
例：有向グラフは、圏 DiGraph
から への関手とみなすことができます。(第3章①)
関手としての有向グラフ について、「
から
への自然変換」はグラフの構造を保つようなものとなります。
関手圏は、「有向グラフを対象とし、その構造を保つ対応付けを射とする圏」となります。
「米田の補題」によって「局所的に小さいあらゆる圏は関手圏に埋め込める」ということらしいので、「米田の補題」のところ(④⑤)まで見た後でまた考えることにします。
②自然変換の定義2
圏 から圏
への関手
、
から
への関手
で、関手圏の対象として
、
なるものが存在するとき
、
は圏同値であると言います。
③自然変換の例1：前順序集合に関する例
前順序集合は、二つの対象の間に射が存在しないか、ただ一つしかないという圏となります。(第2章⑥)
圏 、
を前順序集合とし、
を
から
への関手(順序を保つ写像)とします。このとき、
から
への自然変換とは、「任意の
に対して
」として定義される順序関係となります。このとき、図式の可換性は自明となります。
このとき関手圏 は、
から
への「順序を保つ写像全体」に「自然な順序付け」をしたものとなります。
任意の集合は、恒等射しか存在しない圏(離散圏)と考えられます。つまり、任意の集合は前順序集合と考えられます。
このとき、「自明な前順序集合」としての任意の集合 から、ある前順序集合
への任意の写像は順序を保つ写像となります。
関手圏 は、「集合
から、ある前順序集合
への写像全体」に「自然な順序付け」をしたものとなります。
以上、ほぼ定義を引用しただけです。
「エレファントな整数論」で写像から作られる前順序集合について調べているのですが、今のところ圏論的な議論として書けるような内容がないので何かできたらまた書きたいと思います。
トポスについて書かれていたのでこれも引用しておきます。
関手圏
は普通の集合の圏
にとてもよく似た性質を持つ圏、いわゆる「トポス」となる。
トポスについては詳しくないので想像で書きますが、論理式の中には論理プログラミングとして書けるものと書けないものがあって、論理プログラミングとして書けるプログラムの「型」を表すものとして使えるのではないか、と考えています。
サーバー側のプロクラムとクライアント側のプログラムで全体で1つのプログラムの中で、クライアント側のプログラムを変更する事は全体としてはどういう意味になっているのかということを考えると、クライアント側の「型」とサーバー側の「型」を合成したものと考えることができます。
様々なクライアント側のプログラムを作るためのプログラミング言語がありますが、そのプログラムを論理プログラミングのプログラムとして表したときの「型」を表すような機能があれば、そのクライアント側のプログラムを更新するだけで全体を更新することができると考えられます。
