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. We obtain that a morphism between K-injective cochain complexes is a quasi-isomorphism iff it is a homotopy equivalence. In particular, a morphism between cochain complexes indexed by ℕ which consist of injective objects is a quasi-isomorphism iff it is a homotopy equivalence.

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] : Function.Bijective DerivedCategory.Qh.map

theorem CochainComplex.IsKInjective.quasiIso_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {K L : CochainComplex C ℤ} [K.IsKInjective] [L.IsKInjective] (f : K ⟶ L) : QuasiIso f ↔ HomologicalComplex.homotopyEquivalences C (ComplexShape.up ℤ) f

theorem CochainComplex.HomComplex.CohomologyClass.bijective_toSmallShiftedHom_of_isKInjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (K L : CochainComplex C ℤ) (n : ℤ) [CategoryTheory.Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L] [L.IsKInjective] : Function.Bijective toSmallShiftedHom

noncomputable def CochainComplex.HomComplex.CohomologyClass.equivOfIsKInjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {K L : CochainComplex C ℤ} {n : ℤ} [CategoryTheory.Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L] [L.IsKInjective] : CohomologyClass K L n ≃ CategoryTheory.Localization.SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n

When L is a K-injective cochain complex, cohomology classes in CohomologyClass K L n identify to elements in a type SmallShiftedHom relatively to quasi-isomorphisms.

Equations

• CochainComplex.HomComplex.CohomologyClass.equivOfIsKInjective = Equiv.ofBijective CochainComplex.HomComplex.CohomologyClass.toSmallShiftedHom ⋯

theorem CochainComplex.HomComplex.CohomologyClass.equivOfIsKInjective_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {K L : CochainComplex C ℤ} {n : ℤ} [CategoryTheory.Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L] [L.IsKInjective] (x : CohomologyClass K L n) : equivOfIsKInjective x = x.toSmallShiftedHom

theorem CochainComplex.HomComplex.CohomologyClass.equivOfIsKInjective_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {K L : CochainComplex C ℤ} {n : ℤ} [CategoryTheory.Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L] [L.IsKInjective] (b : CategoryTheory.Localization.SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n) : equivOfIsKInjective.symm b = Function.surjInv ⋯ b

theorem CochainComplex.quasiIso_iff_of_injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {K L : CochainComplex C ℕ} [∀ (n : ℕ), CategoryTheory.Injective (K.X n)] [∀ (n : ℕ), CategoryTheory.Injective (L.X n)] (f : K ⟶ L) : QuasiIso f ↔ HomologicalComplex.homotopyEquivalences C (ComplexShape.up ℕ) f