of_hasExactColimitsOfShape_nat — Mathlib

English

If all countable and finite discrete shapes have exact colimits, then Countable AB4 holds.

Русский

Если для всех счетных и конечных дискретных форм существуют точные колимиты, то выполняется Countable AB4.

LaTeX

$$$\\operatorname{CountableAB4}(C) \\Leftarrow \\operatorname{HasExactColimitsOfShape}(\\Discrete Nat) C$$

Lean4

/-- Checking AB of shape `Discrete ℕ` is enough for countable AB4, provided that the category has
finite biproducts and finite limits.
-/
theorem of_hasExactColimitsOfShape_nat [HasFiniteLimits C] [HasCountableCoproducts C]
    [HasExactColimitsOfShape (Discrete ℕ) C] : CountableAB4 C :=
  by
  apply (config := { allowSynthFailures := true }) CountableAB4.of_hasExactColimitsOfShape_nat_and_finite
  exact fun _ ↦ inferInstance

Похожие утверждения