of_hasExactLimitsOfShape_nat_and_finite

English

If a category has countable coproducts and finite limits and exact limits for discrete Nat, then Countable AB4 holds.

Русский

Если в категории есть счетные coproducts и конечные пределы и точные пределы для дискретного Nat, то Countable AB4 выполняется.

LaTeX

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

Lean4

/-- Checking exactness of limits of shape `Discrete ℕ` and `Discrete J` for finite `J` is enough for
countable AB4*.
-/
theorem of_hasExactLimitsOfShape_nat_and_finite [HasCountableProducts C] [HasFiniteColimits C]
    [∀ (J : Type) [Finite J], HasExactLimitsOfShape (Discrete J) C] [HasExactLimitsOfShape (Discrete ℕ) C] :
    CountableAB4Star 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 hasExactLimitsOfShape_of_initial C (Discrete.equivalence (Denumerable.eqv J)).inverse

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