Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Derived Generator Comparison

Abstract

Exact supplier isolation for the constructor closure. The frozen Localizing module also imports a second copy of the already imported homotopy adjunction. Only its actually needed projectivity declarations are extracted verbatim, followed by the verbatim accepted ProjectiveGeneratorHom proof bodies. Source/license: CWComparison.Localizing, copyright (c) 2026, Apache 2.0 (src/licenses/LICENSE.LeanCondensed), frozen simplex review; and immutable accepted projective-checkpoint/CWSolid/ProjectiveGeneratorHom.lean, Apache 2.0. Exact source identities and unchanged extraction bodies are recorded in tmp/projective-hom-isolation.json. The accepted original sources/oleans remain unchanged. No declaration body or target interface is replaced by an assumption.

Definition 1.1 (solid PHom Comparison Equiv).

Lean statement: D5/S3/HomologicalAlgebra/Solid/DerivedGeneratorComparison.solidPHomComparisonEquiv

Formalization. D5/S3/HomologicalAlgebra/Solid/DerivedGeneratorComparison.solidPHomComparisonEquiv (✓ std3).

Source. Repository-derived.

Commentary.

The canonical comparison is an equivalence of Hom groups for these actual sources. This does not assert full faithfulness of derivedInclusion on other sources.

Theorem 1.2 (solid PHom Comparison Equiv apply).

Lean statement: D5/S3/HomologicalAlgebra/Solid/DerivedGeneratorComparison.solidPHomComparisonEquiv_apply

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. Exact supplier isolation for the constructor closure. The frozen Localizing module also imports a second copy of the already imported homotopy adjunction. Only its actually needed projectivity declarations are extracted verbatim, followed by the verbatim accepted ProjectiveGeneratorHom proof bodies. Source/license: CWComparison.Localizing, copyright (c) 2026, Apache 2.0 (src/licenses/LICENSE.LeanCondensed), frozen simplex review; and immutable accepted projective-checkpoint/CWSolid/ProjectiveGeneratorHom.lean, Apache 2.0. Exact source identities and unchanged extraction bodies are recorded in tmp/projective-hom-isolation.json. The accepted original sources/oleans remain unchanged. No declaration body or target interface is replaced by an assumption.

Theorem 1.3 (solid PHom Comparison Equiv naturality).

Lean statement: D5/S3/HomologicalAlgebra/Solid/DerivedGeneratorComparison.solidPHomComparisonEquiv_naturality

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. Exact supplier isolation for the constructor closure. The frozen Localizing module also imports a second copy of the already imported homotopy adjunction. Only its actually needed projectivity declarations are extracted verbatim, followed by the verbatim accepted ProjectiveGeneratorHom proof bodies. Source/license: CWComparison.Localizing, copyright (c) 2026, Apache 2.0 (src/licenses/LICENSE.LeanCondensed), frozen simplex review; and immutable accepted projective-checkpoint/CWSolid/ProjectiveGeneratorHom.lean, Apache 2.0. Exact source identities and unchanged extraction bodies are recorded in tmp/projective-hom-isolation.json. The accepted original sources/oleans remain unchanged. No declaration body or target interface is replaced by an assumption.

References