Markov Fibrations [efr-U4RA]

Recall that, given a functor R: \mathcal {C} \to \mathcal {D} with left adjoint L, there is a "standard resolution" of any object X \in \mathcal {C}, given by the "cofork" LRLRX \rightrightarrows LRX \to X, where the two parallel maps are the two possible applications of the adjunction counit. The adjunction is monadic if and only if this is always a coequalizer, in which case the RL-algebra corresponding to X is RLRX \to RX---conversely, given an algebra \alpha : RLA \to A, there are two parallel maps LRLA \rightrightarrows LA (given by L(\alpha ) and the counit,) and the object in \mathcal {C} corresponding to this algebra is given by this coequalizer.

Example

Consider the adjunction |-|: \mathsf {Mon} \leftrightarrows \mathsf {Set} : (-)^* between the category of monoids and the category of sets. Given a monoid M, |M|^* consists of lists of elements in M, and ||M|^*|^* consists of lists of such lists. The two maps ||M|^*|^* \to |M|^* consist in either concatenating the lists, or replacing each list with its product. Clearly these two maps are coequalized by the product map |M|^* \to M. Moreover it's clear that two lists have the same product if and only if they are identified in this coequalizer (simply consider a singleton list-of-lists, which identifies any given list with the singleton corresponding to its product).

As a generalization of this, if this coequalizer exists for every algebra, they form a left adjoint to the canonical functor \mathcal {C} \to \mathsf {Alg}_\mathcal {D}(RL). Since we have seen that the monad of free Markov prefibrations commutes with taking fiberwise opposites, we may hope that such a left adjoint exists---a simple argument shows that, if it is, it is fully faithful, and we may say that those prefibrations in the image are the "fibrations" and define their fiberwise opposite as the fiberwise opposite applied to their underlying algebras. Although it turns out to not be quite so simple, we will take this idea as our starting point.

Example

Let \mathsf {GrpTop} be the category of topological groups, and let R: \mathsf {GrpTop} \to \mathsf {Set} forget both the group structure and the topology. Clearly this is right adjoint to the free group in the discrete topology, and the monad of this adjunction is the free group monad, which we write RL for now. The canonical comparison functor \mathsf {GrpTop} \to \mathsf {Grp} just forgets the topology. Given a (non-topological) group, described by a map RLG \to G, we can form the diagram of topological groups LRLG \rightrightarrows LG. Here LG is the free, discrete group on G and LRLG is the free discrete group on the underlying set of LG. Their coequalizer is simply G equipped with the discrete topology, which is indeed the left adjoint to \mathsf {GrpTop} \to \mathsf {Grp}

In what follows, we will denote the monad \overline {(-)}|_\mathrm {det} simply by \operatorname {Free} to avoid too many complicated nestings of overlines and parentheses.

Definition Markov Fibration [efr-HVUT]

If \mathcal {D} is a Markov prefibration, we call it a Markov fibration if the diagram \overline {\operatorname {Free}(\mathcal {D}|_\mathrm {det})} \rightrightarrows \overline {\mathcal {D}|_\mathrm {det}} \to \mathcal {D} is a coequalizer in \mathsf {Cat}_{/\mathcal {C}}.

Given an algebra \alpha : \operatorname {Free}(\mathcal {D}_0) \to \mathcal {D}_0 of the free Markov prefibration monad, let \overline {\operatorname {Free}(\mathcal {D}_0)} \rightrightarrows \overline {\mathcal {D}_0} \in \mathsf {MarkPreFib} be as above. We say \alpha presents a Markov fibration if the coequalizer of these maps in \mathsf {Cat}_{/\mathcal {C}} is a Markov prefibration.

The terminology "presents a Markov fibration" is justified by the following proposition.

Proposition [efr-MAUM]

Let \alpha : \operatorname {Free}(\mathcal {D}_0) \to \mathcal {D}_0 be stochastic module which presents a Markov fibration. Then the underlying algebra of the Markov prefibration obtained as the coequalizer of \overline {\operatorname {Free}(\mathcal {D}_0)} \rightrightarrows \bar {\mathcal {D}_0} is isomorphic to \alpha , and in particular this prefibration is a Markov fibration.

This correspondence determines an equivalence of categories between the full subcategory \mathsf {MarkFib}(\mathcal {C}) of \mathsf {MarkPreFib}(\mathcal {C}) spanned by the Markov fibrations, and the full subcategory \mathsf {SFib}(\mathcal {C})^p \subseteq \mathsf {SFib}(\mathcal {C}) spanned by those algebras which present a Markov fibration.

Proof

Let \alpha be an algebra as assumed, and let \mathcal {D}_0^\alpha \in \mathsf {MarkPreFib} denote the coequalizer given. By general nonsense there is an induced functor \mathcal {D}_0 \to \mathcal {D}_0^\alpha |_\mathrm {det} which is moreover an algebra homomorphism---the claim is that this is an isomorphism. By Lemma [efr-L7L2], pullback to the deterministic part preserves these coequalizers, so this amounts to the claim that the diagram \operatorname {Free}^2(\mathcal {D}_0) \rightrightarrows \operatorname {Free}(\mathcal {D}_0) \to \mathcal {D}_0 is a coequalizer. But this is true for any algebra of any monad (in fact, the unit gives a splitting of this coequalizer).

By general nonsense the fibration associated to an algebra which presents a fibration forms a partial left adjoint to \mathsf {MarkPreFib}(\mathcal {C}) \to \mathsf {SFib}(\mathcal {C}). This left adjoint, by the above, has its image inside \mathsf {MarkFib}, and hence there is an adjunction \mathsf {MarkFib}(\mathcal {C}) \leftrightarrows \mathsf {SFib}(\mathcal {C})^p. The preceding furthermore proves that the unit of this adjunction is the identity, which implies that the left adjoint is fully faithful---but by definition it is essentially surjective, finishing the argument.

Let us briefly summarize the relationship between Markov prefibrations, Markov fibrations, and stochastic module fibrations at this stage.

  • A stochastic module fibration is a (Grothendieck) fibration \mathcal {D} over \mathcal {C}_\mathrm {det}, equipped with some extra structure involving the whole category \mathcal {C}. Given a deterministic map f: A \to B two objects X,Y \in \mathcal {D}_B, and a map \phi : f^*X \to f^*Y, we can think of this as a map parameterized by the fibers A_b. Given a stochastic section s: B \to A, the stochastic module structure picks out a map X \to Y \in \mathcal {D}_B corresponding to choosing this parameter randomly according to s.
  • A Markov prefibration is a category \mathcal {D} over \mathcal {C} with a particular unique lifting property. In the above situation, it gives a unique lift X \to f^*X of s, corresponding to choosing a \in A_b according to s and leaving the x \in X-coordinate unchangd. By composing this lift with \phi , then with the Cartesian f^*Y \to Y, we get a stochastic module structure on the part of \mathcal {D} lying over deterministic maps (which is also a Grothendieck fibration).

    • Given a stochastic module structure, there is a way of generating a category over \mathcal {C}, by freely adding the lifts corresponding to a Markov prefibration, then quotienting by the relations implied by the stochastic module structure. This does not necessarily yield a Markov prefibration.

    A Markov prefibration is called a Markov fibration if it is presented by its underlying stochastic module in the above sense.

Definition Weak supports [efr-YFV2]

Let \mathcal {D}_0 \to \mathcal {C}_\mathrm {det} be a stochastic module fibration.

Let \alpha : X \to M be a stochastic section, let \bar {X} \in \mathcal {D}_{0,X} be an object, and let \phi : \bar {X}_M \to \bar {X}_M \in \mathcal {D}_{0,M} be an endomorphism of its pullback. Observe that if there exists f: N \to M so that f^*(\phi ) = 1 and \alpha factors over f, then \alpha _*(\phi ) = 1. We say \mathcal {D}_0 has weak supports if this implication is an equivalence

We will make use of the following lemma:

Lemma [efr-L7L2]

