Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finite Approximation Square

Abstract

The actual representative-difference square. Its map into the compact parameter cover is continuous and lands in its full closure by density of finite rows. Thus equality is of condensed morphisms, not merely finite-point values. The zeroth row retains the finite initial quotient. New proofs, Apache-2.0; Rodríguez Camargo, Notes on Solid Geometry, Lemma 3.3.2.

Theorem 1.1 (finite Approximation Shift Previous).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FiniteApproximationSquare.finiteApproximationShiftPrevious

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

Source. Repository-derived.

Commentary.

The predecessor cancels the protected successor shift, including infinity.

Theorem 1.2 (finite Approximation Coefficient numerator square).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FiniteApproximationSquare.finiteApproximationCoefficient_numerator_square

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

Source. Repository-derived.

Commentary.

The free coefficient map factors through the genuine descended sequence.

Theorem 1.3 (finite Approximation Remainder square).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FiniteApproximationSquare.finiteApproximationRemainder_square

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

Source. Repository-derived.

Commentary.

The actual finite-difference square, in the original ordinary category.

References