Avendia20

日記 (2021 年 10 月 12 日)

今回は、 10 月 10 日で紹介したコエンドレンズを一般化したオプティックを定義する。 さらに、 10 月 9 日で紹介したレンズのプロ関手エンコーディングを、 オプティックに対しても使えるように一般化する。

以降の議論ではモノイダル圏の作用を用いるので、 まずはそれについて復習しておく。 なお、 モノイダル圏の演算は常に ⊗ で表し、 その単位対象は ⊤ で表す。

定義 4.1.

圏 󰒚 およびモノイダル圏 󰒢 をとる。 End(󰒚) を合成に関してモノイダル圏と見なすとき、 強モノイダル関手 ⊘:󰒢→End(󰒚) のことを 󰒢 の 󰒚 への作用 (action) という。

モノイダル圏の作用 ⊘:󰒢→End(󰒚) があると、 各 󰒢 の対象 K に対して End(󰒚) の対象 K⊘- が定まる。 これは関手 K⊘-:󰒚→󰒚 であるから、 さらに 󰒚 の対象 X があれば 󰒚 の対象 K⊘X が定まる。 ⊘:󰒢→End(󰒚) が強モノイダル関手であることから、 この演算は 󰒢 のモノイダル構造と次の意味で適合している。 すなわち、 任意の 󰒢 の対象 K,L と 󰒚 の対象 X に対し、 K⊘(L⊘X)≅(K⊗L)⊘X⊤⊘X≅X が成り立つ。 逆に言えば、 モノイダル圏 󰒢 の圏 󰒚 への作用とは、 󰒢 の対象と 󰒚 の対象から 󰒚 の対象を得る演算であって、 両方の変数に関して関手性があり上記の形の自然同型をもつようなもののことである。

さて、 レンズのコエンドによる表現について思い出そう。 コエンドレンズとは、 対象 S,󰔄S,A,󰔄A に対し、 Lens󰒚(S,󰔄S;A,󰔄A):=󰄵K∈󰒚(Hom(S,K×A)×Hom(K×󰔄A,󰔄S)) というコエンドで書かれた集合の元であった。 この形を見ると、 コエンドをとっている K が動く圏を 󰔄󰒚 ではなく別のモノイダル圏 󰒢 にして、 コエンド内部の K×- の部分をモノイダル圏の作用 K⊘- に置き換えることができそうである。 さらに、 コエンド内部に K×- の形は 2 ヶ所あるが、 これをモノイダル圏の作用で書き換えるときに同じ作用にする必要もなさそうである。 加えて、 コエンド内部には 2 つの射集合があるが、 これを別々の圏でとることもできそうである。 以上の観察から、 レンズは次のように一般化できる。

定義 4.2.

圏 󰒚,󰔄󰒚 とモノイダル圏 󰒢 について、 󰒢 の 󰒚 への作用 ⊘:󰒢→End(󰒚) および 󰒢 の 󰔄󰒚 への作用 ⦸:󰒢→End(󰔄󰒚) が定まっているとする。 これらの組 (󰒚,󰔄󰒚,󰒢;⊘,⦸) をオプティック領域 (optic domain) と呼ぶ。

定義 4.3.

オプティック領域 󰒮:=(󰒚,󰔄󰒚,󰒢;⊘,⦸) をとる。 このとき、 󰒚 の対象 S,A と 󰔄󰒚 の対象 󰔄S,󰔄A に対し、 Optic󰒮(S,󰔄S;A,󰔄A):=󰄵K∈󰒢(Hom󰒚(S,K⊘A)×Hom󰔄󰒚(K⦸󰔄A,󰔄S)) の元 γ をコエンドオプティック (coend optic) と呼び、 γ:(S,󰔄S)→(A,󰔄A) で表す。

圏 󰒚 は有限積をもてば、 その積によって 󰒚 をモノイダル圏と見なすことができ、 さらにその積は作用 ×:󰒚→End(󰒚) を定める。 このセッティングのものでのオプティックがレンズである。 すなわち、 対象 S,󰔄S,A,󰔄A に対し、 Optic(󰒚,󰒚,󰒚;×,×)(S,󰔄S;A,󰔄A)≅Lens󰒚(S,󰔄S;A,󰔄A) が成り立つ。

コエンドオプティックの合成がコエンドレンズと同様に定められ、 コエンドオプティックを射とする圏が定義できる。

定義 4.4.

オプティック領域 󰒮:=(󰒚,󰔄󰒚,󰒢;⊘,⦸) をとる。 圏 COptic(󰒮) を、

によって定義する。

このように一般化されたオプティックについても、 プロ関手によるエンコーディングをすることができる。 その方法は 10 月 9 日で触れたものとほぼ同じで、 積だった箇所をモノイダル圏の作用に置き換えれば良いだけである。

定義 4.5.

オプティック領域 (󰒚,󰔄󰒚,󰒢;⊘,⦸) をとる。 さらに、 プロ関手 P:󰔄󰒚⇸󰒚 をとる。 対象 M,X,󰔄X に対し、 全ての変数に関して自然な射 ξMX󰔄X:P(X,󰔄X)⟶P(M⊘X,M⦸󰔄X) が定まっていて、 任意の対象 M,N,X,󰔄X に対し、 図式 P(X,󰔄X)P((M⊗N)⊘X,(M⊗N)⦸󰔄X)P(N⊘X,N⦸󰔄X)P(M⊘(N⊘X),M⦸(N⦸󰔄X))ξM⊗N,X,󰔄XξNX󰔄XξM,N⊘X,N⦸󰔄X P(X,󰔄X)P(⊤⊘X,⊤⦸󰔄X)P(X,󰔄X)ξ⊤X󰔄X が全て可換であるとする。 なお、 ラベルのない射は標準的な同型射を表している。 このとき、 ξ を P に対する Tambara 構造 (— structure) といい、 組 (P,ξ) を Tambara 加群 (— module) という。

