theorem DirectLimitHomology.homology_preservesFilteredColimits (n : ℤ) : CategoryTheory.Limits.PreservesFilteredColimits (HomologicalComplex.homologyFunctor AddCommGrpCat (ComplexShape.down ℤ) n)

Homology commutes with filtered colimits. In the abelian category AddCommGrpCat, the degree-n homology functor on chain complexes preserves filtered colimits. This is the categorical content underlying Corollary 23.13 (singular homology commutes with direct limits of spaces) and Lemma 23 (homology of a direct limit of chain complexes is the direct limit of the homologies).