Unbounded Truncation Colimit

Abstract

Copyright (c) 2026. Released under Apache 2.0. The actual increasing brutal lower truncations of every unbounded cochain complex have that complex as their colimit. Each fixed coefficient is eventually the original coefficient with identity transition. This is the concrete first telescope input for unbounded realization, not a hypothesis postulating generation or a realization equivalence. Research: Juan Esteban Rodríguez Camargo, Notes on Solid Geometry, Theorem 3.3.1, unbounded extension by truncations.

Definition 1.1 (lower Truncation Cocone).

Lean statement: D5/S3/HomologicalAlgebra/Solid/UnboundedTruncationColimit.lowerTruncationCocone

Formalization. D5/S3/HomologicalAlgebra/Solid/UnboundedTruncationColimit.lowerTruncationCocone (✓ std3).

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. Copyright (c) 2026. Released under Apache 2.0. The actual increasing brutal lower truncations of every unbounded cochain complex have that complex as their colimit. Each fixed coefficient is eventually the original coefficient with identity transition. This is the concrete first telescope input for unbounded realization, not a hypothesis postulating generation or a realization equivalence. Research: Juan Esteban Rodríguez Camargo, Notes on Solid Geometry, Theorem 3.3.1, unbounded extension by truncations.

Theorem 1.2 (lower Truncation Diagram eventually Constant).

Lean statement: D5/S3/HomologicalAlgebra/Solid/UnboundedTruncationColimit.lowerTruncationDiagram_eventuallyConstant

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

Source. Repository-derived.

Commentary.

Each coefficient of this specific unbounded diagram stabilizes.

Definition 1.3 (lower Truncation Cocone is Colimit).

Lean statement: D5/S3/HomologicalAlgebra/Solid/UnboundedTruncationColimit.lowerTruncationCocone_isColimit

Formalization. D5/S3/HomologicalAlgebra/Solid/UnboundedTruncationColimit.lowerTruncationCocone_isColimit (✓ std3).

Source. Repository-derived.

Commentary.

Every arbitrary unbounded complex is the actual colimit of its bounded-below lower truncations. No completeness premise is used.

References

• Truth anchor: D5/S3/HomologicalAlgebra/Solid/UnboundedTruncationColimit.lowerTruncationCocone
• Truth anchor: D5/S3/HomologicalAlgebra/Solid/UnboundedTruncationColimit.lowerTruncationCocone_isColimit
• Truth anchor: D5/S3/HomologicalAlgebra/Solid/UnboundedTruncationColimit.lowerTruncationDiagram_eventuallyConstant
• Dependency: D5/S3/HomologicalAlgebra/Solid/DerivedCoproduct