lens

lens

• definition
  • a lens
  • $$\begin{pmatrix} f^{\#} \\ f \end{pmatrix} : \begin{pmatrix} A^{-} \\ A^{+} \end{pmatrix} \leftrightarrows \begin{pmatrix} B^{-} \\ B^{+} \end{pmatrix}$$
  • in a cartesian category $\mathcal{C}$ consists of
    • a passforward map $f: A^{+} \to B^{+}$
      • sending information downstream
    • a passback map $f^{\#}: A^{+} \times B^{-} \to A^{-}$
      • sending information back upstream
      • it allows to use the value in $A^{+}$, used by the downstreaming, to calculate how to pass information back upstream
• compose: lenses compose
  • given
    • $$\begin{pmatrix} f^{\#} \\ f \end{pmatrix} : \begin{pmatrix} A^{-} \\ A^{+} \end{pmatrix} \leftrightarrows \begin{pmatrix} B^{-} \\ B^{+} \end{pmatrix}$$
    • $$\begin{pmatrix} g^{\#} \\ g \end{pmatrix} : \begin{pmatrix} B^{-} \\ B^{+} \end{pmatrix} \leftrightarrows \begin{pmatrix} C^{-} \\ C^{+} \end{pmatrix}$$
    • we define their composite $\begin{pmatrix}g^{\#} \\ g\end{pmatrix} \circ \begin{pmatrix}f^{\#} \\ f\end{pmatrix}$, with
      • passforward given by $g \circ f$
      • passback given by
        • $$(a^{+}, c^{-}) \mapsto f^{\#}\left( a^{+}, g^{\#}(f(a^{+}), c^{-}) \right)$$
        • failed to execute js (detail: String("InternalError: stack overflow")) (a^{+}, c^{-}) \mapsto \underbrace{ f^{\#}\left( a^{+}, \underbrace{ g^{\#}(\underbrace{ f(a^{+}) }_{ b^{+} }, c^{-}) }_{ b^{-} } \right) }_{ a^{-} }

category of lenses $\mathbf{Lens}_{\mathbf{\mathcal{C}}}$

• let $\mathcal{C}$ be a cartesian category, then the category $\mathbf{Lens}_{\mathbf{\mathcal{C}}}$ has:
• objects: pairs $\begin{pmatrix}A^{-}\\A^{+}\end{pmatrix}$ of objects in $\mathcal{C}$, called arenas
• morphisms: the lenses
  • $$\begin{pmatrix} f^{\#} \\ f \end{pmatrix} : \begin{pmatrix} A^{-} \\ A^{+} \end{pmatrix} \leftrightarrows \begin{pmatrix} B^{-} \\ B^{+} \end{pmatrix}$$
• identity lens
  • $$\begin{pmatrix} \pi_{2} \\ id \end{pmatrix} : \begin{pmatrix} A^{-} \\ A^{+} \end{pmatrix} \leftrightarrows \begin{pmatrix} A^{-} \\ A^{+} \end{pmatrix}$$
  • where $\pi_{2}: A^{+} \times A^{-} \to A^{-}$ is the projection
• the composition is giving by lens composition
• it’s named for its morphisms (lenses) rather than objects (arenas)
  • the category of charts, has arenas as objects but the morphisms are not lenses
  • double category $\mathbf{Arena}^{\mathcal{C}}$, combining the category of lenses and category of charts, is named after its objects

Proposition: Functoriality of $\mathbf{Lens}$

• Every cartesian functor $F: \mathcal{C} \to \mathcal{D}$ induces a functor $\begin{pmatrix}F \\ F\end{pmatrix}: \mathbf{Lens_{\mathcal{C}}} \to \mathbf{Lens_{\mathcal{D}}}$, given by
  • $$\begin{pmatrix} F \\ F \end{pmatrix} \begin{pmatrix} f^{\#} \\ f \end{pmatrix} : \begin{pmatrix} F f^{\#} \circ \mu^{-1} \\ F f \end{pmatrix}$$
  • where $\mu = (F \pi_{1}, F \pi_{2}): F(X \times Y) \overset{ \sim }{ \to } FX \times FY$ is the isomorphism witnessing that $F$ preserves products

Parallel product $\otimes$

• put two arenas in parallel
  • $\begin{pmatrix}A_{1} \\ B_{1}\end{pmatrix}$ and $\begin{pmatrix}A_{2} \\ B_{2}\end{pmatrix}$
  • we just take their product in our cartesian category $\mathcal{C}$
  • $$\begin{pmatrix}A_{1} \\ B_{1}\end{pmatrix} \otimes\begin{pmatrix}A_{2} \\ B_{2}\end{pmatrix} := \begin{pmatrix}A_{1} \times A_{2} \\ B_{1} \times B_{2} \end{pmatrix}$$
• parallel product for morphisms in $\mathbf{Lens}$
  • given
    • $$\begin{pmatrix} f^{\#} \\ f \end{pmatrix} : \begin{pmatrix} A_{1} \\ B_{1} \end{pmatrix} \leftrightarrows \begin{pmatrix} C_{1} \\ D_{1} \end{pmatrix}$$
    • $$\begin{pmatrix} g^{\#} \\ g \end{pmatrix} : \begin{pmatrix} A_{2} \\ B_{2} \end{pmatrix} \leftrightarrows \begin{pmatrix} C_{2} \\ D_{2} \end{pmatrix}$$
    • their parallel product is defined by
    • $$\begin{pmatrix}f_{\#} \\ f\end{pmatrix} \otimes \begin{pmatrix}g_{\#} \\ g\end{pmatrix} := \begin{pmatrix}A_{1} \times A_{2} \\ B_{1} \times B_{2} \end{pmatrix} \leftrightarrows \begin{pmatrix}C_{1} \times C_{2} \\ D_{1} \times D_{2} \end{pmatrix}$$
  • it has
    • passforward $f \times g$
    • passback
      • $((b_{1}, b_{2}), (c_{1}, c_{2})) \mapsto (f^{\#}(b_{1}, c_{1}), g^{\#}(b_{2}, c_{2}))$
      • in terms of morphism, this is
      • $(B_1\times B_2)\times(C_1\times C_2)\overset{\sim}{\rightarrow}(B_1\times C_1)\times(B_2\times C_2)\overset{f^\#\times g^\#}{\longrightarrow}A_1\times A_2$
  • together with $\begin{pmatrix}1 \\ 1\end{pmatrix}$, this gives $\mathbf{Lens}_{\mathcal{C}}$ the structure of a monoidal category
• Proposition
  • for cartesian functor $F: \mathcal{C} \to \mathcal{D}$, the induced functor $\begin{pmatrix}F \\ F\end{pmatrix}: \mathbf{Lens_{\mathcal{C}}} \to \mathbf{Lens_{\mathcal{D}}}$
  • preserves the monidal product $\otimes$, ie, it’s strong monidal with respect to the parallel product
  • reference: 1.3.2.4 of Categorical System Theory

related

• cartesian category
• Categorical System Theory