Proposition [efr-10CM]

Suppose given a square

in \widetilde {\mathsf {\mathbb Span}}(\mathcal {D})^\mathrm {lens} (or \widetilde {\mathsf {\mathbb Span}}(\mathcal {D})^\mathrm {chart}) Suppose further the underlying square in \mathcal {C} is deterministic. Then:

  1. If there exists a filling decorated span 2-cell, the image in \mathsf {\mathbb Arena}(\mathcal {D}|_\mathrm {det}) commutes.
  2. If M_1 is the carrier of \phi _1 and the left leg M_1 \to X_1 is an isomorphism, then this implication is an equivalence.

Proof

Given a stochastic chart carried by X \leftarrow M \to Y, so that X \to Y is deterministic, recall that we can first pull back to the equalizer M' \hookrightarrow M of the two maps M \to X \to Y, M \to Y, then along the prescribed section X \to M'. Note that this gives a 2-cell from this canonical representative with carrier X to the initial representative.

Given two such cells, we get a square

But as part of the square surrounding the 2-cell, there is given a map X_1 \to X_2, which must make this square commute. The functoriality of base change (pulling back the map \phi _2) proves this bottom map is again a 2-cell.

But the property for this map to be a 2-cell is exactly the property for this square to be a commutative square in \mathsf {\mathbb Arena}{\mathcal {D}|_\mathrm {det}}. This proves both parts of the statement.

Context

Double categories of stochastic charts and lenses [efr-SIE7]

To construct the double category \mathsf {\mathbb Arena}(\mathcal {A}) of charts and lenses for an ordinary fibration \mathcal {A} \to \mathcal {C}, one can use the following procedure:

  1. Form the square double category \mathcal {A}^\to \rightrightarrows \mathcal {A}
  2. Take the fiberwise opposite of these objects: (\mathcal {A}^\to )^\mathrm {fop} \rightrightarrows \mathcal {A}^\mathrm {fop}.
  3. Observe that fiberwise opposite preserves pullbacks, and hence this is again a double category.

Here we used the following result: If \mathcal {D} \to \mathcal {C} is a Grothendieck fibration and \mathcal {A} is any category, then \mathcal {D}^\mathcal {A} \to \mathcal {C}^\mathcal {A} is again a fibration (which classifies the lax limits of the composite \mathcal {A}^\mathrm {op} \to \mathcal {C}^\mathrm {op} \to \mathsf {Cat}), and a natural transformation is Cartesian iff it is levelwise Cartesian. It would be neat to obtain a similar result for Markov fibrations.

The first problem with this is that \mathcal {C}^\mathcal {A} does not generally inherit a Markov structure from \mathcal {C}. As we noted when we introduced diagram Markov categories, one has to consider the category \mathsf {Fun}(\mathcal {A},\mathcal {C}) of deterministic diagrams instead.

First, we will see that this indeed works for Markov prefibrations. This implies that (-)^\mathcal {A} lifts from fibrations to stochastic modules.

Proposition [efr-6G7N]

Let \mathcal {D} \to \mathcal {C} be a Markov prefibration. Recall that by \mathcal {C}^\to we denote the category of deterministic arrows in \mathcal {C}. Let \mathsf {Ar}(\mathcal {C}) denote the ordinary arrow category. Let now \mathcal {D}^\to denote the category \mathsf {Ar}(\mathcal {D}) \times _{\mathsf {Ar}(\mathcal {C})} \mathcal {C}^\to consisting of those arrows in \mathcal {D} which lie over a deterministic base (but again, where the morphisms consist of commutative squares whose other sides do not necessarily have deterministic bases). Then \mathcal {D}^\to \to \mathcal {C}^\to is a Markov prefibration.

This yields a functor \mathsf {MarkPreFib}(\mathcal {C}) \to \mathsf {MarkPreFib}(\mathcal {C}^\to ), so that (\mathcal {D}^\to )|_\mathrm {det} = (\mathcal {D}|_\mathrm {det})^\to . This equation induces a natural transformation \overline {(\mathcal {D}_0^\to )}|_\mathrm {det} \to (\overline {\mathcal {D}_0}|_\mathrm {det})^\to , which in turns gives a lift of (-)^\to to the category of stochastic module fibrations, where the induced algebra structure acts pointwise.

Proof

Noting that \mathcal {C}^\to is a Markov category with the "pointwise" structure, and the deterministic maps consist precisely of the pointwise deterministic maps, clearly \mathcal {D}^\to |_\mathrm {det} = \mathcal {D}|_\mathrm {det}^\to , and fibrations are stable under the formation of arrow categories, with Cartesian maps formed pointwise.

