Theorem [lcc-000A]

In \mathsf {Lens} = \mathsf {Lens}(\mathsf {Set}), a tuple of lenses \binom {A_i}{X_i} \overset {\phi _i}{\to } \binom {B}{Y} is a coproduct diagram if and only if the forwards passes X_i \to Y form a coproduct diagram in \mathsf {Set} and one of these conditions hold:

  1. For all i, and for each x \in X_i, the function \phi ^-(x, -): B \to A_i is a bijection
  2. For at least one i, A_i = \emptyset and X_i is nonempty. (In this case the existence of any lens \phi _i: \binom {A_i}{X_i} \to \binom {B}{Y} implies that B is also empty)

Proof

We divide the proofs into a few lemmata, which may be of some independent interest. It is unfortunate that this result only holds for \mathsf {Lens}(\mathsf {Set}), and not for \mathsf {Lens}(\mathcal {C}) with \mathcal {C} a general Cartesian category. The statement as given is not true in general, but hopefully the proof will give an idea of how these things work in a general Cartesian category.

Lemma [lcc-000B]

Fix a (Cartesian) distributive category \mathcal {C}. Denote the initial object by 0.

The functor \mathsf {Lens}(\mathcal {C}) \to \mathcal {C} which maps \binom {A}{X} \mapsto X and carries each lens to its forward pass is left adjoint. Its right adjoint is given by X \mapsto \binom {0}{X}. In particular, it preserves coproducts.

Theorem [lcc-000C]

Let X_i \in \mathcal {C} be a collection of objects with coproduct \sum _i X_i. Let A \in \mathcal {C}. Then the family of lenses \binom {A}{X_i} \to \binom {A}{\sum _i X_i} given by the inclusions as the forwards pass, and the projection X_i \times A \to A as the backwards pass, is a coproduct diagram.

This is essentially due to Hedges, in Morphisms of Open Games

Lemma [lcc-000E]

Let \binom {A_i}{X_i} \overset {\phi }{\to } \binom {B}{\coprod _j X_j} be a tuple of lenses, where the forwards pass \phi ^+_i in each case is given by the coproduct inclusion X_i \to \coprod _j X_j.

Given an object C \in \mathcal {C}, each backwards pass \phi _i^+: X_i \times B \to A determines a map (\phi _i^-)^*: \mathcal {C}(X_i \times C, B) \to \mathcal {C}(X_i \times C, A), given on elements by (\phi _i^-)^*(\psi )(x,c) = \phi ^-_i(x,\psi (x,c)). The tuple (\phi _i) is a coproduct diagram if, for all C, one of these conditions hold (note the order of the quantifiers, here!)

  1. Each (\phi ^-_i)^* is a bijection
  2. For some i, the set \mathcal {C}(X_i \times C, A_i) is empty.

Proof

Note that \binom {B}{\sum _i X_i} \cong \sum _i \binom {B}{X_i}, and each of the \phi _i factors as \binom {A_i}{X_i} \to \binom {B}{X_i} \to \sum _i \binom {B}{X_i}.

Hence if \binom {C}{Z} is a test object, the natural transformation \mathsf {Lens}(\mathcal {C})(\binom {B}{\sum _i X_i}, \binom {C}{Z}) \to \prod _i \mathsf {Lens}(\mathcal {C})(\binom {A_i}{X_i},\binom {C}{Z}) is isomorphically the morphism \prod _i \mathsf {Lens}(\mathcal {C})(\binom {B}{X_i}, \binom {C}{Z}) \to \prod _i \mathsf {Lens}(\mathcal {C})(\binom {A_i}{X_i},\binom {C}{Z}) given by the product of the precomposition maps.

The tuple is a coproduct diagram if and only if this is a bijection. A product of maps in \mathsf {Set} is a bijection if and only if either each individual map is a bijection, or one of the sets in the codomain product is empty (in which case both products must be empty).

