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.

Context

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.

Backlinks

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.