ΤΑ ΖΙΦΙΛΟΥΒΙΒΛΙΑ

日記 (2022 年 1 月 3 日)

前回までの日記で、 レンズの様々なエンコーディング方法に触れ、 これらが全て等価であることを示した。 さらに、 レンズを一般化してオプティックという概念を導入し、 レンズの場合と同様にコエンドによるエンコーディングとプロ関手を用いたエンコーディングを定式化し、 これらが等価であることも示した。

このオプティックの 2 つのエンコーディングが等価であることは 10 月 12 日ですでに示したが、 今日は Román†2 による別の証明をまとめようと思う。 この証明は、 前回の証明よりも見通しが良く、 Tambara 加群がコモナド余代数やモナド代数として実現できることに注目しているという特徴がある。

初めに定義の確認をしておこう。 オプティックは、 次のようにモノイダル圏が 2 つの圏に作用しているという状況で定義される。

定義 5.1.

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

定義 5.2.

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

コエンドを用いたオプティックの定義は次のようであった。

定義 5.3.

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

一方、 オプティックにはプロ関手を用いたエンコーディングもあり、 これは Tambara 加群の圏上の自然変換として実現される。

定義 5.4.

オプティック領域 (󰒚,󰔄󰒚,󰒢;⊘,⦸) をとる。 さらに、 プロ関手 P:󰔄󰒚⇸󰒚 をとる。 対象 M,X,󰔄X に対し、 全ての変数に関して自然な射 ξMX󰔄X:P(X,󰔄X)⟶P(M⊘X,M⦸󰔄X) が定まっていて、 任意の対象 M,N,X,󰔄X に対し、 図式 P(X,󰔄X)P(⊤⊘X,⊤⦸󰔄X)P(X,󰔄X)ξ⊤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 に対する 「Tambara 構造 (— structure)」 といい、 組 (P,ξ) を 「Tambara 加群 (— module)」 という。

定義 5.5.

オプティック領域 (󰒚,󰔄󰒚,󰒢;⊘,⦸) をとる。 さらに、 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,ζ) で表す。

定義 5.6.

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

  • Tamb(󰒮) の対象は、 󰒚 上の Tambara 加群 (P,ξ) の全体とする。
  • Tamb(󰒮) の 2 つの対象 (P,ξ),(Q,ζ) の間の射は、 Tambara 加群の射 θ:(P,ξ)⇒(Q,ζ) の全体とする。

によって定義する。

定義 5.7.

オプティック領域 (󰒚,󰔄󰒚,󰒢;⊘,⦸) をとる。 このとき、 󰒚 の対象 S,A と 󰔄󰒚 の対象 󰔄S,󰔄A に対し、 POptic󰒮(S,󰔄S;A,󰔄A):=󰄵(P,ξ)∈Tamb(󰒮)Hom(P(A,󰔄A),P(S,󰔄S)) の元 φ を 「プロ関手オプティック (profunctor optic)」 と呼ぶ。

上記の定義において、 POptic󰒮(S,󰔄S;A,󰔄A) は射集合のエンドとして定義されているので、 これは自然変換の全体である。 具体的には、 Tambara 加群 (P,ξ) に対して、 構造射 ξ を忘れて (A,󰔄A) での像を返す関手を -(A,󰔄A): Tamb(󰒮) ⟶ Set (P,ξ) ⟼ P(A,󰔄A) と書くことにすると、 自然変換 φ:-(A,󰔄A)⇒-(S,󰔄S) がプロ関手オプティックである。

さて、 オプティック領域 󰒮:=(󰒚,󰔄󰒚,󰒢;⊘,⦸) 上の Tambara 加群 (P,ξ) の構造射 ξ とは、 対象 M,X,󰔄X に対する ξMX󰔄X:P(X,󰔄X)⟶P(M⊘X,M⦸󰔄X) という形の自然な写像の族であった。 これは、 特に M に関する自然性から、 対象 X,󰔄X に対する ξX󰔄X:P(X,󰔄X)⟶󰄵M∈󰒢P(M⊘X,M⦸󰔄X) という形の自然な写像の族と 1 対 1 に対応する。 この右辺を簡単のため Φ󰒮P(X,󰔄X) と書くことにする。 すると、 上記の ξX󰔄X は X と 󰔄X に関して自然だったから、 これは ξ:P⇒Φ󰒮P という自然変換と 1 対 1 に対応する。 これで、 Tambara 加群 (P,ξ) の構造射 ξ が、 P 自身から P が定める別のプロ関手への自然変換であることが分かった。

