KProjective Coproduct

Abstract

Closure under arbitrary coproducts for an unbounded resolution construction.

Theorem 1.1 (is KProjective coproduct).

Lean statement: D5/S3/HomologicalAlgebra/Solid/KProjectiveCoproduct.isKProjective_coproduct

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

Source. Repository-derived.

Commentary.

Arbitrary coproducts of K-projective cochain complexes are K-projective. The members may have unrelated bounds, and may themselves be unbounded.

References

• Truth anchor: D5/S3/HomologicalAlgebra/Solid/KProjectiveCoproduct.isKProjective_coproduct
• Dependency: D5/S3/HomologicalAlgebra/Solid/ComplexAdjunction