Inverse-Limit Descent and Reverse Criterion

Abstract

Compatible finite-stage maps induce a unique map on inverse-limit families, and surjective coordinates recover finite naturality.

Theorem 1.1 (Inverse-limit maps descend uniquely and reflect finite naturality).

$$\forall I,S,T,delta,\mathrm{Compatible}(S,T,delta)\Rightarrow (\exists !D:\mathrm{CompatibleStageFamily}(S)\Rightarrow \mathrm{CompatibleStageFamily}(T),\forall a,i,Delta(a{)}_i=delt{a}_i(a_i)\wedge \forall D:\mathrm{CompatibleStageFamily}(S)\Rightarrow \mathrm{CompatibleStageFamily}(T),(\forall a,i,Delta(a{)}_i=delt{a}_i(a_i))\Rightarrow (\forall i,\mathrm{Surjective}(a_i))\Rightarrow \forall h,x,\mathrm{restrict}(T,h,delt{a}_j(x))=delt{a}_i(\mathrm{restrict}(S,h,x))).$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Refinement/InverseLimitDescent.inverse_limit_descent_and_reverse (✓ std3). ∎

Source. Repository-derived.

Commentary.

The source and target are inverse-stage systems with restriction channels satisfying identity and composition. A stage map is assumed to commute with every restriction channel.

The induced map sends a compatible source family to the family obtained by applying the corresponding stage map at every coordinate. The public statement includes both its coordinate equation and uniqueness.

Conversely, if every source coordinate is surjective from compatible families and a map with the displayed coordinate equation exists, evaluating compatibility on a lifted family recovers strict finite-stage naturality.

The proof reuses the canonical InverseStageSystem and CompatibleStageFamily types from CompletionIsomorphismCriterion. Repository search found no existing theorem packaging this induced map with the reverse clause.

References

• Truth anchor: D5/S3/ObserverMemory/Refinement/InverseLimitDescent.inverse_limit_descent_and_reverse
• Dependency: D5/S3/ObserverMemory/InverseLimits/CompletionIsomorphismCriterion