そこで、 今 Φ󰒮 と書いたプロ関手からプロ関手を得る操作に注目することにしよう。 これは、 Φ󰒮: Prof(󰔄󰒚,󰒚) ⟶ Prof(󰔄󰒚,󰒚) P ⟼ ❲ 󰒚∘×󰔄󰒚 ⟶ Set (X,󰔄X) ⟼ 󰄵M∈󰒢P(M⊘X,M⦸󰔄X)❲ という Prof(󰔄󰒚,󰒚) 上の自己関手を定める。 次に示すように、 これはコモナドの構造をもつ。

命題 5.8.

オプティック領域 󰒮:=(󰒚,󰔄󰒚,󰒢;⊘,⦸) をとる。 上記で定まる Prof(󰔄󰒚,󰒚) 上の自己関手 Φ󰒮 はコモナドの構造をもつ。

証明.

まず、 余単位 ε:idProf(󰔄󰒚,󰒚)⇒Φ を定める。 これを定めるには、 プロ関手 P と対象 X,󰔄X に対して、 写像 εPX󰔄X:ΦP(X,󰔄X)→P(X,󰔄X) を全変数に関して自然になるように定めれば良い。 そこで、 合成 󰄵MP(M⊘X,M⦸󰔄X)P(⊤⊘X,⊤⦸󰔄X)P(X,󰔄X)pr⊤ を εPX󰔄X と定める。

次に、 余乗法 δ:Φ∘Φ⇒Φ を定める。 そのために、 プロ関手 P と対象 X,󰔄X に対して、 写像 δPX󰔄X:ΦP(X,󰔄X)→ΦΦP(X,󰔄X) を全変数に関して自然になるように定める。 エンドの普遍性から、 任意の対象 M,N に対し、 図式 󰄵MP(M⊘X,M⦸󰔄X)󰄵N󰄵MP(M⊘(N⊘X),M⦸(N⦸󰔄X))P(M⊗N)⊘X,(M⊗N)⊘XP(M⊘(N⊘X),M⦸(N⦸󰔄X))δPX󰔄XprM⊗NprM∘prN を可換にする破線の射がとれる。 これを δPX󰔄X と定める。

後は、 今定めた ε と δ がコモナドの公理を満たすことを確かめれば良い。 詳細は省略する。

すでに述べたように、 オプティック領域 󰒮:=(󰒚,󰔄󰒚,󰒢;⊘,⦸) 上の Tambara 加群 (P,ξ) の構造射 ξ は、 自然変換 ξ:P⇒Φ󰒮P と見なせる。 この ξ が本当に Tambara 加群の構造射になるためには、 さらに定義 5.4 中の図式 ♡ を可換にする必要があるが、 実は ξ がこの図式を可換にすることと ξ が Φ󰒮 上のコモナド余代数になることが同値になっている。 すなわち、 󰒮 上の Tambara 加群と Φ󰒮 上の余代数は 1 対 1 に対応する。 この対応は、 さらに圏同値にもなる。

定理 5.9.

オプティック領域 󰒮:=(󰒚,󰔄󰒚,󰒢;⊘,⦸) に対し、 圏同値 Tamb(󰒮)≅Prof(󰔄󰒚,󰒚)Φ󰒮 が成立する。 なお、 右辺は Φ󰒮 上の余 Eilenberg–Moore 圏である。

証明.

プロ関手 P:󰔄󰒚⇸󰒚 および自然変換 ξ:P⇒ΦP をとる。 ξ が Φ 上のコモナド余代数であるための条件は、 2 つの図式 PΦPPξεPΦξPΦPΦPΦΦPξξδPΦξ♤ が可換であることである。

