English
If a category has countable coproducts, finite colimits, and exact colimits for all finite discrete shapes, then AB4 holds for countable shapes.
Русский
Если в категории есть счетные coproducts, конечные колимиты и точные колимиты для всех конечных дискретных форм, то AB4 для счетных форм выполняется.
LaTeX
$$$\\operatorname{hasExactColimitsOfShape\\;Discrete\\;Nat}(C) \\Rightarrow \\operatorname{CountableAB4}(C)$$$
Lean4
/-- Checking exactness of colimits of shape `Discrete ℕ` and `Discrete J` for finite `J` is enough for
countable AB4.
-/
theorem of_hasExactColimitsOfShape_nat_and_finite [HasCountableCoproducts C] [HasFiniteLimits C]
[∀ (J : Type) [Finite J], HasExactColimitsOfShape (Discrete J) C] [HasExactColimitsOfShape (Discrete ℕ) C] :
CountableAB4 C where
ofShape
J := by
by_cases h : Finite J
· infer_instance
· have : Infinite J := ⟨h⟩
let _ := Encodable.ofCountable J
let _ := Denumerable.ofEncodableOfInfinite J
exact hasExactColimitsOfShape_of_final C (Discrete.equivalence (Denumerable.eqv J)).inverse