Let F,G: \mathcal {D} \rightrightarrows \mathcal {D}' be a parallel pair in \mathsf {Cat}_{/\mathcal {C}}, and suppose both are identity on objects. Suppose moreover this is a reflexive pair, i.e there is some S: \mathcal {D}' \to \mathcal {D} so that FS = GS = 1_{\mathcal {D}'}. Then the coequalizer in \mathsf {Cat}_{/\mathcal {C}} is again identity on objects, and is given on hom-sets simply by the coequalizer of the parallel pair \mathcal {D}(x,y) \rightrightarrows \mathcal {D}'(x,y)

Proof

The only nontrivial part is to verify that composition is well-defined on the equivalence classes in \mathcal {D}'(x,y)/\sim . It suffices to see that post- and precomposition with a fixed morphism both preserve this equivalence relation. Take some f: x \to y \in \mathcal {C}, and h : y \to z \in \mathcal {C}'. We must show that hF(f) = hG(f). But simply write hF(f) = F(S(h)f) \sim G(S(h)f) = hG(f), and we are done. Clearly the other side follows by duality, finishing the proof.

Proposition Construction of \mathsf {SChart}(\mathcal {D}_0) [efr-TBZZ]

Let \mathcal {D}_0 be a fibration equipped with a stochastic module structure. Consider the equivalence relation on \overline {\mathcal {D}_0}(\bar {X},\bar {Y}) which identifies two precharts (M, \phi ), (N, \phi ') if there exists a map f: N \to M over X,Y and a stochastic section s of f which preserves the section from X, so that s^*\phi ' = \phi (note that this makes sense because pullbacks compose).

Then:

  1. This equivalence relation respects composition, and so defines a category which we denote \mathsf {SChart}(\mathcal {D}_0)
  2. In \mathsf {Cat}_{/\mathcal {C}}, \overline {\operatorname {Free}(\mathcal {D}_0)} \rightrightarrows \overline {\mathcal {D}_0} \to \mathsf {SChart}(\mathcal {D}_0) is a coequalizer diagram. In particular, \mathcal {D}_0 presents a Markov fibration if and only if \mathsf {SChart}(\mathcal {D}_0) is a Markov prefibration (in which case \mathsf {SChart}(\mathcal {D}_0) is the fibration it presents)
  3. If \mathcal {D}_0 has weak supports, \mathsf {SChart}(\mathcal {D}_0) is a prefibration

Proof

Recall that the fibration \operatorname {Free}(\mathcal {D}_0) has fibers whose morphisms \bar {X} \to \bar {X}' are given by tuples s: X \to M: p, p^*\bar {X} \to p^*\bar {X}' (up to a certain equivalence relation). Forming the free Markov prefibration \overline {\operatorname {Free}(\mathcal {D}_0)} on this fibration, we find that the morphisms are given by diagrams

equipped with a map \phi : p^*q^*\bar {X} \to p^*r^*\bar {Y}. The two maps \overline {\operatorname {Free}(\mathcal {D}_0)} \to \overline {\mathcal {D}_0} carry such a thing to first, the map resulting from forgetting M and just composing q,r with p to get a span (and composing the sections to get a new section), and secondly, the map with apex M obtained by using the stochastic module structure to push \phi down into a map over M. It is clear that this is equivalently the equation described in the theorem. This establishes points 1. and 2., since by Lemma [efr-L7L2] we can compute such coequalizers hom-set by hom-set.

Now we wish to prove that \mathsf {SChart}(\mathcal {D}_0) is a Markov prefibration given weak supports. Since by the coequalizer presentation, its deterministic part is isomorphic to \mathcal {D}_0, the fibration property is automatic. It remains to verify that, given a triangle

in \mathcal {C} with the vertical and horizontal maps deterministic, an object \bar {A} \in \mathcal {D}_{0,Y} and Cartesian maps \bar {A}_X \to \bar {A} \leftarrow \bar {A}_Z, there exists a unique lift \bar {A}_X \to \bar {A}_Z in \mathsf {SChart}(\mathcal {D}_0).

Such a lift is given by a diagram

equipped with p^*\bar {A}_X \to q^*\bar {A}_Z. By taking the equalizer of the two maps M \to Y (the section factors over this), we may assume these two are equal, which implies that the pulled-back objects are equal---denote this object \bar {A}_M. Now the hypothesis is that after postcomposing with the Cartesian map \bar {A}_Z \to \bar {A}, this gives the map \bar {A}_X \to \bar {A}. This postcomposition is given simply by postcomposing the leg M \to Z with the map Z \to Y (and observing that, by functoriality of pullbacks, this does not alter the pulled-back object). Then the claim is that integrating this map \bar {A}_M \to \bar {A}_M down into a map \bar {A}_X \to \bar {A}_X, it gives the identity. But by assumption this means we can pull back to some object M' \to M (lifting the section from X) where the two maps are already equal to the identity. But this pull-back can be applied to the original map \bar {A}_X \to \bar {A}_Z as well. But this implies every such map is equal to the one represented by the diagram
and the identity on \bar {A}_{X \otimes Y}, with the map M' \to X \otimes Y giving the witness, since identities pull back. This map only depends on the underlying X \to Y, hence \mathsf {SChart}(\mathcal {D}_0) is indeed a prefibration.

It is not apparent whether weak supports are necessary for \mathsf {SChart}(\mathcal {D}_0) to be a prefibration. We have not found any counterexample, but in general the equivalence relation on charts is fairly complicated, so it is not apparent how to prove the necessity. We will generally not be too bothered about assuming weak supports instead of the more nebulous assumption that \mathcal {D}_0 presents a Markov fibration.

Lemma [efr-26SF]

Let (M,\phi ) and (N,\psi ) be two representatives of charts. Given some possibly stochastic map f: M \to N over X and Y, recall (Lemma [efr-VF6V]) that we can define f^*\psi , regardless of whether f is deterministic or the section of a deterministic map. If there exists such a map f, we can always factor it over the pullback M \times _{X \times Y} N as a section followed by a deterministic map. Hence the equivalence relation defining \mathsf {SChart} is equivalent to the relation identifying two representatives whenever there exists such an f with f^*\psi = \phi

Remark [efr-XZRN]

By construction, for each Markov prefibration \mathcal {D}, there is a canonical functor \mathsf {SChart}(\mathcal {D}|_\mathrm {det}) \to \mathcal {D} over \mathcal {C}, which restricts to an isomorphism on the deterministic part (and in particular preserves Cartesian morphisms). \mathcal {D} is a Markov fibration if and only if this is an isomorphism.

Also by construction, given a morphism of stochastic modules F: \mathcal {D}_0 \to \mathcal {D}_0', there is an induced functor \mathsf {SChart}(\mathcal {D}) \to \mathsf {SChart}(\mathcal {D}') over \mathcal {C}. This restricts to F on the deterministic part and in particular preserves Cartesian morphisms.

Proposition [efr-1YS9]

Let \mathcal {D}_0 be a stochastic module fibration. Then \mathcal {D}_0 presents a Markov fibration if and only if \mathcal {D}_0^\mathrm {fop} does it.

Proof

Consider a triangle of this for in \mathcal {C}:

where the maps to Z are deterministic. Suppose given Cartesian lifts \bar {X} \to \bar {Z}, \bar {Y} \to \bar {Z} of the cospan. These are the same in both cases, coming from Cartesian maps in \mathcal {D}_0 \mathcal {D}_0^\mathrm {fop} (which are the same). We must show that there is a unique lift of f to a chart in \mathsf {SChart}(\mathcal {D}_0) if and only if there is a unique lift to a chart in \mathsf {SChart}(\mathcal {D}_0^\mathrm {fop}). Clearly it suffices to prove the "only if" implication, so suppose \mathsf {SChart}(\mathcal {D}_0) is a prefibration.

By passing to the equalizer as in the proof that \overline {\mathcal {D}_0} is a prefibration, we may assume that any such lift is represented by a diagram

where the outer square and the triangle X \to M \to Y commutes, and f' is a section.

Take such a diagram and let \phi : \bar {Z}_M \to \bar {Z}_M be the map representing a chart. Then the claim is there exists some zig-zag of chart equivalences identifying (M,\phi ) with (M,1). But clearly this is invariant under passing to the fiberwise opposite, and so \mathcal {D}^\mathrm {fop} is also a prefibration.

Definition Stochastic charts and lenses [efr-ANBC]

We refer to \mathsf {SChart}(\mathcal {D}_0) as the category of stochastic charts in \mathcal {D}_0. We refer to \mathsf {SChart}(\mathcal {D}_0^\mathrm {fop}) as stochastic lenses and denote it also \mathsf {SLens}(\mathcal {D}_0)

Example [efr-IAFO]

Kl(\Delta )^\to is a Markov fibration. We have already seen that it is a Markov prefibration, and that the map from the coreflection is full. So it suffices to prove faithfulness. Consider a map in {Kl(\Delta )^\to |_\mathrm {det}}, given by a diagram

We can factor the section X \to M as X \to X \times Y \to M, where the first map is just the pairing and the second is a conditional distribution. This induces a factorization of the lift \bar {X} \to M \times _X \bar {X} over \bar {X} \to \bar {X} \times Y. By composing the map M \times _X \bar {X} \to \bar {Y} with this factorization to build the map \bar {X} \times Y \to \bar {Y}, we have found a new representative for the same map.

Hence every map over X \to Y has a representative where the residual is X \times Y. We would like to argue that, since the map \bar {X} \times Y \to \bar {Y} is given by the conditional distribution of the composite map \bar {X} \to \bar {Y}, it is uniquely determined by it, and thus if two distinct maps in \overline {Kl(\Delta )^\to |_\mathrm {det}} have the same underlying map in Kl(\Delta )^\to , they must have equal representatives of this form, and so be identified in the coreflection (which must therefore be isomorphic to Kl(\Delta )^\to ). But of course, the two maps may only be almost certainly equal.

In this case, there is a simple fix: instead of taking X \times Y as the residual, take the subset S given by those pairs (x,y) where y has positive probability given x. The pairing factors over this, of course, and two maps \bar {X} \times _X S \to \bar {Y} which give the same distribution \bar {X} \to \bar {Y} really must have the same value on every point. This proves that \mathsf {SChart}(Kl(\Delta )^\to ) \to (Kl(\Delta ))^\to is faithful and hence an isomorphism.

Example [efr-C5RE]

\mathsf {BorelStoch}^\to , as we have noted, is a Markov prefibration, and hence induces a stochastic module structure on \mathsf {BorelStoch}^\to |_\mathrm {det}. This structure does not present a Markov fibration. To see this, note that in that case its fiberwise opposite would also present a Markov fibration. Then this fibration, \mathsf {SLens}(\mathsf {BorelStoch}^\to |_\mathrm {det}), would be a prefibration whose deterministic part was \mathsf {BorelStoch}^\to |_\mathrm {det}^\mathrm {fop}. But Example [efr-8B5X] shows that this is impossible.

Proposition [efr-8SXB]

Let \mathcal {C} be a Markov category with supports. Then the stochastic module induced by \mathcal {C}^\to \to \mathcal {C} presents a Markov fibration. If \mathcal {C} has conditionals, this Markov fibration is isomorphic to \mathcal {C}^\to .

Proof

Given a section s: X \to M:p and \phi : A \times _X M \to A \times _X A, simply take the pullback to the support of s. It must be the case that \phi (a,m) = (a,m) s-almost surely, which implies strict equality on the support. Hence by Proposition [efr-TBZZ], \mathcal {C}^\to presents a Markov fibration.

There is an induced map \mathsf {SChart}(\mathcal {C}^\to |_\mathrm {det}) \to \mathcal {C}^\to , which we claim is an isomorphism. So consider a map in \mathcal {C}^\to :

This map is in the image of
where the map \bar {X} \times Y \to \bar {Y} is taken to be a conditional. Note that every map in \mathsf {SChart}(\mathcal {C}^\to |_\mathrm {det}) can be represented in this form, by taking a conditional of M given Y to build a section to M \to X \otimes Y. Since conditionals are almost-surely equal, by restricting to the support of X \to X \otimes Y, we can find a representative which only depends on the overall map \bar {X} \to \bar {Y}, which proves that the map from \mathsf {SChart} is faithful, concluding the proof.

Continuing from Example [efr-CJTH], we have the following trivial case:

Proposition [efr-Z75A]

If \mathcal {C} is Cartesian (even if it does not admit pullbacks), the definition of Markov fibration over \mathcal {C} still makes sense, the Markov fibrations are exactly the Grothendieck fibrations, and their fiberwise opposites are simply their fiberwise opposites in the usual sense.

Proof

This is trivial because \mathsf {MarkPreFib}(\mathcal {C}) \to \mathsf {Fib}(\mathcal {C}_\mathrm {det} = \mathcal {C}) is simply the identity functor, hence it is monadic (with the identity monad,) hence every fibration/prefibration presents a Markov fibration, namely itself, and is in particular a Markov fibration. The fiberwise opposite is simply given by applying the identity (taking the stochastic module on the deterministic part), taking the fiberwise opposite, then applying the identity again (passing to the presented markov fibration).

It is worth noting that, even in the case where \mathsf {SChart}(\mathcal {D}_0^\mathrm {fop}) is not a prefibration, it may still deserve the name "stochastic lenses". For example the stochastic lenses in \mathsf {BorelStoch} can be seen to contain \mathsf {Optic}(\mathsf {BorelStoch}) as a full subcategory, even though it does not form a Markov fibration (see Theorem [efr-K6NM] below).

Part of the motivation for the theory of dependent optics is to identify a category of stochastic optics which admits all coproducts. If \mathcal {C} is distributive, \mathsf {Optic}(\mathcal {C}) satisfies \binom {A}{X} + \binom {A}{Y} = \binom {A}{X+Y}, but this coproduct fails to exist in general if the two secondary objects are distinct. The idea is that this coproduct \binom {A}{X} + \binom {A'}{Y} should exist as a family indexed by X + Y, where E_x = A for x \in X, and E_y = A' for y \in Y. Our theory accommodates this example under the mild additional hypothesis of extensiveness

Definition Extensive Markov Category [efr-B2P7]

A Markov category is said to be an extensive Markov category if it admits finite coproducts, whose injections are deterministic, and which satisfy the following equivalent conditions:

  1. If we let \mathcal {C}_{/a}^\mathrm {det} refer to the full subcategory of the slice spanned by the deterministic morphism x \to a, we have an equivalence of categories \mathcal {C}_{/a}^\mathrm {det} \times \mathcal {C}_{/b}^\mathrm {det} \cong \mathcal {C}_{/a + b}^\mathrm {det}, given by taking coproducts
  2. \mathcal {C}_\mathrm {det} is an extensive category in the usual sense and the inclusion \mathcal {C}_\mathrm {det} \to \mathcal {C} preserves pullbacks along coproduct inclusions.

More generally, for an infinite regular cardinal \kappa , we say that \mathcal {C} is \kappa -extensive if \mathcal {C}_\mathrm {det} is a \kappa -extensive category in the ordinary sense and both coproduct inclusions and pullbacks along them are preserved by the functor \mathcal {C}_\mathrm {det} \to \mathcal {C}.

Proposition [efr-QAV2]

Let \mathcal {C} be an extensive Markov category, let \mathcal {D}_0 \to \mathcal {C}_\mathrm {det} be a fibration which satisfies \mathcal {D}_{0,X+Y} = \mathcal {D}_{0,X} \times \mathcal {D}_{0,Y}. Note that this implies \mathcal {D}_0 admits finite coproducts, and they're given exactly by this pairing. Suppose \mathcal {D}_0 is equipped with a stochastic module structure. Then \mathcal {D}_0 \hookrightarrow \mathsf {SChart}(\mathcal {D}_0) preserves the finite coproducts. In particular, \mathcal {D}_0^\mathrm {fop} has the same coproducts as \mathcal {D}_0, and \mathcal {D}_0^\mathrm {fop} \to \mathsf {SLens}(\mathcal {D}_0) preserves them as well.

Proof

This is straightforward to check---the residual M \to X_1 + X_2 splits into M_1 + M_2 by extensivity of \mathcal {C}, which also implies the section must split as the copairing of a section s_1: X_1 \to M_1, s_2: X_2 \to M_2. By the condition on the fibration, the map in the fiber over M splits into a map over M_1 and a map over M_2. Using the extensivity again, it is straightforward to see that this decomposition respects the equivalence relation.

In particular, \mathsf {SChart}(\mathcal {C}^\to |_\mathrm {det}), \mathsf {SLens}(\mathcal {C}^\to |_\mathrm {det}) both admit coproducts given simply as coproducts in \mathcal {C}^\to , if \mathcal {C} is extensive.

Proposition [efr-XFAO]

Suppose \mathcal {D} is a Markov fibration so that each pullback functor f^*: \mathcal {D}_Y \to \mathcal {D}_X for f: X \to Y \in \mathcal {C}_\mathrm {det} can be taken to be bijective on objects, and that these can furthermore be chosen strictly functorial (so that (fg)^* = g^*f^*). Then, writing objects \bar {X} \in \mathcal {D}_X as \binom {A \in \mathcal {D}_*}{X \in \mathcal {C}}, where A is the unique object in \mathcal {D}_* which pulls back to \bar {X} under the deletion X \to *, (note that this means f^*\binom {A}{Y} = \binom {A}{X}) we may characterize the fiberwise dual as having hom-sets \mathcal {D}^{\mathrm {fop}}(\binom {A}{X},\binom {B}{Y}) = \mathcal {D}(\binom {B}{X},\binom {A}{Y})

Proof

The correspondence in both directions is obvious by just formally reversing the direction of the map f: \binom {A}{M} \to \binom {B}{M} in a representing tuple X \leftarrow M \to Y, a: X \to M, f---the fact that this assignment respects the equivalence relation follows from the fact that the monad preserves fiberwise opposites.

Context

Markov Fibrations and Stochastic Lenses [efr-O088]

Introduction [efr-X0ZV]

Let Kl(\Delta ) denote the Kleisli category of the discrete (countable) distribution monad on \mathsf {Set}. This is a simple setting for working with probability theory---sufficient for many applications. In order to study compositional Bayesian game theory (Reference [hedges-etal-bayesian-games], Reference [towards-cybercat]) one studies the category \mathsf {Optic}(Kl(\Delta )) of optics in Kl(\Delta ). These have the right level of expressivity to talk about players taking random actions, and where payoff depends stochastically on players' decisions.

In \mathsf {Optic}(Kl(\Delta )), {R \choose X} + {R \choose Y} \cong {R \choose X+Y}. Games with this codomain naturally describe the situation of a player who has a binary choice between X or Y. We call coproducts of this form the "good" coproducts---note that also {* \choose *} + {\emptyset \choose *} = {\emptyset \choose 2}, but this is considered somewhat pathological, since it relies on the nonexistence of any morphism {\emptyset \choose X} \to {A \choose Y} when A and X are nonempty.

In order to describe this structure on \mathsf {Optic}(Kl(\Delta )), it would be useful if it had all coproducts. Unfortunately this is not the case. \mathsf {Optic}(\mathsf {Set}) = \mathsf {Lens}(\mathsf {Set}) has a well-known extension with all coproducts, given by the fiberwise opposite of the fibration \mathsf {Fam}(\mathsf {Set}) \to \mathsf {Set} (this is Proposition [efr-VTPS] in the case \mathcal {C} = \mathsf {Set}). Extending this to stochastic maps would be the obvious way of constructing such a category of "dependent optics".

Consider a category Kl(\Delta )^\to defined as follows. Its objects are the objects of \mathsf {Set}^\to ---that is, they are indexed families of sets. A map in Kl(\Delta )^\to is a stochastic map in the base X \to Y \in Kl(\Delta ), and a stochastic map on the total spaces \bar {X} \to \bar {Y} which is compatible with it. Note that if \bar {X} \to X is surjective, the map on the base is fully determined by the map on the fibers, which must merely satisfy the condition that the distribution of the indexing point in Y depends only on the indexing point in X, not the specific point in the fiber \bar {X}_x.

We claim Kl(\Delta )^\to is a reasonable notion of "stochastic charts". Recall that by "chart" we mean something like "lenses where both maps go forward". If stochastic lenses are supposed to include optics as the full subcategory spanned by the "non-dependent" objects, then the charts should include "co-optics"---that is, maps between X' \otimes X \to X and Y' \otimes Y \to Y should be given by the coend \int ^M \operatorname {\mathrm {Hom}}(X, M \otimes Y) \times \operatorname {\mathrm {Hom}}(X' \otimes M, Y')

And in fact this is the case: Clearly there is a map from this coend to maps in Kl(\Delta )^\to . By taking M = X \otimes Y and conditioning on Y, we see this is surjective. Finally, by restricting to the support of the forwards part inside X \otimes Y, we obtain a representative for each element of the coend which is uniquely determined by X \to Y and X' \times X \to Y' (since the conditional is well-defined on the support).

Note: This relies both on the fact that Kl(\Delta ) has conditionals, and on the existence of supports. We've previously seen these defined in abstract Markov categories (Definition [efr-AB57])--supports in Kl(\Delta ) of a morphism p: A \to B are simply given by those b so that p(b | a) > 0. Note that the existence of both conditionals and supports is a very strong assumption---the only categories we are aware of with both properties are those whose probability distributions have a discrete character, like Kl(\Delta ) and \mathsf {FinStoch}. Neither will be essential to the theory, but both will play a role in certain theorems---we will see more of this later.

The goal of the theory of Markov fibrations is to give a notion of "fiberwise opposite" which can be applied to the codomain functor Kl(\Delta )^\to \to Kl(\Delta ) to give a reasonable notion of "stochastic lenses". In particular, we should recover the usual category of optics in the previous case.

It is clear that the codomain functor is not a (Grothendieck) fibration, since this would require Kl(\Delta ) to have pullbacks, which can only hold for a Cartesian Markov category. However, we can do some things. Namely, given a Cartesian (pullback) square in \mathsf {Set}

and a map {\bar {X} \choose X} \to {\bar {B} \choose B} where the base map X \to B is deterministic, for each deterministic factorizing map X \to A there is a unique lift \bar {X} \to \bar {A}. In other words, the pullback over \mathsf {Set} \hookrightarrow Kl(\Delta ) is a fibration---in fact, it is simply the family fibration \mathsf {Fam}(\mathsf {Kl}(\Delta )).

Furthermore, if \bar {X} \to \bar {B} is itself deterministic, there is such a unique lift even without assuming that the factorization X \to A is deterministic.

Moreover, we can factor any map in Kl(\Delta )^\to as such an induced map followed by a map over a deterministic base, as follows:

This gives us a hope that we can, in some way, control the category Kl(\Delta )^\to using the pullback over \mathsf {Set}, which is a fibration, and some information somehow given by these extra maps. Note also that the diagram above is equivalent to giving: a span X \leftarrow M \to Y and a section X \to M, which all lives in the base, and a map p^*\bar {X} \to p^{'*}\bar {Y} in the fiber over M. Thus it would seem to be very amenable to fiberwise dualization.

Analogous to our argument above that "co-optics" are equivalent to maps in Kl(\Delta )^\to , we can do the following:

Suppose given two tuples (M_0,p_0,p_0',s_0,\phi _0), (M_1,p_1,p_1',s_1,\phi _1) as above. Suppose there exists a map f: M_0 \to M_1 over X,Y, so that f s_0 = s_1. Then there is a canonical map p_0^*\bar {X} \to p_1^*\bar {X} over f, because pullbacks commute. If the triangle

moreover commutes, then these two triples represent the same map in Kl(\Delta )^\to

These equivalence relations correspond to "sliding" for deterministic morphisms M \to M'. Note that the condition here can be checked just on the fibration Kl(\Delta )^\to \times _{Kl(\Delta )} \mathsf {Set} \to \mathsf {Set}.

To obtain the full set of sliding equations, we will need to use stochastic maps M \to M', and thus leave that fibration behind. However, we are tantalizingly close to realizing Kl(\Delta )^\to as being presented by some sort of additional structure on the fibration \mathsf {Fam}(\mathsf {Kl}(\Delta )). (For a general monad T acting on C, the category \mathsf {Optic}_{\mathcal {C}}(Kl(T),Kl(T)), of effectful optics up to sliding of pure morphisms, was studied by Riley in Reference [riley-optics], section 4.9, and by Hedges in Reference [hedges-blog-optics-effect])

In this chapter we will indeed provide such a structure, and analyze it. In § [efr-2IMZ], we'll axiomatise the lifting property of Kl(\Delta )^\to discussed above into a property we call a Markov prefibration (Definition [efr-0019]). In § [efr-GO6R], we exhibit a free Markov prefibration associated to a fibration---its morphisms are precisely spans of the form seen above. Naturally, given a prefibration \mathcal {D} \to \mathcal {C}, its underlying fibration on \mathcal {C}_\mathrm {det} becomes an algebra for the monad of this adjunction. In § [efr-U4RA], we characterize the class of prefibrations which are presented by their underlying algebra in this way---these are the Markov fibrations (Definition [efr-HVUT]). Since the monad commutes with fiberwise opposites, this yields a notion of fiberwise opposite for Markov fibrations.

Following this, we review a few properties of the theory of Markov fibrations, including the existence of coproducts in the fibration (Proposition [efr-QAV2]), the stability of Markov fibrations under limits (§ [efr-HWAZ]), and induced monoidal structures (§ [efr-LTEL]). Combining these, we can prove:

Theorem [efr-OSH4]

There exists a (strong) symmetric monoidal functor \mathsf {Optic}(Kl(\Delta )) \to \mathsf {SLens}(Kl(\Delta )^\to ) which

  1. Is fully faithful.
  2. Preserves the good coproducts.
  3. So that the image has all coproducts, and every object of the image is a coproduct of objects in \mathsf {Optic}(Kl(\Delta ))
  4. And so that moreover the monoidal structure on the image is distributive

Markov Prefibrations [efr-2IMZ]

Remark [efr-0045]

Markov categories generally do not have pullbacks, for the same reason that they usually don't have products. This issue generally hinders the construction of fibrations, in the ordinary sense, of Markov categories. However, we can go part of the way. The idea of the following definitions is that given a pullback in the deterministic category, say A \times _Y X, a map P \to A \times _Y X where the X-coordinate is deterministic should be uniquely determined by a choice of (deterministic) map P \to X and (stochastic) P \to A such that the square commutes---as we claimed above (and will see below), this holds for the Markov category of discrete probability Kl(\Delta ). The analogous statement for products---that a map P \to A \otimes X with deterministic X-component is uniquely determined by the projections (or marginals) P \to X, P \to A---is a consequence of positivity (see Proposition [efr-OYB6]), and hence holds in most Markov categories of interest.

Definition Markov prefibration [efr-0019]

Let \mathcal {C} be a Markov category, and let p: \mathcal {D} \to \mathcal {C} be a functor into it. Then we call p a Markov prefibration if the following two conditions hold:

  1. The pullback \mathcal {D} \times _\mathcal {C} \mathcal {C}_\mathrm {det} \to \mathcal {C}_\mathrm {det} is a (Grothendieck) fibration
  2. Given maps f: A \to C, g:B \to C in \mathcal {D}, such that p(f),p(g) are deterministic and f,g are Cartesian for the above fibration, p induces a bijection between maps h: A \to B \in \mathcal {C} such that gh = f, and maps h': p(A) \to p(B) so that p(g)h' = p(f). Note that when restricted to those maps where p(h) is deterministic, this being a bijection is the defining property of g being Cartesian (for any f, not necessarily a Cartesian one).

Given a Markov prefibration \mathcal {D}, we write \mathcal {D}|_\mathrm {det} for \mathcal {D} \times _\mathcal {C} \mathcal {C}_\mathrm {det}. We will refer to this as the deterministic part of \mathcal {D}---note that this does have the potential for confusion, as when \mathcal {D} is itself a Markov category, this is not necessarily the same as the deterministic subcategory of \mathcal {D}. When f \in \mathcal {D} lies inside \mathcal {D}|_\mathrm {det}, and is Cartesian for that fibration, we will simply refer to it as a Cartesian map in \mathcal {D} (there are no other types of Cartesian maps, so this should not lead to confusion). A morphism of Markov prefibrations is a functor \mathcal {D} \to \mathcal {D}' over \mathcal {C} which preserves Cartesian maps. The category of Markov prefibrations over \mathcal {C} thus defined is denoted \mathsf {MarkPreFib}(\mathcal {C}). Taking the deterministic part defines a functor (-)|_\mathrm {det}: \mathsf {MarkPreFib}(\mathcal {C}) \to \mathsf {Fib}(\mathcal {C}_\mathrm {det}).

Remark On 2-category theory [efr-EQ41]

Since we will shortly be working with a number of functors between categories whose objects are themselves categories with some structure, it may be thought that we should give some consideration to the strictness of our constructions---for example, we will shortly construct a left adjoint to (-)|_\mathrm {det}: \mathsf {MarkPreFib}(\mathcal {C}_\mathrm {det}) \to \mathsf {Fib}(\mathcal {C}), and it may well be asked how strict this adjoint is, whether we need to consider the definition of pseudomonad when we get so far, et cetera.

However, we can largely avoid this issue. The key observation is that none of our functors will alter the objects of the underlying category (since \mathcal {C}_\mathrm {det} \to \mathcal {C} is identity on objects,). Hence, all the natural transformations that we would ordinarily ask to be equivalences of categories will instead be isomorphisms, and we can largely ignore considerations of higher category theory---similarly, all our functors will be strictly functorial. As a simple example of this, observe that the pullback functor (-)|_\mathrm {det} is automatically strict---it simply consists in restriction to a subset of the morphisms in \mathcal {D} (which is automatically closed under composition), and thus clearly preserves composition strictly.

Definition [efr-DINO]

In a Markov prefibration p: \mathcal {D} \to \mathcal {C} (as previously noted), a morphism f: \bar {X} \to \bar {Y} in \mathcal {D} is called Cartesian if p(f) is deterministic and f is Cartesian in the fibration \mathcal {D}|_\mathrm {det} \to \mathcal {C}_\mathrm {det}. It is called vertical if p(f) is an identity. It is called a stochastic-Cartesian if there exists a Cartesian map r: \bar {Y} \to \bar {X} so that rf = 1_{\bar {X}} (recall that in this case f is uniquely determined by r and p(f)). Note that if f is stochastic-Cartesian and p(f) is deterministic, then f is Cartesian.

The introduction to this chapter contains the argument that Kl(\Delta ) is a Markov prefibration. This is a key motivating example.

Example Markov prefibrations over Cartesian base [efr-CJTH]

Let \mathcal {C} be a Markov category which is Cartesian (that is, one where all morphisms are deterministic). Then a Markov prefibration over \mathcal {C} is simply a Grothendieck fibration.

Proposition [efr-0044]

Let \mathcal {C} be a Markov category. Then \mathcal {C}^\to \to \mathcal {C} is a Markov prefibration with Cartesian maps given by pullback squares, if and only if \mathcal {C} is pullback-positive.

Proof

Assume first \mathcal {C} is pullback-positive. It is clear that computing pullbacks in \mathcal {C}_\mathrm {det} gives the required Cartesian lifts---pullback positivity is precisely the claim that lifts exist uniquely in the definition of a Cartesian morphism (since the map to the base leg of the pullback is always deterministic in this case). Since Cartesian lifts can be taken to be deterministic (we have just constructed deterministic Cartesian lifts, and such lifts are unique up to unique isomorphism), the second condition also follows from this assumption, simply taking the other leg to be deterministic.

Conversely, suppose \mathcal {C}^\to \to \mathcal {C} is a Markov prefibration and suppose the Cartesian maps are given by the deterministic pullback squares. Let Y \to Z be an object of \mathcal {C}^\to and let X \to Z be a deterministic map, and form the pullback X \times _Z Y, which is Cartesian. Let P \to X be deterministic and let P \to Y be any map. Expanding the latter into a map from the object P \to P to Y \to Z, the Cartesian property of the square implies there is a unique pairing P \to X \times _Z Y

Remark [efr-0040]

In a general Markov category, not every isomorphism is necessarily deterministic. This means that, in general, fibres over isomorphic objects in a Markov prefibration are not necessarily isomorphic or even equivalent as categories. This seemingly immoral situation is, in fact, in accordance with other results indicating that deterministic isomorphism is really the proper notion of identification in a Markov category. See eg Reference [rischel-fritz-infinite-products], Section 4, for further discussion of this point. (Since the basic idea of a Markov category involves objects equipped with some structure which is not preserved by all the morphisms, it is not so paradoxical that an isomorphism in this situation should be insufficient to render two objects identical).

Under very weak assumptions on the Markov category \mathcal {C}, such as positivity, all isomorphisms are deterministic. This implies that all Markov prefibrations over \mathcal {C} are isofibrations, and thus rules out any sort of behavior like the above. As noted, we are only concerned with positive Markov categories.

Relatedly, in the proof of Proposition [efr-0044], a careless prover may have erroneously concluded after the first step that all Cartesian lifts are deterministic---but since Cartesian lifts are characterized only up to isomorphism, not necessarily deterministic isomorphism, this does not automatically follow. (But of course replacing a nondeterministic lift with an isomorphic deterministic one in this situation cannot alter the unique existence of the factorization, so it does not matter).

Proposition [efr-0042]

Let p: \mathcal {D} \to \mathcal {C} be a Markov prefibration, let \mathcal {C}' \subseteq \mathcal {C}, \mathcal {D}' \subseteq \mathcal {D} be full subcategories so that p(\mathcal {D}') is contained in \mathcal {C}', and suppose \mathcal {C}' is a monoidal subcategory (which is then automatically a sub-Markov category). Suppose finally \mathcal {D}' is stable under pullback along deterministic morphisms in \mathcal {C}'. Then \mathcal {D}' \to \mathcal {C}' is again a Markov prefibration.

Proof

By assumption, given Y \in \mathcal {D}' and f: X \to p(Y) \in \mathcal {C}', the Cartesian lift X' \to Y is again in \mathcal {D}'. The fullness of the subcategory inclusions suffices to prove the existence and uniqueness of the required lifts so that this is still Cartesian after restricting. For the same reason, since we have just observed that the Cartesian lifts are the same as in \mathcal {D} \to \mathcal {C}, the second part of the definition also holds.

Example \mathsf {Stoch}^\to as Markov prefibration [efr-NC7D]

Recall that the deterministic maps in \mathsf {Stoch} are those kernels valued in \{0,1\}-valued measures. (And that these are not the same thing as the measurable maps). Given a pair f:X \to Z, g: Y \to Z of such maps, we claim that the subset of X \times Y given by those points where f(x) = g(y) as measures on Z, equipped with the subset \sigma -algebra and its inclusions into X and Y, is a pullback in \mathsf {Stoch}_\mathrm {det}.

To see this, observe that \mathsf {Stoch}_\mathrm {det} is the Kleisli category for the submonad G_{0,1} of the Giry monad which takes a space to the subspace of 0,1-valued probability measures on it. Note that by the general theory of Markov categories this has products given by the products in \mathsf {Meas}. It hence suffices to prove that the pullback of f \times g: X \times Y \to Z \times Z along the diagonal Z \to Z \times Z exists---if it does, it has the universal property of the product X \times _Y Z.

To see that it does (and that it's given by the space described above), note that the diagonal is a split monomorphism, so it suffices to show that h: P \to X \times Y \in \mathsf {Stoch}_\mathrm {det} factors over X \times _Y Z if and only if the composite to Z \times Z lifts over the diagonal.

Now this lift over Z exists if and only if the probability of the diagonal \operatorname {im}(Z) \subseteq Z \times Z under the composite is 1. By definition, it is \int f(\operatorname {im}(Z) \mid x) g(\operatorname {im}(Z) \mid y) h(dx,y \mid p) Since the function being integrated is an indicator, this is simply the measure of the set \{(x,y) : \mathbb {P}(\operatorname {im}(Z) \mid x,y) = 1\}. If the probability of the diagonal is one, clearly the two marginals agree. Conversely, since \mathsf {Stoch}_\mathrm {det} is Cartesian, it must be the case that if the marginals agree the probability of the diagonal is 1. Therefore this is equal to the subset X \times _Z Y \subseteq X \times Y described at the start. But for this to have measure 1 for all p \in P is equivalent to the desired lifting property. This finishes the argument.

Moreover, this argument relied only on the 0,1-valuedness of the maps f,g, not h: P \to X \times Y or its marginals. Hence this also proves that the pullback along the diagonal is preserved by the inclusion \mathsf {Stoch}_\mathrm {det} \to \mathsf {Stoch}. Since \mathsf {Stoch} is known to be positive, this implies \mathsf {Stoch}^\to \to \mathsf {Stoch} is a Markov prefibration.

Proposition [efr-0041]

The codomain functor \mathsf {BorelStoch}^\to \to \mathsf {BorelStoch} is a Markov prefibration.

Proof

We wish to apply Proposition [efr-0042]. The only thing to check is that standard Borel spaces are stable under pullbacks in \mathsf {Meas}. But standard Borel spaces are known to be stable under products and measurable subsets, and this is enough (see eg. Reference [srivastava-borelsets] propositions 3.1.23 and 3.3.15)

Corollary [efr-0043]

\mathsf {FinStoch}^\to \to \mathsf {FinStoch} is a Markov prefibration.

Example [efr-8B5X]

The functor \mathsf {Optic}(\mathsf {BorelStoch}) \to \mathsf {BorelStoch} is not a Markov prefibration, although its pullback over \mathsf {BorelStoch}_\mathrm {det} is a Grothendieck fibration.

To see this, first consider the deterministic pullback. An optic \binom {A}{X} \to \binom {B}{Y} with deterministic base can be identified with a map X \otimes B \to A (and the base deterministic map X \to Y). To see this, first observe that the subset of \mathsf {BorelStoch}(X, Y \otimes M) with the marginal X \to Y deterministic is in bijection with \mathsf {BorelStoch}_\mathrm {det}(X,Y) \times \mathsf {BorelStoch}(X,M), since \mathsf {BorelStoch} is positive. Hence we can calculate \int ^M \mathsf {BorelStoch}_\mathrm {det}(X,Y) \times \mathsf {BorelStoch}(X,M) \times \mathsf {BorelStoch}(M \otimes B, A) \cong \mathsf {BorelStoch}_\mathrm {det}(X,Y) \times \mathsf {BorelStoch}(X \times B, A), using the ninja yoneda lemma as in Proposition [efr-M19V]. Hence this part is a fibration with the fiber over X being the coKleisli category of the X \times - monad, and the pullback functors given by reindexing these parametrized maps. The Cartesian lift of a map X \to Y at \binom {B}{Y} is given by the optic \binom {B}{X} \to \binom {B}{Y} with unit residual and identity backwards component.

Now, let g: I \to \mathbb {R} denote the standard Gaussian distribution, let f: \mathbb {R} \otimes \mathbb {R} \to \mathbb {R} be the function given by f(x,y) = 0 if x=y and y otherwise, and consider the two optics \binom {\mathbb {R}}{*} \to \binom {\mathbb {R}}{\mathbb {R}} given by (I, g: I \to \mathbb {R}, 1_\mathbb {R}: \mathbb {R} \to \mathbb {R}), (\mathbb {R}, \mathrm {copy}_\mathbb {R} g : I \to \mathbb {R} \otimes \mathbb {R}, f: \mathbb {R} \otimes \mathbb {R} \to \mathbb {R}) (where we recall that the first argument is the residual). They cannot be equal, as postcomposition with the optic \binom {\mathbb {R}}{\mathbb {R}} \to \binom {*}{*} given by the identity \mathbb {R} \to \mathbb {R} yields, for the former, the standard Gaussian g: I \to \mathbb {R}, and for the latter, the constant zero map. But postcomposition with the projection \binom {\mathbb {R}}{\mathbb {R}} \to \binom {\mathbb {R}}{*} does give the same optic (the identity), because, for every fixed y \in \mathbb {R}, when x is normally distributed, f(x,y) = y with probability one. Hence the unique lifting of Cartesian maps over Cartesian maps cannot hold.

This counterexample indicates that, although \mathsf {BorelStoch}^\to is a Markov prefibration, we can not expect a dual version of this prefibration---in fact, since over deterministic maps \mathsf {Optic}(\mathsf {BorelStoch}) is the fiberwise dual of (the restriction to trivially-indexed objects of) \mathsf {BorelStoch}^\to , this example shows that there is no Markov prefibration whose deterministic part is the fiberwise dual of \mathsf {BorelStoch}. Moreover, as the example indicates, this is not a mere technical issue, but an unavoidable fact about optics in general measurable spaces---even up to behavioral equivalence, they simply don't satisfy the conditions of being a Markov prefibration. (But see Theorem [efr-K6NM])

On the other hand, we have:

Proposition [efr-UDS9]

Let \mathcal {C} be a positive Markov category with supports. Then \mathsf {Optic}(\mathcal {C}) \to \mathcal {C} is a Markov prefibration.

Proof

As above, we see that the deterministic part is a fibration, so take X \to Y \leftarrow Z deterministic maps, and let \binom {A}{X} \to \binom {A}{Z} be an optic so that the induced triangle with the two Cartesian lifts to \binom {A}{Y} commutes. Let the two parts be f: X \to M \otimes Y, g: M \otimes A \to A. The implication is that X \to M \otimes Y \to M -almost surely, g is equal to the projection to A (and X \to M \otimes Y \to Y renders the triangle in \mathcal {C} commutative). Note that f factors over the support of this map, hence we can assume the marginal X \to M has full support. Hence up to sliding equivalence, g is strictly equal to the projection. This implies the lift is uniquely determined as desired.

The existence of supports rules out the pathological behaviour. Essentially, in the presence of supports, we can sensibly reason about "the points of measure zero" and exclude them from consideration---and Proposition [efr-8MYE] implies that the independent pairing of two measures always have the least "points of measure zero", and so that what can be proven equivalent under the assumption of independence will always be equivalent. By contrast, the map f: \mathbb {R} \times \mathbb {R} \to \mathbb {R} from Example [efr-8B5X] satisfies f(x,y) = y for almost all x when x is normally distributed, for all y, but this does not imply that for all measures on x,y with this marginal, f(x,y) is distributed as the marginal of y.

One point of view is that the map f is simply pathological, and we should restrict our attention to maps that are continuous in some sense (from the point of view of computer science, one argument for this is that computable maps are necessarily continuous). The category \mathsf {TychStoch} of Tychonoff spaces and weakly continuous kernels does indeed have supports. However, since it lacks conditionals, it is still not ideal from our point of view.

Free Markov Prefibrations [efr-GO6R]

Because every map in Kl(\Delta )^\to factors into arrows which are "induced" from arrows in Kl(\Delta )^\to |_\mathrm {det} and the Markov prefibration property, it may initially be hoped that Kl(\Delta )^\to is in some sense "free" on the data of the fibration Kl(\Delta )^\to |_\mathrm {det} \to \mathsf {Set} and the inclusion \mathsf {Set} \to Kl(\Delta ). If that was true, we may further hope that taking the fiberwise opposite of the fibration and applying the same free generation principle would generate a good notion of stochastic lens.

Unfortunately, this is not the case. We will see that the free prefibration is given by gadgets which look a bit like an indexed version of optics, up to a sliding equivalence for deterministic maps on the residual. This prompts us to look for some extra structure on the fibration \mathcal {D}|_\mathrm {det} \to \mathcal {C}_\mathrm {det} which describes sliding equivalences for stochastic maps on the residual. In the next section, we will see that this is exactly the structure of an Eilenberg-Moore algebra for the free prefibration monad on \mathsf {Fib}(\mathcal {C}_\mathrm {det}).

In this section, we will give a description of the free Markov prefibration on a fibration \mathcal {D}_0 \to \mathcal {C}_{\mathrm {det}} (assuming \mathcal {C} is pullback positive). There is a fairly simple description of the hom-sets, but their composition is a bit tricky, and verifying associativity even more so. Hence we will employ a technical trick: by characterizing the hom-sets as "freely generated" in a certain sense from the hom-sets in \mathcal {D}_0, we can identify them with sets of natural transformations using a Yoneda-type argument, and infer composition and associativity from there.

Definition Indexed copresheaf [efr-001I]

Let p: \mathcal {D} \to \mathcal {C} be a functor. An indexed copresheaf on \mathcal {D} is a tuple (X \in \mathcal {C}, F: \mathcal {D} \to \mathsf {Set}, \alpha : F(-) \to \mathcal {C}(X,p(-))) consisting of a copresheaf, an object of \mathcal {C}, and a natural transformation \alpha as indicated. We say the indexed copresheaf is over X, and we will abuse the terminology by referring to F itself as an indexed copresheaf, leaving the transformation \alpha implicit (for example, "let F be an indexed copresheaf over X").

We denote the subset \alpha ^{-1}(\{f\}) \subseteq F(\bar {A}), for f: X \to p(\bar {A}) by F(\bar {A})_f.

A map of indexed copresheaves (X,F,\alpha ) \to (Y,G,\beta ) is a natural transformation F \to G and a map Y \to X \in \mathcal {C} so that the obvious square of natural transformations commutes. We denote the category of indexed copresheaves by \mathsf {IcoPSh}(\mathcal {C} / \mathcal {D}). Note that there is an obvious forgetful functor \mathsf {IcoPSh}(\mathcal {D} / \mathcal {C})^\mathrm {op} \to \mathcal {C}

Observe that for each object A \in \mathcal {D}, there is a corepresentable copresheaf (p(A), \mathcal {D}(A,-), p). Maps between these obey the Yoneda lemma, in the sense that they are in bijection with maps between the underlying objects in \mathcal {D}. This defines a fully faithful functor \mathcal {D} \to \mathsf {IcoPSh}(\mathcal {D} / \mathcal {C})^\mathrm {op} over \mathcal {C}.

Of course, there is a dual notion of indexed presheaf, but this will not interest us.

Proposition [efr-FOJT]

Let p: \mathcal {D} \to \mathcal {C} be any functor and let \mathcal {C}_0 \to \mathcal {C} be an identity-on-objects functor. Write \mathcal {D}_0 = \mathcal {D} \times _\mathcal {C} \mathcal {C}_0 for the pullback. If F: \mathcal {D} \to \mathsf {Set} is a copresheaf indexed over X \in \mathcal {C}, the pullback \bar {A} \mapsto F(\bar {A}) \times _{\mathcal {C}(X,p\bar {A})} \mathcal {C}_0(X,p\bar {A}) is a copresheaf on \mathcal {D}_0 indexed over X again in a unique way. This defines a functor \mathsf {IcoPSh}(\mathcal {D} / \mathcal {C}) \to \mathsf {IcoPSh}(\mathcal {D}_0 / \mathcal {C}_0). Moreover, this functor preserves the corepresentable copresheaves (since \mathcal {C}_0 \to \mathcal {C} is identity on objects, so is \mathcal {D}_0 \to \mathcal {D}, so this statement makes sense).

Corollary [efr-FRQG]

Let \mathcal {D}_0 \to \mathcal {C}_0 be a functor and let \mathcal {C}_0 \to \mathcal {C} be identity-on-objects and faithful. Then the pullback of the composite \mathcal {D}_0 \to \mathcal {C} and the inclusion \mathcal {C}_0 \to \mathcal {C} is identical to \mathcal {D}_0. Therefore, Proposition [efr-FOJT] gives a functor \mathsf {IcoPSh}(\mathcal {D}_0 / \mathcal {C}) \to \mathsf {IcoPSh}(\mathcal {D}_0 / \mathcal {C}_0).

The idea of our construction of the free Markov prefibration is to give a certain monad on \mathsf {IcoPSh}(\mathcal {D}_0 / \mathcal {C}) and consider the Kleisli maps between the representable copresheaves.

At this point, the notion of a deterministic map M \to X equipped with a stochastic (ie not necessarily deterministic) section begins playing a key role. The phrase "stochastic section" will always carry an implicit "of a deterministic map". In most cases the map that the section is a section of will be clear from the context.

Note that, given a stochastic section Y \to M and a deterministic map X \to Y, if \mathcal {C} is pullback-positive, there is a unique lifting of this to a section of the projection Y \times _X M \to Y. We will use this fact several times.

Definition Stochastic Module [efr-Y926]

Let \mathcal {C} be a Markov category, and let \mathcal {D}_0 \to \mathcal {C}_\mathrm {det} be a fibration. Then a stochastic module consists of

  1. An indexed copresheaf F = (A,F,\rho ) \in \mathsf {IcoPSh}(\mathcal {D}_0 / \mathcal {C})
  2. For each \bar {X} \in \mathcal {D}_0, Cartesian morphism \bar {a}: \bar {X}_M \to \bar {X} lying over a: M \to X, and stochastic section \alpha : X \to M, a function \alpha _*: F(\bar {X}) \to F(\bar {X}_M), which acts on the underlying morphisms in \mathcal {C} as composition with \alpha
  3. Satisfying, whenever given a commutative square of Cartesian morphisms:
    and stochastic sections \alpha ,\beta lying over a = p(\bar {a}), b = p(\bar {b}), so that we have a digram in \mathcal {C}:
    Where the maps except \alpha ,\beta are deterministic, \alpha and \beta are sections of a and b, and both the square of deterministic maps and the square involving \alpha ,\beta commute, the condition that the square
    commutes.
  4. And satisfying furthermore the equation, for every two stochastic sections \alpha :X \to M, \beta : M \to N, the equation (\beta \alpha )_* = \beta _*\alpha _* (note that this makes sense because pullbacks compose).

A morphism of stochastic modules is an indexed natural transformation which preserves the operations \alpha _*. The category of stochastic modules is denoted \mathsf {SMod}(\mathcal {D}_0 / \mathcal {C}). There is an apparent forgetful functor \mathsf {SMod}(\mathcal {D}_0 / \mathcal {C}) \to \mathsf {IcoPSh}(\mathcal {D}_0 / \mathcal {C}).

Remark [efr-GL6R]

Note that \alpha _* of course depends on f, not just \alpha .

If f: M \to X is a deterministic map, \alpha :X \to M is a stochastic section, and \bar {X}_M, \bar {X}_M' \to \bar {X} are two Cartesian lifts of f to \bar {X} \in \mathcal {D}_X, then applying the commutativity axiom for stochastic modules implies that the triangle

commutes. In what follows, we will simply write f^*\bar {X} for some choice of cartesian lift, and speak of \alpha _* : F(\bar {X}) \to F(f^*\bar {X}). The above shows that this is a harmless abuse---the actions \alpha _* are preserved by the identification of different Cartesian lifts. In particular, we will often make arguments as if pullbacks compose strictly, although in general they only compose up to isomorphism. The above triangle means this is harmless.

The term "stochastic module" is not very good, but this is mostly a nonce definition in any case, so we won't worry too much about it.

Stochastic modules over a given X \in \mathcal {C} can be seen to be monadic over the category of indexed copresheaves over that X. However, the compatibility of these local left adjoints with the structure of the rest of the category is somewhat subtle. However, we do have free stochastic modules on representable indexed copresheaves, as we will soon see.

Proposition [efr-2XPE]

Let \mathcal {D} \to \mathcal {C} be a Markov prefibration, and let \mathcal {D}_0 = \mathcal {D} \times _\mathcal {C} \mathcal {C}_\mathrm {det}. Then the corepresentable copresheaf \mathcal {D}(\bar {A},-), restricted to \mathcal {D}_0, (but not pulled back---that is, we remember the whole set \mathcal {D}(\bar {A},\bar {X}), even the part over stochastic f, but only the composition with maps in \mathcal {D}_0) is a stochastic module in a canonical way, with \alpha _*: F(\bar {X}) \to F(f^*\bar {X}) given by composition with the unique induced lift of \alpha . Moreover, any morphism of Markov prefibrations \phi : \mathcal {D} \to \mathcal {D}' induces a homomorphism of stochastic modules \mathcal {D}(\bar {A},-) \to \mathcal {D}'(\phi (\bar {A}),-)

Proof

Given f: M \to X and a stochastic section \alpha , it's clear that composition with the unique lift \bar {X} \to f^*\bar {X} is a map of the right type, so we just have to verify the equations. For the first equation (item 3 in the definition of stochastic module), we are comparing two maps F(g^*\bar {X}) \to F(b^*\bar {X}). These are given by composition with two maps, let's call them \\phi, \psi : g^*\bar {X} \to b^*\bar {X}. These two maps are lifts of f\alpha and \beta g, but by assumption these two are equal. Hence by the uniqueness property of Markov prefibrations, \phi = \psi , and we have our equation. The other equation follows in a completely analogous way.

To prove the homomorphism property, note that a morphism of prefibrations preserves Cartesian morphisms, and hence (by uniqueness) must preserve the unique lifts of stochastic sections. Then by functoriality it must preserve composition with these, which finishes the proof.

Lemma [efr-OH7U]
  1. Let \bar {X} \in \mathcal {D}_0 be an object. Then there is a free stochastic module T\mathcal {D}_0(\bar {X},-) on its representable copresheaf, in the sense that if F is another stochastic module, homomorphisms T\mathcal {D}_0(\bar {X},-) \to F are in bijection with indexed natural transformations \mathcal {D}_0(\bar {X},-) \to F
  2. The free stochastic module on a corepresentable presheaf is given as follows: an element of T\mathcal {D}_0(\bar {X},-)(\bar {Y}) consists of a diagram in \mathcal {C} of the form
    (where X = p(\bar {X}), Y = p(\bar {Y}),) where fs = 1_X and f,g are deterministic, plus a map f^*\bar {X} \to \bar {Y} lying over g. This is up to the equivalence relation which, given some other such tuple, identifies them whenever there exists deterministic h: N \to M as in this diagram:
    so that the two deterministic triangles commute, hs' = s, and so that the unique Cartesian map f'^*\bar {X} \to f^*\bar {X} over h forms a commutative triangle with the two maps to \bar {Y}. (Note that we do not claim the relation just described is inherently an equivalence relation, rather we form the equivalence relation generated by this). It is clear how a map \bar {Y} \to \bar {Z} acts on this to make it a copresheaf. It is indexed by taking a tuple as above to the composite X \to M \to Y. Given N \to Y with a stochastic section s': Y \to N,, and an element of T\mathcal {D}_0(\bar {X},-)(\bar {Y}), the induced element in T\mathcal {D}_0(\bar {X},-)(s'^*\bar {Y}) is given by forming the pullback M \times _Y N, taking the pullback of the map over g to one lying over the projection M \times _Y N \to N, and composing the section s with the induced lift M \to M \times _Y N
  3. The underlying copresheaf of this respects Cartesian maps in \mathcal {D}_0 \to \mathcal {C}_\mathrm {det}, in the sense that given a Cartesian map \bar {A} \to \bar {B} and an element \phi \in T\mathcal {D}_0(\bar {X},-)(\bar {B}) lying over a deterministic map X \to B, the natural map from lifts \psi \in T\mathcal {D}_0(\bar {X},-)(\bar {A}) to lifts X \to A is a bijection.

Proof

First, we have to verify the equations of a stochastic module for T\mathcal {D}_0(\overline {X},-). For the first case, suppose we are given a square

with all but the upwards maps stochastic. Now let \bar {Z} be some object over Z and suppose we are given an element of T\mathcal {D}_0(\bar {X}, \bar {Z}_Y), represented by a span X \leftarrow M \to Y, a section X \to M and a map \phi : \bar {X}_M \to \bar {Z}_M over M. Consider then the below diagram:
By definition, the first of the two possible elements of T\mathcal {D}_0(\bar {Z}_W) are given by either forming the pullback M \times _Y N, taking the lift of \alpha to M \to M \times _Y N and composing to get a section X \to M \times _Y N, and pulling back \phi along the projection to get a map \bar {X}_{M \times _Y N} \to \bar {Z}_{M \times _Y N}, then taking the span X \leftarrow M \times _Y N \to W. The second is given by first composing with the map Y \to Z, then applying the above procedure with the pullback M \times _Z W. The induced map M \times _Y N \to M \times _Z W exhibits the equality of these two under the equivalence relation defining T\mathcal {D}_0(\bar {X},-) (commutativity of the bottom-right square implies that triangle of stochastic sections commutes.)

Given some other stochastic module F over A with a map of indexed copresheaves \mathcal {D}_0(\bar {X},-) \to F, over A \to X, there is at most one extension to a map of stochastic presheaves T\mathcal {D}_0(\bar {X},-) \to F over A \to X---given an element with representative (s:X \to M, X \leftarrow M \to Y, \bar {X}_M \to \bar {Y}_M), it must go to the identity element of F(\bar {X}), acted on by the stochastic section s to produce an element of F(\bar {X}_M), followed by F applied to the map \bar {X}_M \to \bar {Y} over M \to Y.

But it is not hard to see that the equivalence relation imposed by T\mathcal {D}_0(\bar {X},-) is implied by the equations of a stochastic module, and so this map is well-defined, establishing the property.

Secondly, let \bar {A} \to \bar {B} be a Cartesian map over A \to B, and take a commutative triangle

of deterministic maps. Finally take an element of T\mathcal {D}_0(\bar {X},-)(\bar {B}) over the given map X \to B. We must show it has a unique lift to A over the given map X \to A. Let us take a representative given by a diagram:
First, note that the two maps M \to X \to B and M \to B do not necessarily agree. However, we can remedy this by replacing M by their equalizer---note that as we argued above, this gives an equivalent element of the stochastic module. (By writing their equalizer in \mathcal {C}_\mathrm {det} as the split pullback M \times _{B \times B} B, we can see that the section factors over this, even if \mathcal {C} does not have all equalizers in general). Hence we can assume the triangle formed by adding the dashed arrow commutes.

Since M \to B now factors over X, the lift X \to A gives a lift M \to A. Now by the Cartesian property of \bar {A} \to \bar {B}, there is a unique lift of p^*\bar {X} \to \bar {B} to this map (here we just use the fact that \mathcal {D}_0 is a fibration). This gives the desired lift.

Finally, given two distinct lifts (again, we can assume their maps M \to A factor over X,) clearly any map N \to M witnessing an identity between their composites \bar {X} \to \bar {Y} would likewise exhibit an identity between their lifts (since pullbacks compose). This proves uniqueness, and finishes the proof.

We are now ready to prove the main proposition of this section:

Proposition [efr-LGOA]

Let \mathcal {C} be a pullback-positive Markov category and let \mathcal {D}_0 \to \mathcal {C}_\mathrm {det} be a fibration. Consider the full subcategory of stochastic modules spanned by the free modules on the corepresentables. Denote the opposite of this category \bar {\mathcal {D}_0}. Clearly there is a commutative diagram

We claim:

  1. \bar {\mathcal {D}_0} \to \mathcal {C} is a Markov prefibration.
  2. There is a bijection \bar {\mathcal {D}_0}(\bar {A},-) \cong T(\mathcal {D}_0(\bar {A},-)). When the left-hand side is equipped with the canonical stochastic module structure, and the right is equipped with the free one, this is moreover a homomorphism (hence isomorphism) of stochastic modules.
  3. \bar {\mathcal {D}_0} \to \mathcal {C} is initial among Markov prefibrations receiving a map from \mathcal {D}_0. In other words, this construction gives a left adjoint to the pullback functor \mathsf {MarkPreFib}(\mathcal {C}) \to \mathsf {Fib}(\mathcal {C}_\mathrm {det})

Proof [efr-0BES]

First observe that, by Lemma [efr-OH7U], the pullback \bar {\mathcal {D}_0}\times _\mathcal {C} \mathcal {C}_\mathrm {det} \to \mathcal {C}_\mathrm {det} is indeed a fibration, with the image of the Cartesian lifts under the functor \mathcal {D}_0 \to \bar {\mathcal {D}_0} being Cartesian again. (This also establishes that \bar {\mathcal {D}_0} really does receive a map of fibrations from \mathcal {D}_0)

Given Cartesian f: \bar {A} \to \bar {B} \leftarrow \bar {C}, and a stochastic lift A \to C (= p\bar {A} \to p\bar {C}), consider the pullback A \times _B C, and the pullback of \bar {A} to it. There is a unique lift of A \to C to a section A \to A \times _B C, and this induces a unique lift \bar {A} \to (f\pi _1)^*\bar {A} using the stochastic module structure. The composite of this with the projection to B is a lift of \bar {A \to \bar {B}} over A \to C, as required by a Markov prefibration.

Analogously to the proof of Lemma [efr-OH7U], given some other lift A \leftarrow N \to C, h: A \to N, h^*\bar {A} \to \bar {C}, the fact this is a factorization implies the existence of some M with maps M \to A, M \to N and a lift A \to M of the section A \to N, so that the induced map between the pullbacks over M and N of \bar {A} makes the triangle into \bar {B} commute. But then since this is a triangle over deterministic bases, this implies the lifted triangle to \bar {C} also commutes, hence this M lifts to another representative of the lift we started with. But then it's not hard to see that this M maps to A \times _B C and exhibits an equation with the previously constructed "canonical" lift.

Hence \bar {\mathcal {D}_0} is a Markov prefibration, and by the above, the induced stochastic module structure on the corepresentable presheaves \bar {\mathcal {D}_0}(\bar {A},-) = T(\mathcal {D}_0(\bar {A},-)) is exactly the one given by T (in other words this equation is not merely a bijection of sets, but an isomorphism of stochastic modules).

Let \phi : \mathcal {D}_0 \to \mathcal {D}' be a functor over \mathcal {C}_\mathrm {det} \to \mathcal {C} into some other Markov prefibration which preserves Cartesian maps. Using the algebra structure on \mathcal {D}'(\phi \bar {B},-), we see there is a unique extension of \phi to \bar {\mathcal {D}_0}(\bar {X},-) which respects the stochastic module structure. By chasing the diagram around it's easy to see that this is functorial, and hence gives a map of Markov prefibrations---conversely, any such map extending \phi must be a stochastic module homomorphism. Thus there is a unique functor, proving initiality.

This characterization of the left adjoint makes it fairly easy to understand the induced monad on \mathsf {Fib}(\mathcal {C}_\mathrm {det}).

Remark [efr-ACIV]

We will sometimes refer to the morphisms of \overline {\mathcal {D}_0} as precharts. Taking the fibration \mathcal {C}^\to |_\mathrm {det} \to \mathcal {C}_\mathrm {det} as an example, it is not too hard to see that the precharts between X \otimes A \to X and B \otimes Y \to Y are representatives of co-optics {A \choose X} \rightrightarrows {B \choose Y}. (To see this, note that any prechart is equivalent to one where the apex of the span has the form M \otimes Y and the right leg is the projection to Y. Then the rest of the data is a map X \to M \otimes Y and a map M \otimes B \to A, since the X-coordiante of the latter map is determined by the span).

In fact their equivalence relation is given by sliding equivalence for deterministic maps (i.e morphisms in \mathsf {Optic}_{\mathcal {C}_\mathrm {det}}(\mathcal {C}_\mathrm {det}, \mathcal {C})). The precharts in \mathcal {D}_0^\mathrm {fop} will be called prelenses. We will speak of the tuple (M, p:M \to X, p':M \to Y, s: X \to M, \phi : p^*\bar {X} \to p^*\bar {Y}) representing a prechart just as a "decorated span (representing ...)". When part of the structure is understood, or can just be left abstracted, we will denote such a decorated span simply by (M,s,\phi ), or even just (M,\phi ). It will be clear from context which part of the structure is being specified.

Proposition [efr-A08L]

Let \mathcal {D}_0 be a fibration. Then the underlying fibration of the free Markov prefibration, \overline {\mathcal {D}_0}|_\mathrm {det}, has fiber over X \in \mathcal {C} given by

  1. Objects are simply objects of \mathcal {D}_{0,X}
  2. A morphism \bar {X} \to \bar {X}' consists of a deterministic f: M \to X, a stochastic section s: X \to M, and a map \phi : f^*\bar {X} \to f^*\bar {X}', up to the equivalence relation generated by, whenever g: N \to M is deterministic and s': X \to N is a factorization of s, identifying (M,f,s,\phi ) with (N,fg, s', g^*(\phi )).
  3. Given two such morphisms (M,f,s,\phi ), (N,f',s',\psi ), their composite is represented by M \times _X N \to X equipped with the section formed as the composite of X \to M and the lift of X \to N to the pullback, and the composite \pi _M^*(\phi )\pi _N^*(\psi ) \in \mathcal {D}_{0,M\times _X N}
  4. Given deterministic f: X \to Y, the pullback is given on such a map by taking the pullback M \times _Y X \to X, the induced section, and the pullback of the map \phi along the projection M \times _Y X \to M

It is immediately obvious that we have:

Corollary [efr-ILIQ]

The free Markov prefibration monad \overline {(-)}|_\mathrm {det} commutes with fiberwise opposites. In particular, algebra structures on \mathcal {D}_0 are in bijection with algebra structures on \mathcal {D}_0^\mathrm {fop}, and fiberwise opposites lifts to an involution of \mathsf {Alg}(\overline {(-)}|_\mathrm {det}).

Definition Stochastic Module Fibration [efr-OEFJ]

Let \mathcal {C} be a pullback-positive Markov category. The adjunction \overline {(-)} \dashv (-)|_\mathrm {det} induces a monad on \mathsf {Fib}(\mathcal {C}_\mathrm {det}). A module for this monad is called a stochastic module over \mathcal {C} (or, to distinguish it from the copresheaves of Definition [efr-Y926], a stochastic module fibration). The category of stochastic module fibrations is denoted \mathsf {SFib}(\mathcal {C})

Let us try to understand the structure of a stochastic module fibration. It is easiest to understand in the case of a projection map P \times X \to X. Suppose we have two objects A,B over X. Then we think of a map f: \pi _X^*A \to \pi _X^*B over P \times X as a map P \times A \to B, that is a map parameterized by P (this is literally the case for a codomain fibration). Given a stochastic section s of \pi _X, which amounts to a stochastic map X \to P, the stochastic module stucture picks out a new map s_*f, which is given over each point x \in X by choosing the parameter according to s, then applying f.

The definition of the composite in Proposition [efr-A08L], in these terms, tells us that given maps f: P \times A \to B, g: Q \times B \to C, and maps s: X \to P, t: X \to Q, the composite of s_*(f) and t_*(q) is equal to the map obtained by forming the parameterized composite Q \times P \times A \to C and applying the independent pairing \langle t,s \rangle : X \to Q \times P. This is of course how composition is supposed to work in a Markov category.

Lemma [efr-VF6V]

Let \mathcal {D} be a stochastic module over \mathcal {C}, and let

be given, so that every map except s,s',t is deterministic. Suppose the deterministic part of the diagram commutes, fs = g, s' is the induced section, and t is a section. Let \bar {A},\bar {B} be two objects over Z. Suppose given a map \phi : f^*\bar {A} \to f^*\bar {B}. Then t^*h^*(P) = (s')^*\pi _Y^*(P) : g^*\bar {A} \to g^*\bar {B}

In particular, this operation depends only on s. Moreover, it is functorial, in the sense that given a diagram

with the downwards maps deterministic, s^*t^* = (ts)^*

Remark [efr-U436]

The operations \alpha ^* associated to stochastic lifts are "functorial" in the sense that (\alpha \beta )^* = \beta ^*\alpha ^*. However they are not functorial in the sense that \alpha ^*(fg) = \alpha ^*(f)\alpha ^*(g)

To make sense of this, consider a simple case of a map m: I \to X in Kl(\Delta ). Given two objects over * (in Kl(\Delta )^\to ), a map \bar {A}_X \to \bar {B}_X is equivalent to a parametrized map X \times \bar {A} \to \bar {B}. The operation m^* consists in sampling this parameter according to the distribution m---but since composition in the fiber over X is defined by copying the parameter, but composition in the fiber over * (i.e just Kl(\Delta )) is defined by composing the kernels under conditional independence, these only agree if the distribution m is assumed to be deterministic.

Note that if either f or g is pulled back from a map \bar {A} \to \bar {B} (i.e, if they do not depend on the parameter X), the composition is preserved.

By construction, two morphisms in \overline {\mathcal {D}}_0 represented by spans with apex M,M', are identified if there exists a zig-zag M \to K_0 \leftarrow K_1 \to \cdots \leftarrow M' of spans (decorated with sections from the domain X and morphisms in the fiber, satisfying equations, etc). We will now prove a lemma that allows us to cut this down to a smaller set in many conditions. We will need the following hypothesis:

Definition Weak conditionals [efr-2MH5]

Let p: \mathcal {D} \to \mathcal {C} be a Markov prefibration. We say p (or, abusing notation, \mathcal {D}) admits weak conditionals if, given a Cartesian map \bar {Y} \to \bar {Z} and any map \bar {X} \to \bar {Z}, the existence part of the Cartesian condition holds---that is, every factorization p(\bar {X}) \to p(\bar {Y}) admits a lift, although not necessarily a unique one.

We say a Markov category \mathcal {C} admits weak conditionals if its codomain functor \mathcal {C}^\to \to \mathcal {C} is a prefibration which admits weak conditionals---this is equivalent to requiring that it is pullback-positive, and that all deterministic pullbacks are carried to weak pullbacks by the inclusion \mathcal {C}_\mathrm {det} \to \mathcal {C} (in other words, that they satisfy the existence part of the universal property even for pairs of nondeterministic maps).

Observe that, if \mathcal {C} admits conditionals, it certainly admits weak conditionals: given a pullback X \times _Z Y, and maps P \to X,Y, form a Bayesian inverse of Y \to Z with respect to the given measure, and use that to build a lifting X \to Y, which gives X \to X \times _Z Y---then a diagram chase verifies that this map has the desired properties.

Lemma [efr-TZ3Y]

Suppose \mathcal {C} admits weak conditionals, and let \mathcal {D} \to \mathcal {C}_\mathrm {det} be a fibration. Then two morphisms f_0,f_1: \bar {X} \to \bar {Y} in \overline {\mathcal {D}}, represented by commutative diagrams

as well as \phi _i: \bar {X}_{M_i} \to \bar {Y}_{M_i}, for i=0,1, are equal if and only if there exists a span M_0 \leftarrow K \to M_1 over X,Y, with a stochastic section X \to K lifting both the sections to M_0,M_1, so that the pullbacks of \phi _0,\phi _1 to K agree.

Proof

The relation here described clearly implies identity, and contains all the generating identities, so it suffices to show it is an equivalence relation. Reflexivity and symmetry are clear, so transitivity is the only issue. It suffices to show that, given a span X \leftarrow S \to Y and maps M_0 \to S \leftarrow M_1 so that the triangles commute, and so that the two induced sections X \to S agree, and a map \bar {X}_S \to \bar {Y}_S which pulls back to \phi _0,\phi _1, we can find K as above.

To do this, take K = M_0 \times _S M_1. Clearly the maps to M_0, M_1 are over X,Y, and by the existence of weak conditionals there exists a common lift of the sections to X \to K. By functoriality of pullbacks, the pullbacks of \phi _0,\phi _1 to K agree.

Markov Fibrations [efr-U4RA]

Recall that, given a functor R: \mathcal {C} \to \mathcal {D} with left adjoint L, there is a "standard resolution" of any object X \in \mathcal {C}, given by the "cofork" LRLRX \rightrightarrows LRX \to X, where the two parallel maps are the two possible applications of the adjunction counit. The adjunction is monadic if and only if this is always a coequalizer, in which case the RL-algebra corresponding to X is RLRX \to RX---conversely, given an algebra \alpha : RLA \to A, there are two parallel maps LRLA \rightrightarrows LA (given by L(\alpha ) and the counit,) and the object in \mathcal {C} corresponding to this algebra is given by this coequalizer.

Example

Consider the adjunction |-|: \mathsf {Mon} \leftrightarrows \mathsf {Set} : (-)^* between the category of monoids and the category of sets. Given a monoid M, |M|^* consists of lists of elements in M, and ||M|^*|^* consists of lists of such lists. The two maps ||M|^*|^* \to |M|^* consist in either concatenating the lists, or replacing each list with its product. Clearly these two maps are coequalized by the product map |M|^* \to M. Moreover it's clear that two lists have the same product if and only if they are identified in this coequalizer (simply consider a singleton list-of-lists, which identifies any given list with the singleton corresponding to its product).

As a generalization of this, if this coequalizer exists for every algebra, they form a left adjoint to the canonical functor \mathcal {C} \to \mathsf {Alg}_\mathcal {D}(RL). Since we have seen that the monad of free Markov prefibrations commutes with taking fiberwise opposites, we may hope that such a left adjoint exists---a simple argument shows that, if it is, it is fully faithful, and we may say that those prefibrations in the image are the "fibrations" and define their fiberwise opposite as the fiberwise opposite applied to their underlying algebras. Although it turns out to not be quite so simple, we will take this idea as our starting point.

Example

Let \mathsf {GrpTop} be the category of topological groups, and let R: \mathsf {GrpTop} \to \mathsf {Set} forget both the group structure and the topology. Clearly this is right adjoint to the free group in the discrete topology, and the monad of this adjunction is the free group monad, which we write RL for now. The canonical comparison functor \mathsf {GrpTop} \to \mathsf {Grp} just forgets the topology. Given a (non-topological) group, described by a map RLG \to G, we can form the diagram of topological groups LRLG \rightrightarrows LG. Here LG is the free, discrete group on G and LRLG is the free discrete group on the underlying set of LG. Their coequalizer is simply G equipped with the discrete topology, which is indeed the left adjoint to \mathsf {GrpTop} \to \mathsf {Grp}

In what follows, we will denote the monad \overline {(-)}|_\mathrm {det} simply by \operatorname {Free} to avoid too many complicated nestings of overlines and parentheses.

Definition Markov Fibration [efr-HVUT]

If \mathcal {D} is a Markov prefibration, we call it a Markov fibration if the diagram \overline {\operatorname {Free}(\mathcal {D}|_\mathrm {det})} \rightrightarrows \overline {\mathcal {D}|_\mathrm {det}} \to \mathcal {D} is a coequalizer in \mathsf {Cat}_{/\mathcal {C}}.

Given an algebra \alpha : \operatorname {Free}(\mathcal {D}_0) \to \mathcal {D}_0 of the free Markov prefibration monad, let \overline {\operatorname {Free}(\mathcal {D}_0)} \rightrightarrows \overline {\mathcal {D}_0} \in \mathsf {MarkPreFib} be as above. We say \alpha presents a Markov fibration if the coequalizer of these maps in \mathsf {Cat}_{/\mathcal {C}} is a Markov prefibration.

The terminology "presents a Markov fibration" is justified by the following proposition.

Proposition [efr-MAUM]

Let \alpha : \operatorname {Free}(\mathcal {D}_0) \to \mathcal {D}_0 be stochastic module which presents a Markov fibration. Then the underlying algebra of the Markov prefibration obtained as the coequalizer of \overline {\operatorname {Free}(\mathcal {D}_0)} \rightrightarrows \bar {\mathcal {D}_0} is isomorphic to \alpha , and in particular this prefibration is a Markov fibration.

This correspondence determines an equivalence of categories between the full subcategory \mathsf {MarkFib}(\mathcal {C}) of \mathsf {MarkPreFib}(\mathcal {C}) spanned by the Markov fibrations, and the full subcategory \mathsf {SFib}(\mathcal {C})^p \subseteq \mathsf {SFib}(\mathcal {C}) spanned by those algebras which present a Markov fibration.

Proof

Let \alpha be an algebra as assumed, and let \mathcal {D}_0^\alpha \in \mathsf {MarkPreFib} denote the coequalizer given. By general nonsense there is an induced functor \mathcal {D}_0 \to \mathcal {D}_0^\alpha |_\mathrm {det} which is moreover an algebra homomorphism---the claim is that this is an isomorphism. By Lemma [efr-L7L2], pullback to the deterministic part preserves these coequalizers, so this amounts to the claim that the diagram \operatorname {Free}^2(\mathcal {D}_0) \rightrightarrows \operatorname {Free}(\mathcal {D}_0) \to \mathcal {D}_0 is a coequalizer. But this is true for any algebra of any monad (in fact, the unit gives a splitting of this coequalizer).

By general nonsense the fibration associated to an algebra which presents a fibration forms a partial left adjoint to \mathsf {MarkPreFib}(\mathcal {C}) \to \mathsf {SFib}(\mathcal {C}). This left adjoint, by the above, has its image inside \mathsf {MarkFib}, and hence there is an adjunction \mathsf {MarkFib}(\mathcal {C}) \leftrightarrows \mathsf {SFib}(\mathcal {C})^p. The preceding furthermore proves that the unit of this adjunction is the identity, which implies that the left adjoint is fully faithful---but by definition it is essentially surjective, finishing the argument.

Let us briefly summarize the relationship between Markov prefibrations, Markov fibrations, and stochastic module fibrations at this stage.

  • A stochastic module fibration is a (Grothendieck) fibration \mathcal {D} over \mathcal {C}_\mathrm {det}, equipped with some extra structure involving the whole category \mathcal {C}. Given a deterministic map f: A \to B two objects X,Y \in \mathcal {D}_B, and a map \phi : f^*X \to f^*Y, we can think of this as a map parameterized by the fibers A_b. Given a stochastic section s: B \to A, the stochastic module structure picks out a map X \to Y \in \mathcal {D}_B corresponding to choosing this parameter randomly according to s.
  • A Markov prefibration is a category \mathcal {D} over \mathcal {C} with a particular unique lifting property. In the above situation, it gives a unique lift X \to f^*X of s, corresponding to choosing a \in A_b according to s and leaving the x \in X-coordinate unchangd. By composing this lift with \phi , then with the Cartesian f^*Y \to Y, we get a stochastic module structure on the part of \mathcal {D} lying over deterministic maps (which is also a Grothendieck fibration).

    • Given a stochastic module structure, there is a way of generating a category over \mathcal {C}, by freely adding the lifts corresponding to a Markov prefibration, then quotienting by the relations implied by the stochastic module structure. This does not necessarily yield a Markov prefibration.

    A Markov prefibration is called a Markov fibration if it is presented by its underlying stochastic module in the above sense.

Definition Weak supports [efr-YFV2]

Let \mathcal {D}_0 \to \mathcal {C}_\mathrm {det} be a stochastic module fibration.

Let \alpha : X \to M be a stochastic section, let \bar {X} \in \mathcal {D}_{0,X} be an object, and let \phi : \bar {X}_M \to \bar {X}_M \in \mathcal {D}_{0,M} be an endomorphism of its pullback. Observe that if there exists f: N \to M so that f^*(\phi ) = 1 and \alpha factors over f, then \alpha _*(\phi ) = 1. We say \mathcal {D}_0 has weak supports if this implication is an equivalence

We will make use of the following lemma:

Lemma [efr-L7L2]

Let F,G: \mathcal {D} \rightrightarrows \mathcal {D}' be a parallel pair in \mathsf {Cat}_{/\mathcal {C}}, and suppose both are identity on objects. Suppose moreover this is a reflexive pair, i.e there is some S: \mathcal {D}' \to \mathcal {D} so that FS = GS = 1_{\mathcal {D}'}. Then the coequalizer in \mathsf {Cat}_{/\mathcal {C}} is again identity on objects, and is given on hom-sets simply by the coequalizer of the parallel pair \mathcal {D}(x,y) \rightrightarrows \mathcal {D}'(x,y)

Proof

The only nontrivial part is to verify that composition is well-defined on the equivalence classes in \mathcal {D}'(x,y)/\sim . It suffices to see that post- and precomposition with a fixed morphism both preserve this equivalence relation. Take some f: x \to y \in \mathcal {C}, and h : y \to z \in \mathcal {C}'. We must show that hF(f) = hG(f). But simply write hF(f) = F(S(h)f) \sim G(S(h)f) = hG(f), and we are done. Clearly the other side follows by duality, finishing the proof.

Proposition Construction of \mathsf {SChart}(\mathcal {D}_0) [efr-TBZZ]

Let \mathcal {D}_0 be a fibration equipped with a stochastic module structure. Consider the equivalence relation on \overline {\mathcal {D}_0}(\bar {X},\bar {Y}) which identifies two precharts (M, \phi ), (N, \phi ') if there exists a map f: N \to M over X,Y and a stochastic section s of f which preserves the section from X, so that s^*\phi ' = \phi (note that this makes sense because pullbacks compose).

Then:

  1. This equivalence relation respects composition, and so defines a category which we denote \mathsf {SChart}(\mathcal {D}_0)
  2. In \mathsf {Cat}_{/\mathcal {C}}, \overline {\operatorname {Free}(\mathcal {D}_0)} \rightrightarrows \overline {\mathcal {D}_0} \to \mathsf {SChart}(\mathcal {D}_0) is a coequalizer diagram. In particular, \mathcal {D}_0 presents a Markov fibration if and only if \mathsf {SChart}(\mathcal {D}_0) is a Markov prefibration (in which case \mathsf {SChart}(\mathcal {D}_0) is the fibration it presents)
  3. If \mathcal {D}_0 has weak supports, \mathsf {SChart}(\mathcal {D}_0) is a prefibration

Proof

Recall that the fibration \operatorname {Free}(\mathcal {D}_0) has fibers whose morphisms \bar {X} \to \bar {X}' are given by tuples s: X \to M: p, p^*\bar {X} \to p^*\bar {X}' (up to a certain equivalence relation). Forming the free Markov prefibration \overline {\operatorname {Free}(\mathcal {D}_0)} on this fibration, we find that the morphisms are given by diagrams

equipped with a map \phi : p^*q^*\bar {X} \to p^*r^*\bar {Y}. The two maps \overline {\operatorname {Free}(\mathcal {D}_0)} \to \overline {\mathcal {D}_0} carry such a thing to first, the map resulting from forgetting M and just composing q,r with p to get a span (and composing the sections to get a new section), and secondly, the map with apex M obtained by using the stochastic module structure to push \phi down into a map over M. It is clear that this is equivalently the equation described in the theorem. This establishes points 1. and 2., since by Lemma [efr-L7L2] we can compute such coequalizers hom-set by hom-set.

Now we wish to prove that \mathsf {SChart}(\mathcal {D}_0) is a Markov prefibration given weak supports. Since by the coequalizer presentation, its deterministic part is isomorphic to \mathcal {D}_0, the fibration property is automatic. It remains to verify that, given a triangle

in \mathcal {C} with the vertical and horizontal maps deterministic, an object \bar {A} \in \mathcal {D}_{0,Y} and Cartesian maps \bar {A}_X \to \bar {A} \leftarrow \bar {A}_Z, there exists a unique lift \bar {A}_X \to \bar {A}_Z in \mathsf {SChart}(\mathcal {D}_0).

Such a lift is given by a diagram

equipped with p^*\bar {A}_X \to q^*\bar {A}_Z. By taking the equalizer of the two maps M \to Y (the section factors over this), we may assume these two are equal, which implies that the pulled-back objects are equal---denote this object \bar {A}_M. Now the hypothesis is that after postcomposing with the Cartesian map \bar {A}_Z \to \bar {A}, this gives the map \bar {A}_X \to \bar {A}. This postcomposition is given simply by postcomposing the leg M \to Z with the map Z \to Y (and observing that, by functoriality of pullbacks, this does not alter the pulled-back object). Then the claim is that integrating this map \bar {A}_M \to \bar {A}_M down into a map \bar {A}_X \to \bar {A}_X, it gives the identity. But by assumption this means we can pull back to some object M' \to M (lifting the section from X) where the two maps are already equal to the identity. But this pull-back can be applied to the original map \bar {A}_X \to \bar {A}_Z as well. But this implies every such map is equal to the one represented by the diagram
and the identity on \bar {A}_{X \otimes Y}, with the map M' \to X \otimes Y giving the witness, since identities pull back. This map only depends on the underlying X \to Y, hence \mathsf {SChart}(\mathcal {D}_0) is indeed a prefibration.

It is not apparent whether weak supports are necessary for \mathsf {SChart}(\mathcal {D}_0) to be a prefibration. We have not found any counterexample, but in general the equivalence relation on charts is fairly complicated, so it is not apparent how to prove the necessity. We will generally not be too bothered about assuming weak supports instead of the more nebulous assumption that \mathcal {D}_0 presents a Markov fibration.

Lemma [efr-26SF]

Let (M,\phi ) and (N,\psi ) be two representatives of charts. Given some possibly stochastic map f: M \to N over X and Y, recall (Lemma [efr-VF6V]) that we can define f^*\psi , regardless of whether f is deterministic or the section of a deterministic map. If there exists such a map f, we can always factor it over the pullback M \times _{X \times Y} N as a section followed by a deterministic map. Hence the equivalence relation defining \mathsf {SChart} is equivalent to the relation identifying two representatives whenever there exists such an f with f^*\psi = \phi

Remark [efr-XZRN]

By construction, for each Markov prefibration \mathcal {D}, there is a canonical functor \mathsf {SChart}(\mathcal {D}|_\mathrm {det}) \to \mathcal {D} over \mathcal {C}, which restricts to an isomorphism on the deterministic part (and in particular preserves Cartesian morphisms). \mathcal {D} is a Markov fibration if and only if this is an isomorphism.

Also by construction, given a morphism of stochastic modules F: \mathcal {D}_0 \to \mathcal {D}_0', there is an induced functor \mathsf {SChart}(\mathcal {D}) \to \mathsf {SChart}(\mathcal {D}') over \mathcal {C}. This restricts to F on the deterministic part and in particular preserves Cartesian morphisms.

Proposition [efr-1YS9]

Let \mathcal {D}_0 be a stochastic module fibration. Then \mathcal {D}_0 presents a Markov fibration if and only if \mathcal {D}_0^\mathrm {fop} does it.

Proof

Consider a triangle of this for in \mathcal {C}:

where the maps to Z are deterministic. Suppose given Cartesian lifts \bar {X} \to \bar {Z}, \bar {Y} \to \bar {Z} of the cospan. These are the same in both cases, coming from Cartesian maps in \mathcal {D}_0 \mathcal {D}_0^\mathrm {fop} (which are the same). We must show that there is a unique lift of f to a chart in \mathsf {SChart}(\mathcal {D}_0) if and only if there is a unique lift to a chart in \mathsf {SChart}(\mathcal {D}_0^\mathrm {fop}). Clearly it suffices to prove the "only if" implication, so suppose \mathsf {SChart}(\mathcal {D}_0) is a prefibration.

By passing to the equalizer as in the proof that \overline {\mathcal {D}_0} is a prefibration, we may assume that any such lift is represented by a diagram

where the outer square and the triangle X \to M \to Y commutes, and f' is a section.

Take such a diagram and let \phi : \bar {Z}_M \to \bar {Z}_M be the map representing a chart. Then the claim is there exists some zig-zag of chart equivalences identifying (M,\phi ) with (M,1). But clearly this is invariant under passing to the fiberwise opposite, and so \mathcal {D}^\mathrm {fop} is also a prefibration.

Definition Stochastic charts and lenses [efr-ANBC]

We refer to \mathsf {SChart}(\mathcal {D}_0) as the category of stochastic charts in \mathcal {D}_0. We refer to \mathsf {SChart}(\mathcal {D}_0^\mathrm {fop}) as stochastic lenses and denote it also \mathsf {SLens}(\mathcal {D}_0)

Example [efr-IAFO]

Kl(\Delta )^\to is a Markov fibration. We have already seen that it is a Markov prefibration, and that the map from the coreflection is full. So it suffices to prove faithfulness. Consider a map in {Kl(\Delta )^\to |_\mathrm {det}}, given by a diagram

We can factor the section X \to M as X \to X \times Y \to M, where the first map is just the pairing and the second is a conditional distribution. This induces a factorization of the lift \bar {X} \to M \times _X \bar {X} over \bar {X} \to \bar {X} \times Y. By composing the map M \times _X \bar {X} \to \bar {Y} with this factorization to build the map \bar {X} \times Y \to \bar {Y}, we have found a new representative for the same map.

Hence every map over X \to Y has a representative where the residual is X \times Y. We would like to argue that, since the map \bar {X} \times Y \to \bar {Y} is given by the conditional distribution of the composite map \bar {X} \to \bar {Y}, it is uniquely determined by it, and thus if two distinct maps in \overline {Kl(\Delta )^\to |_\mathrm {det}} have the same underlying map in Kl(\Delta )^\to , they must have equal representatives of this form, and so be identified in the coreflection (which must therefore be isomorphic to Kl(\Delta )^\to ). But of course, the two maps may only be almost certainly equal.

In this case, there is a simple fix: instead of taking X \times Y as the residual, take the subset S given by those pairs (x,y) where y has positive probability given x. The pairing factors over this, of course, and two maps \bar {X} \times _X S \to \bar {Y} which give the same distribution \bar {X} \to \bar {Y} really must have the same value on every point. This proves that \mathsf {SChart}(Kl(\Delta )^\to ) \to (Kl(\Delta ))^\to is faithful and hence an isomorphism.

Example [efr-C5RE]

\mathsf {BorelStoch}^\to , as we have noted, is a Markov prefibration, and hence induces a stochastic module structure on \mathsf {BorelStoch}^\to |_\mathrm {det}. This structure does not present a Markov fibration. To see this, note that in that case its fiberwise opposite would also present a Markov fibration. Then this fibration, \mathsf {SLens}(\mathsf {BorelStoch}^\to |_\mathrm {det}), would be a prefibration whose deterministic part was \mathsf {BorelStoch}^\to |_\mathrm {det}^\mathrm {fop}. But Example [efr-8B5X] shows that this is impossible.

Proposition [efr-8SXB]

Let \mathcal {C} be a Markov category with supports. Then the stochastic module induced by \mathcal {C}^\to \to \mathcal {C} presents a Markov fibration. If \mathcal {C} has conditionals, this Markov fibration is isomorphic to \mathcal {C}^\to .

Proof

Given a section s: X \to M:p and \phi : A \times _X M \to A \times _X A, simply take the pullback to the support of s. It must be the case that \phi (a,m) = (a,m) s-almost surely, which implies strict equality on the support. Hence by Proposition [efr-TBZZ], \mathcal {C}^\to presents a Markov fibration.

There is an induced map \mathsf {SChart}(\mathcal {C}^\to |_\mathrm {det}) \to \mathcal {C}^\to , which we claim is an isomorphism. So consider a map in \mathcal {C}^\to :

This map is in the image of
where the map \bar {X} \times Y \to \bar {Y} is taken to be a conditional. Note that every map in \mathsf {SChart}(\mathcal {C}^\to |_\mathrm {det}) can be represented in this form, by taking a conditional of M given Y to build a section to M \to X \otimes Y. Since conditionals are almost-surely equal, by restricting to the support of X \to X \otimes Y, we can find a representative which only depends on the overall map \bar {X} \to \bar {Y}, which proves that the map from \mathsf {SChart} is faithful, concluding the proof.

Continuing from Example [efr-CJTH], we have the following trivial case:

Proposition [efr-Z75A]

If \mathcal {C} is Cartesian (even if it does not admit pullbacks), the definition of Markov fibration over \mathcal {C} still makes sense, the Markov fibrations are exactly the Grothendieck fibrations, and their fiberwise opposites are simply their fiberwise opposites in the usual sense.

Proof

This is trivial because \mathsf {MarkPreFib}(\mathcal {C}) \to \mathsf {Fib}(\mathcal {C}_\mathrm {det} = \mathcal {C}) is simply the identity functor, hence it is monadic (with the identity monad,) hence every fibration/prefibration presents a Markov fibration, namely itself, and is in particular a Markov fibration. The fiberwise opposite is simply given by applying the identity (taking the stochastic module on the deterministic part), taking the fiberwise opposite, then applying the identity again (passing to the presented markov fibration).

It is worth noting that, even in the case where \mathsf {SChart}(\mathcal {D}_0^\mathrm {fop}) is not a prefibration, it may still deserve the name "stochastic lenses". For example the stochastic lenses in \mathsf {BorelStoch} can be seen to contain \mathsf {Optic}(\mathsf {BorelStoch}) as a full subcategory, even though it does not form a Markov fibration (see Theorem [efr-K6NM] below).

Part of the motivation for the theory of dependent optics is to identify a category of stochastic optics which admits all coproducts. If \mathcal {C} is distributive, \mathsf {Optic}(\mathcal {C}) satisfies \binom {A}{X} + \binom {A}{Y} = \binom {A}{X+Y}, but this coproduct fails to exist in general if the two secondary objects are distinct. The idea is that this coproduct \binom {A}{X} + \binom {A'}{Y} should exist as a family indexed by X + Y, where E_x = A for x \in X, and E_y = A' for y \in Y. Our theory accommodates this example under the mild additional hypothesis of extensiveness

Definition Extensive Markov Category [efr-B2P7]

A Markov category is said to be an extensive Markov category if it admits finite coproducts, whose injections are deterministic, and which satisfy the following equivalent conditions:

  1. If we let \mathcal {C}_{/a}^\mathrm {det} refer to the full subcategory of the slice spanned by the deterministic morphism x \to a, we have an equivalence of categories \mathcal {C}_{/a}^\mathrm {det} \times \mathcal {C}_{/b}^\mathrm {det} \cong \mathcal {C}_{/a + b}^\mathrm {det}, given by taking coproducts
  2. \mathcal {C}_\mathrm {det} is an extensive category in the usual sense and the inclusion \mathcal {C}_\mathrm {det} \to \mathcal {C} preserves pullbacks along coproduct inclusions.

More generally, for an infinite regular cardinal \kappa , we say that \mathcal {C} is \kappa -extensive if \mathcal {C}_\mathrm {det} is a \kappa -extensive category in the ordinary sense and both coproduct inclusions and pullbacks along them are preserved by the functor \mathcal {C}_\mathrm {det} \to \mathcal {C}.

Proposition [efr-QAV2]

Let \mathcal {C} be an extensive Markov category, let \mathcal {D}_0 \to \mathcal {C}_\mathrm {det} be a fibration which satisfies \mathcal {D}_{0,X+Y} = \mathcal {D}_{0,X} \times \mathcal {D}_{0,Y}. Note that this implies \mathcal {D}_0 admits finite coproducts, and they're given exactly by this pairing. Suppose \mathcal {D}_0 is equipped with a stochastic module structure. Then \mathcal {D}_0 \hookrightarrow \mathsf {SChart}(\mathcal {D}_0) preserves the finite coproducts. In particular, \mathcal {D}_0^\mathrm {fop} has the same coproducts as \mathcal {D}_0, and \mathcal {D}_0^\mathrm {fop} \to \mathsf {SLens}(\mathcal {D}_0) preserves them as well.

Proof

This is straightforward to check---the residual M \to X_1 + X_2 splits into M_1 + M_2 by extensivity of \mathcal {C}, which also implies the section must split as the copairing of a section s_1: X_1 \to M_1, s_2: X_2 \to M_2. By the condition on the fibration, the map in the fiber over M splits into a map over M_1 and a map over M_2. Using the extensivity again, it is straightforward to see that this decomposition respects the equivalence relation.

In particular, \mathsf {SChart}(\mathcal {C}^\to |_\mathrm {det}), \mathsf {SLens}(\mathcal {C}^\to |_\mathrm {det}) both admit coproducts given simply as coproducts in \mathcal {C}^\to , if \mathcal {C} is extensive.

Proposition [efr-XFAO]

Suppose \mathcal {D} is a Markov fibration so that each pullback functor f^*: \mathcal {D}_Y \to \mathcal {D}_X for f: X \to Y \in \mathcal {C}_\mathrm {det} can be taken to be bijective on objects, and that these can furthermore be chosen strictly functorial (so that (fg)^* = g^*f^*). Then, writing objects \bar {X} \in \mathcal {D}_X as \binom {A \in \mathcal {D}_*}{X \in \mathcal {C}}, where A is the unique object in \mathcal {D}_* which pulls back to \bar {X} under the deletion X \to *, (note that this means f^*\binom {A}{Y} = \binom {A}{X}) we may characterize the fiberwise dual as having hom-sets \mathcal {D}^{\mathrm {fop}}(\binom {A}{X},\binom {B}{Y}) = \mathcal {D}(\binom {B}{X},\binom {A}{Y})

Proof

The correspondence in both directions is obvious by just formally reversing the direction of the map f: \binom {A}{M} \to \binom {B}{M} in a representing tuple X \leftarrow M \to Y, a: X \to M, f---the fact that this assignment respects the equivalence relation follows from the fact that the monad preserves fiberwise opposites.

Limits of Markov fibrations [efr-HWAZ]

The class of fibrations is stable under pullback. This turns \mathsf {Fib}(-) into an indexed category, which represents a fibration over \mathsf {Cat}---this is the "global" category of fibrations \mathsf {Fib}, whose objects are fibrations \mathcal {D} \to \mathcal {C}, and whose morphisms are commutative squares

where the top map preserves Cartesian morphisms.

By considering universal constructions like limits and colimits in \mathsf {Fib}, additional fibrations can be constructed. It would similarly be useful to study limits in the category of Markov fibrations. Moreover, the products in \mathsf {Fib} allow one to express notions of internal pseudomonoid---these turn out to be monoidal fibrations, and this is a key part of Moeller and Vasilakopoulou's treatment of the monoidal Grothendieck construction, Reference [moeller-vasilakopoulou]. Since we want to study monoidal Markov fibrations, we should study their limits.

Lemma [efr-9VAH]

Let \mathcal {D} \to \mathcal {C} be a Markov prefibration, and let F: \mathcal {C}' \to \mathcal {C} be any functor from another Markov category which preserves deterministic maps. Then the pullback \mathcal {D}' = \mathcal {D} \times _{\mathcal {C}} \mathcal {C}' \to \mathcal {C}' is again a Markov prefibration, and the functor \mathcal {D}' \to \mathcal {D} preserves Cartesian maps.

Proof

Since pullbacks compose, \mathcal {D}'|_\mathrm {det} \to \mathcal {C}'_\mathrm {det} is the pullback of \mathcal {D}|_\mathrm {det} along \mathcal {C}'_\mathrm {det} \to \mathcal {C}_\mathrm {det}. Since fibrations are stable under pullback, this is a fibration.

Now consider a triangle in \mathcal {C}':

with X, A \to B deterministic, and let \bar {B}_X \to \bar {B} \leftarrow \bar {B}_A be Cartesian maps lying over these. We must show there is a unique lift \bar {f}: \bar {B}_X \to \bar {B}_A rendering the lifted triangle commutative. By definition, to give such a morphism is to given one over F(f), and the triangle commutes if and only if its image in \mathcal {D} commutes.

The triangle in \mathcal {C}' goes to a triangle of the same class in \mathcal {C}, and the Cartesian maps go to Cartesian maps of the same type. Hence there is a unique lift of F(f) of the given type, which is exactly what we needed to show.

Remark [efr-Z8X4]

Given any functor F: \mathcal {C} \to \mathcal {C}' between Markov categories, we may attempt to define an oplax monoidal structure F(X \otimes Y) \to F(X) \otimes F(Y) by pairing the projections.

This is not necessarily a natural transformation. However, if it is, F it automatically equips F with the structure of an oplax monoidal functor. Recall that oplax monoidal functors carry comonoids to comonoids. An oplax monoidal functor between Markov categories preserves the given comonoids if and only if it is induced like this.

Hence, there is at most one way to equip a functor between Markov categories with such a structure---it is a property, not extra structure. Call such a functor an oplax Markov functor. Note that oplax Markov functors preserve deterministic morphisms.

(Fritz Reference [fritz-synthetic-markov-cats] defines a Markov functor to be a strong monoidal functor which preserves the comonoids. Clearly this is a proper subset of our oplax markov functors.)

Definition [efr-FNYQ]

We will denote by \mathsf {MarkPreFib} the category whose objects are Markov prefibrations \mathcal {D} \to \mathcal {C}, and whose functors are commutative squares

where \bar {F} preserves Cartesian maps, and F is an oplax Markov functor.

We will let \mathsf {Markov}^\mathrm {oplax} denote the category of Markov categories and oplax Markov functors. Note that by Lemma [efr-9VAH], the forgetful functor \mathsf {MarkPreFib} \to \mathsf {Markov}^\mathrm {oplax} is a fibration.

There is an obvious functor \mathsf {MarkPreFib} \to \mathsf {Fib} \times _\mathsf {Cat} \mathsf {Markov}^\mathrm {oplax}, which carries a prefibration to the pair of its Markov category and its underlying fibration onto the deterministic part. On each fiber, this admits a left adjoint, as constructed in § [efr-GO6R]. By abstract nonsense these left adjoints commute laxly with the pullbacks---that is, given an oplax Markov functor f: \mathcal {C} \to \mathcal {C}' and a map of fibrations \mathcal {D} \to \mathcal {D}' over the deterministic part, there is an induced functor \overline {\mathcal {D}} \to \overline {\mathcal {D}'} over f, although this assignment does not preserve Cartesian squares.

However this does give a functor \mathsf {Fib} \times _\mathsf {Cat} \mathsf {Markov}^\mathrm {oplax} \to \mathsf {MarkPreFib}, left adjoint to the restriction. The category of algebras over this monad is fibred over \mathsf {Markov}^\mathrm {oplax}, with each fiber being the category of stochastic modules over that markov category, and we get a global functor from \mathsf {MarkPreFib}. In the same way, we get a global functor \mathsf {SChart}(-) to \mathsf {Cat}^\to which carries each stochastic module \mathcal {D}_0 \to \mathcal {C}_\mathrm {det} \to \mathcal {C} to the functor \mathsf {SChart}(\mathcal {D}_0) \to \mathcal {C}

We would like to study the limits in here. At this point, we are forced to consider for a moment a bit of higher category theory. Structures on a category defined "up to isomorphism" generally don't play well together with limits in the category \mathsf {Cat}, since they are defined "up to equality". For example, we cannot infer from the fact that \mathcal {C},\mathcal {D} have products and the functors F,G: \mathcal {C} \rightrightarrows \mathcal {D} preserve them that the equalizer of F,G has products, since given A,B in the equalizer, we have F(A \times B) \cong G(A \times B), but not necessarily equality!

For the moment we will restrict ourselves to limits of strict (and in particular, strong) monoidal Markov functors, since these always exist. In general one should probably consider some form of homotopy limit, but we will not go into that now. We clearly have:

Proposition [efr-OMMA]

Let \mathsf {Markov}_s \subseteq \mathsf {Markov}^\mathrm {oplax} denote the subcategory of strictly monoidal Markov functors (i.e those where the oplaxator F(X \otimes Y) \to F(X) \otimes F(Y) is the identity).

  1. \mathsf {Markov}_s and \mathsf {Markov}^\mathrm {oplax} admit all products, computed simply as products in \mathsf {Cat}.
  2. \mathsf {Markov}_s admits all finite limits, and these are preserved by the inclusion into \mathsf {Markov}^\mathrm {oplax}

Proposition [efr-G0AN]

The category \mathsf {MarkPreFib}(\mathcal {C}) admits all products, and pullbacks along isofibrations. These are simply computed as limits in \mathsf {Cat}_{/\mathcal {C}}

Proof

It is immediately apparent that products (that is, pullbacks over \mathcal {C}) of prefibrations are again prefibrations, since the Cartesian lifts can simply be computed coordinatewise, and the uniqueness property checked coordinatewise.

Let \mathcal {D} \times _\mathcal {E} \mathcal {D}' be a pullback of Markov prefibrations, with \mathcal {D} \to \mathcal {E} an isofibration. (Note that their pullback in \mathsf {Cat}_{/\mathcal {C}} is simply their pullback in \mathsf {Cat}). First note that since limits commute, the deterministic part is given by \mathcal {D}_\mathrm {det} \times _{\mathcal {E}_\mathrm {det}} \mathcal {D}'_\mathrm {det}. Thus to prove this is a fibration, it suffices to note that fibrations are stable under pullback along isofibrations. Given f: X \to Y \in \mathcal {C} and two lifts \bar {Y},\bar {Y}' which are identified in \bar {E}, we get two Cartesian lifts f^*\bar {Y} \to \bar {Y}, f^*\bar {Y}' \to \bar {Y}'. These go to two Cartesian lifts in \mathcal {E}, and are therefore identified up to isomorphism, but we can lift this isomorphism to \mathcal {D} and obtain a pair of lifts in the strict pullback---this is a Cartesian lift.

Since Cartesian lifts are given by pointwise Cartesian lifts, given a triangle X \to Y \leftarrow Z and a stochastic lift X \to Y, we have a unique lift in both \mathcal {D}, \mathcal {D}'. These both go to lifts in \mathcal {E}---since such a lift is also unique, they are identified. Hence there is a unique lift in the pullback.

Proposition [efr-FXBP]

The functor \overline {(-)}: \mathsf {Fib} \times _\mathsf {Cat} \mathsf {Markov}^\mathrm {oplax} \to \mathsf {MarkPreFib} preserves products.

For each Markov category \mathcal {C} with weak conditionals, \overline {(-)}: \mathsf {Fib}(\mathcal {C}_\mathrm {det}) \to \mathsf {MarkPreFib}(\mathcal {C}) preserves the terminal object, and pullbacks along isofibrations.

Proof

The product-preservation is clear from the description of \overline {(-)}. Let \mathcal {C} admit weak conditionals. It suffices to show that \overline {(-)} preserves the terminal object and pullbacks in \mathsf {Fib}(\mathcal {C}_\mathrm {det})

The terminal fibration is \mathcal {C}_\mathrm {det} \to \mathcal {C}_\mathrm {det}. Clearly the terminal Markov prefibration is \mathcal {C} \to \mathcal {C}, so we must show that \overline {\mathcal {C}_\mathrm {det}} \to \mathcal {C} is an isomorphism.

Its morphisms are simply spans X \leftarrow M \to Y with the left leg equipped with a stochastic section s:X \to M, which goes to the composite X \to Y. As noted before, this is clearly full, by taking M = X \otimes Y, and faithful because the pairing M \to X \otimes Y exhibits the equality of this canonical representative with any other.

Now let \mathcal {D} \to \mathcal {E} \leftarrow \mathcal {D}' be a cospan of fibrations over \mathcal {C}_\mathrm {det}, with \mathcal {D} \to \mathcal {E} an isofibration, and consider the pullback \mathcal {D} \times _\mathcal {E} \mathcal {D}'. There is a natural transformation \overline {\mathcal {D} \times _\mathcal {E} \mathcal {D}'} \to \overline {\mathcal {D}} \times _{\overline {\mathcal {E}}} \overline {\mathcal {D}'} which we must show to be an isomorphism.

Maps on the left-hand side are given by a span X \leftarrow M \to Y, a stochastic section X \to M, and a map in the pullback of the fibers \mathcal {D}_M \times _{\mathcal {E}_M} \mathcal {D}'_M. A map on the right-hand side is given by two spans each equipped with a map, so that they become identified in \overline {\mathcal {E}}. Let the apexes of the two spans be M, M'. It suffices to consider the case of a span M \leftarrow K \to M' with a common lifting X \to K, so that the pullbacks of the two maps to \mathcal {E}_K agree. But then the original maps may also be pulled back to have K as the underlying span, and thus are in the completion of the pullback.

Similarly, given two maps which become identified in the image, we can again use the identifying maps in \mathcal {C} to identify the original maps, proving faithfulness. This finishes the proof.

Proposition [efr-TZ9L]

For any (pullback-positive) \mathcal {C}, the monad \overline {(-)}|_\mathrm {det} on \mathsf {Fib}(\mathcal {C}_\mathrm {det}) preserves products.

Proof

There is a canonical map \overline {\mathcal {D} \times _\mathcal {C} \mathcal {D}'}|_\mathrm {det} \to \bar {\mathcal {D}}|_\mathrm {det} \times _\mathcal {C} \bar {\mathcal {D}}|_\mathrm {det}. Clearly the deterministic parts are both isomorphic to \mathcal {D} \times _\mathcal {C} \mathcal {D}', and so on this part it is an isomorphism---in particular, bijective on objects. To see it is full, consider an morphism in the codomain, given by a pair of maps M', M \to X, sections s: X \to M, s': X\to M', and maps \phi ,\phi ' in \mathcal {D}_M, \mathcal {D}'_{M'}. Then this pair is equivalent to M \times _X M' equipped with the pairing \langle s,s' \rangle : X \to M \times _X M' and the pullbacks of \phi ,\phi ', which is in the image. Given two maps M \to N, M' \to N' witnessing equations with another pair of maps, it's easy to see that this lifts to a map M \times _X M' \to N \times _X N' witnessing the identity between these, so it's faithful. This concludes the proof.

Lemma [efr-UF7B]

The property of having weak supports is stable under equalizers in stochastic module fibrations over \mathcal {C}. If \mathcal {C} has weak conditionals, it is also stable under finite products (hence all finite limits).

Proof

(Note that stochastic modules themselves do not admit all finite limits, requiring some sort of isofibration property---we merely claim here that if the limit exists, it again admits weak supports)

It is clear that the terminal object 1_\mathcal {C}: \mathcal {C} \to \mathcal {C} has weak supports (regardless of \mathcal {C}). Given an equalizer \mathcal {E} \hookrightarrow \mathcal {D} \rightrightarrows \mathcal {D}', if M \to X is a deterministic map with a stochastic section and \phi : \bar {X}_M \to \bar {X}_M is a map in \mathcal {E}_M which goes to the identity in \mathcal {E}_X, find a factorization X \to N \to M so that the image in \mathcal {D} pulls back to the identity over N. Then clearly the same is true for \phi itself.

Now consider a product \mathcal {D} \times _{\mathcal {C}} \mathcal {D}'. The point is that given a pair of maps that go to the identity, we can find N_0 \to M, N_1 \to M where the pullbacks are the identity. We form the pullback N_0 \times _M N_1, and use the weak conditionals to find a common lift of the two given sections to this. This gives the required weak supports.

Monoidal Markov Fibrations [efr-LTEL]

Recall that if \mathcal {C} is symmetric monoidal, \mathsf {Optic}(\mathcal {C}) inherits a symmetric monoidal structure. At the same time, if \mathcal {D} \to \mathcal {C} is a monoidal fibration, the fiberwise opposite retains a monoidal structure. Since these monoidal structures play an important role both in compositional game theory (where it would not be much of an exaggeration to say the entire point is to use string diagrammatic syntax to work with games) and in categorical systems theory, it is clearly important to understand the monoidal structure on Markov fibrations. Luckily, as we will see in this section, there are essentially no difficulties in accounting for the monoidal structure.

The theory of monoidal fibrations has been developed by Moeller and Vasilakopoulou, Reference [moeller-vasilakopoulou], and Shulman Reference [shulman-monfibs]. We briefly sketch it here for convenience. There are essentially two available notions of monoidal fibration:

  1. For any category \mathcal {C}, the 2-category \mathsf {Fib}(\mathcal {C}) admits products, and we can ask for an internal pseudomonoid in this 2-category. This is equivalent to asking for a functor \mathcal {C}^\mathrm {op} \to \mathsf {MonCat}---in other words, for a monoidal structure on each fiber so that the base-change functors become (strong) monoidal.
  2. The global category of fibrations \mathsf {Fib} admits products, and we may ask for an internal pseudomonoid here. This is what Shulman calls a monoidal fibration: a fibration where \mathcal {D}, \mathcal {C} both come equipped with monoidal structures, the fibration is a strict monoidal functor, and Cartesian maps are stable under monoidal product.

By a result of Moeller and Vasilakopoulou, these notions coincide in the case where \mathcal {C} is Cartesian monoidal. Since we are only interested in ordinary fibrations over \mathcal {C}_\mathrm {det}, which is indeed Cartesian, we may apply this result. However, our notion of monoidal Markov fibration will be a modified version of the latter.

Definition Monoidal markov prefibration [efr-CSLQ]

A monoidal Markov prefibration is a markov prefibration p: \mathcal {D} \to \mathcal {C} equipped with a monoidal category structure on \mathcal {D} so that p is strict monoidal and so that the underlying fibration is a monoidal fibration (i.e so that p preserves Cartesian lifts).

A braided or symmetric monoidal Markov prefibration is a monoidal prefibration equipped with a braiding or symmetry on \mathcal {D} so that p is moreover a braided monoidal functor.

Note that a monoidal Markov prefibration is the same thing as an internal pseudomonoid in the global category of prefibrations. We will not delve further into this point, however.

We will need this lemma:

Lemma [efr-7GH5]

Let F,G: \mathcal {C}' \rightrightarrows \mathcal {C}, S: \mathcal {C} \to \mathcal {C}' be a reflexive pair of identity-on-objects, strict monoidal functors. Let E: \mathcal {C} \to \mathcal {D} be the coequalizer in \mathsf {Cat}. Then \mathcal {D} inherits a monoidal structure making E strict monoidal. Moreover, if \mathcal {C} is symmetric or braided, \mathcal {D} inherits this structure making E a braided functor.

Proof

The only thing to check is that the equivalence relation on morphisms is stable under tensoring. But this is clear: let f : X \to Y \in \mathcal {C}', g: A \to B \in \mathcal {C}. Then f \otimes S(g) witnesses the identification of F(f) \otimes g and G(f) \otimes g. Tensoring on the right is analogous. This finishes the proof for the monoidal structure.

In the braided or symmetric case, it is clear that the image of the braiding of \mathcal {C} in \mathcal {D} becomes a braiding on \mathcal {D} it clearly satisfies the coherence equations (being a quotient), and naturality follows by simply choosing representatives and noting that the tensor in \mathcal {D} is defined by tensoring representatives in \mathcal {C}. Finally if \mathcal {C} is symmetric clearly the equation \sigma _{A,B}\sigma _{B,A} = 1 passes to \mathcal {D}.

Theorem [efr-85DX]
  1. The free prefibration monad on \mathsf {Fib}(\mathcal {C}_\mathrm {det}) has a canonical lifting to \mathsf {MonFib}(\mathcal {C}_\mathrm {det})
  2. Given a monoidal prefibration, its underlying stochastic module acquires the structure of an algebra of this lifted monad.
  3. Given an algebra for the lifted monad \mathcal {D}_0, \mathsf {SChart}(\mathcal {D}_0) acquires a monoidal structure so that \mathsf {SChart}(\mathcal {D}_0) \to \mathcal {C} is a strict monoidal functor.
  4. If \mathcal {D}_0 moreover has weak supports, this forgetful functor is a monoidal prefibration.

    5. Every statement holds also for braided or symmetric fibrations.

Proof

By Reference [moeller-vasilakopoulou], \mathsf {MonFib}(\mathcal {C}_\mathrm {det}) is equivalent to the category of pseudomonoids in \mathsf {Fib}(\mathcal {C}_det). Since the monad preserves products, it must preserve pseudomonoids, which is all we need.

Now suppose \mathcal {D} \to \mathcal {C} is a monoidal prefibration. Then its underlying fibration is a monoidal fibration, hence an object of \mathsf {MonFib}(\mathcal {C}_\mathrm {det}). The claim is that the functor \overline {\mathcal {D}|_\mathrm {det}}|_\mathrm {det} \to \mathcal {D}|_\mathrm {det} is monoidal. The induced monoidal structure is given on objects by \otimes _\mathcal {D} and takes a pair of morphisms in the fiber represented by sections (s: X \to M, \phi : \bar {X_0}_M) \to \bar {X_1}_M and s': X \to M', \phi ': \bar {X'_0}_M \to \bar {X'_1}_M to \langle s,s' \rangle : X \to M \times _X M', \pi _M^*\phi \otimes _\mathcal {D} \pi _{M'}^*\phi '. Recalling that the algebra structure is defined by taking (s,\phi ) to the composite \bar {X_0} \to \bar {X_0}_M \xrightarrow {\phi } \bar {X_1}_M \to \bar {X_1}, and chasing the below diagram around, it is apparent that the algebra structure preserves the monoidal structure.

Now let \mathcal {D}_0 be a monoidal stochastic module in this sense. It suffices to show that the free prefibration \overline {\mathcal {D}_0} is a monoidal prefibration, by Lemma [efr-7GH5], and the induced functor \mathsf {SChart}(\mathcal {D}_0) \to \mathcal {C} will clearly be strict monoidal if \overline {\mathcal {D}_0} \to \mathcal {C} is.

To construct this monoidal structure on \mathcal {D}_0, simply note that since \overline {(-)} preserves global limits as well, there is an induced monoidal structure on \overline {\mathcal {D}_0} so that the forgetful functor is strict monoidal. Recalling that the Cartesian lifts of f: X \to Y \in \mathcal {C} to \overline {\mathcal {D}_0} are given by the span X = X \to Y and the morphism 1_{f^*\bar {Y}}, it is easy to see by unwinding the definition that these are stable under tensor.

If \mathcal {D}_0 has weak supports, we have already proven that \mathsf {SChart}(\mathcal {D}_0) \to \mathcal {C} is a strict monoidal functor, and weak supports are equivalent to the claim that it is a prefibration. Since the Cartesian lifts are just the equivalence classes of the Cartesian lifts in \overline {\mathcal {D}_0}, the preceding claim that they are stable under tensor implies the same for \mathsf {SChart}(\mathcal {D}_0), finishing the proof.

The last point is mostly trivial. The product preservation still establishes the lifting to \mathsf {BrMonFib}(\mathcal {C}_\mathrm {det}) and \mathsf {SymMonFib}(\mathcal {C}_\mathrm {det}). Given a braided or symmetric monoidal prefibration, the braidings are Cartesian and in the deterministic part, so the underlying fibration is braided/symmetric and they are preserves by the stochastic module structure. The braiding/symmetry on \mathsf {SChart} follows again from Lemma [efr-7GH5], and there is nothing to show for the last point.

Definition Monoidal Markov fibration [efr-T9F4]

A monoidal Markov fibration is a monoidal prefibration \mathcal {D} \to \mathcal {C} which is a Markov fibration. It is braided or symmetric if it is braided or symmetric as a prefibration

Remark [efr-KMX6]

Since \overline {(-)} preserves both global products and fiberwise ones, it induces both a fiberwise monoidal structure and a "global" monoidal structure on \overline {\mathcal {D}_0}. Here we only use the global one. If \mathcal {C} were Cartesian, the global one would be induced from the local one by, given maps \bar {X_1} \to \bar {X_2}, \bar {Y_1} \to \bar {Y_2}, pulling each of them back along the square

(and the analogous one for Y) and tensoring them over X_1\otimes Y_1. In a Markov prefibration, of course, these pullbacks are not unique unless X_1 \to X_2 is deterministic, but there are "canonical" lifts given by tensoring globally with the (fiberwise) unit map over Y_1 \to Y_2, and the global tensor is indeed given by the tensor of these canonical lifts (this doesn't provide a noncircular definition of the global tensor, of course). This provides a consistency relation between the two tensor products. Again, we will not dwell on this point.

Proposition Markov structure on stochastic charts [efr-P4T0]

Let \mathcal {D} be a monoidal stochastic module fibration over \mathcal {C} and suppose each fiber \mathcal {D}_X is a Markov category, and this structure is preserved by the pullback functors f^*. Then \mathsf {SChart}(\mathcal {D}) carries the structure of a Markov category, so that \mathsf {SChart}(\mathcal {D}) \to \mathcal {C} is a Markov functor.

If \mathcal {D} \to \mathcal {C} is a Markov prefibration which is also a strict Markov functor, the induced monoidal structure on \mathcal {D}|_\mathrm {det} acquires a fiberwise Markov structure.

Proof

Every equation in the definition of Markov category involves only deterministic maps, so this can be verified entirely over \mathcal {C}_\mathrm {det}. Thus this reduces to the claim: given a monoidal fibration over a Cartesian base, if each fiber has a Markov structure, the global monoidal structure has one as well. Given an object \bar {X} = {\bar {X} \choose X}, a map \bar {X} \to \bar {X} \otimes \bar {X} is by definition a map f: X \to X \otimes X plus a map \bar {X} \to f^*(\bar {X} \otimes \bar {X}). Taking f to be the copy map, the codomain there is by definition the monoidal product in the fiber \mathcal {D}_X, and so we simply use the copying map of the fiberwise monoidal structure.

Given a Markov structure on the total category \mathcal {D}, we simply apply this idea in reverse and take the map \bar {X} \to \mathrm {copy}_X^*(\bar (X) \otimes \bar {X}) =: \bar {X} \otimes _X \bar {X} to be the copy map.

The deletion maps can be handled in an analogous way.

Corollary [efr-FT8J]

Let \mathcal {D} be a stochastic module fibration, and suppose each fiber has coproducts, and these are preserved by the pullback functors. Then \mathsf {SLens}(\mathcal {D}) is a Markov category, with monoidal structure given by \binom {\bar {X}}{X} \& \binom {\bar {Y}}{Y} = \binom {\pi _X^*\bar {X} + \pi _Y^*\bar {Y}}{X \otimes Y}

The Markov structure of Corollary [efr-FT8J] is a generalization of the fact that, if \mathcal {C} has products and coproducts, and the products distribute over the coproducts, then \mathsf {Lens}(\mathcal {C}) has products given by \binom {A}{X} \times \binom {B}{Y} \cong \binom {A \coprod B}{X \times Y}. See eg Reference [hedges-morphisms-open-games], section 8 for more on this.

Examples [efr-IMLW]

We have already noted several examples throughout. We'll gather a few more here, and also collect a few scattered throughout to make the picture more clear.

First, let us make explicit the example of optics, as strongly as it can be stated

Proposition [efr-A6YR]

Let \mathcal {C} act on \mathcal {D}. Then \mathsf {Optic}_\mathcal {C}(\mathcal {D}) := \mathsf {Optic}_\mathcal {C}(\mathcal {C},\mathcal {D}) has a functor to \mathcal {C}. The deterministic part \mathsf {Optic}_\mathcal {C}(\mathcal {D})|_\mathrm {det} admits the structure of a stochastic module fibration. There is an isomorphism \mathsf {Optic}_\mathcal {C}(\mathcal {D}) \to \mathsf {SChart}(\mathsf {Optic}_\mathcal {C}(\mathcal {D})|_\mathrm {det}).

If \mathcal {D} is itself symmetric monoidal and the action is symmetric (meaning it is given by M \cdot A = F(M) \otimes A for some symmetric monoidal functor F: \mathcal {C} \to \mathcal {D}, see Reference [actegories-amthematician-capucci-gavranovic] 5.4.3 and 5.5.12), this stochastic module is symmetric monoidal and the isomorphism is an isomorphism of symmetric monoidal categories.

Proof

We have essentially already seen that the deterministic part \mathsf {Optic}_\mathcal {C}(\mathcal {D})|_\mathrm {det} \to \mathcal {C}_\mathrm {det} is a fibration, with maps {A \choose X} \leftrightarrows {B \choose X} over X given by X \cdot B \to A, and with the pullback functors acting by reparametrization. Since a map X \to M \otimes Y with deterministic marginal on Y is always equal to the independent pairing of X \to M, X \to Y, we can slide the former through and identify each optic over a given X \to Y with a map X \times B \to A, and note that this map is conversely an invariant of an optic, since it is obtained by postcomposing with {B \choose Y} \to {B \choose *}.

Given M \to X, objects {A \choose X}, {B \choose X}, and a map over M classified by M \cdot B \to A, a section s :X \to M act by reparametrization. It is clear that this gives the structure of a stochastic module.

The functor from optics takes f: X \to M \otimes Y, g: M \cdot B \to A to the span X \leftarrow M \otimes X \otimes Y \to Y equipped with the obvious map (M \otimes X \otimes Y) \cdot B \to A that simply forgets X,Y. Note that every chart is equivalent to one of this form (given X \leftarrow M' \to Y and \phi : M' \cdot B \to A, the map M' \to M' \otimes X \otimes Y exhibits the required equivalence), hence the functor is full.

Moreover, note that each chart is associated with a well-defined optic, given by the maps X \to M \to M \otimes Y, M \cdot B \to A. Is is straightforward to see both of these maps are preserved by chart equivalence. This gives an inverse to the functor, proving it is faithful. Since it is identity on objects, this finishes the argument.

In the symmetric monoidal case, it is immediately clear that the fibration on \mathcal {C}_\mathrm {det} is symmetric monoidal. Since the action is symmetric monoidal, given maps X \to M, X \to M' and M \cdot B \to A, M' \cdot B' \to A', it is clear that composing to get maps X \cdot B \to A, X \cdot B' \to A', then tensoring and composing with the diagonal to get X \cdot (B \otimes B' ) \to A \otimes A', gives the same map as tensoring, then using the map X \to M \otimes M'. Hence we have a symmetric monoidal module. It's straightforward to see the functor is symmetric monoidal, and that finishes the argument.

Slightly orthogonally, we have the following comparison between \mathsf {SLens}(\mathcal {C}^\to ) and \mathsf {Optic}(\mathcal {C}):

Theorem [efr-K6NM]

Let \mathcal {C} be any pullback-positive Markov category. Then \mathcal {C}^\to \to \mathcal {C} is a Markov prefibration which thus induces a stochastic module structure on \mathcal {C}^\to |_\mathrm {det}. Writing simply \mathsf {SChart}(\mathcal {C}), \mathsf {SLens}(\mathcal {C}) for \mathsf {SChart}(\mathcal {C}^\to |_\mathrm {det}), \mathsf {SLens}(\mathcal {C}^\to |_\mathrm {det}), we have:

  1. There is a functor \mathsf {Optic}(\mathcal {C}) \to \mathsf {SLens}(\mathcal {C}), which is fully faithful. Dually there is a functor \mathsf {coOptic}(\mathcal {C}) \to \mathsf {SChart}(\mathcal {C}) which is fully faithful.
  2. \mathsf {SLens}(\mathcal {C}) and \mathsf {SChart}(\mathcal {C}) both admit symmetric monoidal structures, which make the functors \mathsf {SChart}(\mathcal {C}), \mathsf {SLens}(\mathcal {C}) \to \mathcal {C} strict symmetric monoidal, as well as the functors \mathsf {Optic}(\mathcal {C}) \to \mathsf {SLens}(\mathcal {C}), \mathsf {coOptic}(\mathcal {C}) \to \mathsf {SChart}(\mathcal {C}) strong symmetric monoidal.
  3. If \mathcal {C} is extensive, this functor preserves the coproducts {A \choose X} + {A \choose Y} = {A \choose X+Y}, and \mathsf {SChart}(\mathcal {C}),\mathsf {SLens}(\mathcal {C}) both admit all finite coproducts.
  4. If \mathcal {C} moreover has conditionals and supports, \mathsf {SChart}(\mathcal {C}) = \mathcal {C}^\to

Thus we have our previous claim that \mathsf {SLens}(\mathsf {BorelStoch}^\to |_\mathrm {det}) contains \mathsf {Optic}(\mathsf {BorelStoch}).

We also have some examples of an analytic flavor:

Example [efr-TO9K]

Given a compact Hausdorff space X, a Banach space bundle is a space over X, V \to X, equipped with a fiberwise (complex) vector space structure +: V \times _X V \to V, \cdot : \mathbb {C} \times V \to V, so that there exists a cover \{U_i\} of X so that for each U_i, there exists a Banach space V_i and a homeomorphism V \times _X U_i =: V_{U_i} \cong V_i \times U_i over U_i, which is moreover linear in each fiber, where V_i is equipped with the norm topology.

Note that this determines a local norm on each V_{U_i} (and in particular each V_x) up to equivalence (but no stricter than that). In particular each V_x is a Banach space.

A morphism of Banach space bundles is a continuous map f: V \to W over X which is linear on each bundle. Note that this implies that on a suitable cover U_i, the maps f: V_{U_i} \to W_{U_i} obey \left \lVert f(v) \right \rVert \leq C_i \left \lVert v \right \rVert for some C_i \in \mathbb {R}, for any local norms inducing the topologies, and hence by compactness there exists some C so that \left \lVert f(v) \right \rVert \leq C \left \lVert v \right \rVert for each v.

If X \to Y is a continuous map, there is a pullback functor \mathsf {Ban}_Y \to \mathsf {Ban}_X. The Grothendieck construction of this gives a fibration \mathsf {BanBun} \to \mathsf {CHaus}

Note that Tychonoff spaces include all compact Hausdorff spaces. Therfore consider the full subcategory \mathsf {CHausStoch} \hookrightarrow \mathsf {TychStoch} spanned by these. The fibration \mathsf {BanBun} admits the structure of a stochastic module: given M \to X, s: X \to M a kernel, and a linear continuous map f: V \times _X M \to W \times _X M, given v \in V_x, there is an induced function M_x \to W_x given by f(v,-). Since this is bounded (being continuous on a compact space) it is (Bochner) integrable, define s^*f(v) to be this integral.

This example is analogous to optics for the action of categories of markov kernels on categories of vector spaces (as in Proposition [efr-A6YR]). Note that we do not expect this type of example to present a Markov fibration. The reason is simply that, given a parametrized linear map M \times \mathbb {R}^n \to \mathbb {R}^n and a measure on M, the fact that the expectation map \mathbb {R}^n \to \mathbb {R}^n is the identity by no means implies that the original map is almost surely the identity or anything like that. If (m,e_0) \mapsto e_1 and m has positive probability, this can be canceled out by (m',e_0) \mapsto -e_1. This is impossible for probability kernels.

If we add an assumption of positivity, it seems plausible that examples of this type will present Markov fibrations---but of course, that brings us quite close to categories of Markov kernels in any case.

Note that, as in this example, we do not generally expect \mathsf {Optic}_\mathcal {C}(\mathcal {C},\mathcal {D}) to yield a Markov fibration if \mathcal {D} is not another Markov category (and not even then in general, as the case of \mathsf {BorelStoch} shows).---for these, we expect to need a sort of positivity in the fiber as well, which restricts us to things that look like probability kernels.

Proposition Stochastic module of P-algebras [efr-O6GQ]

Let \mathcal {C} be a representable, positive Markov category so that \mathcal {C}_\mathrm {det} admits intersections and the probability monad P preserves them. Then each slice (\mathcal {C}_\mathrm {det})_{/X} inherits a monad structure given by P_X(B \to X) = P(B) \times _{P(X)} X. This is pseudofunctorial in X. Moreover, the stochastic module structure on \mathcal {C}^\to |_\mathrm {det} extends to a stochastic module structure on the fibration representing the pseudofunctor X \mapsto \mathsf {Alg}(P_X).

Proof

The monad is induced by the adjunction \mathcal {C}_\mathrm {det}{/X} \leftrightarrows \mathsf {Alg}(P)_{PX}. Let f: X \to Y (deterministic). For abstract reasons there is a natural transformation P_Yf^* \to f^*P_X. Writing this out, we find P(A \times _Y X) \times _{PX} X \to P(A) \times _{PY} X

By representability, the unit X \to PX is a monomorphism. Hence a map into P(A \times _Y X) \times _{PX} X is precisely a map in \mathcal {C} into A \times _Y X so that the marginal on X is deterministic. But by pullback-positivity this is precisely a map (in \mathcal {C}_\mathrm {det}) into P(A) \times _{PY} X.

Let M \to X, two P_X-algebras A, B, and a map M \times _X A \to M \times _X B which is a homomorphism for the induced P_M-algebras, and a map X \to PM be given. Note that by the above, P_M(M \times _X A) \cong M \times _X P_XA. Then the induced map A \to B is given by A \to PM \times _{PX} A \cong P_X(M) \times _X A \hookrightarrow P_X(M \times _X A) \to P_X(B) \to B

We must show this is a P_X-homomorphism. Let us simplify by working internally to (\mathcal {C}_{\mathrm {det}})_{/X}---thus we have a Cartesian category equipped with a strong commutative monad P, a map * \to PM, and a map M \times A \to B which is a parametrized algebra homomorphism, in the sense that the diagram

commutes. Now we must show the map A \to PM \times A \to P(M \times A) \to PB \to B is a P-homomorphism. Write E_A,E_B for the structure maps of the two algebras. Consider this diagram:

The triangle at the top left commutes because P is strong. The square to the right does not commute in general---however, since P is commutative, the composite maps PM \times PA \to P^2(M \times A) \xrightarrow {\mu } P(X \times A) agree. Since the map P^2(M \times A) \to B factors over this, we may replace one edge of this square with another. The square to the right of that is simply P(-) applied to the previous diagram, and so commutes by assumption. The "triangle" under that is just two copies of the same maps, so commutes. The square on the left of the diagram commutes by functoriality of product. The square to the right of that commutes again because P is strong. Hence the outer square commutes, which is precisely the homomorphism property we wanted.

It is apparent that, if A, B = P_XA', P_B' are free algebras, this restricts to the stochastic module structure of \mathcal {C}^\to |_\mathrm {det} (viewing \mathcal {C} as the Kleisli category of P). But since every algebra is a coequalizer of free algebras, it follows that the action on general algebras is determined uniquely by this. This implies the equations of a stochastic module.

As in Example [efr-TO9K], this cannot be expected to come from a Markov prefibration in general.

The vast majority of examples seem to occur as subcategories of stochastic modules of the form given by Proposition [efr-O6GQ] (of course, \mathcal {C}^\to is just the subcategory spanned fiberwise by the free algebras). In fact, since a stochastic module necessitates in some sense an action of P on the objects of the fiber, it seems they do all have this form in a generalized way, although we have not found a better way to make this precise than the existing definition of stochastic module.

Backlinks

Markov Fibrations and Stochastic Lenses › Introduction [efr-X0ZV]

Let Kl(\Delta ) denote the Kleisli category of the discrete (countable) distribution monad on \mathsf {Set}. This is a simple setting for working with probability theory---sufficient for many applications. In order to study compositional Bayesian game theory (Reference [hedges-etal-bayesian-games], Reference [towards-cybercat]) one studies the category \mathsf {Optic}(Kl(\Delta )) of optics in Kl(\Delta ). These have the right level of expressivity to talk about players taking random actions, and where payoff depends stochastically on players' decisions.

In \mathsf {Optic}(Kl(\Delta )), {R \choose X} + {R \choose Y} \cong {R \choose X+Y}. Games with this codomain naturally describe the situation of a player who has a binary choice between X or Y. We call coproducts of this form the "good" coproducts---note that also {* \choose *} + {\emptyset \choose *} = {\emptyset \choose 2}, but this is considered somewhat pathological, since it relies on the nonexistence of any morphism {\emptyset \choose X} \to {A \choose Y} when A and X are nonempty.

In order to describe this structure on \mathsf {Optic}(Kl(\Delta )), it would be useful if it had all coproducts. Unfortunately this is not the case. \mathsf {Optic}(\mathsf {Set}) = \mathsf {Lens}(\mathsf {Set}) has a well-known extension with all coproducts, given by the fiberwise opposite of the fibration \mathsf {Fam}(\mathsf {Set}) \to \mathsf {Set} (this is Proposition [efr-VTPS] in the case \mathcal {C} = \mathsf {Set}). Extending this to stochastic maps would be the obvious way of constructing such a category of "dependent optics".

Consider a category Kl(\Delta )^\to defined as follows. Its objects are the objects of \mathsf {Set}^\to ---that is, they are indexed families of sets. A map in Kl(\Delta )^\to is a stochastic map in the base X \to Y \in Kl(\Delta ), and a stochastic map on the total spaces \bar {X} \to \bar {Y} which is compatible with it. Note that if \bar {X} \to X is surjective, the map on the base is fully determined by the map on the fibers, which must merely satisfy the condition that the distribution of the indexing point in Y depends only on the indexing point in X, not the specific point in the fiber \bar {X}_x.

We claim Kl(\Delta )^\to is a reasonable notion of "stochastic charts". Recall that by "chart" we mean something like "lenses where both maps go forward". If stochastic lenses are supposed to include optics as the full subcategory spanned by the "non-dependent" objects, then the charts should include "co-optics"---that is, maps between X' \otimes X \to X and Y' \otimes Y \to Y should be given by the coend \int ^M \operatorname {\mathrm {Hom}}(X, M \otimes Y) \times \operatorname {\mathrm {Hom}}(X' \otimes M, Y')

And in fact this is the case: Clearly there is a map from this coend to maps in Kl(\Delta )^\to . By taking M = X \otimes Y and conditioning on Y, we see this is surjective. Finally, by restricting to the support of the forwards part inside X \otimes Y, we obtain a representative for each element of the coend which is uniquely determined by X \to Y and X' \times X \to Y' (since the conditional is well-defined on the support).

Note: This relies both on the fact that Kl(\Delta ) has conditionals, and on the existence of supports. We've previously seen these defined in abstract Markov categories (Definition [efr-AB57])--supports in Kl(\Delta ) of a morphism p: A \to B are simply given by those b so that p(b | a) > 0. Note that the existence of both conditionals and supports is a very strong assumption---the only categories we are aware of with both properties are those whose probability distributions have a discrete character, like Kl(\Delta ) and \mathsf {FinStoch}. Neither will be essential to the theory, but both will play a role in certain theorems---we will see more of this later.

The goal of the theory of Markov fibrations is to give a notion of "fiberwise opposite" which can be applied to the codomain functor Kl(\Delta )^\to \to Kl(\Delta ) to give a reasonable notion of "stochastic lenses". In particular, we should recover the usual category of optics in the previous case.

It is clear that the codomain functor is not a (Grothendieck) fibration, since this would require Kl(\Delta ) to have pullbacks, which can only hold for a Cartesian Markov category. However, we can do some things. Namely, given a Cartesian (pullback) square in \mathsf {Set}

and a map {\bar {X} \choose X} \to {\bar {B} \choose B} where the base map X \to B is deterministic, for each deterministic factorizing map X \to A there is a unique lift \bar {X} \to \bar {A}. In other words, the pullback over \mathsf {Set} \hookrightarrow Kl(\Delta ) is a fibration---in fact, it is simply the family fibration \mathsf {Fam}(\mathsf {Kl}(\Delta )).

Furthermore, if \bar {X} \to \bar {B} is itself deterministic, there is such a unique lift even without assuming that the factorization X \to A is deterministic.

Moreover, we can factor any map in Kl(\Delta )^\to as such an induced map followed by a map over a deterministic base, as follows:

This gives us a hope that we can, in some way, control the category Kl(\Delta )^\to using the pullback over \mathsf {Set}, which is a fibration, and some information somehow given by these extra maps. Note also that the diagram above is equivalent to giving: a span X \leftarrow M \to Y and a section X \to M, which all lives in the base, and a map p^*\bar {X} \to p^{'*}\bar {Y} in the fiber over M. Thus it would seem to be very amenable to fiberwise dualization.

Analogous to our argument above that "co-optics" are equivalent to maps in Kl(\Delta )^\to , we can do the following:

Suppose given two tuples (M_0,p_0,p_0',s_0,\phi _0), (M_1,p_1,p_1',s_1,\phi _1) as above. Suppose there exists a map f: M_0 \to M_1 over X,Y, so that f s_0 = s_1. Then there is a canonical map p_0^*\bar {X} \to p_1^*\bar {X} over f, because pullbacks commute. If the triangle

moreover commutes, then these two triples represent the same map in Kl(\Delta )^\to

These equivalence relations correspond to "sliding" for deterministic morphisms M \to M'. Note that the condition here can be checked just on the fibration Kl(\Delta )^\to \times _{Kl(\Delta )} \mathsf {Set} \to \mathsf {Set}.

To obtain the full set of sliding equations, we will need to use stochastic maps M \to M', and thus leave that fibration behind. However, we are tantalizingly close to realizing Kl(\Delta )^\to as being presented by some sort of additional structure on the fibration \mathsf {Fam}(\mathsf {Kl}(\Delta )). (For a general monad T acting on C, the category \mathsf {Optic}_{\mathcal {C}}(Kl(T),Kl(T)), of effectful optics up to sliding of pure morphisms, was studied by Riley in Reference [riley-optics], section 4.9, and by Hedges in Reference [hedges-blog-optics-effect])

In this chapter we will indeed provide such a structure, and analyze it. In § [efr-2IMZ], we'll axiomatise the lifting property of Kl(\Delta )^\to discussed above into a property we call a Markov prefibration (Definition [efr-0019]). In § [efr-GO6R], we exhibit a free Markov prefibration associated to a fibration---its morphisms are precisely spans of the form seen above. Naturally, given a prefibration \mathcal {D} \to \mathcal {C}, its underlying fibration on \mathcal {C}_\mathrm {det} becomes an algebra for the monad of this adjunction. In § [efr-U4RA], we characterize the class of prefibrations which are presented by their underlying algebra in this way---these are the Markov fibrations (Definition [efr-HVUT]). Since the monad commutes with fiberwise opposites, this yields a notion of fiberwise opposite for Markov fibrations.

Following this, we review a few properties of the theory of Markov fibrations, including the existence of coproducts in the fibration (Proposition [efr-QAV2]), the stability of Markov fibrations under limits (§ [efr-HWAZ]), and induced monoidal structures (§ [efr-LTEL]). Combining these, we can prove:

Theorem [efr-OSH4]

There exists a (strong) symmetric monoidal functor \mathsf {Optic}(Kl(\Delta )) \to \mathsf {SLens}(Kl(\Delta )^\to ) which

  1. Is fully faithful.
  2. Preserves the good coproducts.
  3. So that the image has all coproducts, and every object of the image is a coproduct of objects in \mathsf {Optic}(Kl(\Delta ))
  4. And so that moreover the monoidal structure on the image is distributive

Related

Theorem [efr-K6NM]

Let \mathcal {C} be any pullback-positive Markov category. Then \mathcal {C}^\to \to \mathcal {C} is a Markov prefibration which thus induces a stochastic module structure on \mathcal {C}^\to |_\mathrm {det}. Writing simply \mathsf {SChart}(\mathcal {C}), \mathsf {SLens}(\mathcal {C}) for \mathsf {SChart}(\mathcal {C}^\to |_\mathrm {det}), \mathsf {SLens}(\mathcal {C}^\to |_\mathrm {det}), we have:

  1. There is a functor \mathsf {Optic}(\mathcal {C}) \to \mathsf {SLens}(\mathcal {C}), which is fully faithful. Dually there is a functor \mathsf {coOptic}(\mathcal {C}) \to \mathsf {SChart}(\mathcal {C}) which is fully faithful.
  2. \mathsf {SLens}(\mathcal {C}) and \mathsf {SChart}(\mathcal {C}) both admit symmetric monoidal structures, which make the functors \mathsf {SChart}(\mathcal {C}), \mathsf {SLens}(\mathcal {C}) \to \mathcal {C} strict symmetric monoidal, as well as the functors \mathsf {Optic}(\mathcal {C}) \to \mathsf {SLens}(\mathcal {C}), \mathsf {coOptic}(\mathcal {C}) \to \mathsf {SChart}(\mathcal {C}) strong symmetric monoidal.
  3. If \mathcal {C} is extensive, this functor preserves the coproducts {A \choose X} + {A \choose Y} = {A \choose X+Y}, and \mathsf {SChart}(\mathcal {C}),\mathsf {SLens}(\mathcal {C}) both admit all finite coproducts.
  4. If \mathcal {C} moreover has conditionals and supports, \mathsf {SChart}(\mathcal {C}) = \mathcal {C}^\to

Example Markov prefibrations over Cartesian base [efr-CJTH]

Let \mathcal {C} be a Markov category which is Cartesian (that is, one where all morphisms are deterministic). Then a Markov prefibration over \mathcal {C} is simply a Grothendieck fibration.