まず、 式 ♤ の左側の図式について考える。 これは、 任意の対象 X,󰔄X に対して、 図式 P(X,󰔄X)󰄵MP(M⊘X,M⦸󰔄X)P(X,󰔄X)ξX󰔄XεPX󰔄X♤1󰎘 が可換であることと同値である。 この図式の可換性が、 図式 P(X,󰔄X)P(⊤⊘X,⊤⦸󰔄X)P(X,󰔄X)ξ⊤X󰔄X♡1󰎘 の可換性と同値であることを示す。 ここで、 P(X,󰔄X)󰄵MP(M⊘X,M⦸󰔄X)P(⊤⊘X,⊤⦸󰔄X)P(X,󰔄X)ξX󰔄Xζ⊤X󰔄Xpr⊤εPX󰔄X を考えると、 この図式の最も外側部分が図式 ♤1󰎘 であり、 この図式の左下にある三角形部分が図式 ♡1󰎘 である。 一方で、 この図式の残りの部分は定義から可換だから、 これにより 2 つの図式 ♤1󰎘 と ♡1󰎘 の可換性は同値である。

次に、 式 ♤ の右側の図式について考える。 これは、 任意の対象 X,󰔄X に対して、 図式 P(X,󰔄X)󰄵MP(M⊘X,M⦸󰔄X)󰄵MP(M⊘X,M⦸󰔄X)󰄵N󰄵MP(M⊘(N⊘X),M⦸(N⦸󰔄X))ξX󰔄XξX󰔄XδPX󰔄X(Φξ)X󰔄X♤2󰎘 が可換であることと同値である。 この図式の可換性が、 任意の対象 M,N に対して図式 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♡2󰎘 が可換になることと同値であることを示す。 ここで、 2 つの図式 P(X,󰔄X)󰄵MP(M⊘X,M⦸󰔄X)󰄵N󰄵MP(M⊘(N⊘X),M⦸(N⦸󰔄X))P((M⊗N)⊘X,(M⊗N)⦸󰔄X)󰄵MP(M⊘(N⊘X),M⦸(N⦸󰔄X))P(M⊘(N⊘X),M⦸(N⦸󰔄X))ξX󰔄XξM⊗N,X,󰔄XδPX󰔄XprM⊗NprNprM P(X,󰔄X)󰄵MP(M⊘X,M⦸󰔄X)󰄵N󰄵MP(M⊘(N⊘X),M⦸(N⦸󰔄X))P(N⊘X,N⦸󰔄X)󰄵MP(M⊘(N⊘X),M⦸(N⦸󰔄X))P(M⊘(N⊘X),M⦸(N⦸󰔄X))ξX󰔄XξNX󰔄XξM,N⊘X,N⦸󰔄X(Φξ)X󰔄XprNprNprM は可換である。 図式 ♤2󰎘 が可換であることは、 このそれぞれの図式について左上から右上を経由して右下へ進む経路が等しいことと同値である。 また、 図式 ♡2󰎘 が可換であることは、 このそれぞれの図式について左上から右下へ斜めに進む経路が等しいことと同値である。 この図式は全て可換だったから、 これにより 2 つの図式 ♤2󰎘 と ♡2󰎘 の可換性は同値である。

以上により、 式 ♤ 中の 2 つの図式と式 ♡ 中の 2 つの図式の可換性は同値である。 すなわち、 ξ を自然変換 ξ:P⇒ΦP と見なしたときに ξ が Φ 上のコモナド余代数になることと、 ξ を定義 5.4 にあるような写像の族と見なしたときに ξ が Tambara 加群になることは同値である。 これより、 Φ 上のコモナド余代数 (P,ξ) と Tambara 加群 (P,ξ) は 1 対 1 に対応する。

また、 この対応は関手に拡張され、 それが定理中の圏同値を与えることが示せる。 この詳細は省略する。

加えて、 この関手は左随伴をもつ。

定理 5.10.

オプティック領域 󰒮:=(󰒚,󰔄󰒚,󰒢;⊘,⦸) に対し、 Φ󰒮 は左随伴をもつ。

証明.

