of_AB5 — Mathlib

English

If a category has finite biproducts and finite limits, then AB4 follows from AB5.

Русский

Если у категории есть конечные бинпродукты и конечные пределы, то AB4 следует из AB5.

LaTeX

$$$\\text{AB4OfSize}(C) \\Leftarrow \\text{AB5OfSize}(C) \\text{, при условии наличия конечных бинпродуктов и пределов.}$$$

Lean4

/-- A category with finite biproducts and finite limits is AB4 if it is AB5. -/
theorem of_AB5 [HasFilteredColimitsOfSize.{w, w} C] [AB5OfSize.{w, w} C] : AB4OfSize.{w} C where
  ofShape _ := hasExactColimitsOfShape_discrete_of_hasExactColimitsOfShape_finset_discrete _ _

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