オプティックの圏とコエンドと米田テンソル計算

「論理や型理論の圏論的意味論」より：

今年いっぱいくらい、まとまった時間が取りにくい状況があるので、長いブログエントリーは書けそうにない。短いエントリーをチョコチョコと書くことにします。短くて完結した書き物は難しいので、続き物になる可能性が高いです。

と書きましたが、その後まーまーの長さの記事を書いてます。今回もまーまーの長さの記事ですが、備忘と予定のメモです。いずれ説明するつもりの話題に関するメモです。$`
\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\mbf}[1]{ \mathbf{#1} }
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\o}[1]{ \overline{#1} }
%\newcommand{\id}{ \mathrm{id} }
\newcommand{\In}{ \text{ in }}
\newcommand{\op}{ \mathrm{op}}
`$

内容：

オプティックの圏のホムセット

最近、エンド／コエンドに関して再論（蒸し返し）をしました。

• 圏論のエンドとコエンドは双対なんだよ
• 等式の二種類の使用法： 選別条件と同一視宣言

コエンドの応用として思いつくのは、オプティックの圏の定義です。オプティック（特に具象オプティック）については以下の過去記事で述べています。

• 圏論的レンズ 2： 具象オプティック

上記過去記事ではコエンドを明示的には使っていませんが、具象オプティックの圏 $`\mbf{ConcOptic}`$ のホムセットをコエンドを使って書くと次のようです*1。

$`\quad {\displaystyle
\int^{R\in |\mbf{Set}|} \mbf{Set}(A, R\times B) \times\mbf{Set}(R\times Y, X)
}
`$

集合圏の代わりに、対称モノイド圏 $`\cat{C}`$ を使うと、以下のようです。

$`\quad {\displaystyle
\int^{R\in |\cat{C}|} \cat{C}(A, R\otimes B) \times\cat{C}(R\otimes Y, X)
}
`$

上記のコエンドは、パラメータ $`A,B, X,Y`$ を含むので、 $`|\cat{C}|\times |\cat{C}|`$ の要素のペア（ペアのペア）ごとに集合を対応させます。

$`\quad (|\cat{C}|\times |\cat{C}|)^2 \ni ( (A, B), (X, Y)) \mapsto \\
\quad {\displaystyle \left(\int^{R\in |\cat{C}|} \cat{C}(A, R\otimes B) \times \cat{C}(R\otimes Y, X)\right) \in |\mbf{Set}| }
`$

$`(|\cat{C}|\times |\cat{C}|)^2 \to |\mbf{Set}|`$ という対応〈集合族 | ファミリー〉があるので、集合 $`|\cat{C}|\times |\cat{C}|`$ を頂点集合とする有向グラフが定義できます。有向グラフは圏の下部構造なので、圏を定義する第一歩となります。

米田テンソル

次の定義を考えます。

$`\quad P(A, B, X, Y, R, S) :=
\cat{C}(A, R\otimes X)\times \cat{C}(S\otimes Y, B)
`$

$`P(A, B, X, Y, R, S)`$ は6つの変数〈パラメータ〉を持つ集合です。とりあえず、非常に雑な定義として、幾つかの変数により決まる集合を米田テンソル〈Yoneda tensor〉と呼ぶ、と約束します。

もう少し補足が必要です； 幾つかの変数は圏の対象または射を表します。大文字が対象で小文字が射を表すと約束すると、射に対しては集合間の写像〈関数〉が対応します。

$`\quad P(a, b, x, y, r, s) : P(A, B, X, Y, R, S) \to P(A', B', X', Y', R', S')\In \mbf{Set}\\
\text{Where}\\
\quad a : A' \to A \In \cat{C}\\
\quad b : B \to B' \In \cat{C}\\
\quad x : X \to X' \In \cat{C}\\
\quad y : Y' \to Y \In \cat{C}\\
\quad r : R \to R' \In \cat{C}\\
\quad s : S' \to S \In \cat{C}
`$

方向を図示すると：

$`\quad \[email protected]{
A
& B \ar[d]|{b}
& X \ar[d]|{x}
& Y
& R \ar[d]|{r}
& S
\\
A' \ar[u]|{a}
& B'
& X'
& Y' \ar[u]|{y}
& R'
& S' \ar[u]|{s}
}`$

そして、$`P`$ は関手性を持つとします。結局、この米田テンソル $`P`$ は、集合圏に値を持つ6引数〈6変数 | 6項〉の関手です。6つの引数には、共変と反変が混じっています。反変を反対圏を使って表すことにすると、$`P`$ のプロファイルは次のように書けます。

$`\quad P :
\cat{C}^\op \times
\cat{C} \times
\cat{C} \times
\cat{C}^\op \times
\cat{C} \times
\cat{C}^\op \to \mbf{Set} \In \mbf{CAT}
`$

「圏論のエンドとコエンドは双対なんだよ」で説明したオーバーライン記法を使うと、次のように書けます。（[追記]説明不足だったので、すぐ後に補足説明を追加。[/追記]）

$`\quad P(\o{a}, b, x, \o{y}, r, \o{s}) : P(\o{A}, B, X, \o{Y}, R, \o{S}) \to P(\o{A'}, B', X', \o{Y'}, R', \o{S'})\In \mbf{Set}
`$

[補足]
「ラテン文字小文字は射を表す」はいいのですが、小文字 $`a`$ の最初の出現では、

$`\quad a : A' \to A \In \cat{C}`$

方向の図示では、$`a`$ を下から上の“逆行”で描いています。そして、オーバーライン記法では、

$`\quad \o{a} : A \to A' \In \cat{C}^\op`$

下から上の“逆行”の意味は：

• もとの圏 $`\cat{C}`$ 内では、$`a : A' \to A`$
• 反対圏 $`\cat{C}^\op`$ 内では、$`\o{a} : A \to A'`$

[/補足]

変数は、圏 $`\cat{C}`$ の対象または射を表すという暗黙の前提のもとで、6引数〈6変数 | 6項〉の関手を次のように書くと約束します。

$`\quad P(\o{A}, B, X, \o{Y}, R, \o{S})`$

関手の値だけではなくて、関手そのものもこの書き方で表します。この書き方は伝統的・前近代的なもので、次の点を注意する必要があります。

1. 関手の値（特定の集合）と、関手そのものを区別していない。文脈により判断する。
2. 引数変数は対象を表す変数（大文字）を使っているが、引数には射も許される（関手だから）。
3. 引数変数が、圏 $`\cat{C}`$ の対象または射を表すことは暗黙化されている。
4. 引数変数が共変か反変かはオーバーラインで区別するので、プロファイルの宣言はイチイチしない。

暗黙の前提や省略により曖昧となり、解読・解釈が困難にはなりますが、書く側にとってはとても楽ちんで便利です。このような“便利な書き方”は、古典テンソル計算の手法です。多引数〈多変数 | 多項〉の関手を「米田テンソル」と呼びたいのは、古典テンソル計算の手法を使う心積もりがあるからです。

古典テンソル計算と米田テンソル計算

古典テンソル計算では、添字〈インデックス〉を上下に振り分けます。ここで、「添字」とか「インデックス」は「引数〈argument〉」と同義語です。分野と伝統・習慣により違う呼び名を使っているだけで、意味的には同じことです。

前節の米田テンソルでは、オーバーライン記法で共変と反変の区別をしましたが、反変の引数変数〈添字 | インデックス〉を下側に、共変の引数変数を上側に書くと約束すると、オーバーラインは不要となります。

$`\quad P\left(
\begin{array}{l}
B, X, R
\\
A, Y, S
\end{array}
\right)
`$

これだと場所を取るので、引数変数〈添字 | インデックス〉を小さくして、引数達を囲む括弧は省略すると次のようになります。

$`\quad P^{B, X, R}_{A, Y, S}`$

さらに、引数達を区切るカンマも省略してしまうと：

$`\quad P^{B\, X\, R}_{A\, Y\, S}`$

非常にコンパクトに書けます。これが古典テンソル計算の標準的な記法です。

古典テンソル計算の記法で、米田テンソル $`P`$ の定義をもう一度書くと：

$`\quad P^{B\, X\, R}_{A\, Y\, S} := \cat{C}(A, R\times X)\times \cat{C}(S\times Y, B)`$

ところで、コエンドを使ったオプティックの議論は、下のようなストリング図を使って進めるのが効果的です（「圏論的レンズ 2： 具象オプティック」より）。

しかし、毎回ストリング図を描くのは大変なので、図だけでなくテキスト記法も欲しいのです。図の情報を律儀にテキストにエンコードすると、とても煩雑になります。テキトーにサボらないとやってられません。古典テンソル計算がサボる手法を提供してくれます。

米田テンソル計算の目的は、集合圏に値を持つ多引数〈多変数 | 多項〉関手の記述と計算を、古典テンソル計算にならった記法で行うことです。

過去（2021年）に、米田テンソル計算について述べています。

• 米田テンソル計算 1： 経緯と発想

このシリーズは途中までしか書いてないので、古典テンソル計算にならった記法については説明していません。なので、（図ではなく）テキストによる記述と計算の説明も今後したいと思っています。

なぜにまた米田テンソル計算

米田テンソル計算を考えるキッカケのひとつは、マリオ・ロマン〈Mario Román〉の論文 "Open Diagrams via Coend Calculus"（「米田テンソル計算 1： 経緯と発想」参照）です。最近、ロマンの論文をまた見る機会があって（ほとんど忘れていた(苦笑)が）、「そう言えば、米田テンソル計算は中断していた」と思い出したわけです。

計算体系だけいじっていても面白くないので、レンズ／オプティック／フィードバック付き射などの圏をコエンド（テンソル計算の言葉では縮約）により構成する例を調べたいですね。

それと、コエンドによりホムセットを定義する際のストリング図と、ホムセットの要素（つまり射）のストリング図は無関係ではないのですが、どういう関係があるかハッキリしない。これがハッキリしたら楽しい気がします。

*1:大きな圏 $`\mbf{Set}`$ の上でコエンドを構成しているので、サイズの問題を考慮する必要があります。