Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Cellular Telescope

Abstract

The actual mapping telescope of the saved unbounded cellular sequence. Its derived universal comparison is proved against all derived-local targets. A quasi-isomorphism to the ordinary cellular colimit and realization in D(Solid) remain separate obligations. New proofs, Apache 2.0.

Theorem 1.1 (solid Cellular Telescope derived Precomp bijective).

Lean statement: D5/S3/HomologicalAlgebra/Solid/CellularTelescope.solidCellularTelescope_derivedPrecomp_bijective

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

Source. Repository-derived.

Commentary.

The saved sequence’s actual mapping telescope has a universal derived comparison to every derived-local object: existence and uniqueness hold for all roofs and for arbitrary unbounded starting complexes.

References