lin-0221
18.4 Tangent descent
Assume the predictive category carries tangent structure [ Cockett and Cruttwell , 2014b ] .
Theorem
18.4
Tangent descent
If \(T\) preserves the finite products defining \(M_{\mathcal U}\) and \(O_{\mathcal U}\), and preserves the equalizer defining \(Z_{\mathcal U}\), then
\[ TZ_{\mathcal U} \cong \operatorname {Eq}(Td_0,Td_1). \]
Consequently, at a compatible smooth family \(z\), an infinitesimal local update \(v\) preserves compatibility exactly when
\[ T_zd_0(v)=T_zd_1(v). \]
Proof
Apply \(T\) to the equalizer cone. The preservation hypotheses make the lifted cone an equalizer.
This is a preservation theorem. Away from the descent locus, tangent vectors to two restrictions lie over different base points and cannot be directly identified. Repair needs an additional lift.