Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finite Approximation Coefficient

Abstract

The actual coefficient morphism D_S : P tensor free(S) -> P for the free-profinite generator retract. It descends the continuous representative selector through the exact protected infinity cokernel. This is an ordinary condensed morphism, with no realization or derived-adjunction premise. New proofs, Apache-2.0; Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.2.

Theorem 1.1 (finite Approximation Coefficient Numerator relation).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FiniteApproximationCoefficient.finiteApproximationCoefficientNumerator_relation

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. The actual coefficient morphism D_S : P tensor free(S) -> P for the free-profinite generator retract. It descends the continuous representative selector through the exact protected infinity cokernel. This is an ordinary condensed morphism, with no realization or derived-adjunction premise. New proofs, Apache-2.0; Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.2.

References