sec-reading-derived-continuity

1.17 Reading the derived skeletal-continuity theorem

The later finite-consistency theorem compares incremental and all-at-once homotopy-coherent UDL. Its comparison has the form

\[ \gamma ^h: \operatorname *{hocolim}_t \operatorname {Ran}^h_K\operatorname {Lan}^h_J\widetilde F_t \longrightarrow \operatorname {Ran}^h_K\operatorname {Lan}^h_J \operatorname *{hocolim}_t\widetilde F_t. \]

The online–offline comparison is a map between two orders of construction, not yet a numerical regret. When \(\gamma ^h\) is an equivalence, incremental universal construction recovers the all-at-once semantic object. An observer is still required to turn any remaining defect… — Figure 1.10 The online–offline comparison is a map between two orders of construction, not yet a numerical regret. When \(\gamma ^h\) is an equivalence, incremental universal construction recovers the all-at-once semantic object. An observer is still required to turn any remaining defect into a scalar.

Each symbol now has a declared role:

\(\widetilde F_t\) is the evidence available at finite stage \(t\), extended to a common diagram domain.
The homotopy colimit retains the progressively assembled evidence up to semantic weak equivalence.
\(\operatorname {Lan}^h_J\) generates candidates and preserves the filtered homotopy colimit because it is a left adjoint.
\(\operatorname {Ran}^h_K\) enforces consistency through pointwise homotopy limits.
Finite consistency shapes and a stable target allow the filtered colimit to commute with those finite limits.
Under these hypotheses, \(\gamma ^h\) is an equivalence.

Admission contract

A claimed derived online-to-offline theorem must identify the weak equivalences, the localization, the common diagram domain, the existence of both derived Kan extensions, the pointwise right-Kan limit shapes, and the exact colimit–limit interchange being used. Without these declarations, the superscript \(h\) is only suggestive notation.