Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Lower Truncation Layers

Abstract

Copyright (c) 2026. Released under the Apache 2.0 license. The concrete one-term filtration of the verified brutal lower truncations. For arbitrary unbounded K, increasing the truncation cutoff by one fits into an actual short exact sequence with the newly added coefficient as its single-complex quotient. These are the finite cone steps used with the actual generator resolution and the two unbounded telescopes. Research: Rodríguez Camargo, Notes on Solid Geometry, Theorem 3.3.1.

Definition 1.1 (lower Truncation Layer Projection).

Lean statement: D5/S3/HomologicalAlgebra/Solid/LowerTruncationLayers.lowerTruncationLayerProjection

Formalization. D5/S3/HomologicalAlgebra/Solid/LowerTruncationLayers.lowerTruncationLayerProjection (✓ std3).

Source. Repository-derived.

Commentary.

Project the newly added bottom coefficient onto its literal stalk.

Definition 1.2 (lower Truncation Layer Sequence).

Lean statement: D5/S3/HomologicalAlgebra/Solid/LowerTruncationLayers.lowerTruncationLayerSequence

Formalization. D5/S3/HomologicalAlgebra/Solid/LowerTruncationLayers.lowerTruncationLayerSequence (✓ 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. The concrete one-term filtration of the verified brutal lower truncations. For arbitrary unbounded K, increasing the truncation cutoff by one fits into an actual short exact sequence with the newly added coefficient as its single-complex quotient. These are the finite cone steps used with the actual generator resolution and the two unbounded telescopes. Research: Rodríguez Camargo, Notes on Solid Geometry, Theorem 3.3.1.

Theorem 1.3 (lower Truncation Layer Sequence short Exact).

Lean statement: D5/S3/HomologicalAlgebra/Solid/LowerTruncationLayers.lowerTruncationLayerSequence_shortExact

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

Source. Repository-derived.

Commentary.

The filtration is short exact on all integer coefficients, including the zero coefficients below the cutoff. No boundedness of K is used.

References

  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/LowerTruncationLayers.lowerTruncationLayerProjection
  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/LowerTruncationLayers.lowerTruncationLayerSequence
  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/LowerTruncationLayers.lowerTruncationLayerSequence_shortExact
  • Dependency: D5/S3/HomologicalAlgebra/Solid/UnboundedTruncationColimit