PS

Lens

いわゆるgetter/setterの圏論による表現。

Associated (co)monad with an adjunction

Adjunctionからのmonad - PSより、adjunction:

  •  F \overset{\epsilon}{\underset{\eta}{\dashv}} U : \mathcal{D} \to \mathcal{C}

について

  •  (UF, \eta, U \epsilon F)

monadに、

  •  (FU, \epsilon, F \eta U)

はcomonadになる。

EM category for a (co)monad

Eilenberg-Moore adjunction - PSより、monad:

  •  (T: \mathcal{C} \to \mathcal{C}, \eta : 1 _ \mathcal{C} \Rightarrow T, \mu : T ^ 2 \Rightarrow T)

について、 (T, \eta, \mu)-algebraをobjectとするcategoryを

  •  \mathcal{C} ^ T

と書くのであった。同様にして、comonad:

  •  (G : \mathcal{C} \to \mathcal{C}, \epsilon : G \Rightarrow 1 _ \mathcal{C}, \delta : G \Rightarrow G ^ 2)

について、  (G, \epsilon, \delta)-coalgebraをobjectとするcategoryを

と書くことにする。

記法

以下、

  • cartesian closed category:  \mathcal{C}
  •  \mathcal{C}-object:  V

について・・・

View-operation adjunction

Slice category  \mathcal{C}/ _ V からのforgetful functor:

  •  \Sigma : \mathcal{C}/ _ V \to \mathcal{C}

とfunctor:

  •  \Delta : \mathcal{C} \to \mathcal{C}/ _ V
  •  \Delta _ 0(S) := \pi : V \times S \to V
  •  \Delta _ 1(f : S \to S') := 1 _ V \times f : V \times S \to V \times S'

について

  •  \Sigma \dashv \Delta

Cartesian closure adjunction (Curry adjunction)

  •  (\unicode{x2013}) \times V \overset{\epsilon}{\underset{\eta}{\dashv}} (\unicode{x2013}) ^ V

Curryingによるadjunctionのこと。

Costate(Store) comonad

上記のadjunctionからassociated comonad:

  •  \big( D := (\unicode{x2013}) ^ V \times V, \epsilon, ( \delta _ S := \eta _ {S ^ V} \times 1 _ V ) _ S \big)

を作れる。

命題

  •  (\mathcal{C}/ _ V) ^ {\Delta \Sigma} \cong D ^ {\mathcal{C}}

Lens

上記の同値なEM category(のいずれか)のobjectをlens、morphismをlens morphismという。

Lens laws

  •  \langle p, g \rangle : S \to S ^ V \times V in  D ^ {\mathcal{C}}

とすると、 D ^ {\mathcal{C}} の定義により

  •  \epsilon _ S \circ \langle p, g \rangle = 1 _ S  (get-put law)
  •  g ^ V \circ p = \pi ^ V \circ \eta _ S  (put-get law)
  •  p ^ V \circ p = \pi ^ V \circ \eta _ {S ^ V} \circ p  (put-put law)

特に  \mathcal{C} := \mathcal{Set} のとき、これらは

  •  p(s)(g(s)) = s
  •  g(p(s)(u) ) = u
  •  p(p(s)(u) )(v) = p(s)(v)

に対応する。*2

参考文献

*1:こちらもEilenberg-Moore categoryと言ってしまうらしい

*2:Monadで(co)algebraの満たすべき要件を表現している