Proposition [efr-JQI9]

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

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

Proof

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

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

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

Context

Double Categories of Stochastic Dynamical System [efr-7DV5]

Definition Stochastic Dynamical Systems Theories [efr-HS7G]

A stochastic dynamical systems theory consists of a stochastic module \mathcal {D} over \mathcal {C} equipped with a section T: \mathcal {C}_\mathrm {det} \to \mathcal {D}|_\mathrm {det} of the underlying fibration.

We adopt the notation \widetilde {\mathsf {\mathbb Arena}}(\mathcal {D}) for the double category which was denoted \widetilde {\mathsf {\mathbb Span}}(\mathcal {D})^\mathrm {lens} above. We use the symbol \leftrightarrows for the horizontal (span) morphisms and \rightrightarrows for the vertical morphisms (in \mathcal {D}).

Given a stochastic dynamical systems theory (\mathcal {D}, T), the double category of dynamical systems \mathsf {Sys}(\mathcal {D},T) has

  1. Objects triples S \in \mathcal {C}, \bar {A} \in \mathcal {D}, \xi : TS \leftrightarrows \bar {A} \in \widetilde {\mathsf {\mathbb Arena}}
  2. Horizontal morphisms given by a pair f: S \to S', g: \bar {A} \rightrightarrows \bar {B} \in \mathcal {D}, c where c is a square filling \xi , \xi ', Tf, g
  3. Vertical morphisms given by a pair f: S \to S', g: \bar {A} \leftrightarrows \bar {B} \in \overline {\mathcal {D}}, c where c is a square filling Tf, g \xi , \xi ', 1_{\bar {B}}

Proposition [efr-N5V5]

Let T,\mathcal {D} be a stochastic dynamical systems theory. Then T,\mathcal {D}|_\mathrm {det} is an ordinary dynamical systems theory. There is a double functor \mathsf {Sys}(T,\mathcal {D}|_\mathrm {det}) \to \mathsf {Sys}(T,\mathcal {C}). This functor is full on vertical morphisms, and on 2-cells.

Let \mathsf {Sys}(T,\mathcal {D})_\mathrm {det} denote the subcategory spanned by systems with deterministic readout, prelenses with deterministic base, and all the morphisms of \mathcal {D}. Then the restricted functor \mathsf {Sys}(T,\mathcal {D}|_\mathrm {det}) \to \mathsf {Sys}(T,\mathcal {D})_\mathrm {det} admits a chartwise right adjoint, which assigns to each system or prelens its equivalence class.

Proof

The functor simply acts as the functor in Proposition [efr-JQI9]. Since that inclusion is full on 2-cells, this one is full on vertical morphisms, and since a 2-cell in \mathsf {Sys} is merely a 2-cell in \mathsf {\mathbb Arena} between specific objects, it is also full on 2-cells.

The right adjoint property likewise follows from the analogous property of the inclusion functor on arenas.

Proposition [efr-JQI9]

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

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

Proof

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

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

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

Recall that in Myers' categorical dynamical systems theory, trajectories of a system \xi : TS \leftrightarrows \bar {A} are identified with chart morphisms from a "clock" system---thus for example trajectories of a smooth dynamical system M \to TM are exactly those maps \gamma : \mathbb {R} \to M which, when \mathbb {R} is equipped with the vectorfield dx/dt = 1, are homomorphisms.

In general this presents an issue for our replacement category \mathsf {Sys}(T,\mathcal {D})---since we wish to regard two systems given by equivalent lenses as equivalent, but their set of homomorphisms from a given clock system is not necessarily in bijection. In the general case, we do not presently have a way around this problem---but at least for clock systems with deterministic readout, the above presents a solution: choosing the initial representative for such a system, we find that the set of trajectories does not depend on the equivalence class of the target system.

Backlinks

Proposition [efr-N5V5]

Let T,\mathcal {D} be a stochastic dynamical systems theory. Then T,\mathcal {D}|_\mathrm {det} is an ordinary dynamical systems theory. There is a double functor \mathsf {Sys}(T,\mathcal {D}|_\mathrm {det}) \to \mathsf {Sys}(T,\mathcal {C}). This functor is full on vertical morphisms, and on 2-cells.

Let \mathsf {Sys}(T,\mathcal {D})_\mathrm {det} denote the subcategory spanned by systems with deterministic readout, prelenses with deterministic base, and all the morphisms of \mathcal {D}. Then the restricted functor \mathsf {Sys}(T,\mathcal {D}|_\mathrm {det}) \to \mathsf {Sys}(T,\mathcal {D})_\mathrm {det} admits a chartwise right adjoint, which assigns to each system or prelens its equivalence class.

Proof

The functor simply acts as the functor in Proposition [efr-JQI9]. Since that inclusion is full on 2-cells, this one is full on vertical morphisms, and since a 2-cell in \mathsf {Sys} is merely a 2-cell in \mathsf {\mathbb Arena} between specific objects, it is also full on 2-cells.

The right adjoint property likewise follows from the analogous property of the inclusion functor on arenas.

Related

Proposition [efr-10CM]

Suppose given a square

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

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

Proof

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

Given two such cells, we get a square

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

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