sec-online-offline-comparison

9.11 The online-to-offline comparison

The skeletal filtration creates a canonical comparison between incremental and all-at-once UDL. Put \(\mathcal S=\Delta /X\), \(\mathcal S_t=\mathsf{Simp}_{\leq t}(X)\), and extend each compatible decoration to the fixed domain by

\[ \widetilde F_t=\operatorname {Lan}_{j_t}F_t:\mathcal S\to \mathcal D. \]

Let \(F=\operatorname *{colim}_t\widetilde F_t\), fix \(J:\mathcal S\to \mathcal C\) and \(K:\mathcal C\to \mathcal Q\), and write

\[ G_t=\operatorname {Lan}_J\widetilde F_t, \qquad G=\operatorname {Lan}_JF. \]

The maps \(G_t\to G\) induce the online-to-offline comparison

\begin{equation} \gamma : \operatorname *{colim}_t\operatorname {Ran}_KG_t \longrightarrow \operatorname {Ran}_KG. \end{equation}

9.4

Theorem 9.11 Skeletal continuity of UDL

Assume the displayed Kan extensions and filtered colimits exist. Suppose also that filtered colimits in \(\mathcal D\) commute with every limit used in the pointwise formula for \(\operatorname {Ran}_K\). Then the comparison \(\gamma \) in 9.4 is an isomorphism. Consequently,

\[ \operatorname *{colim}_t \mathsf U_t^{\Delta }(F_t) \cong \mathsf U(F) \]

after the declared extensions to the common domain.

Proof ▼

The left Kan extension \(\operatorname {Lan}_J\) is a left adjoint and therefore preserves the filtered colimit:

\[ G =\operatorname {Lan}_J\! \left(\operatorname *{colim}_t\widetilde F_t\right) \cong \operatorname *{colim}_t\operatorname {Lan}_J\widetilde F_t =\operatorname *{colim}_tG_t. \]

Pointwise right Kan extension is computed by the declared limits. The commutation hypothesis moves the filtered colimit through each such limit, giving

\[ \operatorname *{colim}_t\operatorname {Ran}_KG_t \cong \operatorname {Ran}_K\! \left(\operatorname *{colim}_tG_t\right) \cong \operatorname {Ran}_KG. \]

This composite is the canonical comparison \(\gamma \).

The theorem localizes the obstruction. Incremental candidate generation commutes with revelation because the left Kan stage preserves colimits. The possible failure lies in interchanging gradual revelation with the limits of right-Kan consistency. If \(\gamma \) is not invertible, its defect measures semantic structure available to the all-at-once UDL construction but not preserved by the filtered online construction. A LINCS observer may map that structural defect to a numerical quantity, but the defect exists before any regret scalar is chosen.