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

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

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

参照用 記事

インスティチューションと忘却関手

昨日(2019-06-06(日曜))、インスティチューション理論についてほんの少しだけ説明しました(チアガールズの説明のほうが長かった気がする)。インスティチューションについては、「キマイラ飼育記」の初期の頃からチョコチョコ触れています。

インスティチューションに関する資料として、僕が最初に思い浮かべるのはゴグエン〈Joseph Goguen〉による次のページです。

Maintained by Joseph Goguen
Last modified: Fri Jan 6 07:46:59 PST 2006

ゴグエン先生は2006年7月3日に亡くなられているので、それ以降はメンテナンスされていません。このページに目ぼしい論文へのリンクがあります。外部サイト(arXivとか)へのリンクではなくて、ローカルリンクですね。PostScript形式が多いです。

インスティチューション理論では、指標の圏Signと、指標Σに対するモデルの圏 Model[Σ] は公理的に与えられるのですが、Sign, Model[Σ] を具体的に作りたいことが多いので、作り方(の一例)を述べます。

まず、指標Σはコンピュータッド(nLab項目 computad)だとします。(適当な条件を付けた)コンピュータッドとコンピュータッド準同型からなる圏が Sign = (指標の圏) ですね。コンピュータッドΣから生成されるn-圏をΣとしましょう。モデル(指標の意味となる実体)が棲むn-圏をCとして、Model[Σ] を次のように定義します。

  • Model[Σ] = C-Model[Σ] := [Σ, C]

, C] は関手圏です。n = 2 、つまりΣは2-コンピュータッドであり、CSetを自明に2-圏とみなしたもの*1であるケースが一番よく使われる設定です。

例えば、有向グラフ(ここでは単に「グラフ」と呼ぶ)の指標は次だとします。

signature Graph :=
begin
  sorts
    V /* 頂点集合 */
    E /* 辺集合 */
  operations
    src:E→V  /* 辺の始点 */
    trg:E→V  /* 辺の終点 */
  laws
    /* 特になし */
end

指標Graphから、ソートEとオペレーション src, trg を落としてしまえば、集合の指標になります。

signature Set :=
begin
  sorts
    V
  operations

  laws

end

Set⊆Graph という包含を表す指標射を j:Set→Graph in Sign として、Model[j]:Model[Graph]→Model[Set] in CAT が対応する忘却関手です。

*1:写像のあいだのイコール関係を2-射とします。