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
KandLare 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]
:
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]
: