Quasi-isomorphisms are stable under coproducts #
Quasi-isomorphisms in the homotopy category are stable under coproducts of a shape along which
homology of complexes commutes with coproducts, in particular under coproducts of every shape
when C is abelian with exact coproducts (AB4), by
ShortComplex.homologyFunctor_preservesColimitsOfShape. This is the last input to coproducts
in the derived category: with coproducts in the homotopy category and the localization theorem
for coproducts, D(C) has coproducts of every such shape.
Main results #
HomotopyCategory.quasiIso_isStableUnderCoproductsOfShape: the instance.
instance
HomotopyCategory.quasiIso_isStableUnderCoproductsOfShape
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.CategoryWithHomology C]
{ι : Type u_1}
{c : ComplexShape ι}
{κ : Type w}
[CategoryTheory.Limits.HasCoproductsOfShape κ C]
[∀ (n : ι),
CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete κ)
(HomologicalComplex.homologyFunctor C c n)]
:
Quasi-isomorphisms in the homotopy category are stable under coproducts of shape κ when
homology of complexes preserves them: Sigma.map of a family of quasi-isomorphisms is
inverted by homology in every degree.