It is not trivial that this is a prefibration, because given a triangle in \mathcal {C}_\mathrm {det}^\to ---a "prism"---and a Cartesian lifting, we only know that the maps "at the ends" are Cartesian, not the maps between the triangles. Therefore we can not immediately apply the unique lifting property to say that the square between the induced lifts \bar {Y_i}_{X_i} \to \bar {Y_i}_{Z_i} commute, given some map \bar {Y}_0 \to \bar {Y}_1 over Y_0 \to Y_1. However, by taking the pullback on both sides (and noting that pullbacks are functorial,) we can factor this square into two which live entirely over a deterministic base, and where the Cartesian property therefore imply commutativity.

We have already argued that this commutes with restriction to the deterministic part. The natural transformation is induced for completely abstract reasons, by applying (-)^\to to the unit to obtain a map \mathcal {D}_0^\to \to (\overline {\mathcal {D}_0}|_\mathrm {det})^\to = (\overline {\mathcal {D}_0}^\to )|_\mathrm {det}, which by the universal property of \overline {(-)} induces the desired map \overline {(\mathcal {D}_0^\to )}|_\mathrm {det} \to (\overline {\mathcal {D}_0}|_\mathrm {det})^\to .

Corollary [efr-DXJR]

Let \mathcal {A} be a small category, and let \mathcal {D} \to \mathcal {C} be a Markov prefibration. Let \mathsf {Fun}(\mathcal {A},\mathcal {D}) := \mathcal {D}^\mathcal {A} \times _{\mathcal {C}^\mathcal {A}} \mathsf {Fun}(\mathcal {A},\mathcal {C}). Then the functor \mathsf {Fun}(\mathcal {A},\mathcal {D}) \to \mathsf {Fun}(\mathcal {A},\mathcal {C}) is a Markov prefibration.

Proof

Note that \mathsf {Fun}(\mathcal {A},\mathcal {D}) is a limit of the categories \mathcal {D}^\to and prefibrations are stable under these limits.

The question is now

  1. If \mathcal {D} is a Markov fibration, we get a stochastic module structure on \mathcal {D}|_\mathrm {det}^\mathcal {A}---does it present a markov fibration?
  2. There is an induced map \mathsf {SChart}(\mathsf {Fun}(\mathcal {A},\mathcal {D}|_\mathrm {det})) \to \mathsf {Fun}(\mathcal {A},\mathcal {D}) (where the latter is taken by convention to mean the full subcategory of functors whose image in \mathcal {C} consists of deterministic arrows). Is this an isomorphism? (If it is, clearly this implies point 1)

Unfortunately it's not clear that either of these are true---the surjectivity of \mathsf {SChart}(\mathcal {D}|_\mathrm {det}) \to \mathcal {D} cannot a priori be lifted to the arrow category. The issue is that, given a map in \mathcal {D}^\to consisting of, say \phi _0,\phi _1, it is not sufficient to find charts representing each of these---we must find a chart of squares representing the square. This is not guaranteed by the Markov fibration structure, and a similar issue comes into play for the equivalence witnesses.

We may attempt to ignore this issue and simply try to form a double category \mathsf {SLens}(\mathcal {D}^\to ) \rightrightarrows \mathsf {SLens}(\mathcal {D}), given a stochastic module \mathcal {D}, but here the problem is that \mathsf {SLens} does not commute with limits in general. Hence we can not easily define a composition on the 2-cells of lenses obtained this way.

There are various ways we might attempt to remedy this problem. One approach would be to formulate a behavioural notion of "commutativity" for squares of stochastic lenses and charts, but the problem with this is that it is not obvious whether this property is stable under composition.

