Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finite Approximation Descent

Abstract

Actual free descent of representative differences along the full compact kernel pair, then through the protected infinity cokernel. Constructs P -> free(S), without any derived-adjunction/realization premise. New proofs, Apache-2.0; Juan Esteban Rodríguez Camargo, Notes on Solid Geometry, Lemma 3.3.2. Effective-epi proof pattern: immutable Apache-2.0 CWComparison.FreeCoverPresentation (2026); no supplier source is modified.

Theorem 1.1 (finite Approximation Free Difference relation).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FiniteApproximationDescent.finiteApproximationFreeDifference_relation

Proof. Machine-checked in Lean as D5/S3/HomologicalAlgebra/Solid/FiniteApproximationDescent.finiteApproximationFreeDifference_relation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Equality on the entire relation follows from a genuine finite cover.

Theorem 1.2 (finite Approximation Free Sequence infty).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FiniteApproximationDescent.finiteApproximationFreeSequence_infty

Proof. Machine-checked in Lean as D5/S3/HomologicalAlgebra/Solid/FiniteApproximationDescent.finiteApproximationFreeSequence_infty (✓ std3). ∎

Source. Repository-derived.

Commentary.

An actual infinity lift kills the infinity value of the descended sequence.

References