Commit 2025-12-12 17:04 95b192f4

feat(Algebra/Homology): K-projective cochain complexes (#32741) We define the notion of K-projective cochain complex in an abelian category, and show that bounded above complexes of projective objects are K-projective. This is the dual results to #31941: the main lemma is obtained by dualising the corresponding lemma for K-injective complexes. We also dualise the result from #31900: morphisms in the derived category from a K-projective cochain complex identify to homotopy classes of morphisms.