Morphisms between bounded complexes are small

Let C be an abelian category. Assuming HasExt.{w} C, we show that if two cochain complexes K and L are cohomologically in a single degree, then the type of morphisms from K to L⟦n⟧ in the derived category is w-small for any n : ℤ, which we phrase here by saying that HasSmallLocalizedShiftedHom.{w} (HomologicalComplex.quasiIso _ _) ℤ K L hold.

TODO

• When more definitions are introduced for t-structures (e.g. the heart), show that the conclusion holds when K and L are cohomologically bounded.

theorem CategoryTheory.HasExt.hasSmallLocalizedShiftedHom_of_isLE_of_isGE {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (K L : CochainComplex C ℤ) (a b : ℤ) [K.IsGE a] [K.IsLE a] [L.IsGE b] [L.IsLE b] : Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L

instance CategoryTheory.HasExt.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoOfIsGEOfIsLEOfNat (C : Type u) [Category.{v, u} C] [Abelian C] [HasExt C] (K L : CochainComplex C ℤ) [K.IsGE 0] [K.IsLE 0] [L.IsGE 0] [L.IsLE 0] : Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L