Telescope Comparison

Abstract

The actual comparison from the mapping telescope to the previously saved ordinary cellular colimit. This defines and proves the comparison equations; its quasi-isomorphism property is an explicit remaining theorem, not an assumed bridge. New proofs, released under Apache 2.0.

Theorem 1.1 (solid Cellular Telescope To Colimit input).

Lean statement: D5/S3/HomologicalAlgebra/Solid/TelescopeComparison.solidCellularTelescopeToColimit_input

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

Source. Repository-derived.

Commentary.

In particular, the comparison preserves the map from the original arbitrary unbounded complex into the ordinary saved cellular colimit.

Theorem 1.2 (solid Cellular Telescope Short Complex exact).

Lean statement: D5/S3/HomologicalAlgebra/Solid/TelescopeComparison.solidCellularTelescopeShortComplex_exact

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

Source. Repository-derived.

Commentary.

Exactness at the middle of the actual telescope presentation. The remaining short-exactness input is monicity of its first map.

References

• Truth anchor: D5/S3/HomologicalAlgebra/Solid/TelescopeComparison.solidCellularTelescopeShortComplex_exact
• Truth anchor: D5/S3/HomologicalAlgebra/Solid/TelescopeComparison.solidCellularTelescopeToColimit_input
• Dependency: D5/S3/HomologicalAlgebra/Solid/CellularTelescope