Essential smallness of categories of complexes and of homotopy categories

If C is essentially small relative to a universe w and the index type of a complex shape is w-small, then the category HomologicalComplex C c is essentially small relative to w. Every complex is isomorphic to one whose terms are chosen among the objects of a small model of C: transport each term along the unit of the equivalence C ≌ SmallModel C, and conjugate the differentials accordingly. Complexes with such terms are indexed by a family of terms and a compatible family of differentials, and that indexing type is small. The homotopy category has the same objects and quotient morphism types, so it inherits both smallness properties.

This is what makes categories built from complexes over an essentially small category, such as the homotopy category of bounded complexes, eligible for categorical Grothendieck groups.

Main results

• HomologicalComplex.essentiallySmall: complexes over an essentially small category, indexed by a small type, form an essentially small category.
• HomotopyCategory.locallySmall and HomotopyCategory.essentiallySmall: the same holds for the homotopy category.

instance HomologicalComplex.essentiallySmall (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type t} (c : ComplexShape ι) [CategoryTheory.EssentiallySmall.{w, v, u} C] [Small.{w, t} ι] : CategoryTheory.EssentiallySmall.{w, max t v, max (max t u) v} (HomologicalComplex C c)

Complexes over a w-essentially small category, indexed by a w-small type, form a w-essentially small category.

instance HomotopyCategory.locallySmall (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {ι : Type t} (c : ComplexShape ι) [CategoryTheory.LocallySmall.{w, v, u} C] [Small.{w, t} ι] : CategoryTheory.LocallySmall.{w, max t v, max (max t u) v} (HomotopyCategory C c)

The homotopy category of complexes over a w-locally small category, indexed by a w-small type, is w-locally small.

instance HomotopyCategory.essentiallySmall (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {ι : Type t} (c : ComplexShape ι) [CategoryTheory.EssentiallySmall.{w, v, u} C] [Small.{w, t} ι] : CategoryTheory.EssentiallySmall.{w, max t v, max (max t u) v} (HomotopyCategory C c)

The homotopy category of complexes over a w-essentially small category, indexed by a w-small type, is w-essentially small.