このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」（http://d.hatena.ne.jp/m-hiyama-memo/）のデータを移行・保存したものであり、今後（2019年1月以降）更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

ローヴェル・フレームワーク

高次圏論 プログラム意味論 まとめ セオリー論

代数的定義形式とアンビエント構造 - 檜山正幸のキマイラ飼育記 メモ編 の続きで、ローヴェル・セオリーを可能とするフレームワークについて。

ローヴェル・セオリー

ローヴェル・セオリーの導入・説明では、有限集合の圏FinSetの骨格として、基数（それ自身集合）の集合アレフ0を取り、基数のあいだの写像からなるSet充満部分圏を考える。が、これは分かりにくい。次のfinを代わりに使う。

  • |fin| = N
  • fin(n, m) := Set([n], [m])

Nを対象類とする圏とidentity-on-objects関手の圏Cat[N]を考える。a:fin→A in Cat[N] が有限積を厳密に保存するとき、(A, a)をローヴェル・セオリーと呼ぶ。Aはセオリーの台圏、aはセオリーの構造射（関手）。

ローヴェル・セオリーは、単ソート有限積セオリーなので、アンビエントとして有限積圏〈category with finnite product〉の圏FPCatを考える。FPCatはCat上の具象2-圏で、

  1. 対象は有限積圏
  2. 射は、有限積をタイトに保存する関手（厳密でなくてもよい）
  3. 2-射は、自然変換

このケースでは、FPCatが1-アンビエント〈1-ドクトリン | 1-宇宙 | 1-レルム〉で、1-圏を対象に持ち、それ自身は2-圏。厳密に積を保存する関手からなる部分2-圏はFPCatstrとする。FPCatstrは、役割としては厳密アンビエント、またはファーム・アンビエント〈firm ambient〉。

finは、アンビエント内でのコア対象〈core object〉。コア対象は、アンビエントが2-モナドTのEM代数だとして、2-モナドTの単位対象1 = 1(2)0 による像。

  • fin = T(1)

単一の対象からなる自明な圏から、Tにより生成されるアンビエント内対象がfin。

アンビエントのコア対象からの関手で、ファーム（厳密）で対象を動かさない（identity-on-objects）射を構造射として持つアンビエント内対象（1-圏）がローヴェル・セオリー。

  • Law = fin/(FPCat[N])str

ローヴェル・セオリーは、0-射記号＝ソートを1つだけ持つ定義形式〈指標 | 仕様〉で定義される。この定義形式には、1-生成射も2-生成射（等式）も無限個（可算無限個）を許す。したがって、可算無限個までの0-生成射、1-生成射、2-生成射を許す代数的定義形式はセオリーと呼んでも問題ない。コア対象からのファーム相対対象（オーバー圏の対象）と単一ソートの定義形式が対応し、どちらもセオリーと呼んでよい。

  1. コア対象の下の相対圏としてのセオリー
  2. 単ソートで、可算無限の1, 2-構成素を持つ1-定義形式としてのセオリー

次の関係がある。

  1. セオリー指標からローヴェル・セオリー圏を作れる。
  2. すべてのローヴェル・セオリー圏は、適当な指標から作られる。ローヴェル・セオリー圏Aを生成する指標を（役割として）Aのプレゼンテーションと呼ぶ。

セオリーのモデル

ローヴェル・セオリー (A, a) があると、台圏Aは1-アンビエントであるFPCatの対象である。よって、同じFPCat内の対象である有限積圏Cへの射（有限積保存関手）M:A→C は定義できる。これが(A, a)のモデル。Cをセマンティック圏と呼ぶのは定義形式のモデルのときと同じ。

セマンティック圏を固定すると、セオリーとセオリー射の圏は、Law = fin/(Cat[N])str、この圏をベース圏〈インデキシング圏〉として、モデルの圏をファイバーとするインデックス付き圏が作れる。

さらにセマンティック圏も動かすと、セオリーの圏の対象と、アンビエント圏の対象をパラメータとする双加群ができる。これはセオリーの圏を底領域、アンビエント圏を指数領域とする指数演算だと思われる。底の役割を持つ対象（1-圏）をセマンティック圏と呼ぶことになる。指数（肩）の役割がセオリー。

モデルは指数なので、底であるセマンティック圏に関しては共変に動き、指数（肩）であるセオリーに関しては反変に動く。

ローヴェル・フレームワーク

ローヴェル・セオリーには次の登場者がいる。

  1. 1-アンビエントであるFPCat、有限積を持つ圏の圏（それ自体は2-圏）。
  2. 1-アンビエントは、とある2-モナドのアイレンベルグ／ムーア2-圏なので、1-アンビエントを生じさせる2-モナドT。TはCat上に働く2-モナドで、有限積を持つ圏を自由生成する。
  3. 1-アンビエント＝EM(Cat, T) 内のコア対象。コア対象は常にT(1)で定義される。
  4. コア対象（と呼ばれる圏）と同じ対象類を持つ圏と、ファーム関手を射とする圏。この圏の対象と射が、セオリーの構成素となる。

このなかで、一番の基本は2-モナドT、Tがあれば、次のようにして他のモノを作れる。

  1. EM(Cat, T)としてアンビエントを作る。
  2. T(1)としてコア対象を作る。
  3. コア対象を含む、アンビエントの部分圏であるファーム部分圏を作る。
  4. ファーム部分圏内で、コア対象のアンダー圏を作ることによりセオリーの圏を作る。

Cat上の2-モナドと、Set上の1-モナドの組み合わせで、構造を持つ圏内に作れる構造を持つ対象（集合）を定義することがローヴェル・セオリーの理論であり、それを可能とするセッティングをローヴェル・フレームワークと呼ぶ。

ローヴェル・セオリーのハイライト

セオリーの射（関手） T→T' は、反変的にCモデル圏の関手 [T', C]→[T, C] を導く。これは、（一般化された）忘却関手と考えてよい。

  • （一般化された）忘却関手には左随伴が存在して、（一般化された）自由生成関手となる。
  • 忘却・自由生成の随伴ペアからモナドとコモナドを作れる。
  • C = Set とすると、集合モデル [T, Set] から、Tを再現できる。