of_hasExactLimitsOfShape_nat — Mathlib

English

If a category has countable products and finite colimits, then CountableAB4 holds given discrete Nat exact limits.

Русский

Если в категории есть счетные продукты и конечные колимиты, то при наличии точных дискретных Nat пределов выполняется CountableAB4.

LaTeX

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

Lean4

/-- Checking AB* of shape `Discrete ℕ` is enough for countable AB4*, provided that the category has
finite biproducts and finite colimits.
-/
theorem of_hasExactLimitsOfShape_nat [HasFiniteColimits C] [HasCountableProducts C]
    [HasExactLimitsOfShape (Discrete ℕ) C] : CountableAB4Star C :=
  by
  apply (config := { allowSynthFailures := true }) CountableAB4Star.of_hasExactLimitsOfShape_nat_and_finite
  exact fun _ ↦ inferInstance

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