Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Bounded Coefficient Descent

Abstract

Descent of the bounded coefficient maps to the actual condensed object B_Z. This constructs D : P tensor B_Z -> P as an honest condensed morphism. New proofs, Apache-2.0; the construction is the coefficient map in Rodríguez Camargo’s Notes on Solid Geometry, Lemma 3.3.3.

Theorem 1.1 (bounded Measure Coefficient on section).

Lean statement: D5/S3/HomologicalAlgebra/Solid/BoundedCoefficientDescent.boundedMeasureCoefficient_on_section

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

Source. Repository-derived.

Commentary.

D agrees with the concrete coefficient selector map on every actual bounded test section. This is the required descent comparison.

Theorem 1.2 (bounded Measure Coefficient on family).

Lean statement: D5/S3/HomologicalAlgebra/Solid/BoundedCoefficientDescent.boundedMeasureCoefficient_on_family

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. Descent of the bounded coefficient maps to the actual condensed object B_Z. This constructs D : P tensor B_Z -> P as an honest condensed morphism. New proofs, Apache-2.0; the construction is the coefficient map in Rodríguez Camargo’s Notes on Solid Geometry, Lemma 3.3.3.

References