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

Context

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.

Backlinks

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.