Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Localization Coproduct

Abstract

Coproduct preservation for a localization with a right calculus of fractions. This is the specific missing sum argument needed for the actual unbounded cellular telescope. New proofs, released under Apache 2.0.

Theorem 1.1 (localization coproduct hom zero).

Lean statement: D5/S3/HomologicalAlgebra/Solid/LocalizationCoproduct.localization_coproduct_hom_zero

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

Source. Repository-derived.

Commentary.

Vanishing on every summand detects zero after localization, including all roofs. The proof refines the denominators separately and then sums the actual weak equivalences.

References

  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/LocalizationCoproduct.localization_coproduct_hom_zero