Coproducts in the derived category

For an abelian category C with coproducts of shape κ that are exact (HasExactColimitsOfShape (Discrete κ) C, the axiom AB4 for that shape), the derived category D(C) has coproducts of shape κ, and the localization functors Q and Qh and the homology functors Hⁿ : D(C) ⥤ C preserve them.

The argument is the composite of three facts. The homotopy category has coproducts of shape κ and the quotient functor preserves them; quasi-isomorphisms are stable under them because homology commutes with exact coproducts; and a localization at a class with a right calculus of fractions, stable under coproducts, has them and is preserved by the localization functor.

Main results

• DerivedCategory.hasCoproductsOfShape, Qh_preservesCoproductsOfShape, Q_preservesCoproductsOfShape, singleFunctor_preservesCoproductsOfShape, homologyFunctor_preservesCoproductsOfShape: the instances.

References

• Neeman, Triangulated categories, Lemma 3.2.10: a Verdier quotient by a localizing subcategory has the coproducts and the quotient functor preserves them
• Stacks, Tag 0A5L, Lemma 13.33.5, the countable case

instance DerivedCategory.trW_subcategoryAcyclic_isStableUnderCoproductsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {κ : Type w'} [CategoryTheory.Limits.HasCoproductsOfShape κ C] [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete κ) C] : (HomotopyCategory.subcategoryAcyclic C).trW.IsStableUnderCoproductsOfShape κ

The class of morphisms with acyclic cone is stable under coproducts: it is the class of quasi-isomorphisms.

instance DerivedCategory.hasCoproductsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {κ : Type w'} [CategoryTheory.Limits.HasCoproductsOfShape κ C] [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete κ) C] : CategoryTheory.Limits.HasCoproductsOfShape κ (DerivedCategory C)

D(C) has coproducts of shape κ when C has exact ones, Neeman's Lemma 3.2.10 taken at the localization Qh : K(C) ⥤ D(C): the homotopy category has them (HomotopyCategory.hasColimitsOfShape_discrete), quasi-isomorphisms are stable under them because homology commutes with exact coproducts (HomotopyCategory.quasiIso_isStableUnderCoproductsOfShape), and a localization at a class with a right calculus of fractions that is stable under coproducts inherits them (Localization.hasCoproductsOfShape).

instance DerivedCategory.Qh_preservesCoproductsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {κ : Type w'} [CategoryTheory.Limits.HasCoproductsOfShape κ C] [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete κ) C] : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete κ) Qh

Qh preserves coproducts of shape κ: the coproduct in D(C) of a family is the image of its coproduct in the homotopy category.

instance DerivedCategory.Q_preservesCoproductsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {κ : Type w'} [CategoryTheory.Limits.HasCoproductsOfShape κ C] [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete κ) C] : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete κ) Q

Q preserves coproducts of shape κ, so the coproduct in D(C) of a family of complexes is their termwise coproduct (Stacks 0A5L in the countable case): Q is the quotient followed by Qh, and both preserve them.

instance DerivedCategory.singleFunctor_preservesCoproductsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {κ : Type w'} [CategoryTheory.Limits.HasCoproductsOfShape κ C] [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete κ) C] (n : ℤ) : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete κ) (singleFunctor C n)

The single-object functor into the derived category preserves coproducts of shape κ: the complex single-object functor preserves them termwise and Q preserves them.

instance DerivedCategory.homologyFunctor_preservesCoproductsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {κ : Type w'} [CategoryTheory.Limits.HasCoproductsOfShape κ C] [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete κ) C] (n : ℤ) : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete κ) (homologyFunctor C n)

Homology on the derived category preserves coproducts of shape κ: it factors through the essentially surjective Q, which preserves them, as homology of complexes, which commutes with exact coproducts.