Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Augmented Kernel Resolution

Abstract

Copyright (c) 2026. Released under the Apache 2.0 license. The actual augmentation of Mathlib’s successive-kernel left resolution is quasi-isomorphic to the input object. This supplies both the solid generator resolution and the ambient nonprojective free resolution. The resolution is constructed from the given natural epi data; no resolution-existence hypothesis is introduced. Mathlib construction: copyright (c) 2025 Joël Riou, Apache-2.0, commit 5e0c4e5239cb0a2d86d68a884bf52cfd963fce22.

Theorem 1.1 (kernelResolutionEvaluation exact).

Lean statement: D5/S3/HomologicalAlgebra/Solid/AugmentedKernelResolution.kernelResolutionEvaluation_exact

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

Source. Repository-derived.

Commentary.

The compiled statement supplies kernelResolutionEvaluation exact. The canonical augmentation is built by iterated kernels and proved exact; its cochain form is concentrated in nonpositive degrees.

Theorem 1.2 (kernelResolutionEvaluation epi).

Lean statement: D5/S3/HomologicalAlgebra/Solid/AugmentedKernelResolution.kernelResolutionEvaluation_epi

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

Source. Repository-derived.

Commentary.

The compiled statement supplies kernelResolutionEvaluation epi. The canonical augmentation is built by iterated kernels and proved exact; its cochain form is concentrated in nonpositive degrees.

Theorem 1.3 (kernelResolutionCochain strictlyLE).

Lean statement: D5/S3/HomologicalAlgebra/Solid/AugmentedKernelResolution.kernelResolutionCochain_strictlyLE

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

Source. Repository-derived.

Commentary.

The compiled statement supplies kernelResolutionCochain strictlyLE. The canonical augmentation is built by iterated kernels and proved exact; its cochain form is concentrated in nonpositive degrees.

References

  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/AugmentedKernelResolution.kernelResolutionCochain_strictlyLE
  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/AugmentedKernelResolution.kernelResolutionEvaluation_epi
  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/AugmentedKernelResolution.kernelResolutionEvaluation_exact