Proposition [efr-M19V]

If \mathcal {C} is Cartesian monoidal, \mathsf {Optic}(\mathcal {C})\left ({A \choose X},{B \choose Y}\right ) \cong \mathcal {C}(X,Y) \times \mathcal {C}(X \times B,A)

Proof

\int ^M \mathcal {C}(X, M \times Y) \times \mathcal {C}(M \times B,A) \cong \int ^M \mathcal {C}(X,Y) \times \mathcal {C}(X,M) \times \mathcal {C}(M \times B,A) \cong \mathcal {C}(X,Y) \times \mathcal {C}(X \times B,A).

Here we use a general fact about coends, that \int ^M \mathcal {C}(X,M) \times F(M) \cong F(X)---this has been called the ninja Yoneda lemma, see Reference [fosco-coend-calculus].

References

Reference (Co)end Calculus [fosco-coend-calculus]

Abstract

  • June 30, 2021
  • Fosco Loregian

The language of ends and (co)ends provides a natural and general way of expressing many phenomena in category theory, in the abstract and in applications. Yet although category-theoretic methods are now widely used by mathematicians, since (co)ends lie just beyond a first course in category theory, they are typically only used by category theorists, for whom they are something of a secret weapon. This book is the first systematic treatment of the theory of (co)ends. Aimed at a wide audience, it presents the (co)end calculus as a powerful tool to clarify and simplify definitions and results in category theory and export them for use in diverse areas of mathematics and computer science. It is organized as an easy-to-cite reference manual, and will be of interest to category theorists and users of category theory alike. 

 @book
{fosco-coend-calculus, edition={1}, title={(Co)end Calculus}, rights={https://www.cambridge.org/core/terms}, ISBN={978-1-108-77865-7}, url={https://www.cambridge.org/core/product/identifier/9781108778657/type/book}, DOI={10.1017/9781108778657}, abstractNote={The language of ends and (co)ends provides a natural and general way of expressing many phenomena in category theory, in the abstract and in applications. Yet although category-theoretic methods are now widely used by mathematicians, since (co)ends lie just beyond a first course in category theory, they are typically only used by category theorists, for whom they are something of a secret weapon. This book is the first systematic treatment of the theory of (co)ends. Aimed at a wide audience, it presents the (co)end calculus as a powerful tool to clarify and simplify definitions and results in category theory and export them for use in diverse areas of mathematics and computer science. It is organized as an easy-to-cite reference manual, and will be of interest to category theorists and users of category theory alike.}, publisher={Cambridge University Press}, author={Loregian, Fosco}, year={2021}, month={Jun} }

Context

Optics and Lenses [efr-ZCTD]

We have already given somewhat of an account of lenses, optics, and their applications in the introduction. We briefly review the theory here, especially to normalize the notation and definitions. The best general source for this material is still Reference [riley-optics].

The definition of optic relies on the notion of coend, which we briefly recall, see Reference [fosco-coend-calculus] for a textbook account. If F: \mathcal {I}^\mathrm {op} \times \mathcal {I} \to \mathcal {C} is a functor, the coend \int ^{i \in I} F(i,i) is defined as the initial object receiving a map f_i : F(i,i) \to \int ^{i \in I} F(i,i) for each i \in I, so that for each \phi : i \to j, the square

commutes.

If \mathcal {C} has enough colimits, we may express the coend as the coequalizer of the diagram \coprod _{f : i \to j \in \mathcal {I}} F(i,j) \rightrightarrows \coprod _{i} F(i,i), where the two maps are given on each component by F(i,f): F(i,j) \to F(i,i) and F(f,j) : F(i,j) \to F(j,j), respectively. (This is Remark 1.2.4 in Reference [fosco-coend-calculus]). Note that in particular this implies that if \mathcal {C} has all colimits, then it also has all coends.

Definition Optic [efr-MMQZ]

Let \mathcal {M} be a monoidal category which acts on two categories \mathcal {C}, \mathcal {D}. Then the category of optics \mathsf {Optic}_\mathcal {M}(\mathcal {C},\mathcal {D}) has

  1. Objects pairs {A \in \mathcal {D} \choose X \in \mathcal {C}}
  2. The set of morphisms {A \choose X} \to {B \choose Y} given by the coend \int ^{M \in \mathcal {M}} \mathcal {C}(X, M \cdot Y) \times \mathcal {D}(M \cdot B,A)
  3. Given two optics with representatives (M,f: X \to M \cdot Y,g : M \cdot B \to A), (N, f': Y \to N \cdot Z, g': N \cdot C \to B), their composite is given by (M \otimes N, (1_M \cdot f')f, g (1_M \cdot g')), where we omit coherence morphisms.

When \mathcal {C} is a monoidal category acting on itself by tensor, we write \mathsf {Optic}_\mathcal {C}(\mathcal {C},\mathcal {C}) =: \mathsf {Optic}(\mathcal {C})

Note that if \mathcal {M},\mathcal {C},\mathcal {D} are symmetric monoidal and these actions are symmetric, \mathsf {Optic}_\mathcal {M}(\mathcal {C},\mathcal {D}) inherits a symmetric monoidal structure given by {A \choose X} \otimes {B \choose Y} = {A \otimes B \choose X \otimes Y}. (Also given a braiding one can induce a non-symmetric monoidal structure, but this almost never comes up).

Remark On notation [efr-CRYH]

Objects and morphisms in the category of optics have two parts---one going "forwards", in the same direction as the optic, and one going "backwards". In Reference [riley-optics] the objects are written (X,A), where X is the forwards part. Hedges' work on open games used the binomial notation \binom {X}{A}, but wrote the forwards part on top.

To make the connection to fibrations more natural, we instead write the forwards part on the bottom, {A \choose X}. It is the backwards part which depends on the forwards part, hence the forwards part is the base of the fibration (when one exists)---and every part of the language of fibrations is built around a mental model where the base is at the bottom and the fibers are over it (including the word "base"). When reading the references, this may cause some confusion, but hopefully this can be overcome.

While we're at it, let us note that when talking about optics we will freely use terms like "the forwards part" "the backwards object" and so on---the meaning of this should now be clear. Of course, once we get to cooptics/charts, this would be more than a little confusing, since in that case both components are in the same direction. In those cases we will speak of either the primary (forwards) part or the secondary (backwards) part, or use the language of fibrations and speak of the map or object "in the base" and "in the fiber".

As noted above, the coend \int ^M \mathcal {C}(X, M \cdot Y) \times \mathcal {D}(M \cdot B, A) consists of triples (M, f: X \to M \cdot Y, g: M \cdot B \to A) up to the equivalence relation which, for every \phi : M \to M', f: X \to M \cdot Y, g: M' \cdot B \to A, identifies the two tuples (M', (\phi \cdot 1_Y) f, g) and (M, f, g (\phi \cdot 1_B)). Note that this relation is not assumed to be inherently an equivalence relation---one takes the transitive-symmetric closure as usual.

We call this relation the sliding relation (because we slide the map \phi from the backwards part to the forwards part).

Remark [efr-50T5]

Suppose \mathcal {M}, \mathcal {C}, \mathcal {D} are small categories. Then the coend defining \mathsf {Optic}_\mathcal {M}(\mathcal {C},\mathcal {D})\left ( {A \choose X}, {B \choose Y} \right ) is a small colimit of small sets, hence again small. Since clearly the set of objects \operatorname {\mathbf {ob}} \mathcal {C} \times \operatorname {\mathbf {ob}} \mathcal {D} is small, \mathsf {Optic}_\mathcal {M}(\mathcal {C},\mathcal {D}) is again a small category.

However, if \mathcal {M},\mathcal {D},\mathcal {C} are merely assumed to be locally small, we can not guarantee the same is true of \mathsf {Optic}_\mathcal {M}(\mathcal {C},\mathcal {D}), since the hom-sets are now defined by a coend/colimit with large indexing category. However, in many special cases, it can still be seen to be locally small, such as in the Cartesian case (where \mathsf {Lens}(\mathcal {C}) is clearly locally small).

In this thesis, we will not delve further into this subtlety, simply working inside some universe where all our categories are small.

Of course, we can also let the arrows in \mathcal {D} go in the same direction as \mathcal {C}. This does not seem to have played any role in the literature, but we will give this a name, as it is a useful example to have in mind for Markov fibrations (where we will construct our dependent optics, conceptually, as a fiberwise opposite)

Definition Co-Optics [efr-G0YN]

Given \mathcal {M} acting on \mathcal {C}, \mathcal {D}, the category of co-optics, \mathsf {coOptic}_\mathcal {M}(\mathcal {C},\mathcal {D}) has objects pair {A \in \mathcal {D} \choose X \in \mathcal {C}}, and morphisms given by the coend \int ^M \mathcal {C}(X, M \cdot Y) \times \mathcal {D}(M \cdot A, B)

Remark [efr-J0WW]

For any monoidal category \mathcal {C}, \mathsf {Optic}_\mathcal {C}\left ({A \choose X}, {I \choose I}\right ) = \mathcal {C}(X,A). One way to think of an optic {A \choose X} \leftrightarrows {B \choose Y} is as a string diagram X \to A, but which has a hole with space for a morphism B \to Y. One inserts such a morphism by composing the optic with the optic {B \choose Y} \leftrightarrows {I \choose I} representing it. This idea of "open diagrams" has been developed in much more detail by Román, Reference [roman-optics-coend].

Proposition [efr-UNIN]

Suppose \mathcal {M} is semicartesian---in other words, that I \in \mathcal {M} is terminal. Then there is a functor \mathsf {Optic}_\mathcal {M}(\mathcal {C},\mathcal {D}) \to \mathcal {C}, which takes a {A \choose X} to X, and pair \langle f: X \to M \cdot Y, g \rangle to the composite X \to M \cdot Y \to I \cdot Y \cong Y.

In the case of \mathsf {Optic}(\mathcal {M}), the map \mathsf {Optic}(\mathcal {M})({I \choose I}, {A \choose X}) \to \mathcal {M}(I,X) is a bijection.

The fact that in \mathsf {Optic}(\mathcal {M}), states (maps from the monoidal unit) on {A \choose X} are given by states on X, while costates are given by maps X \to A plays an important role in the use of optics to describe open games. See § [efr-GFG0] for more on this.

Let us say a few things about lenses.

Proposition [efr-M19V]

If \mathcal {C} is Cartesian monoidal, \mathsf {Optic}(\mathcal {C})\left ({A \choose X},{B \choose Y}\right ) \cong \mathcal {C}(X,Y) \times \mathcal {C}(X \times B,A)

Proof

\int ^M \mathcal {C}(X, M \times Y) \times \mathcal {C}(M \times B,A) \cong \int ^M \mathcal {C}(X,Y) \times \mathcal {C}(X,M) \times \mathcal {C}(M \times B,A) \cong \mathcal {C}(X,Y) \times \mathcal {C}(X \times B,A).

Here we use a general fact about coends, that \int ^M \mathcal {C}(X,M) \times F(M) \cong F(X)---this has been called the ninja Yoneda lemma, see Reference [fosco-coend-calculus].

In this case we sometimes write \mathsf {Lens}(\mathcal {C}) for the category \mathsf {Optic}(\mathcal {C}). We have the following fact:

Proposition [efr-2793]

The functor {A \choose X} \mapsto X, \mathsf {Lens}(\mathcal {C}) \to \mathcal {C}, is a fibration. The fiber \mathsf {Lens}(\mathcal {C})_X has the following description:

  1. Its objects are the objects of \mathcal {C}.
  2. A map A \to B \in \mathsf {Lens}(\mathcal {C})_X is a map X \times B \to A \in \mathcal {C}.
  3. The composite of X \times B \to A, X \times C \to B is given by composing the two into X \times X \times C \to A, then using the diagonal.
  4. Given f: X \to Y, the pullback functor \mathsf {Lens}(\mathcal {C})_Y \to \mathsf {Lens}(\mathcal {C})_X is given by precomposing by f.

Proposition [efr-VTPS]

If \mathcal {C} moreover admits pullbacks, there is a fibred functor \mathsf {Lens}(\mathcal {C})^\mathrm {fop} \to \mathcal {C}^\to \to \mathcal {C}, which carries an object {A \choose X} to X \times A\xrightarrow {\pi _X} X, and a morphism f:X \times A \to B to the map X \times A \xrightarrow {\langle \pi _X,F \rangle } X \times B over X. This is fully faithful.

This is the first way to see the maps of (\mathcal {C}^\to )^\mathrm {fop} as dependent lenses---they receive the category of lenses as a full subcategory.

Remark [efr-TZ0P]

The squares

are pullbacks in any category with products, even if it does not admit pullbacks in general. It follows that the full subcategory of \mathcal {C}^\to spanned by objects of this form is always a fibration over \mathcal {C}, which is isomorphic to \mathsf {coOptic}(\mathcal {C})---the fiberwise dual is isomorphic to \mathsf {Lens}(\mathcal {C}).

Backlinks

Example [efr-8B5X]

The functor \mathsf {Optic}(\mathsf {BorelStoch}) \to \mathsf {BorelStoch} is not a Markov prefibration, although its pullback over \mathsf {BorelStoch}_\mathrm {det} is a Grothendieck fibration.

To see this, first consider the deterministic pullback. An optic \binom {A}{X} \to \binom {B}{Y} with deterministic base can be identified with a map X \otimes B \to A (and the base deterministic map X \to Y). To see this, first observe that the subset of \mathsf {BorelStoch}(X, Y \otimes M) with the marginal X \to Y deterministic is in bijection with \mathsf {BorelStoch}_\mathrm {det}(X,Y) \times \mathsf {BorelStoch}(X,M), since \mathsf {BorelStoch} is positive. Hence we can calculate \int ^M \mathsf {BorelStoch}_\mathrm {det}(X,Y) \times \mathsf {BorelStoch}(X,M) \times \mathsf {BorelStoch}(M \otimes B, A) \cong \mathsf {BorelStoch}_\mathrm {det}(X,Y) \times \mathsf {BorelStoch}(X \times B, A), using the ninja yoneda lemma as in Proposition [efr-M19V]. Hence this part is a fibration with the fiber over X being the coKleisli category of the X \times - monad, and the pullback functors given by reindexing these parametrized maps. The Cartesian lift of a map X \to Y at \binom {B}{Y} is given by the optic \binom {B}{X} \to \binom {B}{Y} with unit residual and identity backwards component.

Now, let g: I \to \mathbb {R} denote the standard Gaussian distribution, let f: \mathbb {R} \otimes \mathbb {R} \to \mathbb {R} be the function given by f(x,y) = 0 if x=y and y otherwise, and consider the two optics \binom {\mathbb {R}}{*} \to \binom {\mathbb {R}}{\mathbb {R}} given by (I, g: I \to \mathbb {R}, 1_\mathbb {R}: \mathbb {R} \to \mathbb {R}), (\mathbb {R}, \mathrm {copy}_\mathbb {R} g : I \to \mathbb {R} \otimes \mathbb {R}, f: \mathbb {R} \otimes \mathbb {R} \to \mathbb {R}) (where we recall that the first argument is the residual). They cannot be equal, as postcomposition with the optic \binom {\mathbb {R}}{\mathbb {R}} \to \binom {*}{*} given by the identity \mathbb {R} \to \mathbb {R} yields, for the former, the standard Gaussian g: I \to \mathbb {R}, and for the latter, the constant zero map. But postcomposition with the projection \binom {\mathbb {R}}{\mathbb {R}} \to \binom {\mathbb {R}}{*} does give the same optic (the identity), because, for every fixed y \in \mathbb {R}, when x is normally distributed, f(x,y) = y with probability one. Hence the unique lifting of Cartesian maps over Cartesian maps cannot hold.