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]
:
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]
:
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]
:
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
Instances For
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)
:
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)
: