日記 (2021 年 10 月 10 日)
7 月 7 日と 10 月 9 日で、 それぞれレンズの van Laarhoven エンコーディングとプロ関手エンコーディングについて触れた。
今回は、 レンズのコエンドを用いた表現方法について触れる。
概念の定義にコエンドを用いるが、 その後で集合としての具体的な表示も行うので、 コエンドを知らなくても読めるようにはしたつもりである。
コエンドの基本については Loregian2 を参照すると良い。
さて、 少々天下り的ではあるが、 次のような集合を定義する。
定義 3.1
有限積をもつ圏 をとる。
対象 S,S,A,A に対し、
Lens(S,S;A,A):=K∈(Hom(S,K×A)×Hom(K×A,S))
とおく。
この元 γ をコエンドレンズcoend lens と呼び、 γ:(S,S)→(A,A) で表す。
このコエンドは具体的に以下のように表すことができる。
命題 3.2
有限積をもつ圏 をとる。
対象 S,S,A,A に対し、
Lens(S,S;A,A)= K∈(Hom(S,K×A)×Hom(K×A,S)) ≈
が成り立つ。
ただし、 上記の ≈ とは、 任意の射 l:S→K×A, r:K×A→S, k:K→K に対し、
((k×idA)∘l,r)≈(l,r∘(k×idA))
が成り立つような最小の同値関係とする。
上記の命題により、 有限積をもつ圏の対象 S,S,A,A に対し、 各コエンドレンズ γ:(S,S)→(A,A) は、 ある対象 K を用いた 2 つの射 l:S→K×A, r:K×A→S によって代表される同値類として表せる。
そこで、 このときに γ のことを ⟨l,r⟩K と書くことにする。
上記の命題中の同値関係の定義により、 任意の射 l:S→K×A, r:K×A→S, k:K→K に対し、
⟨(k×idA)∘l,r⟩K=⟨l,r∘(k×idA)⟩K
が成り立つ。
コエンドレンズに対しても合成が定義でき、 これによって圏を成す。
定義 3.3
有限積をもつ圏 をとる。
コエンドレンズ ⟨l,r⟩K:(S,S)→(A,A), ⟨l,r⟩L:(A,A)→(B,B) に対し、
l := ❲SK×AK×L×Blid×l❲ r := ❲K×L×BK×ASid×rr❲
と定める。
これによって得られる素朴レンズ ⟨l,r⟩K×L:(S,S)→(B,B) を ⟨l,r⟩K と ⟨l,r⟩L の合成composition という。
定義 3.4
有限積をもつ圏 をとる。
圏 CLens() を、
- CLens() の対象は、 の 2 つの対象の組 (S,S) の全体とする。
- CLens() の 2 つの対象 (S,S),(A,A) の間の射は、 コエンドレンズ γ:(S,S)→(A,A) の全体とする。
すなわち、
HomCLens()((S,S),(A,A))=K∈(Hom(S,K×A)×Hom(K×A,S))
である。
- CLens() の射の合成は、 上記で定めたコエンドレンズの合成とする。
によって定義する。
最後に、 コエンドレンズがこれまでに出てきたレンズと等価であることを示そう。
定理 3.5
有限積をもつ圏 をとる。
対象 S,S,A,A に対し、 全単射
HomCLens()((S,S),(A,A))≅HomNLens()((S,S),(A,A))
が存在する。
証明
コエンドに関する Yoneda の補題を用いると、
HomCLens()((S,S),(A,A)) = K∈(Hom(S,K×A)×Hom(K×A,S)) ≅ K∈(Hom(S,K)×Hom(S,A)×Hom(K×A,S)) ≅ Hom(S,A)×Hom(S×A,S) ≅ HomNLens()((S,S),(A,A))
が得られる。
この全単射による元の対応は、 以下のように具体的に書くこともできる。
コエンドレンズ ⟨l,r⟩K:(S,S)→(A,A) をとる。
fstKA:K×A→K と sndKA:K×A→A をそれぞれ積の射影とすると、
g := ❲SK×AAlsndKA❲ p := ❲S×AK×A×AK×ASl×idfstKA×idr❲
によって、 素朴レンズ (g,p):(S,S)→(A,A) が得られる。
逆に素朴レンズ (g,p):(S,S)→(A,A) からは、
l := (idS,g):S→S×A r := p:S×A→S
とおくことで、 コエンドレンズ ⟨l,r⟩S:(S,S)→(A,A) が得られる。
この対応が上の全単射を与えている。
定理 3.6
カルテシアン閉圏 をとる。
圏同型
CLens()≅PLens()≅LLens()≅NLens()
が成立する。
証明
圏同型 PLens()≅LLens()≅NLens() はすでに定理 2.10 で示されているので、 定理 3.5 の全単射が合成を保つことを示せば良い。
以上で、 レンズの主要な表現方法を紹介し終えた。
ここで軽くまとめておこう。
1 つ目の素朴レンズは、 ゲッターとセッターの組だと素朴に見なしたときのレンズの表現方法で、 数式で書けば
HomNLens()((S,S),(A,A))=Hom(S,A)×Hom(S×A,S)
の元であった。
2 つ目の van Laarhoven レンズは、 強度付きの自己関手で添字付けられた写像群としてレンズを表現したもので、
HomLLens()((S,S),(A,A))=Hom[StrEnd(),Set](Hom(A,-A),Hom(S,-S))
の元として表したものであった。
これは Haskell のレンズライブラリで用いられているエンコーディング方法である。
3 つ目のプロ関手レンズは、 強度付きの自己関手の代わりに Tambra 構造をもった自己プロ関手を考え、 それで添字付けられた写像群としてレンズを表現したもので、
HomPLens()((S,S),(A,A))=Hom[Tamb(),Set](-(A,A),-(S,S))
の元であった。
こちらは Purecript のレンズライブラリで用いられている。
van Laarhoven レンズとプロ関手レンズに共通する特徴として、 レンズの合成が本当の写像の合成として実現できるという点がある。
4 つ目のコエンドレンズとは、 特定のコエンドの元としてレンズを表現するもので、
HomCLens()((S,S),(A,A))=K∈(Hom(S,K×A)×Hom(K×A,S))
の元であった。
そして、 これらの表現方法は全て等価なのであった。
すなわち、 上記の 4 つの集合の間には全単射が存在し、 さらにその全単射はそれぞれの表現方法について定義された合成を保存する。
レンズのこれら 4 つの表現方法のうち、 プロ関手レンズとコエンドレンズはモノイダル圏の作用を用いた一般化が可能で、 一般化したものはオプティックと呼ばれている。
レンズの一般化がオプティックなので、 オプティックの具体例の 1 つがレンズということになるが、 オプティックからは他にもデータの取得や操作に使えるたくさんの有用な具体例が出てくることが知られている。
逆に、 一見別々のものに見えるそのような具体例が、 全てオプティックという一般概念にまとめられるのは、 理論としても美しく驚くべきことである。
次回は、 オプティックの定義をし、 その具体例をいくつか紹介しようと思う。
参考文献
- B. Clarke et al (2020) 「Profunctor optics, a categorical update」 arXiv:2001.07488
- F. Loregian (2021) 『(Co)end Calculus』 Cambridge University Press
- K. Riley (2018) 「Categories of optics」 arXiv:1809.00738