Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Coefficient Linearity

Abstract

Additivity of the concrete bounded coefficient maps, by finite covers of closed coefficient fibers. These maps must be additive before they can be assembled into D : P tensor B_Z -> P. This argument uses actual condensed descent; no injectivity of PToIntegerMeasures is assumed. New proofs, Apache-2.0. The covering epimorphism supplier is reused from root’s immutable CWComparison.ProfiniteCover checkpoint, whose copyright and Apache-2.0 attribution are preserved in its frozen source.

Theorem 1.1 (measure Coefficient Numerator prequotient).

Lean statement: D5/S3/HomologicalAlgebra/Solid/CoefficientLinearity.measureCoefficientNumerator_prequotient

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. Additivity of the concrete bounded coefficient maps, by finite covers of closed coefficient fibers. These maps must be additive before they can be assembled into D : P tensor B_Z -> P. This argument uses actual condensed descent; no injectivity of PToIntegerMeasures is assumed. New proofs, Apache-2.0. The covering epimorphism supplier is reused from root’s immutable CWComparison.ProfiniteCover checkpoint, whose copyright and Apache-2.0 attribution are preserved in its frozen source.

Theorem 1.2 (bounded Coefficient Map add).

Lean statement: D5/S3/HomologicalAlgebra/Solid/CoefficientLinearity.boundedCoefficientMap_add

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

Source. Repository-derived.

Commentary.

The actual coefficient map is additive, before ordinary or derived solidification. This supplies the linearity required for descent to B_Z.

References