Cell Factorization

Abstract

Finite-stage factorization for the concrete two-term localization cells.

Theorem 1.1 (solid Cellular Colimit cell Map factors).

Lean statement: D5/S3/HomologicalAlgebra/Solid/CellFactorization.solidCellularColimit_cellMap_factors

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

Source. Repository-derived.

Commentary.

Every chain map from a defining two-term cell into the full cellular colimit factors through an actual finite stage. The incoming complex is arbitrary and unbounded.

References

• Truth anchor: D5/S3/HomologicalAlgebra/Solid/CellFactorization.solidCellularColimit_cellMap_factors
• Dependency: D5/S3/HomologicalAlgebra/Solid/CellularSolidification