Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Complex Colimit

Abstract

Exact colimits of arbitrary unbounded complexes. These new proofs are used to assemble weak equivalences in the cellular localization argument. Released under the Apache 2.0 license.

Theorem 1.1 (complex Diagram Colimit Iso naturality).

Lean statement: D5/S3/HomologicalAlgebra/Solid/ComplexColimit.complexDiagramColimitIso_naturality

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. Exact colimits of arbitrary unbounded complexes. These new proofs are used to assemble weak equivalences in the cellular localization argument. Released under the Apache 2.0 license.

Theorem 1.2 (quasi Iso colimit Map).

Lean statement: D5/S3/HomologicalAlgebra/Solid/ComplexColimit.quasiIso_colimitMap

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

Source. Repository-derived.

Commentary.

Exact colimits preserve all quasi-isomorphisms of arbitrary unbounded diagrams. In particular, this covers filtered colimits and arbitrary sums in the protected light condensed category.

References

  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/ComplexColimit.complexDiagramColimitIso_naturality
  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/ComplexColimit.quasiIso_colimitMap