オプティックは双方向データ変換の技法ですが、抽象的定式化の枠組みとしては丹原/ペイストロ*1/ストリート理論〈Tambara-Pastro-Street theory〉が使われているようです。なので、オプティックのための丹原/ペイストロ/ストリート理論の枠組みについてザッと眺めてみます。
内容:
丹原/ペイストロ/ストリート理論
原典は次の2つの論文です。
丹原2006:
- Title: Distributors on a tensor category
- Author: D. Tambara〈丹原 大介〉
- Received: 30 September 2004
- Published: May 2006, Hokkaido Math. Journal 35 (2006), pp.379–425
- Pages: 47p
- URL: https://projecteuclid.org/journals/hokkaido-mathematical-journal/volume-35/issue-2/Distributors-on-a-tensor-category/10.14492/hokmj/1285766362.full (ダウンロードページ)
ペイストロ/ストリート2007:
- Title:Doubles for monoidal categories
- Authors: Craig Pastro, Ross Street
- Submitted: 13 Nov 2007
- Pages: 13p
- URL: https://arxiv.org/abs/0711.1859
モノイド圏とプロ関手に関する代数的な話題を扱った論文なので、著者達も、後にプログラミングとデータ処理に利用されるとは思ってなかったでしょうね。
アクテゴリーとプロ関手
「両側アクテゴリーとその準同型射」の最後で紹介した以下の記法を使います。
ここで、 はモノイド圏で、2つのモノイド圏を係数域とする両側アクテゴリーの圏を表しています。射は強関手ですが、強度の緩さ〈looseness〉が右肩の に入ります*2。
を自明な圏に自明なモノイド構造を入れたモノイド圏だとすると、左アクテゴリーと右アクテゴリーは特殊な両側アクテゴリー〈双アクテゴリー〉だとみなせます。
よって、両側アクテゴリーについて考えればいいことになります。以下、両側アクテゴリーを考えます。両側アクテゴリーは、次のように略記します。
ここで、 は台圏で、 は左作用と右作用です。
さて、次のような圏(実際は2-圏)を考えます。
圏の対象集合とホム圏は以下のようです。
ここで、 はプロ関手の圏です。射の結合はプロ関手の結合として定義して、恒等射は恒等プロ関手とします。直積によりデカルト構造が入ります。
この圏はちょっと奇妙な圏で、対象は両側アクテゴリーであるにも関わらず、射はアクテゴリー構造を無視した台圏のあいだのプロ関手です。
は自然変換を2-射とする2-圏の構造を持つので、同じく自然変換を2-射とすれば も2-圏構造を持ちます。したがって、ホム対象 は単なる集合ではなくて圏です。
ホム圏のホムセットは次のように書けます。
ここで、 は自然変換の集合です。丸括弧のペアが3つ並ぶのが平板なので、次のようにも書きます。
丹原/ペイストロ/ストリート理論、あるいはその応用であるオプティック理論の舞台は2-圏 ですが、どの範囲を扱うかによって次のように分類されるでしょう。
- インデックス付き理論: 係数域であるモノイド圏ペア をインデックス〈パラメータ〉だとみなして、動かして考える。インデックス付き2-圏の構造が出てくる。
- 係数域固定理論: 係数域であるモノイド圏ペアは固定するが、2-圏を考える。
- ホム局所理論: 2-圏全体ではなくて、特定のホム圏〈1-圏〉だけに注目して考える。
他の分類方法もありますが、それは後の節で触れます。なおこの記事では、ホム局所理論の話をします。
プロ強プロ関手
「両側アクテゴリーとその準同型射」で色々な強度と強関手について述べました。左厳密強度(等式)は次の可換図式で表現できます。(下線は台圏を示します。)
この四角形のなかに、右上から左下にラックスな(可逆とは限らない)2-射を描けば、それはラックス左強度になります。
ブログ内でペースティング図を描くことがうまく出来ないので、同じ情報を次のように書くことにします。
この書き方は、ロマン〈Mario Román〉の描画法と相性が良かったりします。
同じ図式をプロ関手の圏で考えます。
下付きの は(一般化した)余米田埋め込みを表します(説明は省略)。
プロ関手の圏で考えたこの自然変換も通常はラックス左強度と呼びます。図式レベルで見ると、関手に対する強度もプロ関手に対する強度も同じですが、具体的に書き下すとだいぶ違うので、ここでは、プロ関手に対する強度をプロ強度〈prostrenght〉と呼ぶことにします。
プロ強度を備えたプロ関手がプロ強プロ関手〈prostrong profunctor〉です。強関手の場合と同様に、強度の種類に応じて様々なプロ強プロ関手があります。ここでは主に、両側ラックス・プロ強度を考えます。
プロ強度と協調する自然変換として、プロ強プロ関手のあいだの射(自然変換)が定義できます。これにより、アクテゴリー構造を反映したホム圏を定義できます。“ホム圏=プロ強プロ関手の圏”を次のように書きます。
丹原加群とペイストロ/ストリート・モナド
丹原加群〈Tambara module〉は、プロ強プロ関手の同義語です。丹原加群は、プロ関手を台として、プロ強度を演算とする代数系と考えます。丹原加群の圏はプロ強プロ関手の圏なので:
ロマンは "Profunctor optics and traversals" の50ページで、丹原加群の圏をひらがな「た」と書くと約束していますが、ちょっと使いにくいので "Tamb" にします。
丹原加群はプロ関手の上に演算(強度)を載せた代数構造なので、台プロ関手だけを取り出す忘却関手があります。忘却関手を次のように書きます。
この忘却関手には左随伴関手、つまり自由生成関手が存在します。それを次のように書きます。
もちろん、これらの関手は随伴ペアです。
丹原加群の忘却関手・自由生成関手ペアが構成する随伴系〈adjunction | adjoint system〉を丹原/ペイストロ/ストリート随伴系〈Tambara-Pastro-Street adjunction〉と呼びます。
丹原/ペイストロ/ストリート随伴系に付随するモナドをペイストロ/ストリート・モナド〈Pastro-Street Monad〉と呼び と書くことにします。記号の乱用で、モナドとモナドの台関手を同じ名前でオーバーロードします。
なので:
しかし、自己関手 の構成にはアクテゴリーの情報が必要です。
ペイストロ/ストリート・モナドに関して次が言えます。
セッティングの分類
丹原/ペイストロ/ストリートのホム局所理論だけを扱う場合でも、けっこうややこしいですよね。セッティングに次のパラメータが入るからです。
- モノイド圏
- モノイド圏
- アクテゴリー
- アクテゴリー
以下に述べるような選択肢があります。
係数域のモノイド圏はどんなモノイド圏とするか?
- 任意のモノイド圏
- 対称モノイド圏
- デカルト圏
- その他
アクテゴリーはどんなアクテゴリーとするか?
- 左または右の片側アクテゴリー(両側アクテゴリーの片方が自明モノイド圏)
- 一般の両側アクテゴリー
- モノイド圏から誘導される両側アクテゴリー
どのようなホム圏を考えるか?
- 域・余域が任意な混合ケース〈mixed case〉
- 域・余域が一致する非混合ケース〈non-mixed case〉
単純なセッティングの例として、モノイド圏 から誘導される両側アクテゴリーを使った非混合ケースを考えると、その丹原加群の圏は次のようです。
ここに挙げた以外にもバリエーションがあるので、どんなセッティングで議論するかは意識しておく必要があります。
おわりに
が前節で述べたセッティング・パラメータだとして、コエンド形式のオプティック公式〈optic formula〉を使ってオプティックの圏
を定義できます。
オプティックの埋め込み定理は、オプティックの圏が“丹原加群の圏の余前層の圏”に埋め込めることを主張します。埋め込みを とすると:
この埋め込みの構成を、僕は追いきれてないのですが、ライブラリ設計などに応用されているようです。
この状況を見ると、丹原加群の圏よりむしろ、“丹原加群の圏の余前層の圏”がより良い環境を提供するのかも知れません。
*1:発音は「パストロ」かと思ったんですが、https://www.howtopronounce.com/pastro で聞くと「ペイストロ」に近いようです。ほんとのところは分かりませんが。
*2:強度と協調する自然変換を2-射として2-圏の構造も入りますが、今は不要です。