ヒューズ・アローと丹原プロ関手 - 檜山正幸のキマイラ飼育記 (はてなBlog)

最近のマイブームは二重圏です（「二重圏、縦横をもう一度」参照）。既存の概念を二重圏ベースで再考してみるとちょっと楽しいです。

アローは、ジョン・ヒューズ〈John Hughes〉が考案した関数プログラミングの道具・手法です。ヒューズのアローを二重圏ベースで再考してみたいと思います。細部の確認をしてないので、話半分だと思ってください。[追記]案の定「話半分」でした。誤認と間違いがあります。が、本文の修正はしないで、追記の節を設けます。[/追記]$`\newcommand{\In}{\text{ in }}
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\o}[1]{\overline{#1}}
\newcommand{\dblcat}[1]{\mathbb{#1}}
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\twoto}{ \Rightarrow }
\newcommand{\lact}{ \triangleright }
\newcommand{\ract}{ \triangleleft }
\newcommand{\proar}{\dashrightarrow }
`$

内容：

言葉の約束
丹原プロ関手
丹原プロ関手の二重圏
二重圏内のモノイド
追記：誤認と間違い
ヒューズ・アロー

本文に誤認と間違いが含まれます。が、本文を修正してないので、「追記：誤認と間違い」を先に読んでください。

関連する記事：

丹原プロ関手の二重圏、いやっ三重圏？

言葉の約束

「アロー」という言葉は一般的過ぎますね。例えば、最近（2024年3月）の記事「自然変換は関手」でアロー圏を扱ってますが、ヒューズのアローとは何の関係もありません。単なる「アロー」ではなくてヒューズ・アロー〈Hughes arrow〉と呼ぶことにします。

代数学の“環上の左加群”に相当する圏類似代数系〈category-like algebraic system〉は左アクテゴリー〈left actegory〉と呼ばれます。左加群的圏〈left modular category〉とも呼ばれます。ここでは単に、左加群圏〈left module category〉とします。代数学で使われている名詞をそのまま（「的」とか付けずに）形容詞に使います。

そういうわけで、代数学の“双加群〈両側加群〉”に相当する圏類似代数系は双加群圏〈bimodule category〉と呼びます。双加群圏は、左加群圏であり右加群圏でもあり、左右のモノイド作用がバランス〈平衡〉している圏類似代数系です。

「圏論的レンズ 6：丹原／ペイストロ／ストリート随伴系」において、ペイストロ／ストリート〈Craig Pastro, Ross Street〉が定義した丹原加群〈Tambara module〉について紹介しました。ここでは、丹原加群を丹原プロ関手〈Tambara profunctor〉と呼ぶことにします。丹原加群は実際プロ関手であるからです。それと、「加群」をモノイド作用を持つ圏の意味で使うので、その意味の「加群」との混同を避けるためです。

その他、用語・記法・概念・定義は次の論文を参考にしています。

[AGGKLF21-]
Title: Compositional Game Theory, Compositionally
Authors: Robert Atkey, Bruno Gavranović, Neil Ghani, Clemens Kupke, Jérémy Ledent, Fredrik Nordvall Forsberg
Submitted: 26 Jan 2021
Pages: 17p
URL: https://arxiv.org/abs/2101.12045

[BR23-]
Title: Collages of String Diagrams
Authors: Dylan Braithwaite, Mario Román
Submitted: 4 May 2023 (v1), 14 Dec 2023 (v2)
Pages: 15p
URL: https://arxiv.org/abs/2305.02675

丹原プロ関手

内容は「圏論的レンズ 6：丹原／ペイストロ／ストリート随伴系」とかぶりますが記法は変わります。以下のように記法を約束します。

$`\cat{M},\cat{N}`$ はモノイド圏とする。
モノイド圏による左モノイド作用を $`\lact`$ 、右モノイド作用を $`\ract`$ と書く。
$`\cat{M},\cat{N}`$ による左右両側の作用を持つ双加群圏を、記号の乱用で $`\cat{C} = (\cat{C}, \lact, \ract)`$ と書く。
圏 $`\cat{C}`$ から $`\cat{D}`$ へのプロ関手とは、双関手 $`\cat{C}^\mrm{op}\times \cat{D} \to {\bf Set}`$ のことだとする（向きの約束）。
プロ関手は $`P: \cat{C} \not\to \cat{D}`$ のように書く。
プロ関手を二重圏の二重射〈2-射〉とみなす場合は、ギリシャ文字小文字で $`\phi: \cat{C} \twoto \cat{D}`$ のように書く。

