English
Let C be a category. If C has filtered colimits of a sufficiently large size and satisfies AB5 for those sizes, then C has filtered colimits of smaller sizes and AB5 for those smaller sizes. In particular, AB5OfSize and HasFilteredColimitsOfSize descend along shrinkage of the size parameters.
Русский
Пусть C — категория. Если в C существуют фильтрованные пределы для sufficiently large размера и выполняется условие AB5 для этих размеров, то у C существуют фильтрованные пределы меньшего размера и AB5 для этих меньших размеров. В частности, свойство AB5OfSize и существование фильтрованных пределов уменьшаются по мере уменьшения параметров размера.
LaTeX
$$$\\operatorname{HasFilteredColimitsOfSize}^{(w,w')}(C) \\land \\operatorname{AB5OfSize}^{(w,w')}(C) \\Leftarrow \\operatorname{HasFilteredColimitsOfSize}^{(\\max w w',\\max w' w_2')}(C) \\land \\operatorname{AB5OfSize}^{(\\max w w',\\max w' w_2')}(C)$$$
Lean4
theorem AB5OfSize_shrink [HasFilteredColimitsOfSize.{max w w₂, max w' w₂'} C] [AB5OfSize.{max w w₂, max w' w₂'} C] :
haveI : HasFilteredColimitsOfSize.{w, w'} C := hasFilteredColimitsOfSize_shrink
AB5OfSize.{w, w'} C :=
AB5OfSize_of_univLE C
