Derived Generator Sums

Abstract

Copyright (c) 2026. Released under the Apache 2.0 license. Full faithfulness of the exact protected derived inclusion on arbitrary small sums of the concrete generator, in every integer degree and against arbitrary unbounded solid targets. The sums are actual colimits, and the comparison is the literal derivedInclusion.map. No all-source full faithfulness, realization, or derived adjunction is assumed. Research: Rodríguez Camargo, Notes on Solid Geometry, Theorem 3.3.1.

Theorem 1.1 (derived Inclusion generator Copower map bijective).

Lean statement: D5/S3/HomologicalAlgebra/Solid/DerivedGeneratorSums.derivedInclusion_generatorCopower_map_bijective

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

Source. Repository-derived.

Commentary.

This is the actual map on derived morphisms from any generator copower, for every integer n and every arbitrary unbounded target.

References

• Truth anchor: D5/S3/HomologicalAlgebra/Solid/DerivedGeneratorSums.derivedInclusion_generatorCopower_map_bijective
• Dependency: D5/S3/HomologicalAlgebra/Solid/DerivedGeneratorComparison
• Dependency: D5/S3/HomologicalAlgebra/Solid/SolidTruncationTelescopes