Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Solid Truncation Telescopes

Abstract

Copyright (c) 2026. Released under the Apache 2.0 license. Both verified unbounded truncation colimits become genuine mapping-cone quasi-isomorphisms in the protected Solid category. The colimit proofs are imported unchanged. Monicity reuses the actual AB5 sequence presentation; no unbounded completeness or generation premise is assumed. Research: Rodríguez Camargo, Notes on Solid Geometry, Theorem 3.3.1.

Definition 1.1 (solid Upper Truncation Telescope).

Lean statement: D5/S3/HomologicalAlgebra/Solid/SolidTruncationTelescopes.solidUpperTruncationTelescope

Formalization. D5/S3/HomologicalAlgebra/Solid/SolidTruncationTelescopes.solidUpperTruncationTelescope (✓ std3).

Source. Repository-derived.

Commentary.

Actual good upper telescope in Solid, with no boundedness premise.

Definition 1.2 (solid Upper Truncation Telescope To Input).

Lean statement: D5/S3/HomologicalAlgebra/Solid/SolidTruncationTelescopes.solidUpperTruncationTelescopeToInput

Formalization. D5/S3/HomologicalAlgebra/Solid/SolidTruncationTelescopes.solidUpperTruncationTelescopeToInput (✓ std3).

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. Copyright (c) 2026. Released under the Apache 2.0 license. Both verified unbounded truncation colimits become genuine mapping-cone quasi-isomorphisms in the protected Solid category. The colimit proofs are imported unchanged. Monicity reuses the actual AB5 sequence presentation; no unbounded completeness or generation premise is assumed. Research: Rodríguez Camargo, Notes on Solid Geometry, Theorem 3.3.1.

Theorem 1.3 (solid Upper Truncation Telescope To Input quasi Iso).

Lean statement: D5/S3/HomologicalAlgebra/Solid/SolidTruncationTelescopes.solidUpperTruncationTelescopeToInput_quasiIso

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. Copyright (c) 2026. Released under the Apache 2.0 license. Both verified unbounded truncation colimits become genuine mapping-cone quasi-isomorphisms in the protected Solid category. The colimit proofs are imported unchanged. Monicity reuses the actual AB5 sequence presentation; no unbounded completeness or generation premise is assumed. Research: Rodríguez Camargo, Notes on Solid Geometry, Theorem 3.3.1.

References