The basic problem stems from the fact that chart equivalences have a "directed" nature, and given a morphism of precharts (M,\phi ) \to (N,\psi ) and an equivalence (N,\psi ) \leftarrow (N',\psi ') (for example given by a stochastic section N' \to N satisfying suitable conditions), there is not in general a way to lift this back into an equivalent (M',\phi ') with a map to N'.

This observation leads to the idea that we might define a double category of precharts which has the directed equivalences among its morphisms (going only in one direction). We will begin by constructing this double category.

Definition [efr-KO4T]

Let \mathcal {D} \to \mathcal {C} be a (Grothendieck) fibration, and let \mathcal {C} \to \mathcal {C}' be a faithful, identity-on-objects functor. Suppose \mathcal {C} admits pullbacks, and given a pair of morphisms P \to X,Y \in \mathcal {C}' over Z, where P \to X is in \mathcal {C}, there is a unique common factorization P \to X \times _Z Y.

  1. The double category \mathsf {\mathbb Span}_{\mathcal {C}'}(\mathcal {C}) has \mathcal {C} as the vertical category, spans X \leftarrow P \to Y in \mathcal {C} equipped with a section X \to P \in {\mathcal {C}'} as horizontal cells, and maps of spans which commute with the sections as 2-cells.
  2. The double category \mathsf {\mathbb Span}_{\mathcal {C}'}(\mathcal {D} / \mathcal {C}) lying over \mathsf {\mathbb Span}_{\mathcal {C}'}(\mathcal {C}) has \mathcal {D} as the vertical category, and spans \bar {X} \xleftarrow {f} \bar {P} \xrightarrow {g} \bar {Y} where f is Cartesian, decorated with a section X \to P in \mathcal {C}' as the horizontal cells, and maps of such spans (so that the underlying thing commutes with the sections) as the 2-cells. We will call the horizontal cells decorated spans.
  3. There is an apparent forgetful functor \mathsf {\mathbb Span}_{\mathcal {C}'}(\mathcal {D} / \mathcal {C}) \to \mathsf {\mathbb Span}_{\mathcal {C}'}(\mathcal {C})

To spell it out, a 2-cell in \mathsf {\mathbb Span}_{\mathcal {C}'}(\mathcal {D} / \mathcal {C}) consists of a diagram of this form in \mathcal {D}, where f_1,f_2 are Cartesian, and (writing X_1 for the object underlying \overline {X_1}, and so on) two sections s_1,s_2 of the underlying maps in \mathcal {C}', so that the second diagram also commutes in \mathcal {C}':

Naturally, we are interested in the case of \mathsf {\mathbb Span}_{\mathcal {C}}(\mathcal {D} / \mathcal {C}_\mathrm {det}) for a stochastic module \mathcal {D}. Then the decorated spans are representatives for stochastic charts. We will start by introducing a loosed notion of 2-cell for these spans, which combines the directed equivalences with the ordinary deterministic 2-cells of spans.

Definition [efr-RD28]

Let \mathcal {C} be a Markov category and let \mathcal {D} be a stochastic module over \mathcal {C}. Let (M_1, \phi _1): \bar {X_1} \leftrightarrows \bar {Y_1}, (M_2, \phi _2): \bar {X_2} \leftrightarrows \bar {Y_2} be decorated spans in \mathsf {\mathbb Span}_{\mathcal {C}}(\mathcal {D} / \mathcal {C}_\mathrm {det}), and let f: \bar {X_1} \rightrightarrows \bar {X_2}, g: \bar {Y_1} \to \bar {Y_2} be morphisms in \mathcal {D}, so that we have a square

A 2-cell of decorated spans for this data consists of a morphism m: M_1 \to M_2 \in \mathcal {C} (that is, possibly stochastic), satisfying the following two conditions. First, the diagram

in the base must commute. Given this, there is an induced square
in \mathcal {D}_{M_1}, where the bottom map is given by pulling back \phi _2 along m, in the sense of Lemma [efr-VF6V]. The second condition is that this square must also commute.

Lemma [efr-DRU6]

2-cells of decorated spans compose---that is, given a diagram

where the horizontal maps are decorated spans, and the vertical maps are maps in \mathcal {D} with deterministic base, and given maps of decorated spans \phi _1 \xrightarrow {\alpha } \phi _2 \xrightarrow {\beta } \phi _3, there is a map of decorated spans \phi _1 \to \phi _3

Proof

We can easily compose the two maps to get M_1 \to M_3. Now, the question is whether the perimeter of this diagram commutes:

Note that the top square is commutative by assumption, since pullbacks compose (even along stochastic maps) and this is the assumption that \alpha is a cell. The bottom square is the result of pulling back a commutative square over M_2 again along \alpha . Note that pullback along stochastic morphisms is not in general functorial---but since the vertical parts of this square are themselves pulled back from X_2,Y_2, this composition is preserved by pullback along \alpha : M_1 \to M_2. This finishes the proof.

Proposition [efr-L7X0]

2-cells of decorated spans compose horizontally: Given a square

where the horizontal maps are precharts and the vertical maps are morphisms in \mathcal {D}|_\mathrm {det}, and given \alpha : \phi _1 \to \phi _2 and \beta : \psi _1 \to \psi _2, there is a prechart morphism \psi _1\phi _1 \to \psi _2\phi _2.

Proof

Unlike the proof of Lemma [efr-DRU6], this is straightforward: If the carrier of \phi _i is M_i, and of \psi _i, N_i (for i=1,2), then by definition the composites are carried by the pullback M_i \times _{Y_i} N_i. There is a canonical map M_1 \times _{Y_1} N_1 \to M_2 \times _{Y_2} N_2 over M_2, N_2, given by the independent pairing of \alpha and \beta .

Since pullbacks compose, the square over M_1 \times _{Y_1} N_1 that must commute is given by the two commutative squares induced by \alpha ,\beta , pulled back and composed with each other. Here we are pulling back along the deterministic projections from the pullback, and hence these commutative squares are preserved, and hence the composite square commutes as well.

Corollary [efr-MUNG]

Let \mathcal {D} be a stochastic module over \mathcal {C}. There is a double category \widetilde {\mathsf {\mathbb Span}}(\mathcal {D})^\mathrm {chart} which has decorated spans as its horizontal maps, morphisms in \mathcal {D}|_\mathrm {det} as its vertical maps, and decorated span 2-cells as its 2-cells.

Moreover, there is another double category \widetilde {\mathsf {\mathbb Span}}(\mathcal {D})^\mathrm {lens} which has decorated spans in \mathcal {D}^\mathrm {fop} as its horizontal maps instead.

(The modification of everything above to lenses instead of charts is obvious).

In fact, the globular 2-cells are in a sense exactly the equations defining the set of charts:

Lemma [efr-CU3J]

Let \phi , \psi : \bar {A} \to \bar {B} be parallel decorated spans in \widetilde {\mathsf {\mathbb Span}}(\mathcal {D})^\mathrm {chart} (or \widetilde {\mathsf {\mathbb Span}}(\mathcal {D})^\mathrm {lens} ).

They represent the same stochastic chart (lens) if and only if there exists a zig-zag of globular 2-cells between them.

Proof

Unwinding the definitions, a 2-cell M_\phi \to M_\psi is precisely a map exhibiting the equality of the two decorated spans, as in Lemma [efr-26SF]

The following straightforward lemma shows that charts over deterministic bases have initial representatives as spans. This will be important later:

Proposition [efr-10CM]

Suppose given a square

in \widetilde {\mathsf {\mathbb Span}}(\mathcal {D})^\mathrm {lens} (or \widetilde {\mathsf {\mathbb Span}}(\mathcal {D})^\mathrm {chart}) Suppose further the underlying square in \mathcal {C} is deterministic. Then:

  1. If there exists a filling decorated span 2-cell, the image in \mathsf {\mathbb Arena}(\mathcal {D}|_\mathrm {det}) commutes.
  2. If M_1 is the carrier of \phi _1 and the left leg M_1 \to X_1 is an isomorphism, then this implication is an equivalence.

Proof

Given a stochastic chart carried by X \leftarrow M \to Y, so that X \to Y is deterministic, recall that we can first pull back to the equalizer M' \hookrightarrow M of the two maps M \to X \to Y, M \to Y, then along the prescribed section X \to M'. Note that this gives a 2-cell from this canonical representative with carrier X to the initial representative.

Given two such cells, we get a square

But as part of the square surrounding the 2-cell, there is given a map X_1 \to X_2, which must make this square commute. The functoriality of base change (pulling back the map \phi _2) proves this bottom map is again a 2-cell.

But the property for this map to be a 2-cell is exactly the property for this square to be a commutative square in \mathsf {\mathbb Arena}{\mathcal {D}|_\mathrm {det}}. This proves both parts of the statement.

Backlinks

Proposition [efr-JQI9]

Let \mathcal {D} be a Markov prefibration. Then there is a double functor \mathsf {\mathbb Arena}(\mathcal {D}|_\mathrm {det}) \to \widetilde {\mathsf {\mathbb Arena}}(\mathcal {D}), which acts as identity on the morphisms of \mathcal {D}, and carries each lens (f: X \to Y, \phi : f^*\bar {Y} \to \bar {X}) to the prelens (X \leftarrow X \to Y, \phi ). This double functor is full on 2-cells.

The restriction to \mathsf {\mathbb Arena}(\mathcal {D}|_\mathrm {det}) \to \mathsf {\mathbb Arena}(\mathcal {D})_\mathrm {det} admits a right adjoint, which carries every prelens to its equivalence class.

Proof

First we must verify functoriality with respect to lens composition. To that end, let X \xrightarrow {f} Y \xrightarrow {g} Z be deterministic morphisms and \phi ,\psi be lenses over them. Their composite as prelenses has carrier X \times _Y Y = X and f^*(\psi )\phi as the morphism in the fiber, which is exactly the prelens associated to their composite as lenses.

Second, we must verify fullness on 2-cells. But this is a special case of Proposition [efr-10CM].

Finally, Proposition [efr-10CM] is precisely the statement that assigning a prelens to its equivalence class lens is right adjoint to this (and in particular that it forms a functor)