Theorems · Theorem · category theory

CochainComplex.HomComplex.CohomologyClass.bijective_toSmallShiftedHom_of_isKProjective

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

Defined in

Mathlib.Algebra.Homology.DerivedCategory.KProjective

Cited by

1 results in Mathlib

Foundations

Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.Localization.HasSmallLocalizedShiftedHomCochainComplex.IsKProjective