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.

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},
}

Related

Dependent optics [lcc-0003]

Definition Simple Bimorphic Lens [lcc-0001]

Let \mathcal {C} be a Cartesian monoidal category. Then \mathsf {Lens}(\mathcal {C}) is the category whose objects are pairs \binom {X}{A} of objects in \mathcal {C}, where morphisms are defined by \operatorname {\mathrm {Hom}}\left (\binom {X}{A}, \binom {Y}{B}\right ) = \mathcal {C}(X,Y) \times \mathcal {C}(X \times B, A), and where composition is defined by (f^+: X \to Y, f^-: X \times B \to A) ; (g^+: Y \to Z, g^-: Y \times C \to B) \\= (f^+;g^+, (x,c) \mapsto f^-(x,g^-(f^+(x),c))) (The expression of the composite of the backwards passes in terms of elements is easily seen to correspond to a composite of maps between products in a generic Cartesian category)

Polynomial functors as lenses [lcc-0002]

Let \mathcal {C} be a locally Cartesian closed category. Recall the definition of polynomial functor. We will only be interested in the simple case of polynomial endofunctors, which means a polynomial is given simply by a morphism p: A \to X \in \mathcal {C}.

We think of the object p: A \to X as being an X-indexed family of objects, given by the "fibers" p^{-1}(\{x\}) = A_x. Then a transformation of polynomials (p: A \to X) \to (p': B \to Y) consists of a map f^+: X \to Y and a map f^-: B \times _Y X \to A over X. If \mathcal {C} = \mathsf {Set}, this backwards map amounts to a family of maps f^-_x: B_{f(x)} \to A_x

The problem of dependent optics is how to combine both the nondeterminism (or some more general form of effects) of optics with the dependent backwards pass of dependent lenses. The basic issue is that, given a nondeterministic forwards pass p: X \to Y, and an element x \in X, there is no particular element p(x) \in Y so that we can ask for a backwards map B_{p(x)} \to A_x.

The idea, then, is to demand that the forwards stochastic process generate not just an element y by also some residual m \in M which is compatible with the y - that is, there is an indexed family M_{xy}, and we generate a pair y,m \in M_{xy}, and then there is a family of backwards processes q: M_{xy} \otimes B_y \to A_x.

With a little bit of elaboration, this definitions works to produce what you might call coproduct optics or indexed optics - when the indexed object is a coproduct of "trivial" ones, (which is, of course, always the case for sets), we get a suitable definition.

With significantly more elaboration, we get what has been called fibre optics, which is about the widest possible generality for the above idea. It is not entirely clear that this captures everything someone might mean by "dependent optics" - in particular, the cases covered by the definition are forced to be somewhat "Markovesque", in the sense that there has to be a Cartesian subcategory in there.

To elaborate on this, in an ordinary optic, the backwards map M \otimes B \to A doesn't see "the Y part" of the forwards pass X \to M \otimes Y - in a Cartesian or Markov setting, of course, we could just copy the value in Y and pass that along to the residual, so that doesn't matter. But in the general monoidal case, optics might not be able to depend on "which y \in Y happened" (in a sense, this is the whole difficulty of dependent optics). Fibre optics only effectively cover cases where the information which the dependent types depend on can be copied at will.

Fibre Optics [lcc-0005]

Let \mathcal {I} have all finite limits, and equip it with the Cartesian monoidal structure. Let \mathcal {C},\mathcal {M},\mathcal {D} \to \mathcal {I} be bifibrations which have the Beck-Chevalley condition. Suppose \mathcal {M} is a monoidal bifibration in the sense of Framed bicategories and monoidal fibrations, and suppose further that \mathcal {M} acts on \mathcal {C} and \mathcal {D} in a way compatible with the fibrations.

Note that we are only asking for compatibility with the fibration, not with the bifibration - that is, we expect tensors of Cartesian lifts to be again Cartesian, but not that this is the case for coCartesian lifts.

Then the objects of the category of fibre optics, \mathsf {FibOptic}^\mathcal {I}_\mathcal {M}(\mathcal {C},\mathcal {D}), are tuples (I \in \mathcal {I}, X \in \mathcal {C}_I, A \in \mathcal {D}_I) The set of morphisms (I,X,A) \to (J,Y,B) is given by the scary-looking expression \int ^{M \in \mathcal {M}_{I \times J}} \mathcal {C}_\mathcal {I}(X, \pi _J^!(M \cdot \pi _J^*Y)) \times \mathcal {D}_\mathcal {I}(\pi _I^!(M \cdot \pi _J^*B), A)

Apart from the previously mentioned conceptual quibbles, the obvious complexity of the definition is probably the biggest downside to this notion (it's even worse than it looks, since the functors \pi ^*, \pi ^! are only defined up to isomorphism).

The flavor of the intended examples of fibre optics is given by the following construction on Markov categories:

[lcc-0006]

Let \mathcal {C} be a Markov category. We may define a category of "bundles", which we will denote \mathsf {Bun}(\mathcal {C}), as follows: its objects are deterministic maps X \to I \in \mathcal {C}_\mathrm {det}, and its morphisms are squares

where g, but not f, is required to be deterministic.

There is a forgetful functor \mathsf {Bun}(\mathcal {C}) \to \mathcal {C}_\mathrm {det} which takes X \to I to I. If \mathcal {C} itself is Cartesian, then this is just the codomain opfibration, and this thing will be a bifibration if and only if \mathcal {C} has pullbacks.

In the Markov case, it's not necessarily sufficient that \mathcal {C}_\mathrm {det} has pullbacks. What is required is, given a diagram of this form where all the maps are deterministic:

there is a bijection between (nondeterministic) maps X \to Y making the outer square commute, and maps X \to Y \times _J I making the triangle over I commute. This is true, for example, in \mathsf {FinStoch}, as can be readily verified, and it seems like it "should" be true based on an intuitive model of probability.

If we impose this condition, \mathsf {Bun}(\mathcal {C}) \to \mathcal {C}_\mathrm {det} becomes not only a bifibration, but a monoidal fibration, and a bifibration with the Beck-Chevalley condition. (The monoidal structure on \mathsf {Bun}(\mathcal {C}) simply being the obvious one). The fibration being monoidal follows from the fact that products of pullback diagrams are pullback diagrams, and the Beck-Chevalley condition holds because it holds for codomain fibrations, and all the morphisms involved in checking it are deterministic

Theorem Fibre Optics for Markov Bundles [lcc-0007]

Let \mathcal {C} be a Markov category, and consider the category of bundles in \mathcal {C}. Suppose \mathcal {C} satisfies the pullback condition for \mathsf {Bun}(\mathcal {C}) \to \mathcal {C}_\mathrm {det} to be a fibration

Now consider fibre optics applied to the self-action of the fibration \mathsf {Bun}(\mathcal {C}) \to \mathcal {C}_\mathrm {det}. Let us abbreviate \mathsf {FibOptic}^{\mathcal {C}_\mathrm {det}}_{\mathsf {Bun}(\mathcal {C})}(\mathsf {Bun}(\mathcal {C}),\mathsf {Bun}(\mathcal {C})) by merely \mathsf {FibOptic}(\mathcal {C}). Let us also abbreviate \mathsf {Bun}(\mathcal {C}) = \mathsf {Bun}, and write the fibers as usual as \mathsf {Bun}_I

  • Given two objects (I,X \to I, A \to I), (J, Y \to J, A \to J) of \mathsf {FibOptic}(\mathcal {C}), the set of morphisms can be written as \int ^{M \in \mathsf {Bun}_{I \times J}} \mathsf {Bun}_I(X, M \times _J Y) \times \mathsf {Bun}_I(M \times _J B, A)
  • Given an object (I, Y,B), this object is isomorphic to (Y, Y, B \times _I Y)
  • The set of maps into an object (Y,Y,B) of this form (out of I, X, A) is given by \int ^{M \in \mathsf {Bun}_{I \times Y}} \mathsf {Bun}_I(X,M) \times \mathsf {Bun}_I(M \times _J B, A).
  • In particular, \mathsf {FibOptic}(\mathcal {C}) is equivalent to the category where objects are deterministic morphisms A \to X \in \mathcal {C}, and the set of morphisms (A \to X) \to (B \to Y) is given by \int ^{M \in \mathsf {Bun}_{X \times Y}} \mathcal {C}_{/X}(X,M) \times \mathcal {C}_{/X}(M \times _Y B, A)
  • The set of maps (X, X, A \times X) \to (Y, Y, B \otimes Y) is in bijection with the set of simple optics \mathsf {Optic}(\mathcal {C})((X,A),(Y,B))

Proof

The first statement is simply rewriting using the fact that the pullback operations f^* are given by actual pullbacks in \mathcal {C}_\mathrm {det}, and so is the local tensor product on each fiber \mathsf {Bun}_I. We also suppress the pushforwards f_!, since they simply change the morphism to the base, which is implicit in this notation anyway. Do note that these pullbacks in \mathcal {C}_\mathrm {det} are not pullbacks in \mathsf {Bun}_I!

For the second statement, by definition the set of maps from an arbitrary test object into (Y,Y,Y \times _J B) is given by \int ^{M \in \mathsf {Bun}_{I \times Y}} \mathsf {Bun}_I(X, M \times _Y Y) \times \mathsf {Bun}_I(M \times _Y B \times _J Y, A) But clearly M \times _Y Y = M, and similarly M \times _Y B \times _J Y = M \times _J B, so we can write \int ^{M \in \mathsf {Bun}_{I \times Y}} \mathsf {Bun}_I(X, M) \times \mathsf {Bun}_I(M \times _J B, A) The claim is that this is in bijection with \int ^{M \in \mathsf {Bun}_{I \times J}} \mathsf {Bun}_I(X, M \times _J Y) \times \mathsf {Bun}_I(M \times _J B, A)

We construct a bijection. Given a tuple in the first set M, \phi : X \to M, \psi : M \times _J B \to A, we carry it to M, \phi ;(1_M,p_Y), \psi , by just postcomposing the structural map to Y with Y \to J. The map p_Y is the structural map M \to Y - we form M to M \times _J Y in the obvious way and compose it with \phi . \psi , we can just leave in place.

For the other direction, given a tuple (M, \phi : X \to M \times _J Y, \psi : M \times _J B \to A), we form the tuple (M \times _J Y, \phi , \pi ;\psi ) - here we use the obvious projection \pi : M \times _J Y \times _J B \to M \times _J B.

The functoriality of these constructions makes it easy to verify that they're well-defined. Let's verify they're inverses. In one case, I start with M over J (and I), and obtain M \times _J Y. There is an obvious projection map M\times _J Y \to M, and this witnesses the equivalence of the two optics in this case. In the other case, I start with M over Y, and obtain M \times _J Y again. In this case, it's the diagonal map M \to M \times _J Y which does it.

The third statement is, again, a straightforward rewriting. The fourth statement is just a simple rewriting of the third, plus the observation that, since every object is isomorphic to one of this form, the subcategory on those is equivalent.

For the fifth statement, note that the set of ordinary optics is the set \int ^{M \in \mathcal {C}} \mathcal {C}(X, M \otimes Y) \times \mathcal {C}(M \otimes B, A)\\ \cong \int ^{M \in \mathsf {Bun}_{* \times *}}\mathsf {Bun}_*(X, M \times Y) \times \mathsf {Bun}_*(M \times B, A)\\ \cong \mathsf {FibOptic}(\mathcal {C})((*,X,A),(*,Y,B)) \cong \mathsf {FibOptic}(\mathcal {C})((X,X,X \times A),(Y,Y,Y\times A)), where the last step uses the preceding

Coproducts in the category of lenses [coprods-lens-blogpost]

Introduction

The category of bimorphic lenses and its many generalizations has been widely studied and utilized in applied category theory. We will not give a review of the literature here, but see e.g. Riley's paper on "optics" (one of the many generalizations) Reference [riley-optics], which includes a decent overview.

Dispensing with a point of notation, we will denote objects of the category of lenses \binom {A}{X}, and morphisms \varphi : \binom {A}{X} \to \binom {B}{Y} as (\varphi ^+: X \to Y,\varphi ^- : X \times B \to A). Note that we write the *forwards* pass on the bottom of the tuple, breaking with the convention used by Riley and many others.

The category \mathsf {Lens}= \mathsf {Lens}(\mathsf {Set}) of lenses embeds into the category of polynomial functors \mathsf {Poly} and natural transformations as the full subcategory of functors of the form X \times (-)^A. Since \mathsf {Poly} admits all coproducts, and these are computed pointwise, one immediate consequence is that we have the coproducts \binom {A}{X} + \binom {A}{Y} = \binom {A}{X + Y} in \mathsf {Lens}. These seem to have been studied first by Hedges (Reference [hedges-morphisms-open-games]). (For a reference on \mathsf {Poly}, including this inclusion, see eg Spivak Reference [spivak-poly-abundant]. \mathsf {Poly} is another branch on the tree of generalizations of \mathsf {Lens}, studied extensively by Spivak and others).

Given the above, one might expect these to be all the coproducts of \mathsf {Lens} (up to isomorphism) - they are certainly the only ones preserved by this inclusion11 There is a quibble here, since \binom {A}{0} \cong \binom {B}{0} for any sets A,B, these being the initial objects of \mathsf {Lens}. This is of course the natural "nullary" version of the binary formula, but it also means that \binom {A}{0}+\binom {B}{X} = \binom {B}{X}, and that this coproduct is preserved by the inclusion into \mathsf {Poly}, even if A \not \cong B. . But this turns out not to be the case.

Let's begin with a worked example of the "exotic" coproducts. Note that I simply denote by n \in \mathbb {N} the set \{1, \dots n\} with n elements. In particular 0 is the empty set.

Example

In \mathsf {Lens}, \binom {0}{1} + \binom {1}{1} = \binom {0}{2}, with the coproduct inclusions having as their forwards pass the two distinct maps 1 \to 2, and the backwards passes in both cases being trivial.

To see this is a coproduct, consider the natural transformation

\mathsf {Lens}\left (\binom {0}{2},\binom {A}{X}\right ) \to \mathsf {Lens}\left (\binom {0}{1},\binom {A}{X}\right ) \times \mathsf {Lens}\left (\binom {1}{1},\binom {A}{X}\right )

In the case where A is nonempty, this is simply the map 0 \to 0, because there are no maps 2 \times A \to 0, and also no maps 1 \times A \to 0. Clearly 0 \to 0 is a bijection. On the other hand if A is empty, all the backwards passes are trivial, so we're just left with the map \mathsf {Set}(2,A) \to \mathsf {Set}(1,A) \times \mathsf {Set}(1,A), which is clearly a bijection. Hence this is a natural isomorphism, so we have a coproduct.

To see why this is not preserved by the inclusion \mathsf {Lens}\hookrightarrow \mathsf {Poly}, consider the polynomial y \mapsto y + 1 (this is the actual coproduct of the polynomials corresponding to these lenses). The inclusion maps from y = 1 \times y^1 and 1 = 1 \times y^0 into this polynomial should induce a map from 2 = 2 \times y^0, but of course there's no way to map into the y (unless we map the entire thing into the 1 component, but this clearly won't pull back to the inclusion map of y when we compose with the map y \to 2). The problem is that, where in the lens/monomial case, to have any maps at all the backwards set must be 0, making the whole backwards pass trivial, in the polynomial case we can have the backwards set be empty only when it's forced to be.

The coproducts in \mathsf {Lens}

Having seen the above, we may begin to lose hope of understanding the coproducts in \mathsf {Lens} at all. Fortunately the situation is not completely chaotic - in some sense, the preceding example is the *only* problem - all the coproducts in \mathsf {Lens} are either of the form \binom {A}{\coprod _i X_i} (up to isomorphism), or they are of the same form as the example.

Theorem

In \mathsf {Lens}= \mathsf {Lens}(\mathsf {Set}), a tuple of lenses \{\binom {A_i}{X_i} \overset {\varphi _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 all x \in X_i, the function \varphi _i(x, -): B \to A_i is a bijection.
  2. For at least one i, A_i is empty and X_i is nonempty. (The existence of any lens \binom {A_i}{X_i} \to \binom {B}{Y} then implies that B must be empty as well)

The first class of coproducts are the "good" ones - these are preserved by the functor from lenses to polynomial functors, and seem to capture the correct notion of "branching" for bidirectional systems. The other class, the "exotic" coproducts, are more mysterious.

We will begin the proof of this theorem with some preliminaries about lenses in a general (Cartesian) distributive category. While we can't obtain the preceding theorem in this generality (for reasons that will become clear later), it may be useful to know what can be said here.

Let us fix a (Cartesian) distributive category \mathcal {C} - that is, \mathcal {C} has finite products and coproducts, and the universal map \coprod _i A \times X_i \to A \times (\coprod _i X_i) is always an isomorphism. I will denote the initial object by 0.

Proposition

The functor \mathsf {Lens}(\mathcal {C}) \to \mathcal {C} which carries \binom {A}{X} to X and a lens (\varphi ^+, \varphi ^-) to its foward pass \varphi ^+ admits a right adjoint, given by X \mapsto \binom {0}{X}.

Proof

We simply have to verify \mathsf {Lens}(\mathcal {C})(\binom {A}{X},\binom {0}{Y}) = \mathcal {C}(X,Y). But this is trivial - the forwards pass of such a lens is clearly an element of the right-hand side, so it suffices to prove that there is always a unique choice of backwards pass. But the backwards pass is a map 0 \times X \to A, and by distributivity 0 \times X is initial. This concludes the proof.

Because left adjoints preserve (in particular) coproducts, we obtain the following:

Corollary

For a tuple \{\binom {A_i}{X_i} \overset {\varphi _i}{\to } \binom {B}{Y}\} to be a coproduct diagram, the forwards passes X_i \to Y must form a coproduct diagram in \mathcal {C}.

The following result, characterizing the "good" coproducts, was already essentially proven by Hedges in Reference [hedges-morphisms-open-games]22 Hedges states it only for \mathcal {C} = \mathsf {Set}, but his proof goes through unaltered for our case. He also only constructs a particular family of coproduct diagrams, but the ones considered here are just his composed with isomorphisms in \mathsf {Lens}, so there is really nothing serious going on , but I'll state it here and sketch a proof for completeness.

Proposition

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

Proof

\mathsf {Lens}(\mathcal {C})(\binom {A}{\coprod _i X_i},\binom {B}{Y}) = \mathcal {C}(\coprod _i X_i, B) \times \mathcal {C}((\coprod _i X_i) \times B, a) \cong \prod _i \left (\mathcal {C}(X_i, B) \times \mathcal {C}(X_i \times B, a)\right ),

using the universal property of coproducts and the distributivity. This is clearly the set of tuples of lenses \binom {A}{X_i} \to \binom {B}{Y}, and moreover precomposition with the inclusion maps clearly picks out the elements of the tuple, verifying the universal property of the coproduct.

Proposition

Let a tuple \{\binom {A_i}{X_i} \overset {\varphi _i}{\to } \binom {B}{\coprod _i X_i}\} be given, such that each \varphi _i^+: X_i \to \coprod _j X_j is the coproduct inclusion.

Given some object C \in \mathcal {C}, each \varphi _i^-: X_i \times B \to A_i determines a map (\varphi _i^-)^*: \mathcal {C}(X_i \times C, B) \to \mathcal {C}(X_i \times C, A_i) , given by (\varphi _i^-)^*\psi (x,c) = \varphi _i^-(x,\psi (x,c)). The tuple (\varphi _i) is a coproduct diagram if and only if, for all C, one of these conditions hold (not necessarily the same one for each C):

1. Each (\varphi _i^-)^* is a bijection.

2. For some i, the set \mathcal {C}(X_i \times C, A_i) is empty.

Proof

Note that each of the lenses \varphi _i factors as \binom {A_i}{X_i} \to \binom {B}{X_i} \to \binom {B}{\coprod X_i} = \coprod _i \binom {B}{X_i}, where the first map is (1_{X_i},\varphi _i^-), and the second map is the coproduct inclusion.

Hence the natural transformation

\alpha : \mathsf {Lens}(\mathcal {C})\left (\binom {B}{\coprod _i X_i},\binom {C}{Z}\right ) \to \prod _i \mathsf {Lens}(\mathcal {C})\left (\binom {A_i}{X_i},\binom {C}{Z}\right )

factors as

\mathsf {Lens}(\mathcal {C})\left (\binom {B}{\coprod _i X_i},\binom {C}{Z}\right ) \cong \prod _i\mathsf {Lens}(\mathcal {C})\left (\binom {B}{X_i},\binom {C}{Z}\right ) \to \prod _i\mathsf {Lens}(\mathcal {C})\left (\binom {A_i}{X_i},\binom {C}{Z}\right )

where the second map is the parallel product of the precomposition morphisms - \circ (1_{X_i},\varphi _i^-) for each i.

The tuple is a coproduct diagram if and only if this composite is a bijection, which is true if and only if this second map is a bijection.

A product of functions in \mathsf {Set} is a bijection if and only if each component map is a bijection, or one of the product sets in the target is empty (in which case the corresponding set in the domain must be empty as well for a map to exist, and so both products are empty).

We can rewrite the sets involved here as

\mathsf {Lens}(\mathcal {C})\left (\binom {B}{X_i},\binom {C}{Z}\right ) = \mathsf {Set}(X_i,Z) \times \mathsf {Set}(X_i \times C, B),

and

\mathsf {Lens}(\mathcal {C})\left (\binom {A_i}{X_i},\binom {C}{Z}\right ) = \mathsf {Set}(X_i,Z) \times \mathsf {Set}(X_i \times C, A_i).

This is simply the definition of \mathsf {Lens}

Under this expansion the map - \circ (1_{X_i},\varphi _i^-) carries a lens (\psi ^+, \psi ^-) to (\psi ^+, (\varphi _i^-)^*\psi ^-). So - \circ (1_{X_i},\varphi _i^-)i is a bijection if and only if we have \mathsf {Set}(X_i,Z) empty or (\varphi _i^-)^* a bijection (or both).

Now, clearly if condition 1. holds, we've just seen that each - \circ (1_{X_i},\varphi _i^-) becomes a bijection, and so our map \alpha is a bijection. If condition 2. holds, then \mathsf {Lens}(\mathcal {C})\left (\binom {A_i}{X_i},\binom {C}{Z}\right ) is empty, and so we again have a (trivial) bijection.

So if at least one of the conditions hold for each C, \alpha is always a bijection, and so we have a coproduct.

On the other hand, suppose there is some C so that neither condition holds. Take Z = \coprod _i X_i. Then none of the mapping sets \mathsf {Set}(X_i, Z = \coprod _i X_i) are empty, so the only way for - \circ (1_{X_i},\varphi _i^-) to be a bijection is for (\varphi _i^-)^* to be a bijection, but by hypothesis this fails for at least one i. By assumption none of the sets \mathsf {Set}(X_i \times C, A_i) are empty, and none of the sets \mathsf {Set}(X_i, Z) are empty either, so the product is not empty - hence the map \alpha is not a bijection in this case.

We can now return to the main theorem. The following argument is somewhat clunky and ad hoc. The main point is that we can characterize the cases where \mathsf {Set}(U,V) is empty, namely only when V is empty and U is not. In a general category, this can be much more complicated, and there does not seem to be any completely general method. This means we don't know which possible C we need to deal with when understanding when the backwards pass is a bijection, which makes it seemingly impossible to give a general classification of the coproducts by this method.

(The second point is that it's easy to understand when the maps between hom-spaces are bijections in \mathsf {Set} - we have a somewhat clunky argument but it's pretty straightforward and it can probably be done in a more conceptual way, if one took the time to find it).

We can replace Y with the coproduct \coprod _i X_i, and each forwards pass \varphi _i^+ with the inclusion, without loss of generality (if we are not in this situation up to isomorphism, we don't have a coproduct by the above)

Proof Proof of the theorem

It's clear that the first condition of the theorem implies that \mathsf {Set}(X_i \times C, B) \to \mathsf {Set}(X_i \times C, A_i) is a bijection always, and so we have a coproduct. As for the second condition, suppose X_i is nonempty and A_i is empty. Then for nonempty C, the set \mathsf {Set}(X_i \times C, A_i) is clearly empty, fulfilling the second condition of the lemma, whereas for empty C, the map \mathsf {Set}(X_i \times C, B) \to \mathsf {Set}(X_i \times C, A_i) is a map between two singletons (since X_i \times C is empty), and hence a bijection.

This proves that if one of the two conditions hold, we have a coproduct. To see the other direction, suppose neither condition holds. If the second condition doesn't hold, then there is always a map X_i \to A_i, and hence the set \mathsf {Set}(X_i \times C, A_i) is never empty, so according to the lemma, it suffices to show that for some i and some C, the map (\varphi _i^-)^*: \mathsf {Set}(X_i \times C, B) \to \mathsf {Set}(X_i \times C, A_i) is not a bijection.

Since the first condition doesn't hold, let j, x' \in X_j be such that the map \varphi ^-_j(x',-): B \to A_j is not a bijection. Suppose first it's not surjective and let a' be something not in the image.

Take C = *. Then the constant function - \mapsto a' : X_j \times * \to A_j is clearly not in the image of (\varphi _j^-)^*, since that would require, for some \psi , \varphi _j^-(x,\psi (x,*)) = a' for all x, and in particular for x = x', but that's a contradiction.

On the other hand suppose it's not injective, and that \varphi _j^-(x',b_0) = \varphi _j^-(x',b_1) for some b_0,b_1 \in B. Now take C = B and consider a function \psi : X_j \times B \to B, defined by \psi (x',b_0) = b_1, and \psi (x,b) = b for all other pairs (x,b). Now \varphi _j^-(x',\psi (x',b_0)) = \varphi _j^-(x',b_1) = \varphi _j^-(x',b_0). And for all other x or b, clearly \varphi _j^-(x,\psi (x,b)) = \varphi _j^-(x,b). Hence (\varphi _j^-)^*\psi = (\varphi _j^-)*(\pi _B: X_j \times B \to B) (\pi _B being the projection). But \psi \neq \pi _B, so (\varphi _j^-)^* is not injective in this case. This concludes the proof.

The forwards part of this proof almost works for any distributive category \mathcal {C} with a *strict* initial object (meaning the only maps X \to 0 are isomorphisms, i.e X has to be another initial object). The trouble is that X_i \times C can be initial even when neither X_i nor C is, meaning even when A_i is initial and X_i isn't, the nonemptyness of \mathsf {Set}(X_i \times C, A_i) does not imply that C is initial, meaning that we don't automatically get that all the (\varphi _i^-)^* maps are bijections. A simple example of this is something like \mathcal {C} = \mathsf {Set}^k for some natural number k > 1. Then as long as we have C^{(n)} empty *or* X_i^{(n)} empty for each n = 1 \dots k, their product is empty.

A more general class of example with the same flavor is \mathcal {C} = Sh(X) the category of sheaves on a topological space. Then again as long as the supports of C and X_i are disjoint, their product is empty.

It may be possible to develop a generalization of the theorem, or at least of the forwards part of the theorem, using considerations like these to control the sets of morphisms.