We can rewrite the individual sets as follows: \mathsf {Lens}(\mathcal {C})(\binom {B}{X_i},\binom {C}{Z}) = \mathcal {C}(X_i, Z) \times \mathcal {C}(X_i \times C, B) \mathsf {Lens}(\mathcal {C})(\binom {A_i}{X_i},\binom {C}{Z}) = \mathcal {C}(X_i, Z) \times \mathcal {C}(X_i \times C, A_i) by definition of \mathsf {Lens}. The precomposition maps then carry (\psi ^+, \psi ^-) to (\psi ^+, (\phi _i^-)^*\psi ^-).

So clearly, if condition 1 holds---if each (\phi _i^-)^* is a bijection---each of these maps is a bijection, as desired. If condition 2 holds, both products are empty. This establishes the forwards direction: if, for each C, one of the conditions hold, the natural transformation is a bijection, and so we have a coproduct.

On the other hand, let C be so that neither condition holds. Take Z = \sum _i X_i.

By assumption all of the sets \mathcal {C}(X_i \times C, A_i) are nonempty, and so are the sets \mathcal {C}(X_i, Z). Hence neither product is empty, so each map must be a bijection. But by assumption there is some i where this is not the case.

Now we are ready to prove the theorem.

Without loss of generality, we can assume we are in the situation of Lemma [lcc-000E], where the forwards passes are given by coproduct inclusions.

Now we will use the two following observations:

  1. If C is empty, the map (\phi _i^-)^*: \mathsf {Set}(X_i \times C, B) \to \mathsf {Set}(X_i \times C, A_i) is always a bijection, since it is a map between two singleton sets. If C is nonempty, it is a bijection only if the lens (1_{X_i},\phi ^-_i): \binom {A_i}{X_i} \to \binom {B}{X_i} is an isomorphism, i.e only if each of the maps \phi ^-_i(x,-): B \to A_i are bijections
  2. The set \mathcal {C}(X_i \times C, A_i) is empty if and only if X_i, C are nonempty, and A_i is empty

Verifying the first statement is routine but somewhat tiresome. The second statement is trivial.

Hence, if (\phi _i) form a coproduct diagram, by taking C any nonempty set, we find that condition 1. of Lemma [lcc-000E] implies condition 1. of this theorem. And condition 2., implies there is some i with X_i nonempty and A_i empty, so in either case, we have what we wanted. Conversely, if either of the conditions of this theorem hold, they imply the corresponding condition of Lemma [lcc-000E], and so we have the desired equivalence.

References

Reference Morphisms of Open Games [hedges-morphisms-open-games]

  • April 4, 2021
  • Jules Hedges 
@article{hedges-morphisms-open-games,
  title = {Morphisms of open games},
  url = {http://arxiv.org/abs/1711.07059},
  abstract = {We define a notion of morphisms between open games, exploiting a surprising connection between lenses in computer science and compositional game theory. This extends the more intuitively obvious definition of globular morphisms as mappings between strategy profiles that preserve best responses, and hence in particular preserve Nash equilibria. We construct a symmetric monoidal double category in which the horizontal 1-cells are open games, vertical 1-morphisms are lenses, and 2cells are morphisms of open games. States (morphisms out of the monoidal unit) in the vertical category give a flexible solution concept that includes both Nash and subgame perfect equilibria. Products in the vertical category give an external choice operator that is reminiscent of products in game semantics, and is useful in practical examples. We illustrate the above two features with a simple worked example from microeconomics, the market entry game.},
  journaltitle = {{arXiv}:1711.07059 [cs, math]},
  author = {Hedges, Jules},
  urldate = {2021-04-04},
  date = {2017-11-23},
  langid = {english},
  eprinttype = {arxiv},
  eprint = {1711.07059},
  keywords = {Mathematics - Category Theory, Computer Science - Computer Science and Game Theory},
}

Context

Wild coproducts in the category of simple lenses [lcc-0008]

This note contains material previously posted on my blog, here

The category of simple (bimorphic) lenses (let's just say over \mathsf {Set}, for now) has a monoidal structure, given by \binom {A}{X} \otimes \binom {B}{Y} = \binom {A \times B}{X \times Y}, which is neither Cartesian nor coCartesian. It also has Cartesian products, given by \binom {A}{X} \times \binom {B}{Y} = \binom {A + B}{X \times Y}. However, it does not in general have coproducts.

In the category of containers/dependent set lenses/polynomials, which is an extension of \mathsf {Lens}(\mathsf {Set}), coproducts do exist. If we think of an element of this category as a base set X and an indexed family of fiber sets A_x, x \in X, then the coproduct just takes the disjoint union of the bases and combines the two indexed families.

The polynomials in the image of \mathsf {Lens}(\mathsf {Set}) are those where the family is constant - B_x = B for all x - and so the problem with \mathsf {Lens}(\mathsf {Set}) when it comes to coproducts is that, if A \ncong B, computing the coproduct of \binom {A}{X} and \binom {B}{Y} in polynomials takes us out of lenses. And indeed in the case A = B, these coproducts do exist in \mathsf {Lens}(\mathsf {Set}) and are given by \binom {A}{X + Y}.

This defect is part of what motivated the development of Dependent optics.

For a while, it was thought that coproducts of this form were the only coproducts in \mathsf {Lens}(\mathsf {Set}), and that therefore the category of dependent lenses could be constructed as the universal completion under coproducts of \mathsf {Lens}(\mathsf {Set}) preserving the existing coproducts. This would then provide a universal property for a category of dependent optics as well.

Unfortunately, this is not true. \mathsf {Lens}(\mathsf {Set}) has the following "wild" coproduct as well:

Example [lcc-0009]

In \mathsf {Lens}{\mathsf {Set}} \binom {0}{1} + \binom {1}{1} = \binom {0}{2}. To see this, let \binom {A}{X} be a test object, and consider \operatorname {\mathrm {Hom}}(\binom {0}{1}, \binom {A}{X}) \times \operatorname {\mathrm {Hom}}(\binom {1}{1},\binom {A}{X}). If A is empty, the backwards pass is trivial in both cases, and so this just amounts to choosing two points of X. If A is nonempty, it is impossible to define the backwards pass in the first map (or the forwards pass, if X is also empty), and so this product is empty. On the other hand, \operatorname {\mathrm {Hom}}(\binom {0}{2}, \binom {A}{X}) is exactly the same - if A is empty, it is X^2, and if A is nonempty, it is the empty set. Hence this is a coproduct.

We have the following theorem characterizing all the coproducts in \mathsf {Lens}(\mathsf {Set})

Theorem [lcc-000A]

In \mathsf {Lens} = \mathsf {Lens}(\mathsf {Set}), a tuple of lenses \binom {A_i}{X_i} \overset {\phi _i}{\to } \binom {B}{Y} is a coproduct diagram if and only if the forwards passes X_i \to Y form a coproduct diagram in \mathsf {Set} and one of these conditions hold:

  1. For all i, and for each x \in X_i, the function \phi ^-(x, -): B \to A_i is a bijection
  2. For at least one i, A_i = \emptyset and X_i is nonempty. (In this case the existence of any lens \phi _i: \binom {A_i}{X_i} \to \binom {B}{Y} implies that B is also empty)

Proof

We divide the proofs into a few lemmata, which may be of some independent interest. It is unfortunate that this result only holds for \mathsf {Lens}(\mathsf {Set}), and not for \mathsf {Lens}(\mathcal {C}) with \mathcal {C} a general Cartesian category. The statement as given is not true in general, but hopefully the proof will give an idea of how these things work in a general Cartesian category.

Lemma [lcc-000B]

Fix a (Cartesian) distributive category \mathcal {C}. Denote the initial object by 0.

The functor \mathsf {Lens}(\mathcal {C}) \to \mathcal {C} which maps \binom {A}{X} \mapsto X and carries each lens to its forward pass is left adjoint. Its right adjoint is given by X \mapsto \binom {0}{X}. In particular, it preserves coproducts.

Theorem [lcc-000C]

Let X_i \in \mathcal {C} be a collection of objects with coproduct \sum _i X_i. Let A \in \mathcal {C}. Then the family of lenses \binom {A}{X_i} \to \binom {A}{\sum _i X_i} given by the inclusions as the forwards pass, and the projection X_i \times A \to A as the backwards pass, is a coproduct diagram.

This is essentially due to Hedges, in Morphisms of Open Games

Lemma [lcc-000E]

Let \binom {A_i}{X_i} \overset {\phi }{\to } \binom {B}{\coprod _j X_j} be a tuple of lenses, where the forwards pass \phi ^+_i in each case is given by the coproduct inclusion X_i \to \coprod _j X_j.

Given an object C \in \mathcal {C}, each backwards pass \phi _i^+: X_i \times B \to A determines a map (\phi _i^-)^*: \mathcal {C}(X_i \times C, B) \to \mathcal {C}(X_i \times C, A), given on elements by (\phi _i^-)^*(\psi )(x,c) = \phi ^-_i(x,\psi (x,c)). The tuple (\phi _i) is a coproduct diagram if, for all C, one of these conditions hold (note the order of the quantifiers, here!)

  1. Each (\phi ^-_i)^* is a bijection
  2. For some i, the set \mathcal {C}(X_i \times C, A_i) is empty.

Proof

Note that \binom {B}{\sum _i X_i} \cong \sum _i \binom {B}{X_i}, and each of the \phi _i factors as \binom {A_i}{X_i} \to \binom {B}{X_i} \to \sum _i \binom {B}{X_i}.

Hence if \binom {C}{Z} is a test object, the natural transformation \mathsf {Lens}(\mathcal {C})(\binom {B}{\sum _i X_i}, \binom {C}{Z}) \to \prod _i \mathsf {Lens}(\mathcal {C})(\binom {A_i}{X_i},\binom {C}{Z}) is isomorphically the morphism \prod _i \mathsf {Lens}(\mathcal {C})(\binom {B}{X_i}, \binom {C}{Z}) \to \prod _i \mathsf {Lens}(\mathcal {C})(\binom {A_i}{X_i},\binom {C}{Z}) given by the product of the precomposition maps.

The tuple is a coproduct diagram if and only if this is a bijection. A product of maps in \mathsf {Set} is a bijection if and only if either each individual map is a bijection, or one of the sets in the codomain product is empty (in which case both products must be empty).

We can rewrite the individual sets as follows: \mathsf {Lens}(\mathcal {C})(\binom {B}{X_i},\binom {C}{Z}) = \mathcal {C}(X_i, Z) \times \mathcal {C}(X_i \times C, B) \mathsf {Lens}(\mathcal {C})(\binom {A_i}{X_i},\binom {C}{Z}) = \mathcal {C}(X_i, Z) \times \mathcal {C}(X_i \times C, A_i) by definition of \mathsf {Lens}. The precomposition maps then carry (\psi ^+, \psi ^-) to (\psi ^+, (\phi _i^-)^*\psi ^-).

So clearly, if condition 1 holds---if each (\phi _i^-)^* is a bijection---each of these maps is a bijection, as desired. If condition 2 holds, both products are empty. This establishes the forwards direction: if, for each C, one of the conditions hold, the natural transformation is a bijection, and so we have a coproduct.

On the other hand, let C be so that neither condition holds. Take Z = \sum _i X_i.

By assumption all of the sets \mathcal {C}(X_i \times C, A_i) are nonempty, and so are the sets \mathcal {C}(X_i, Z). Hence neither product is empty, so each map must be a bijection. But by assumption there is some i where this is not the case.

Now we are ready to prove the theorem.

Without loss of generality, we can assume we are in the situation of Lemma [lcc-000E], where the forwards passes are given by coproduct inclusions.

Now we will use the two following observations:

  1. If C is empty, the map (\phi _i^-)^*: \mathsf {Set}(X_i \times C, B) \to \mathsf {Set}(X_i \times C, A_i) is always a bijection, since it is a map between two singleton sets. If C is nonempty, it is a bijection only if the lens (1_{X_i},\phi ^-_i): \binom {A_i}{X_i} \to \binom {B}{X_i} is an isomorphism, i.e only if each of the maps \phi ^-_i(x,-): B \to A_i are bijections
  2. The set \mathcal {C}(X_i \times C, A_i) is empty if and only if X_i, C are nonempty, and A_i is empty

Verifying the first statement is routine but somewhat tiresome. The second statement is trivial.

Hence, if (\phi _i) form a coproduct diagram, by taking C any nonempty set, we find that condition 1. of Lemma [lcc-000E] implies condition 1. of this theorem. And condition 2., implies there is some i with X_i nonempty and A_i empty, so in either case, we have what we wanted. Conversely, if either of the conditions of this theorem hold, they imply the corresponding condition of Lemma [lcc-000E], and so we have the desired equivalence.

Related

Lemma [lcc-000E]

Let \binom {A_i}{X_i} \overset {\phi }{\to } \binom {B}{\coprod _j X_j} be a tuple of lenses, where the forwards pass \phi ^+_i in each case is given by the coproduct inclusion X_i \to \coprod _j X_j.

Given an object C \in \mathcal {C}, each backwards pass \phi _i^+: X_i \times B \to A determines a map (\phi _i^-)^*: \mathcal {C}(X_i \times C, B) \to \mathcal {C}(X_i \times C, A), given on elements by (\phi _i^-)^*(\psi )(x,c) = \phi ^-_i(x,\psi (x,c)). The tuple (\phi _i) is a coproduct diagram if, for all C, one of these conditions hold (note the order of the quantifiers, here!)

  1. Each (\phi ^-_i)^* is a bijection
  2. For some i, the set \mathcal {C}(X_i \times C, A_i) is empty.

Proof

Note that \binom {B}{\sum _i X_i} \cong \sum _i \binom {B}{X_i}, and each of the \phi _i factors as \binom {A_i}{X_i} \to \binom {B}{X_i} \to \sum _i \binom {B}{X_i}.

Hence if \binom {C}{Z} is a test object, the natural transformation \mathsf {Lens}(\mathcal {C})(\binom {B}{\sum _i X_i}, \binom {C}{Z}) \to \prod _i \mathsf {Lens}(\mathcal {C})(\binom {A_i}{X_i},\binom {C}{Z}) is isomorphically the morphism \prod _i \mathsf {Lens}(\mathcal {C})(\binom {B}{X_i}, \binom {C}{Z}) \to \prod _i \mathsf {Lens}(\mathcal {C})(\binom {A_i}{X_i},\binom {C}{Z}) given by the product of the precomposition maps.

The tuple is a coproduct diagram if and only if this is a bijection. A product of maps in \mathsf {Set} is a bijection if and only if either each individual map is a bijection, or one of the sets in the codomain product is empty (in which case both products must be empty).

We can rewrite the individual sets as follows: \mathsf {Lens}(\mathcal {C})(\binom {B}{X_i},\binom {C}{Z}) = \mathcal {C}(X_i, Z) \times \mathcal {C}(X_i \times C, B) \mathsf {Lens}(\mathcal {C})(\binom {A_i}{X_i},\binom {C}{Z}) = \mathcal {C}(X_i, Z) \times \mathcal {C}(X_i \times C, A_i) by definition of \mathsf {Lens}. The precomposition maps then carry (\psi ^+, \psi ^-) to (\psi ^+, (\phi _i^-)^*\psi ^-).

So clearly, if condition 1 holds---if each (\phi _i^-)^* is a bijection---each of these maps is a bijection, as desired. If condition 2 holds, both products are empty. This establishes the forwards direction: if, for each C, one of the conditions hold, the natural transformation is a bijection, and so we have a coproduct.

On the other hand, let C be so that neither condition holds. Take Z = \sum _i X_i.

By assumption all of the sets \mathcal {C}(X_i \times C, A_i) are nonempty, and so are the sets \mathcal {C}(X_i, Z). Hence neither product is empty, so each map must be a bijection. But by assumption there is some i where this is not the case.