lin-0123
9.6 Functorial and descent-compatible repair
Suppose \(\alpha :D\to D'\) is a repair transformation. A tangent-compatible repair has a transported transformation
If \(D'\) factors through the declared quotient, then a repair advertised as compositionality-preserving must retain that factorization.
For a cover, global and local repairs must also interact with restriction:
with cocycle coherence on overlaps.
Suppose the admissible models form a stack over the chosen cover, the local repairs \(R_iD_i\) agree on overlaps with coherent descent data, and each repaired local model remains admissible. Then the repaired family glues to a global admissible model, unique up to the declared equivalence.
This is the effectivity condition in the stack semantics applied to the compatible repaired family.
The proposition is deliberately conditional. Without effective descent, local repair compatibility is only a necessary condition for a global repair.