Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Cone Colimit

Abstract

Coproducts of the actual mapping cones used by the unbounded cellular construction. New proofs, released under the Apache 2.0 license.

Definition 1.1 (complex Diagram As Functor Iso).

Lean statement: D5/S3/HomologicalAlgebra/Solid/ConeColimit.complexDiagramAsFunctorIso

Formalization. D5/S3/HomologicalAlgebra/Solid/ConeColimit.complexDiagramAsFunctorIso (✓ std3).

Source. Repository-derived.

Commentary.

Transposing the existing complex-to-diagram construction returns the original unbounded complex, with its original differentials.

Definition 1.2 (mapping Cone Coproduct Iso).

Lean statement: D5/S3/HomologicalAlgebra/Solid/ConeColimit.mappingConeCoproductIso

Formalization. D5/S3/HomologicalAlgebra/Solid/ConeColimit.mappingConeCoproductIso (✓ std3).

Source. Repository-derived.

Commentary.

Arbitrary coproducts of mapping cones are the mapping cone of the actual coproduct map. The complexes need not be bounded.

References