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)^*