Unbounded Upper Truncation Colimit

Abstract

Copyright (c) 2026. Released under the Apache 2.0 license. The actual increasing good upper truncations have every unrestricted cochain complex as their colimit. Together with the accepted lower truncation construction, this is the concrete double truncation step in unbounded generation. No realization equivalence or completeness premise is asserted. Research: Rodríguez Camargo, Notes on Solid Geometry, Theorem 3.3.1, unbounded extension by truncations and telescopes.

Theorem 1.1 (upperTruncationDiagram eventuallyConstant).

Lean statement: D5/S3/HomologicalAlgebra/Solid/UnboundedUpperTruncationColimit.upperTruncationDiagram_eventuallyConstant

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

Source. Repository-derived.

Commentary.

The compiled statement supplies upperTruncationDiagram eventuallyConstant. These eventual-constant component diagrams have the original arbitrary unbounded complex as their colimit.

Definition 1.2 (upperTruncationCocone isColimit).

Lean statement: D5/S3/HomologicalAlgebra/Solid/UnboundedUpperTruncationColimit.upperTruncationCocone_isColimit

Formalization. D5/S3/HomologicalAlgebra/Solid/UnboundedUpperTruncationColimit.upperTruncationCocone_isColimit (✓ std3).

Source. Repository-derived.

Commentary.

The compiled statement supplies upperTruncationCocone isColimit. These eventual-constant component diagrams have the original arbitrary unbounded complex as their colimit.

References

• Truth anchor: D5/S3/HomologicalAlgebra/Solid/UnboundedUpperTruncationColimit.upperTruncationCocone_isColimit
• Truth anchor: D5/S3/HomologicalAlgebra/Solid/UnboundedUpperTruncationColimit.upperTruncationDiagram_eventuallyConstant
• Dependency: D5/S3/HomologicalAlgebra/Solid/DerivedCoproduct