English
If a category has finite biproducts and finite limits, and sequential colimits are exact, then it has countable AB4.
Русский
Если у категории есть конечные бинопродукты и конечные пределы, и последовательные колимиты точны, то у нее есть счетная AB4.
LaTeX
$$$\\text{CountableAB4}(C) \\Leftarrow \\text{AB5OfSize}(C) \\text{ и т.д.}$$$
Lean4
/-- A category with finite biproducts and finite limits has countable AB4 if sequential colimits are
exact.
-/
theorem of_countableAB5 [HasColimitsOfShape ℕ C] [HasExactColimitsOfShape ℕ C] [HasCountableCoproducts C] :
CountableAB4 C where
ofShape
J :=
have : HasColimitsOfShape (Finset (Discrete J)) C :=
Functor.Final.hasColimitsOfShape_of_final (IsFiltered.sequentialFunctor (Finset (Discrete J)))
have := hasExactColimitsOfShape_of_final C (IsFiltered.sequentialFunctor (Finset (Discrete J)))
hasExactColimitsOfShape_discrete_of_hasExactColimitsOfShape_finset_discrete _ _
