lin-0088

6.6 Queries and data migration at tangent level

A schema functor \(F:\mathcal S\to \mathcal S'\) induces the familiar restriction functor \(\Delta _F\) by precomposition and, when they exist, left and right data migrations \(\Sigma _F\dashv \Delta _F\dashv \Pi _F\) [ Spivak , 2012 ] . Tangent lifting interacts differently with the three operations.

Restriction commutes strictly with the pointwise tangent lift:

\[ T_{\mathcal S}\Delta _F = \Delta _F T_{\mathcal S'}. \]

For left and right migration, the canonical comparison maps have directions

\[ \Sigma _F T_{\mathcal S}I \longrightarrow T_{\mathcal S'}\Sigma _F I, \qquad T_{\mathcal S'}\Pi _F I \longrightarrow \Pi _F T_{\mathcal S}I. \]

They are isomorphisms only when the tangent functor preserves the colimits or limits used to compute the corresponding Kan extensions.

Definition 6.8 Query–tangent compatibility

A data migration is query–tangent compatible on an instance when its canonical comparison map is an isomorphism, or when the declaration supplies an admitted weaker comparison sufficient for the intended query.

The failure of compatibility is another useful LINCS obstruction. It asks whether “query, then differentiate” agrees with “differentiate, then query.” Unlike an ordinary numeric discrepancy, the failure identifies the schema migration and the universal construction responsible for the mismatch.

Design principle

Infinitesimal CSQL should expose whether a query commutes with tangent lifting. Foreign-key restriction does so pointwise; aggregation and constraint queries require explicit preservation hypotheses.