Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Free Generator Augmentation

Abstract

Copyright (c) 2026. Released under the Apache 2.0 license. An actual augmented resolution by coproducts of free light-profinite objects. The evaluation is epimorphic by the proved free-generator morphism detection; ambient projectivity is neither asserted nor needed. Successive kernels give every negative cochain degree. This is the concrete ambient resolution used in unbounded derived-local realization. Research: Juan Esteban Rodríguez Camargo, Notes on Solid Geometry, Theorem 3.3.1. Kernel iteration reuses Mathlib’s LeftResolution API, copyright (c) 2025 Joël Riou, Apache-2.0, at Mathlib 5e0c4e5239cb0a2d86d68a884bf52cfd963fce22.

Theorem 1.1 (freeGeneratorEvaluation epi).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FreeGeneratorAugmentation.freeGeneratorEvaluation_epi

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

Source. Repository-derived.

Commentary.

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

Theorem 1.2 (freeGeneratorCochainResolution strictlyLE).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FreeGeneratorAugmentation.freeGeneratorCochainResolution_strictlyLE

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

Source. Repository-derived.

Commentary.

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

Theorem 1.3 (freeGeneratorCochainResolution negative term).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FreeGeneratorAugmentation.freeGeneratorCochainResolution_negative_term

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

Source. Repository-derived.

Commentary.

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

References