hasBinaryProducts_of_hasBinaryBiproducts

English

Let C be a category with binary biproducts for every pair of objects. Then C has binary products.

Русский

Пусть C — категория, в которой для любых пар объектов существуют двоичные би-произведения. Тогда C имеет двоичные произведения.

LaTeX

$$$\operatorname{HasBinaryBiproducts}(\mathcal{C}) \Rightarrow \operatorname{HasBinaryProducts}(\mathcal{C})$$$

Lean4

instance (priority := 100) hasBinaryProducts_of_hasBinaryBiproducts [HasBinaryBiproducts C] : HasBinaryProducts C where
  has_limit F := hasLimit_of_iso (diagramIsoPair F).symm

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