まず、 HomProf(󰔄󰒚,󰒚)(Q,Φ󰒮P) ≅ 󰄵X,󰔄XHom(Q(X,󰔄X),󰄵MP(M⊘X,M⦸󰔄X)( ≅ 󰄵M,X,󰔄XHom(Q(X,󰔄X),P(M⊘X,M⦸󰔄X)) ≅ 󰄵M,X,󰔄XHom(Q(X,󰔄X),󰄵Y,󰔄Y(Hom(Y,M⊘X)⇀(Hom(M⦸󰔄X,󰔄Y)⇀P(Y,󰔄Y)))( ≅ 󰄵M,X,󰔄X,Y,󰔄YHom(Q(X,󰔄X),Hom(Y,M⊘X)⇀(Hom(M⦸󰔄X,󰔄Y)⇀P(Y,󰔄Y))) ≅ 󰄵M,X,󰔄X,Y,󰔄YHom(Q(X,󰔄X)×Hom(Y,M⊘X)×Hom(M⦸󰔄X,󰔄Y),P(Y,󰔄Y)) ≅ 󰄵Y,󰔄YHom(󰄵M,X,󰔄X(Q(X,󰔄X)×Hom(Y,M⊘X)×Hom(M⦸󰔄X,󰔄Y)),P(Y,󰔄Y)( が成り立つ。 そこで、 Ψ󰒮: Prof(󰔄󰒚,󰒚) ⟶ Prof(󰔄󰒚,󰒚) Q ⟼ ❲ 󰒚∘×󰔄󰒚 ⟶ Set (Y,󰔄Y) ⟼ 󰄵M∈󰒢󰄵X∈󰒚󰄵󰔄X∈󰔄󰒚(Q(X,󰔄X)×Hom(Y,M⊘X)×Hom(M⦸󰔄X,󰔄Y))❲ とおくとこれは関手になり、 上式の最右辺は、 󰄵Y,󰔄YHom(Ψ󰒮Q(Y,󰔄Y),P(Y,󰔄Y)) と書ける。 これは Hom(Ψ󰒮Q,P) と同型だから、 以上によって、 HomProf(󰔄󰒚,󰒚)(Q,Φ󰒮P)≅HomProf(󰔄󰒚,󰒚)(Ψ󰒮Q,P) が示された。 これより、 Ψ󰒮 は Φ󰒮 の左随伴である。

これで、 Φ󰒮 の左随伴として、 Ψ󰒮: Prof(󰔄󰒚,󰒚) ⟶ Prof(󰔄󰒚,󰒚) Q ⟼ ❲ 󰒚∘×󰔄󰒚 ⟶ Set (Y,󰔄Y) ⟼ 󰄵M∈󰒢󰄵X∈󰒚󰄵󰔄X∈󰔄󰒚(Q(X,󰔄X)×Hom(Y,M⊘X)×Hom(M⦸󰔄X,󰔄Y))❲ が得られたわけだが、 Φ󰒮 の定義を Yoneda の補題を用いて展開して、 Φ󰒮: Prof(󰔄󰒚,󰒚) ⟶ Prof(󰔄󰒚,󰒚) P ⟼ ❲ 󰒚∘×󰔄󰒚 ⟶ Set (X,󰔄X) ⟼ 󰄵M∈󰒢󰄵Y∈󰒚󰄵󰔄Y∈󰔄󰒚(P(Y,󰔄Y)×Hom(M⊘X,Y)×Hom(󰔄Y,M⦸󰔄X))❲ と書くと、 綺麗に対応していることが見られる。

さて、 ここで以下の随伴モナドに関する一般論を思い出そう。

定理 5.11.

圏 󰒧 上のコモナド (Φ,δ,ε) に対し、 関手 Φ が左随伴関手 Ψ をもつとする。 このとき、

  • Ψ はモナドの構造 (Ψ,μ,η) をもつ。
  • コモナド (Φ,δ,ε) 上の余代数とモナド (Ψ,μ,η) 上の代数は 1 対 1 に対応し、 この対応は圏同値を与える。 すなわち、 (Φ,δ,ε) 上の余 Eilenberg–Moore 圏 󰒧Φ と (Ψ,μ,η) 上の Eilenberg–Moore 圏 󰒧Ψ は圏同値である。
証明.

最初の主張は Eilenberg–Moore†1 の命題 3.1 に記載がある。 次の主張も μ と η の構成を用いて計算することで確かめられる。

この定理から、 Tambara 加群がモナド代数としても書けることが分かり、 さらに任意のプロ関手から自由 Tambara 加群や余自由 Tambara 加群が作れることが分かる。

定理 5.12.

オプティック領域 󰒮:=(󰒚,󰔄󰒚,󰒢;⊘,⦸) に対し、 圏同値 Tamb(󰒮)≅Prof(󰔄󰒚,󰒚)Φ󰒮≅Prof(󰔄󰒚,󰒚)Ψ󰒮 が成立する。

証明.

定理 5.10 と定理 5.11 からすぐに従う。

定理 5.13.

オプティック領域 󰒮:=(󰒚,󰔄󰒚,󰒢;⊘,⦸) をとる。 忘却関手 U:Tamb(󰒮)→Prof(󰔄󰒚,󰒚) は左随伴と右随伴をともにもつ。 すなわち、 任意のプロ関手に対して、 それ上の自由 Tambara 加群と余自由 Tambara 加群がともに存在する。

証明.

コモナド理論の一般論から、 コモナド Φ󰒮 は関手 󰔃Φ󰒮:Prof(󰔄󰒚,󰒚)→Prof(󰔄󰒚,󰒚)Φ󰒮 を誘導し、 これは忘却関手の右随伴になる。 一方で、 定理 5.12 より Prof(󰔄󰒚,󰒚)Φ󰒮 は Tamb(󰒮) と圏同値だから、 この関手は 󰔃Φ󰒮:Prof(󰔄󰒚,󰒚)→Tamb(󰒮) と見なすこともでき、 忘却関手の右随伴を与える。

同様にして、 モナド Ψ󰒮 は関手 󰔃Ψ󰒮:Prof(󰔄󰒚,󰒚)→Prof(󰔄󰒚,󰒚)Ψ󰒮 を誘導し、 これを 󰔃Ψ󰒮:Prof(󰔄󰒚,󰒚)→Tamb(󰒮) と見なせば、 忘却関手の左随伴になる。

以上の結果は、 次のような可換図式としてまとめることができる。 ラベルのない矢印は忘却関手である。

Prof(󰔄󰒚,󰒚)Prof(󰔄󰒚,󰒚)Φ󰒮≅Tamb(󰒮)≅Prof(󰔄󰒚,󰒚)Ψ󰒮Prof(󰔄󰒚,󰒚)󰔃Φ󰒮Φ󰒮⊢Ψ󰒮󰔃Ψ󰒮⊢Φ󰒮Ψ󰒮

さて、 自由 Tambara 加群の存在を使うと、 オプティックの 2 つのエンコーディングが等価であることが示せる。

定理 5.14.

オプティック領域 󰒮:=(󰒚,󰔄󰒚,󰒢;⊘,⦸) をとる。 󰒚 の対象 S,A と 󰔄󰒚 の対象 󰔄S,󰔄A に対し、 POptic󰒮(S,󰔄S;A,󰔄A)≅COptic󰒮(S,󰔄S;A,󰔄A) が成立する。

証明.

(A,󰔄A) による表現可能プロ関手を HA󰔄A: 󰒚∘×󰔄󰒚 ⟶ Set (X,󰔄X) ⟼ Hom(X,A)×Hom(󰔄A,󰔄X) とおくと、 定理 5.13 などを用いて、 POptic󰒮(S,󰔄S;A,󰔄A) = 󰄵(P,ξ)∈Tamb(󰒮)Hom(P(A,󰔄A),P(S,󰔄S)) ≅ 󰄵(P,ξ)∈Tamb(󰒮)Hom(HomProf(󰔄󰒚,󰒚)(HA󰔄A,P),P(S,󰔄S)) ≅ 󰄵(P,ξ)∈Tamb(󰒮)Hom(HomTamb(󰒮)(󰔃Ψ󰒮HA󰔄A,(P,ξ)),P(S,󰔄S)) ≅ Ψ󰒮HA󰔄A(S,󰔄S) = 󰄵K,X,󰔄X(HA󰔄A(X,󰔄X)×Hom(S,K⊘X)×Hom(K⦸󰔄X,󰔄S)) = 󰄵K,X,󰔄X(Hom(X,A)×Hom(󰔄A,󰔄X)×Hom(S,K⊘X)×Hom(K⦸󰔄X,󰔄S)) ≅ 󰄵K(Hom(S,K⊘A)×Hom(K⦸󰔄A,󰔄S)) = COptic󰒮(S,󰔄S;A,󰔄A) が成り立つことが分かり、 定理が示された。

参考文献

  1. S. Eilenberg, J. Moore (1965) 「Adjoint functors and triples」 『Illinois Journal of Mathematics』 9:381–398
  2. M. Román (2020) 「Profunctor optics and traversals」 arXiv:2001.08045