プロ関手は様々な役割りを担います。

圏を対象として、プロ関手を射とする圏の射
圏を対象〈0-射〉、プロ関手を射〈1-射〉、自然変換を2-射とする2-圏の射〈1-射〉
圏を対象、関手をタイト射、プロ関手をプロ射、自然変換を二重射〈2-射〉とする二重圏のプロ射

今回話題にする丹原プロ関手は、次の役割りを担います。

特定した2つのモノイド圏上の双加群圏を対象、丹原プロ関手を射とする圏の射
モノイド圏を対象、ラックス・モノイド関手をタイト射、双加群圏をプロ射、丹原プロ関手を二重射〈2-射〉とする二重圏の二重射

まず、$`\cat{M}, \cat{N}`$ を特定した2つのモノイド圏だとして、$`\cat{M}`$ が左から $`\cat{N}`$ が右から作用する双加群圏達の圏を考えます。それは、「圏論的レンズ 6：丹原／ペイストロ／ストリート随伴系」において、$`(\cat{M}, \cat{N})\text{-}{\bf Tamb}`$ と書いた圏です。ただし過去記事では、$`(\cat{M}, \cat{N})\text{-}{\bf Tamb}`$ を2-圏と考えていましたが、今回は自然変換を捨てて1-圏と考えます。

この圏（2-圏ではない） $`(\cat{M}, \cat{N})\text{-}{\bf Tamb}`$ は：

対象は、$`(\cat{M}, \cat{N})`$-双加群圏〈双アクテゴリー〉
射は、$`(\cat{M}, \cat{N})`$-双加群圏のあいだのプロ強プロ関手

プロ強プロ関手は、丹原プロ関手〈丹原加群〉の別名です。プロ関手に対するテンソル強度〈tensorial strength〉（「モナドとテンソル強度の楽しいお絵描き」、「つわ者達の世界」参照）がプロ強度〈prostrength〉で、プロ強度を備えたプロ関手がプロ強プロ関手〈prostrong profunctor〉です。

プロ関手 $`T:\cat{C} \not\to \cat{D}`$ に付随したプロ強度（あるいは丹原強度）は、$`\cat{M}, \cat{N}, \cat{C}, \cat{D}`$ の対象をインデックスとする写像の族として記述できます。$`T`$ の左プロ強度を $`\mrm{lst}`$ 、右プロ強度を $`\mrm{rst}`$ とすると、次のように書けます。上線〈overline〉については、「状態遷移系としての前層・余前層・プロ関手 // 捻じれ対のテキスト表示と図示」を見てください。

$`\text{For }A\in |\cat{M}|, X \in |\cat{C}|, Y \in |\cat{D}|\\
\quad \mrm{lst}^A_{X, Y} : T(\o{X}, Y) \to T(\o{A\lact X}, A\lact Y) \In {\bf Set}\\
\text{For }B\in |\cat{N}|, X \in |\cat{C}|, Y \in |\cat{D}|\\
\quad \mrm{rst}^B_{X, Y} : T(\o{X}, Y) \to T(\o{X\ract B}, Y\ract B) \In {\bf Set}
`$

$`\mrm{lst}, \mrm{rst}`$ はプロ強度の法則〈公理〉を満たします。左プロ強度と右プロ強度を備えたプロ関手 $`(T, \mrm{lst}, \mrm{rst})`$ がプロ強プロ関手＝丹原プロ関手〈Tambara profunctor〉です。

丹原プロ関手の二重圏

これから定義する、丹原プロ関手を二重射とするような二重圏を $`\dblcat{Tamb}`$ （白抜き黒板文字が含まれる）とします。二重圏の基本事項は「二重圏、縦横をもう一度」を見てください。

二重圏 $`\dblcat{Tamb}`$ の構成素は次のようです。

対象は、モノイド圏
タイト射は、モノイド圏のあいだのラックス・モノイド関手
プロ射は、モノイド圏が左右から作用する双加群圏
二重射は、双加群圏のあいだの丹原プロ関手

二重射のフレーム〈境界〉の四辺形（「圏論におけるフレーム充填問題」参照）を図示すると次のようです。

$`\quad \xymatrix{
\cat{M} \ar[d]_{F} \ar@{-->}[r]^{\cat{C}}
& \cat{N} \ar[d]^{G}
\\
\cat{M'} \ar@{-->}[r]_{\cat{D}}
& \cat{N'}
}\\
\quad \In \dblcat{Tamb}
`$

