ora-0124

9.12.2 Derived skeletal continuity

Return to the skeletal filtration and interpret all diagrams in \(\mathcal D_\infty \). Put

\[ F\simeq \operatorname *{hocolim}_t\widetilde F_t, \qquad G_t=\operatorname {Lan}^h_J\widetilde F_t, \qquad G=\operatorname {Lan}^h_JF. \]

There is a canonical derived comparison

\begin{equation} \gamma ^h: \operatorname *{hocolim}_t\operatorname {Ran}^h_KG_t \longrightarrow \operatorname {Ran}^h_KG. \end{equation}

9.7

Theorem 9.17 Finite-consistency derived skeletal continuity

Let \(\mathcal D_\infty \) be a presentable stable \(\infty \)-category, and assume the declared homotopy Kan extensions exist. If every comma \(\infty \)-category indexing the pointwise right Kan extension along \(K\) is represented by a finite simplicial set, then the comparison \(\gamma ^h\) in 9.7 is an equivalence. Consequently, filtered online construction recovers the homotopy-coherent all-at-once UDL semantics.

Proof ▼

The homotopy left Kan extension is a left adjoint, so it preserves the filtered homotopy colimit:

\[ G\simeq \operatorname {Lan}^h_J\! \left(\operatorname *{hocolim}_t\widetilde F_t\right) \simeq \operatorname *{hocolim}_tG_t. \]

In a stable \(\infty \)-category, finite limits and finite colimits agree. Hence filtered colimits commute with the finite limits appearing in the pointwise formula for \(\operatorname {Ran}^h_K\). Moving the homotopy colimit through those limits identifies the source and target of \(\gamma ^h\).

In this stable setting define the homotopy-coherent online defect by

\[ \mathsf{Def}^h(F)=\operatorname {fib}(\gamma ^h). \]

It is a zero object exactly when \(\gamma ^h\) is an equivalence. Mapping objects out of probes into \(\mathsf{Def}^h(F)\) reveal components and higher coherences of the failure. This defect precedes regret: a numerical observer may evaluate it, but cannot reconstruct the repair structure after reducing it to a scalar.

Finally, tangent lifting must itself be derived. If the tangent functor preserves \(W\), or admits a derived functor \(T^h\), the fundamental comparison becomes

\begin{equation} \theta _F^h: T^h\mathsf U^h(F) \longrightarrow \mathsf U^h(T^hF). \end{equation}

9.8

Determining when \(\theta _F^h\) is an equivalence, and how its fiber interacts with \(\mathsf{Def}^h(F)\), is the first tangent-homotopy problem for UODL. It asks whether infinitesimal variation respects learned semantics only up to coherent deformation, a substantially stronger requirement than equality of point estimates.