Proposition [efr-W3B5]

The functor \mathsf {Optic}(\mathsf {BorelStoch}) \to \mathsf {SLens}(\mathsf {BorelStoch}^\to |_\mathrm {det}) is fully faithful.

We have just seen that this is full. Note that we have previously seen that optics with a deterministic base are in fact in bijection with parametrized maps, and so this is bijective on maps with deterministic base. In particular, it suffices to prove that two optics \binom {A}{X} \to \binom {B}{Y} with the same (not necessarily deterministic) base map X \to Y agree as long as, for every map X \times Y \to B \times S, the composite map X \to A \times S is the same.

Note that by taking conditionals we may restrict to the case of two optics with residual X \times Y and which have the same forwards component (given by the pairing of the identity and the map X \to Y). Without loss of generality, take X=*. Denote by \mu : * \to Y the measure on Y. Let the backwards components be f,g: Y \times B \to A. To prove these two optics agree, it suffices to exhibit a subset Y' \subset Y so that the measure \mu (Y') = 1 and so that f(y',b) = g(y',b) for all y' \in Y'.

Take S = Y \times B, and consider maps Y \to B \times Y \times B given by copying some s: Y \to B. Then the composite map is * \to Y \times B \times A given by Y having the distribution \mu , the conditional of B given Y being s, and the conditional of A given Y,B being either f or g

First, suppose given some s:Y \to B, so that in the induced joint measure on Y \times B, the probability that f \neq g is strictly greater than zero. Note that in the composite distribution on Y \times B \times A, the conditional distribution of A given Y,B is almost surely equal to the backwards part of the optic. Hence if such an s exists, f,g must give different joint measures, since their conditional distributions are different with positive probability.

Hence, if the two optics have the same composite with all maps, in particular for all s: Y \to B, the probability that f,g differ is zero. Note that all measures on Y \times B with marginal given by \mu arise in this way. Let D \subset Y \times B be the (measurable) subset where f \neq g, and let \bar {Y} denote Y equipped with the completion of its \sigma -algebra with respect to \mu .

Note that the image \pi _Y(D) is measurable in \bar {Y}, and there exists a measurable section \pi _Y(D) \to D (the former is the measurable projection theorem, and the latter is a consequence of Von Neumann's selection theorem, see Reference [srivastava-borelsets] 5.5.8). Defining a map \bar {Y} \to B by the value of this section inside \pi _Y(D), and choosing an arbitrary fixed b_0 \in B outside it, we get a measurable function. Integrating this with respect to the completion of \mu , we get a measure on \bar {Y} \times B where the measure of D is \mu (\pi _Y(D)) = \inf _{\pi _Y(D) \subseteq K, K \mathrm {measurable}} \mu (K). Clearly if this is zero, we can choose K with measure zero containing the image, in which case we are done. But if it is positive, we can restrict this measure to the \sigma -algebra of Y \times B to get a measure with marginal \mu where D has positive probability, proving the two optics are distinct. This concludes the proof.