Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Cell Locality

Abstract

Locality of the actual unbounded cellular colimit. These are new proofs over the official Mathlib pin and the protected defining maps. Released under the Apache 2.0 license.

Theorem 1.1 (solid Cellular Colimit defect acyclic).

Lean statement: D5/S3/HomologicalAlgebra/Solid/CellLocality.solidCellularColimit_defect_acyclic

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

Source. Repository-derived.

Commentary.

The complete unbounded cellular colimit has zero locality defect.

Theorem 1.2 (solid Cellular Colimit homology solid).

Lean statement: D5/S3/HomologicalAlgebra/Solid/CellLocality.solidCellularColimit_homology_solid

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

Source. Repository-derived.

Commentary.

The cellular colimit is derived-local in every integer degree. This is locality of an actual construction, with no assumed replacement theorem.

References