lin-0084
6.2 Instance lift, schema expansion, and constraint stability
Three operations that sound similar must not be identified.
- Pointwise instance lift.
The schema \(\mathcal S\) stays fixed and \(I\) is replaced by \(T_{\mathcal S}I\). This is the construction proved above.
- Syntactic tangent expansion.
A new sketch \(\tau \mathcal S\) is presented with tangent objects, projections, zero sections, lifts, or vector field symbols. This changes the database schema.
- Internal tangent schema.
If \(\mathcal S\) itself has tangent structure, one may apply its tangent functor internally. A general database schema does not have such structure automatically.
The second construction is the one most useful for a persistent infinitesimal CSQL atlas. It makes the added infinitesimal columns and foreign keys explicit. It should be called a tangent expansion, rather than written \(T\mathcal S\), unless a tangent structure on \(\mathcal S\) has actually been supplied.
Database schemas often present more than paths. They may declare products, pullbacks, limits, equations, or lifting constraints. Let \(\operatorname {Mod}(\mathbb S,\mathcal C)\) denote the full subcategory of \([\mathcal S,\mathcal C]\) satisfying a database sketch \(\mathbb S\).
A database sketch \(\mathbb S\) is tangent-stable in \(\mathcal C\) when \(I\models \mathbb S\) implies \(T_{\mathcal S}I\models \mathbb S\), with the declared comparison data preserved.
Path equations are preserved because \(T\) is a functor. A declared limit or pullback is preserved only when \(T\) preserves the relevant cone. The tangent category axioms guarantee selected pullbacks needed by tangent structure; they do not say that \(T\) preserves every database constraint.
If \(\mathbb S\) is tangent-stable, the pointwise tangent functor restricts to an endofunctor
If tangent stability fails, its missing comparison or failed cone is a typed obstruction rather than an infinitesimal database instance of the same declared type.
The first claim is the definition of tangent stability applied on objects; naturality of \(T\alpha \) supplies its action on instance morphisms. For the second, a lifted instance that violates a declared cone does not lie in the model subcategory. The failure is therefore a factorization or universal property obstruction of the kind introduced in Chapter 3.
Do not silently coerce \(T_{\mathcal S}I\) back into the constrained database category. Either prove tangent stability, record the necessary comparison maps, or retain their failure as database-level obstruction data.