lin-0096
7.3 Differentiating universal extension
There are two conceivable routes from a local variation to a global one. One may first construct the global decision and differentiate it,
or first differentiate the local data and then transport that variation through a registered tangent lift of the declared Kan construction,
These routes need not agree. Indeed, the second expression is meaningful only when the tangent objects and their base points inhabit a category in which the indicated lifted extensions exist. The superscript \(T\) records this extra structure; it is not obtained by applying an ordinary Kan extension to an untyped vector.
Write
and define \(\dot U_v^{\mathrm{dir}}\) and \(\dot U_v^{\mathrm{ext}}\) analogously at the right Kan stage. Canonical comparison morphisms between the “extended” and “direct” tangent objects declare the desired compatibility; their existence and invertibility are not automatic.
Suppose the comma-category shapes are fixed near \(\theta \), the relevant pointwise limits and colimits exist, and the chosen tangent construction preserves them. Then the canonical tangent comparison maps for the left and right Kan stages are isomorphisms. Consequently, tangent transport through the UDL composite is independent of whether differentiation is performed before or after universal extension.
Pointwise Kan extensions are computed by the stated limits and colimits. Under the preservation hypotheses, applying the tangent construction to either pointwise universal object yields the universal object of the tangent-lifted diagram. The universal comparison maps are therefore isomorphisms at every context, and hence natural isomorphisms.
The hypotheses matter. A maximum may change its active branch, a feasible set may change dimension, an equilibrium may bifurcate, or a comma category may change when the available information changes. At such points, ordinary derivatives can fail to exist even though a meaningful directional or set-valued response remains.
Kan extension and differentiation do not commute by notation alone. Exact commutation is a theorem under preservation and regularity assumptions; its failure is itself a structural diagnostic.