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.

Context

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.