Morphisms from K-projective complexes in the derived category #
In this file, we show that if K : CochainComplex C ℤ is K-projective,
then for any L : HomotopyCategory C (.up ℤ), the functor DerivedCategory.Qh
induces a bijection from the type of morphisms (HomotopyCategory.quotient _ _).obj K) ⟶ L
(i.e. homotopy classes of morphisms of cochain complexes) to the type of
morphisms in the derived category.
theorem
CochainComplex.IsKProjective.Qh_map_bijective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
(K : CochainComplex C ℤ)
(L : HomotopyCategory C (ComplexShape.up ℤ))
[K.IsKProjective]
: