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

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

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

theorem CochainComplex.HomComplex.CohomologyClass.bijective_toSmallShiftedHom_of_isKProjective {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] [K.IsKProjective] : Function.Bijective toSmallShiftedHom

noncomputable def CochainComplex.HomComplex.CohomologyClass.equivOfIsKProjective {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] [K.IsKProjective] : CohomologyClass K L n ≃ CategoryTheory.Localization.SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n

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

Equations

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

theorem CochainComplex.HomComplex.CohomologyClass.equivOfIsKProjective_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] [K.IsKProjective] (x : CohomologyClass K L n) : equivOfIsKProjective x = x.toSmallShiftedHom

theorem CochainComplex.HomComplex.CohomologyClass.equivOfIsKProjective_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] [K.IsKProjective] (b : CategoryTheory.Localization.SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n) : equivOfIsKProjective.symm b = Function.surjInv ⋯ b

theorem ChainComplex.quasiIso_iff_of_projective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {K L : ChainComplex C ℕ} [∀ (n : ℕ), CategoryTheory.Projective (K.X n)] [∀ (n : ℕ), CategoryTheory.Projective (L.X n)] (f : K ⟶ L) : QuasiIso f ↔ HomologicalComplex.homotopyEquivalences C (ComplexShape.down ℕ) f