定義 4.6.

オプティック領域 (󰒚,󰔄󰒚,󰒢;⊘,⦸) をとる。 さらに、 Tambara 加群 (P,ξ),(Q,ζ):󰔄󰒚⇸󰒚 および自然変換 θ:P⇒Q をとる。 任意の対象 M,X,󰔄X に対し、 P(X,󰔄X)Q(X,󰔄X)P(M⊘X,M⦸󰔄X)Q(M⊘X,M⦸󰔄X)θX󰔄XθM×X,M×󰔄XξMX󰔄XζMX󰔄X が可換であるとき、 θ を Tambara 加群の射 (morphism of — modules) といい、 θ:(P,ξ)⇒(Q,ζ) で表す。

定義 4.7.

オプティック領域 󰒮:=(󰒚,󰔄󰒚,󰒢;⊘,⦸) をとる。 圏 Tamb(󰒮) を、

によって定義する。

定義 4.8.

オプティック領域 (󰒚,󰔄󰒚,󰒢;⊘,⦸) をとる。 対象 A,󰔄A に対し、 -(A,󰔄A): Tamb(󰒮) ⟶ Set (P,ξ) ⟼ P(A,󰔄A) とおく。 このとき、 対象 S,󰔄S,A,󰔄A に対し、 自然変換 φ:-(A,󰔄A)⇒-(S,󰔄S) をプロ関手オプティック (profunctor optic) という。

定義 4.9.

オプティック領域 󰒮:=(󰒚,󰔄󰒚,󰒢;⊘,⦸) をとる。 圏 POptic(󰒮) を、

によって定義する。

コエンドオプティックとプロ関手オプティックが等価であることは、 10 月 9 日で行った議論のように表現可能性を介して証明することができる。 ただし、 証明は一般のオプティックの場合に適用できるように少し変える必要がある。

定理 4.10.

オプティック領域 󰒮:=(󰒚,󰔄󰒚,󰒢;⊘,⦸) をとる。 対象 A,󰔄A に対し、 関手 -(A,󰔄A):Tamb(󰒮)→Set は表現可能である。

証明.

Hom(A,-󰔄A):StrEnd(󰔄󰒚)→Set の表現対象を具体的に構成する。 まず、 WA󰔄A: 󰒚∘×󰔄󰒚 ⟶ Set (X,󰔄X) ⟼ Optic󰒮(X,󰔄X;A,󰔄A) とおく。 さらに、 対象 M,X,󰔄X に対し、 χMX󰔄XA󰔄A: Optic󰒮(X,󰔄X;A,󰔄A) ⟶ Optic󰒮(M⊘X,M⦸󰔄X;A,󰔄A) ⟨l,r⟩K ⟼ ⟨idM⊘l,idM⦸r⟩M⊗K とおくと、 これは全ての変数に関して自然であり、 さらに Tambara 構造の公理を満たす。 したがって、 (WA󰔄A,χA󰔄A) は Tambara 加群である。

すると、 この (WA󰔄A,χA󰔄A) が実際に Hom(A,-󰔄A):Tamb(󰒮)→Set の表現対象であること、 すなわち HomTamb(󰒮)((WA󰔄A,χA󰔄A),-)≅-(A,󰔄A) が成り立つ。 ここでは証明は省略する。

定理 4.11.

オプティック領域 󰒮:=(󰒚,󰔄󰒚,󰒢;⊘,⦸) をとる。 対象 S,󰔄S,A,󰔄A に対し、 全単射 HomPOptic(󰒮)((S,󰔄S),(A,󰔄A))≅HomCOptic(󰒮)((S,󰔄S),(A,󰔄A)) が存在する。

証明.

定理 4.10 と Yoneda の補題により、 HomPOptic(󰒮)((S,󰔄S),(A,󰔄A)) = Hom[Tamb(󰒮),Set](-(A,󰔄A),-(S,󰔄S)) ≅ Hom[Tamb(󰒮),Set](Hom((LA󰔄A,χA󰔄A),-),-(S,󰔄S)) ≅ WA󰔄A(S,󰔄S) = Optic󰒮(S,󰔄S;A,󰔄A) ≅ HomCOptic(󰒮)((S,󰔄S),(A,󰔄A)) が成り立つ。

定理 4.12.

オプティック領域 󰒮 をとる。 圏同型 POptic(󰒮)≅COptic(󰒮) が成立する。

証明.

定理 4.11 の全単射が合成を保つことを示せば良い。

以上が、 レンズを一般化したオプティックの定義とそのプロ関手エンコーディングの概要である。 次回は、 オプティックの具体例として、 レンズの他にも様々な有用なデータ形式が得られることを見る予定である。

参考文献

  1. B. Clarke et al (2020) 「Profunctor optics, a categorical update」 arXiv:2001.07488
  2. M. Riley (2018) 「Categories of optics」 arXiv:1809.00738