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