$`\cat{M}, \cat{N},\cat{M'}, \cat{N'}`$ は、二重圏の対象であるモノイド圏
$`F:\cat{M} \to \cat{M'}, G: \cat{N}\to \cat{N'}`$ は、二重圏のタイト射であるラックス・モノイド関手
$`\cat{C}`$ は、二重圏のプロ射である $`(\cat{M}, \cat{N})`$-双加群圏
$`\cat{D}`$ は、二重圏のプロ射である $`(\cat{M'}, \cat{N'})`$-双加群圏

双加群圏 $`\cat{C}, \cat{D}`$ は異なる（かも知れない）モノイド圏ペアの上の双加群圏です。が、ラックス・モノイド関手 $`F, G`$ を経由して、双加群圏 $`\cat{D}`$ を $`(\cat{M}, \cat{N})`$-双加群圏とみなすことができます。$`(\cat{M}, \cat{N})`$ 上に $`F, G`$ で“引き戻された” $`\cat{D}`$ を

$`\quad (F, G)^*\cat{D}`$

と書くことにします。

先のフレーム四辺形を埋める二重射は次のような丹原プロ関手です。

$`\quad \tau : \cat{C} \not\to (F, G)^*\cat{D}`$

丹原プロ関手 $`\tau`$ を、二重圏の二重射として書けば：

$`\quad \xymatrix{
\cat{M} \ar[d]_{F} \ar@{-->}[r]^{\cat{C}}
\ar@{}[dr]|{\tau\,\Downarrow\:}
& \cat{N} \ar[d]^{G}
\\
\cat{M'} \ar@{-->}[r]_{\cat{D}}
& \cat{N'}
}\\
\quad \In \dblcat{Tamb}
`$

タイト射のタイト方向（「添加仮想二重圏」参照）への結合はラックス・モノイド関手の結合です。プロ射のプロ方向への結合〈積 | 乗法〉は、双加群圏のテンソル積により定義します。

二重射である丹原プロ関手のプロ方向への結合〈積 | 乗法〉は、丹原プロ関手のテンソル積によって定義します。丹原プロ関手〈双加群プロ関手〉のテンソル積については、最初の節に挙げた論文 [BR23-] に書いてあります。丹原プロ関手のタイト方向への結合も定義できて、たぶん二重圏の法則を満たすでしょう。「たぶん」なのは、細部まで確認してないからです。

二重圏内のモノイド

一般に、二重圏内のモノイド〈モノイド対象 | 内部モノイド〉という概念を定義できます。ここでは、丹原プロ関手の二重圏 $`\dblcat{Tamb}`$ 内のモノイドを定義・記述します。

$`\dblcat{Tamb}`$ 内のモノイドは、次の構成素からなります。

対象（モノイド圏） $`\cat{M} \in |\dblcat{Tamb}|`$
射（$`(\cat{M}, \cat{M})`$-双加群圏） $`\cat{A}: \cat{M}\proar \cat{M} \In \dblcat{Tamb}`$
二重射〈丹原プロ関手〉 $`\mu :: {\bf id}_\cat{M}[\cat{A}\otimes \cat{A} \twoto \cat{A}]{\bf id}_\cat{M} \In \dblcat{Tamb}`$
二重射〈丹原プロ関手〉 $`\eta :: {\bf id}_\cat{M}[\mrm{I}_\cat{M} \twoto \cat{A}]{\bf id}_\cat{M} \In \dblcat{Tamb}`$

これらを図示すると：

$`\quad \xymatrix{
\cat{M} \ar@{-->}[r]^{\cat{A}} \ar@{=}[d]
\ar@{}[drr]|{\mu\,\Downarrow\:}
&\cat{M} \ar@{-->}[r]^{\cat{A}}
&\cat{M} \ar@{=}[d]
\\
\cat{M} \ar@{-->}[rr]_{\cat{A}}
&{}
&\cat{M}
}\\
\In \dblcat{Tamb}
`$

$`\quad \xymatrix{
\cat{M} \ar@{-->}[r]^{\mrm{I}_\cat{M}} \ar@{=}[d]
\ar@{}[dr]|{\eta\,\Downarrow\:}
&\cat{M} \ar@{=}[d]
\\
\cat{M} \ar@{-->}[r]_{\cat{A}}
&\cat{M}
}\\
\In \dblcat{Tamb}
`$

ここで、

$`{\bf id}_\cat{M}`$ は、$`\cat{M}`$ の恒等関手で、図では縦方向のイコール記号で表している。
プロ射（横方向）のパスは、双加群圏のテンソル積を表す。
$`\mrm{I}_\cat{M}`$ は、単位プロ射。$`\cat{M}`$ の自明な双加群圏構造で与えられる。二重圏では、単位プロ射 $`\mrm{I}_\cat{M}`$ と恒等プロ射 $`\mrm{Id}(\cat{M})`$ の区別はないが、仮想二重圏では異なる概念になる。

$`(\cat{A}, \mu, \eta)/\cat{M}`$ が、通常のモノイド（あるいはモナド）と同様な結合律、左右の単位律を満たすとき、$`(\cat{A}, \mu, \eta)/\cat{M}`$ を $`\dblcat{Tamb}`$ 内のモノイド〈monoid〉といいます。

モノイドのあいだの準同型射〈モノイド射〉も定義できます。二重圏 $`\dblcat{Tamb}`$ 内のモノイド達とそのあいだのモノイド射の全体は圏を形成します。この圏を $`\mrm{Mon}(\dblcat{Tamb})`$ とします。

追記：誤認と間違い

丹原プロ関手を2-射〈二重射〉とする二重圏が構成可能なことは、確認はしてないまでも（今のところ）間違いだとは思っていません。二重圏のなかでモノイドを考えるのも一般論なので問題はありません。

が、そうやって作った二重圏内のモノイドがヒューズ・アローなのか？これはどうも違うようです。$`\dblcat{Tamb}`$ 内のモノイドが実現できたとしても、それはヒューズ・アローとは違うナニカです。よって、次節の記述は間違っています。

ヒューズ・アローを二重圏内のモノイドとして定義することは出来ると思ってますが、$`\dblcat{Tamb}`$ とは違う別な二重圏のなかのモノイドでしょう。セッティングを変える必要があります。どんなセッティングならいいのか？

通常のヒューズ・アローの定義をそのまま写し取るなら、次のような二重圏のモノイドでしょう（おそらく）。

対象は、対称モノイド圏
タイト射は、対称モノイド圏のあいだのラックス対称モノイド関手
プロ射は、プロ強度を持つプロ関手
2-射は、自然変換（対称モノイド構造との整合性が必要か？）

モノイドを考えるときは、タイト射は恒等射になるので、2-圏における定義に退化します。あんまり面白くないかも。

具体的な計算をサポートする目的なら、次のような二重圏のなかで考えるのもよさそう。

対象は、集合
タイト射は、写像
プロ射は、スパン
2-射は、スパンのあいだの射

ただし、モノイド構造やテンソル強度は別途追加する必要があります。

$`\dblcat{Tamb}`$ 内にヒューズ・アローを“素直に”実現できると思ったのは僕の早とちりですが、“無理やり”にでも、ヒューズ・アローを $`\dblcat{Tamb}`$ 内に埋め込む方法はあるのか？

うーむ、また後で考えてみます。

ヒューズ・アロー

この節の記述は間違っています。（前節を参照。）

ヒューズ・アロー〈Hughes arrow〉とは、二重圏 $`\dblcat{Tamb}`$ 内のモノイド $`(\cat{A}, \mu, \eta)/\cat{M}`$ であって、さらに次の条件を満たすものです。

モノイド圏 $`\cat{M}`$ は対称モノイド圏である。
$`|\cat{M}| = |\cat{A}|`$

モノイド乗法 $`\mu`$ はヒューズ・アローの結合〈composition〉と呼ばれ、習慣として中置演算子記号 $`\ggg`$ で書かれます。モノイド単位 $`\eta`$ はヒューズ・アローの単位〈unit〉ですが、習慣として $`\mrm{pure}`$ と書かれます。

ヒューズ・アローの演算達 $`\mu, \eta`$ は丹原プロ関手なので、定義よりプロ強度 $`\mrm{lst}, \mrm{rst}`$ を持ちます。モノイド圏 $`\cat{M}`$ は対称モノイド圏という仮定があるので、左右どちらかのプロ強度から、他方のプロ強度を再構成できます。

「ヒューズ・アローは $`\dblcat{Tamb}`$ 内のモノイド」といきなり言ったら唐突感は否めないでしょう。次なる課題は、この定義をアンパック（具体レベルにブレークダウン）して、唐突ではない定義を与えることです。