of_countableAB5Star — Mathlib

English

If a category has limits and AB5Star for countable sequences, then Countable AB4Star holds.

Русский

Если у категории есть пределы и AB5Star для счетных последовательностей, то выполняется Countable AB4Star.

LaTeX

$$$\\operatorname{CountableAB4Star}(C) \\Leftarrow \\operatorname{AB5Star}(C)$$$

Lean4

/-- A category with finite biproducts and finite limits has countable AB4* if sequential limits are
exact.
-/
theorem of_countableAB5Star [HasLimitsOfShape ℕᵒᵖ C] [HasExactLimitsOfShape ℕᵒᵖ C] [HasCountableProducts C] :
    CountableAB4Star C where
  ofShape
    J :=
    have : HasLimitsOfShape (Finset (Discrete J))ᵒᵖ C :=
      Functor.Initial.hasLimitsOfShape_of_initial (IsFiltered.sequentialFunctor (Finset (Discrete J))).op
    have := hasExactLimitsOfShape_of_initial C (IsFiltered.sequentialFunctor (Finset (Discrete J))).op
    hasExactLimitsOfShape_discrete_of_hasExactLimitsOfShape_finset_discrete_op _ _

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